Merge pull request #3563 from mtzguido/tac_refactor

Tactics: refactor a bit to avoid a cycle

ulib/FStar.Reflection.V2.Arith.fst

@@ -15,7 +15,7 @@
 *)
 module FStar.Reflection.V2.Arith
 
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 open FStar.Reflection.V2
 module O = FStar.Order
 

ulib/FStar.Tactics.Arith.fst

@@ -15,7 +15,7 @@
 *)
 module FStar.Tactics.Arith
 
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 open FStar.Reflection.V2.Formula
 open FStar.Reflection.V2.Arith
 

ulib/FStar.Tactics.BV.fst

@@ -15,7 +15,8 @@
 *)
 module FStar.Tactics.BV
 
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
+open FStar.Tactics.MApply0
 open FStar.Reflection.V2.Formula
 open FStar.Reflection.V2.Arith
 open FStar.BV
@@ -96,8 +97,8 @@ let arith_to_bv_tac () : Tac unit = focus (fun () ->
 too. This can be useful, if we have mixed expressions so I'll leave it
 as is for now *)
 let bv_tac () = focus (fun () ->
-  mapply (`eq_to_bv);
-  mapply (`trans);
+  mapply0 (`eq_to_bv);
+  mapply0 (`trans);
   arith_to_bv_tac ();
   arith_to_bv_tac ();
   set_options "--smtencoding.elim_box true";

ulib/FStar.Tactics.Canon.fst

@@ -16,7 +16,7 @@
 module FStar.Tactics.Canon
 
 open FStar.Reflection.V2
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 open FStar.Reflection.V2.Arith
 open FStar.Mul
 module O = FStar.Order

ulib/FStar.Tactics.CanonCommMonoid.fst

@@ -365,8 +365,8 @@ let canon_monoid_aux
           // dump ("expected after =" ^ term_to_string (norm_term [delta;primops]
           //   (quote (xsdenote m vm (canon vm p r1) ==
           //           xsdenote m vm (canon vm p r2)))));
-          // mapply (quote (monoid_reflect #a #b p pc));
-          mapply (mk_app (`monoid_reflect) [(ta, Q_Implicit);
+          // mapply0 (quote (monoid_reflect #a #b p pc));
+          mapply0 (mk_app (`monoid_reflect) [(ta, Q_Implicit);
                                             (tb, Q_Implicit);
                                             (tp, Q_Explicit);
                                             (tpc, Q_Explicit)]);

ulib/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst

@@ -19,7 +19,7 @@ open FStar.Algebra.CommMonoid.Equiv
 open FStar.List
 open FStar.Classical
 open FStar.Tactics.CanonCommSwaps
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 
 private
 let term_eq = FStar.Reflection.TermEq.Simple.term_eq

ulib/FStar.Tactics.CanonCommMonoidSimple.fst

@@ -18,7 +18,7 @@ module FStar.Tactics.CanonCommMonoidSimple
 open FStar.Algebra.CommMonoid
 open FStar.List
 open FStar.Reflection.V2
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 open FStar.Classical
 open FStar.Tactics.CanonCommSwaps
 

ulib/FStar.Tactics.CheckLN.fst

@@ -1,6 +1,6 @@
 module FStar.Tactics.CheckLN
 
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 open FStar.Tactics.Util
 
 let rec for_all (p : 'a -> Tac bool) (l : list 'a)  : Tac bool =

ulib/FStar.Tactics.CheckLN.fsti

@@ -1,6 +1,6 @@
 module FStar.Tactics.CheckLN
 
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 
 (* Checks if a term is locally nameless. *)
 [@@plugin]

ulib/FStar.Tactics.MApply.fst

@@ -1,85 +1,3 @@
 module FStar.Tactics.MApply
 
-open FStar.Reflection.V2
-open FStar.Reflection.V2.Formula
-
-open FStar.Tactics.Effect
-open FStar.Stubs.Tactics.V2.Builtins
-open FStar.Tactics.NamedView
-open FStar.Tactics.V2.SyntaxHelpers
-open FStar.Tactics.V2.Derived
-open FStar.Tactics.V2.SyntaxCoercions
-
-open FStar.Tactics.Typeclasses
-let push1 #p #q f u = ()
-let push1' #p #q f u = ()
-
-(*
- * Some easier applying, which should prevent frustration
- * (or cause more when it doesn't do what you wanted to)
- *)
-val apply_squash_or_lem : d:nat -> term -> Tac unit
-let rec apply_squash_or_lem d t =
-    (* Before anything, try a vanilla apply and apply_lemma *)
-    try apply t with | _ ->
-    try apply (`FStar.Squash.return_squash); apply t with | _ ->
-    try apply_lemma t with | _ ->
-
-    // Fuel cutoff, just in case.
-    if d <= 0 then fail "mapply: out of fuel" else begin
-
-    let ty = tc (cur_env ()) t in
-    let tys, c = collect_arr ty in
-    match inspect_comp c with
-    | C_Lemma pre post _ ->
-       begin
-       let post = `((`#post) ()) in (* unthunk *)
-       let post = norm_term [] post in
-       (* Is the lemma an implication? We can try to intro *)
-       match term_as_formula' post with
-       | Implies p q ->
-           apply_lemma (`push1);
-           apply_squash_or_lem (d-1) t
-
-       | _ ->
-           fail "mapply: can't apply (1)"
-       end
-    | C_Total rt ->
-       begin match unsquash_term rt with
-       (* If the function returns a squash, just apply it, since our goals are squashed *)
-       | Some rt ->
-        // DUPLICATED, refactor!
-         begin
-         let rt = norm_term [] rt in
-         (* Is the lemma an implication? We can try to intro *)
-         match term_as_formula' rt with
-         | Implies p q ->
-             apply_lemma (`push1);
-             apply_squash_or_lem (d-1) t
-
-         | _ ->
-             fail "mapply: can't apply (2)"
-         end
-
-       (* If not, we can try to introduce the squash ourselves first *)
-       | None ->
-        // DUPLICATED, refactor!
-         begin
-         let rt = norm_term [] rt in
-         (* Is the lemma an implication? We can try to intro *)
-         match term_as_formula' rt with
-         | Implies p q ->
-             apply_lemma (`push1);
-             apply_squash_or_lem (d-1) t
-
-         | _ ->
-             apply (`FStar.Squash.return_squash);
-             apply t
-         end
-       end
-    | _ -> fail "mapply: can't apply (3)"
-    end
-
-(* `m` is for `magic` *)
-let mapply0 (t : term) : Tac unit =
-  apply_squash_or_lem 10 t
+(* This file just here to trigger extraction. *)

ulib/FStar.Tactics.MApply.fsti

@@ -1,19 +1,11 @@
 module FStar.Tactics.MApply
 
-open FStar.Reflection.V2
+open FStar.Stubs.Reflection.Types
+open FStar.Stubs.Reflection.V2.Data
 open FStar.Tactics.Effect
-open FStar.Tactics.Typeclasses
 open FStar.Tactics.V2.SyntaxCoercions
 
-(* Used by mapply, must be exposed, but not to be used directly *)
-private val push1 : (#p:Type) -> (#q:Type) ->
-                        squash (p ==> q) ->
-                        squash p ->
-                        squash q
-private val push1' : (#p:Type) -> (#q:Type) ->
-                         (p ==> q) ->
-                         squash p ->
-                         squash q
+include FStar.Tactics.MApply0
 
 class termable (a : Type) = {
   to_term : a -> Tac term
@@ -27,10 +19,6 @@ instance termable_binding : termable binding = {
   to_term = (fun b -> binding_to_term b);
 }
 
-(* `m` is for `magic` *)
-[@@plugin]
-val mapply0 (t : term) : Tac unit
-
 let mapply (#ty:Type) {| termable ty |} (x : ty) : Tac unit =
   let t = to_term x in
   mapply0 t

ulib/FStar.Tactics.MApply0.fst

@@ -0,0 +1,84 @@
+module FStar.Tactics.MApply0
+
+open FStar.Reflection.V2
+open FStar.Reflection.V2.Formula
+
+open FStar.Tactics.Effect
+open FStar.Stubs.Tactics.V2.Builtins
+open FStar.Tactics.NamedView
+open FStar.Tactics.V2.SyntaxHelpers
+open FStar.Tactics.V2.Derived
+open FStar.Tactics.V2.SyntaxCoercions
+
+let push1 #p #q f u = ()
+let push1' #p #q f u = ()
+
+(*
+ * Some easier applying, which should prevent frustration
+ * (or cause more when it doesn't do what you wanted to)
+ *)
+val apply_squash_or_lem : d:nat -> term -> Tac unit
+let rec apply_squash_or_lem d t =
+    (* Before anything, try a vanilla apply and apply_lemma *)
+    try apply t with | _ ->
+    try apply (`FStar.Squash.return_squash); apply t with | _ ->
+    try apply_lemma t with | _ ->
+
+    // Fuel cutoff, just in case.
+    if d <= 0 then fail "mapply: out of fuel" else begin
+
+    let ty = tc (cur_env ()) t in
+    let tys, c = collect_arr ty in
+    match inspect_comp c with
+    | C_Lemma pre post _ ->
+       begin
+       let post = `((`#post) ()) in (* unthunk *)
+       let post = norm_term [] post in
+       (* Is the lemma an implication? We can try to intro *)
+       match term_as_formula' post with
+       | Implies p q ->
+           apply_lemma (`push1);
+           apply_squash_or_lem (d-1) t
+
+       | _ ->
+           fail "mapply: can't apply (1)"
+       end
+    | C_Total rt ->
+       begin match unsquash_term rt with
+       (* If the function returns a squash, just apply it, since our goals are squashed *)
+       | Some rt ->
+        // DUPLICATED, refactor!
+         begin
+         let rt = norm_term [] rt in
+         (* Is the lemma an implication? We can try to intro *)
+         match term_as_formula' rt with
+         | Implies p q ->
+             apply_lemma (`push1);
+             apply_squash_or_lem (d-1) t
+
+         | _ ->
+             fail "mapply: can't apply (2)"
+         end
+
+       (* If not, we can try to introduce the squash ourselves first *)
+       | None ->
+        // DUPLICATED, refactor!
+         begin
+         let rt = norm_term [] rt in
+         (* Is the lemma an implication? We can try to intro *)
+         match term_as_formula' rt with
+         | Implies p q ->
+             apply_lemma (`push1);
+             apply_squash_or_lem (d-1) t
+
+         | _ ->
+             apply (`FStar.Squash.return_squash);
+             apply t
+         end
+       end
+    | _ -> fail "mapply: can't apply (3)"
+    end
+
+(* `m` is for `magic` *)
+let mapply0 (t : term) : Tac unit =
+  apply_squash_or_lem 10 t

ulib/FStar.Tactics.MApply0.fsti

@@ -0,0 +1,18 @@
+module FStar.Tactics.MApply0
+
+open FStar.Stubs.Reflection.Types
+open FStar.Tactics.Effect
+
+(* Used by mapply, must be exposed, but not to be used directly *)
+private val push1 : (#p:Type) -> (#q:Type) ->
+                        squash (p ==> q) ->
+                        squash p ->
+                        squash q
+private val push1' : (#p:Type) -> (#q:Type) ->
+                         (p ==> q) ->
+                         squash p ->
+                         squash q
+
+(* `m` is for `magic` *)
+[@@plugin]
+val mapply0 (t : term) : Tac unit

ulib/FStar.Tactics.Parametricity.fst

@@ -1,7 +1,7 @@
 module FStar.Tactics.Parametricity
 
 open FStar.List
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 
 type bvmap = list (namedv & (binder & binder & binder))
 let fvmap =  list (fv & fv)
@@ -319,7 +319,7 @@ let param_inductive (se:sigelt) (fv0 fv1 : fv) : Tac decls =
     //Tactics.Util.iter (fun bv -> dump ("param bv = " ^ binder_to_string bv)) param_bs;
     let typ = mk_e_app (param' s typ) [replace_by s false orig; replace_by s true orig] in
     (* dump ("new typ = " ^ term_to_string typ); *)
-    let ctors = Tactics.V2.map (param_ctor nm s) ctors in
+    let ctors = Tactics.V2.Bare.map (param_ctor nm s) ctors in
     let se = Sg_Inductive {nm=inspect_fv fv1; univs; params=param_bs; typ; ctors} in
     (* dump ("param_ind : " ^ term_to_string (quote se)); *)
     [pack_sigelt se]

ulib/FStar.Tactics.TypeRepr.fst

@@ -2,7 +2,7 @@ module FStar.Tactics.TypeRepr
 
 //#set-options "--print_implicits --print_full_names --print_universes"
 
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 
 let add_suffix (s:string) (nm:name) : name =
   explode_qn (implode_qn nm ^ s)

ulib/FStar.Tactics.TypeRepr.fsti

@@ -1,6 +1,6 @@
 module FStar.Tactics.TypeRepr
 
-open FStar.Tactics.V2
+open FStar.Tactics.V2.Bare
 
 private
 let empty_elim (e:empty) (#a:Type) : a = match e with