Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tactics: allow an expected typ for refl_instantiate_implicits #3343

Merged
merged 2 commits into from
Jul 6, 2024
+362 −327
Merged

Tactics: allow an expected typ for refl_instantiate_implicits #3343

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f10d7f4
Tactics: allow an expected typ for refl_instantiate_implicits
mtzguido Jul 6, 2024
fe197bd
snap
mtzguido Jul 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
664 changes: 345 additions & 319 deletions ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml
View file
Open in desktop

Large diffs are not rendered by default.

6 changes: 5 additions & 1 deletion ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 6 additions & 1 deletion src/tactics/FStar.Tactics.V2.Basic.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
//
Expand Down
2 changes: 1 addition & 1 deletion src/tactics/FStar.Tactics.V2.Basic.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 3 additions & 3 deletions src/tactics/FStar.Tactics.V2.Primops.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand Down
2 changes: 1 addition & 1 deletion ulib/FStar.Stubs.Tactics.V2.Builtins.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))

//
Expand Down
Loading