Merge pull request #3343 from mtzguido/expected_type

Tactics: allow an expected typ for refl_instantiate_implicits

ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml

@@ -152,7 +152,7 @@ let check_match_complete         = from_tac_4 "B.refl_check_match_complete" B.re
 let tc_term                      = from_tac_2 "B.refl_tc_term" B.refl_tc_term
 let universe_of                  = from_tac_2 "B.refl_universe_of" B.refl_universe_of
 let check_prop_validity          = from_tac_2 "B.refl_check_prop_validity" B.refl_check_prop_validity
-let instantiate_implicits        = from_tac_2 "B.refl_instantiate_implicits" B.refl_instantiate_implicits
+let instantiate_implicits        = from_tac_3 "B.refl_instantiate_implicits" B.refl_instantiate_implicits
 let try_unify                    = from_tac_4 "B.refl_try_unify" B.refl_try_unify
 let maybe_relate_after_unfolding = from_tac_3 "B.refl_maybe_relate_after_unfolding" B.refl_maybe_relate_after_unfolding
 let maybe_unfold_head            = from_tac_2 "B.refl_maybe_unfold_head" B.refl_maybe_unfold_head

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

@@ -2591,7 +2591,7 @@ let refl_check_match_complete (g:env) (sc:term) (scty:typ) (pats : list RD.patte
     return (Some (List.map inspect_pat pats, List.map bnds_for_pat pats))
   | _ -> return None
 
-let refl_instantiate_implicits (g:env) (e:term)
+let refl_instantiate_implicits (g:env) (e:term) (expected_typ : option term)
   : tac (option (list (bv & typ) & term & typ) & issues) =
   if no_uvars_in_g g &&
      no_uvars_in_term e
@@ -2602,6 +2602,11 @@ let refl_instantiate_implicits (g:env) (e:term)
     dbg_refl g (fun _ -> "refl_instantiate_implicits: starting tc {\n");
     // AR: ghost is ok for instantiating implicits
     let must_tot = false in
+    let g =
+      match expected_typ with
+      | None -> Env.clear_expected_typ g |> fst
+      | Some typ -> Env.set_expected_typ g typ
+    in
     let g = {g with instantiate_imp=false; phase1=true; lax=true} in
     let e, t, guard = g.typeof_tot_or_gtot_term g e must_tot in
     //

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

@@ -137,7 +137,7 @@ val refl_tc_term                      : env -> term -> tac (option (term & (Core
 val refl_universe_of                  : env -> term -> tac (option universe & issues)
 val refl_check_prop_validity          : env -> term -> tac (option unit & issues)
 val refl_check_match_complete         : env -> term -> term -> list pattern -> tac (option (list pattern & list (list RD.binding)))
-val refl_instantiate_implicits        : env -> term -> tac (option (list (bv & typ) & term & typ) & issues)
+val refl_instantiate_implicits        : env -> term -> expected_typ:option term -> tac (option (list (bv & typ) & term & typ) & issues)
 val refl_try_unify                    : env -> list (bv & typ) -> term -> term -> tac (option (list (bv & term)) & issues)
 val refl_maybe_relate_after_unfolding : env -> term -> term -> tac (option Core.side & issues)
 val refl_maybe_unfold_head            : env -> term -> tac (option term & issues)

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

@@ -252,9 +252,9 @@ let ops = [
   mk_tac_step_2 0 "universe_of"             refl_universe_of refl_universe_of;
   mk_tac_step_2 0 "check_prop_validity"     refl_check_prop_validity refl_check_prop_validity;
   mk_tac_step_4 0 "check_match_complete"    refl_check_match_complete refl_check_match_complete;
-  mk_tac_step_2 0 "instantiate_implicits"
-    #_ #_ #(e_ret_t (e_tuple3 (e_list (e_tuple2 RE.e_namedv solve)) solve solve))
-    #_ #_ #(nbe_e_ret_t (NBET.e_tuple3 (NBET.e_list (NBET.e_tuple2 NRE.e_namedv solve)) solve solve))
+  mk_tac_step_3 0 "instantiate_implicits"
+    #_ #_ #_ #(e_ret_t (e_tuple3 (e_list (e_tuple2 RE.e_namedv solve)) solve solve))
+    #_ #_ #_ #(nbe_e_ret_t (NBET.e_tuple3 (NBET.e_list (NBET.e_tuple2 NRE.e_namedv solve)) solve solve))
     refl_instantiate_implicits refl_instantiate_implicits;
   mk_tac_step_4 0 "try_unify"
     #_ #(e_list (e_tuple2 RE.e_namedv RE.e_term))             #_ #_ #(e_ret_t (e_list (e_tuple2 RE.e_namedv RE.e_term)))

ulib/FStar.Stubs.Tactics.V2.Builtins.fsti

@@ -553,7 +553,7 @@ val check_match_complete (g:env) (sc:term) (t:typ) (pats:list pattern)
 //
 //   t' is the elaborated t, and ty is its type
 //
-val instantiate_implicits (g:env) (t:term)
+val instantiate_implicits (g:env) (t:term) (expected_typ : option term)
   : Tac (ret_t (list (namedv & typ) & term & typ))
 
 //