Merge pull request #3501 from mtzguido/projs2

Some tactics and MkProjectors improvements

src/syntax/FStar.Syntax.Util.fst

@@ -362,18 +362,17 @@ let head_and_args t =
     | Tm_app {hd=head; args} -> head, args
     | _ -> t, []
 
-let rec __head_and_args_full unmeta t =
+let rec __head_and_args_full acc unmeta t =
     let t = compress t in
     match t.n with
     | Tm_app {hd=head; args} ->
-      let (head, args') = __head_and_args_full unmeta head
-      in (head, args'@args)
+      __head_and_args_full (args@acc) unmeta head
     | Tm_meta {tm} when unmeta ->
-      __head_and_args_full unmeta tm
-    | _ -> t, []
+      __head_and_args_full acc unmeta tm
+    | _ -> t, acc
 
-let head_and_args_full        t = __head_and_args_full false t
-let head_and_args_full_unmeta t = __head_and_args_full true t
+let head_and_args_full        t = __head_and_args_full [] false t
+let head_and_args_full_unmeta t = __head_and_args_full [] true t
 
 let rec leftmost_head t =
     let t = compress t in

src/tactics/FStar.Tactics.V2.Basic.fst

@@ -202,14 +202,14 @@ let destruct_eq' (typ : typ) : option (term & term) =
 
 let destruct_eq (env : Env.env) (typ : typ) : option (term & term) =
 // TODO: unascribe?
-    let typ = whnf env typ in
+    (* let typ = whnf env typ in *)
     match destruct_eq' typ with
     | Some t -> Some t
     | None ->
         // Retry for a squashed one
         begin match U.un_squash typ with
         | Some typ ->
-          let typ = whnf env typ in
+          (* let typ = whnf env typ in *)
           destruct_eq' typ
         | None -> None
         end
@@ -773,7 +773,7 @@ let intro () : tac RD.binding = wrap_err "intro" <| (
         *)
         set_solution goal sol ;!
         let g = mk_goal env' ctx_uvar goal.opts goal.is_guard goal.label in
-        bnorm_and_replace g ;!
+        replace_cur g ;!
         return (binder_to_binding b)
     | None ->
         fail1 "goal is not an arrow (%s)" (tts (goal_env goal) (goal_type goal))
@@ -807,7 +807,7 @@ let intros (max:Z.t) : tac (list RD.binding) = wrap_err "intros" <| (
     let sol = U.abs bs body (Some (U.residual_comp_of_comp c)) in
     set_solution goal sol ;!
     let g = mk_goal env' ctx_uvar goal.opts goal.is_guard goal.label in
-    bnorm_and_replace g ;!
+    replace_cur g ;!
     return (List.map binder_to_binding bs)
 )
 

src/typechecker/FStar.TypeChecker.Tc.fst

@@ -892,7 +892,7 @@ let tc_decl env se: list sigelt & list sigelt & Env.env =
   in
   if Debug.any () then
     BU.print1 "Processing %s\n" (Print.sigelt_to_string_short se);
-  if Debug.low () then
+  if Debug.medium () then
     BU.print2 ">>>>>>>>>>>>>>tc_decl admit=%s %s\n" (show env.admit) (show se);
   let result =
     if se.sigmeta.sigmeta_already_checked then

src/typechecker/FStar.TypeChecker.TcTerm.fst

@@ -3167,7 +3167,7 @@ and tc_pat env (pat_t:typ) (p0:pat) :
         & guard_t
         & bool =
         if !dbg_Patterns
-        then BU.print2 "Checking pattern %s at type %s\n" (show p) (show t);
+        then BU.print2 "Checking nested pattern %s at type %s\n" (show p) (show t);
 
         let id t = mk_Tm_app
           (S.fvar Const.id_lid None)

ulib/FStar.Tactics.MkProjectors.fst

@@ -26,14 +26,14 @@ let debug (f : unit -> Tac string) : Tac unit =
 [@@plugin]
 let mk_one_projector (unf:list string) (np:nat) (i:nat) : Tac unit =
   debug (fun () -> dump "ENTRY mk_one_projector"; "");
-  let _params = repeatn np intro in
+  let _params = Stubs.Tactics.V2.Builtins.intros np in
   let thing : binding = intro () in
   let r = t_destruct thing in
   match r with
   | [(cons, arity)] -> begin
     if (i >= arity) then
       fail "proj: bad index in mk_one_projector";
-    let _      = repeatn i intro in
+    let _      = Stubs.Tactics.V2.Builtins.intros i in
     let the_b  = intro () in
     let _      = Stubs.Tactics.V2.Builtins.intros (arity-i-1) in
     let eq_b   : binding = intro () in
@@ -152,19 +152,20 @@ let mk_proj_decl (is_method:bool)
     in
     (* The method is just defined based on the projector. *)
     let lb_def =
-      (`(_ by (mk_one_method
-                 (`#(embed_string (implode_qn nm)))
-                 (`#(embed_int np)))))
-      (* NB: if we wanted a 'direct' definition of the method,
-      using a match instead of calling the projector, the following
-      will do. The same mk_one_projector tactic should handle it
-      well.
-
-      (`(_ by (mk_one_projector
-                 (`#unfold_names_tm)
-                 (`#(embed_int np))
-                 (`#(embed_int idx)))))
-      *)
+      if true
+      then
+        (* This generates a method defined to be equal to the projector
+             i.e.  method {| c |} = c.method *)
+        (`(_ by (mk_one_method
+                   (`#(embed_string (implode_qn nm)))
+                   (`#(embed_int np)))))
+      else
+        (* This defines the method in the same way as the projector
+             i.e.  method {| c |} = match c with | Mk ... method ... -> method *)
+        (`(_ by (mk_one_projector
+                   (`#unfold_names_tm)
+                   (`#(embed_int np))
+                   (`#(embed_int idx)))))
     in
     (* dump ("returning se with name " ^ unseal field.ppname); *)
     (* dump ("def = " ^ term_to_string lb_def); *)
@@ -198,7 +199,7 @@ let mk_proj_decl (is_method:bool)
 
 [@@plugin]
 let mk_projs (is_class:bool) (tyname:string) : Tac decls =
-  print ("!! mk_projs tactic called on: " ^ tyname);
+  debug (fun () -> "!! mk_projs tactic called on: " ^ tyname);
   let tyqn = explode_qn tyname in
   match lookup_typ (top_env ()) tyqn with
   | None ->
@@ -215,13 +216,13 @@ let mk_projs (is_class:bool) (tyname:string) : Tac decls =
       (* dump ("ityp = " ^ term_to_string typ); *)
       (* dump ("ctor_t = " ^ term_to_string ctor_t); *)
       let (fields, _) = collect_arr_bs ctor_t in
-      let unfold_names_tm = `(Nil #string) in
+      let unfold_names_tm = `(Nil u#0 #string) in
       let (decls, _, _, _) =
         fold_left (fun (decls, smap, unfold_names_tm, idx) (field : binder) ->
           let (ds, fv) = mk_proj_decl is_class tyqn ctorname univs params idx field unfold_names_tm smap in
           (decls @ ds,
            (binder_to_namedv field, fv)::smap,
-           (`(Cons #string (`#(embed_string (implode_qn (inspect_fv fv)))) (`#unfold_names_tm))),
+           (`(Cons u#0 #string (`#(embed_string (implode_qn (inspect_fv fv)))) (`#unfold_names_tm))),
            idx+1))
         ([], [], unfold_names_tm, 0)
         fields