From fd6cb422467f45168fc7ab00cbe6552846df8428 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 1 Dec 2023 19:41:40 -0800
Subject: [PATCH 1/3] Rel: local caching of meta args (for typeclasses)
---
src/basic/FStar.Common.fst | 7 ++
src/syntax/FStar.Syntax.Util.fst | 7 ++
src/typechecker/FStar.TypeChecker.Rel.fst | 99 ++++++++++++++++-------
3 files changed, 85 insertions(+), 28 deletions(-)
diff --git a/src/basic/FStar.Common.fst b/src/basic/FStar.Common.fst
index f5dbb5c33fd..05ae50b4233 100644
--- a/src/basic/FStar.Common.fst
+++ b/src/basic/FStar.Common.fst
@@ -150,3 +150,10 @@ let max_suffix (f : 'a -> bool) (xs : list 'a) : list 'a * list 'a =
(acc, x::xs)
in
xs |> List.rev |> aux [] |> (fun (xs, ys) -> List.rev ys, xs)
+
+let rec eq_list (f: 'a -> 'a -> bool) (l1 l2 : list 'a)
+ : bool
+ = match l1, l2 with
+ | [], [] -> true
+ | [], _ | _, [] -> false
+ | x1::t1, x2::t2 -> f x1 x2 && eq_list f t1 t2
diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst
index f77e38c3f87..a1fc331dbd6 100644
--- a/src/syntax/FStar.Syntax.Util.fst
+++ b/src/syntax/FStar.Syntax.Util.fst
@@ -2541,3 +2541,10 @@ let is_binder_unused (b:binder) =
let deduplicate_terms (l:list term) =
FStar.Compiler.List.deduplicate (fun x y -> eq_tm x y = Equal) l
+
+let eq_binding b1 b2 =
+ match b1, b2 with
+ | Binding_var bv1, Binding_var bv2 -> bv_eq bv1 bv2 && term_eq bv1.sort bv2.sort
+ | Binding_lid (lid1, _), Binding_lid (lid2, _) -> lid_equals lid1 lid2
+ | Binding_univ u1, Binding_univ u2 -> ident_equals u1 u2
+ | _ -> false
diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst
index 38ef675b461..6c2368ddf28 100644
--- a/src/typechecker/FStar.TypeChecker.Rel.fst
+++ b/src/typechecker/FStar.TypeChecker.Rel.fst
@@ -5404,6 +5404,37 @@ let is_tac_implicit_resolved (env:env) (i:implicit) : bool =
let resolve_implicits' env is_tac is_gen (implicits:Env.implicits)
: list (implicit * implicit_checking_status) =
+ (* Meta argument cache: during a single run of this resolve_implicits' function
+ we keep track of all results of the "cacheable" tactics that are used for meta
+ arguments. The only cacheable tactic, for now, is tcresolve. Before trying to run
+ it, we check the cache to see if we have already solved a problem in the same environment
+ and for the same uvar type (in this case, the constraint). If so, we just take that result.
+
+ This is pretty conservative. e.g. in
+ f (1 + 1);
+ g (1 + 1)
+ we cannot reuse the solution for each +, since there is an extra unit binder when
+ we check `g ...`. But it does lead to big gains in expressions like `1 + 1 + 1 ...`. *)
+ let cacheable tac = U.is_fvar PC.tcresolve_lid tac in
+ let __meta_arg_cache : ref (list (term & env_t & typ & term)) = BU.mk_ref [] in
+ let meta_arg_cache_result (tac : term) (e : env_t) (ty : term) (res : term) : unit =
+ __meta_arg_cache := (tac, e, ty, res) :: !__meta_arg_cache
+ in
+ let meta_arg_cache_lookup (tac : term) (e : env_t) (ty : term) : option term =
+ let rec aux l : option term =
+ match l with
+ | [] -> None
+ | (tac', e', ty', res') :: l' ->
+ if U.term_eq tac tac'
+ && FStar.Common.eq_list U.eq_binding e.gamma e'.gamma
+ && U.term_eq ty ty'
+ then Some res'
+ else aux l'
+ in
+ aux !__meta_arg_cache
+ in
+ (* / cache *)
+
let rec until_fixpoint (acc:tagged_implicits * bool)
(implicits:Env.implicits)
: tagged_implicits =
@@ -5434,34 +5465,46 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits)
| hd::tl ->
let { imp_reason = reason; imp_tm = tm; imp_uvar = ctx_u; imp_range = r } = hd in
- let {
- uvar_decoration_typ;
- uvar_decoration_should_check
- } = UF.find_decoration ctx_u.ctx_uvar_head
- in
- if Env.debug env <| Options.Other "Rel"
- then BU.print3 "resolve_implicits' loop, imp_tm = %s and ctx_u = %s, is_tac: %s\n"
- (show tm)
- (Print.ctx_uvar_to_string ctx_u)
- (string_of_bool is_tac);
- if Allow_unresolved? uvar_decoration_should_check
- then until_fixpoint (out, true) tl
- else if unresolved ctx_u
- then (if flex_uvar_has_meta_tac ctx_u
- then let t = run_meta_arg_tac ctx_u in
- // let the unifier handle setting the variable
- let extra =
- match teq_nosmt env t tm with
- | None -> failwith "resolve_implicits: unifying with an unresolved uvar failed?"
- | Some g -> g.implicits in
-
- until_fixpoint (out, true) (extra @ tl)
- else until_fixpoint ((hd, Implicit_unresolved)::out, changed) tl)
- else if Allow_untyped? uvar_decoration_should_check ||
- Already_checked? uvar_decoration_should_check ||
- is_gen
- then until_fixpoint (out, true) tl
- else begin
+ let { uvar_decoration_typ; uvar_decoration_should_check } = UF.find_decoration ctx_u.ctx_uvar_head in
+ if Env.debug env <| Options.Other "Rel" then
+ BU.print3 "resolve_implicits' loop, imp_tm = %s and ctx_u = %s, is_tac: %s\n"
+ (show tm) (show ctx_u) (show is_tac);
+ begin match () with
+ | _ when Allow_unresolved? uvar_decoration_should_check ->
+ until_fixpoint (out, true) tl
+
+ | _ when unresolved ctx_u && flex_uvar_has_meta_tac ctx_u ->
+ let Some (Ctx_uvar_meta_tac meta) = ctx_u.ctx_uvar_meta in
+ let m_env : env_t = Dyn.undyn (fst meta) in
+ let tac = snd meta in
+ let typ = U.ctx_uvar_typ ctx_u in
+ let solve_with (t:term) =
+ let extra =
+ match teq_nosmt env t tm with
+ | None -> failwith "resolve_implicits: unifying with an unresolved uvar failed?"
+ | Some g -> g.implicits
+ in
+ until_fixpoint (out, true) (extra @ tl)
+ in
+ if cacheable tac then
+ match meta_arg_cache_lookup tac m_env typ with
+ | Some res -> solve_with res
+ | None ->
+ let t = run_meta_arg_tac ctx_u in
+ meta_arg_cache_result tac m_env typ t;
+ solve_with t
+ else
+ let t = run_meta_arg_tac ctx_u in
+ solve_with t
+
+ | _ when unresolved ctx_u ->
+ until_fixpoint ((hd, Implicit_unresolved)::out, changed) tl
+
+ | _ when Allow_untyped? uvar_decoration_should_check ||
+ Already_checked? uvar_decoration_should_check ||
+ is_gen ->
+ until_fixpoint (out, true) tl
+ | _ ->
let env = {env with gamma=ctx_u.ctx_uvar_gamma} in
(*
* AR: Some opportunities for optimization here,
From 10f9228abad2bb0ca2a1d17adafc1394d90969cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 1 Dec 2023 19:41:07 -0800
Subject: [PATCH 2/3] Introduce tests/typeclasses
---
tests/Makefile | 1 +
tests/typeclasses/CoallesceConstraints.fst | 16 ++++++++++++++++
tests/typeclasses/Makefile | 15 +++++++++++++++
3 files changed, 32 insertions(+)
create mode 100644 tests/typeclasses/CoallesceConstraints.fst
create mode 100644 tests/typeclasses/Makefile
diff --git a/tests/Makefile b/tests/Makefile
index a9267332d77..b8f8d6b6ebb 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -12,6 +12,7 @@ ALL_TEST_DIRS += micro-benchmarks
ALL_TEST_DIRS += prettyprinting
ALL_TEST_DIRS += struct
ALL_TEST_DIRS += tactics
+ALL_TEST_DIRS += typeclasses
ALL_TEST_DIRS += vale
all: $(addsuffix .all, $(ALL_TEST_DIRS))
diff --git a/tests/typeclasses/CoallesceConstraints.fst b/tests/typeclasses/CoallesceConstraints.fst
new file mode 100644
index 00000000000..1c57224d182
--- /dev/null
+++ b/tests/typeclasses/CoallesceConstraints.fst
@@ -0,0 +1,16 @@
+module CoallesceConstraints
+
+open FStar.Class.Printable
+
+(* tcresolve runs only once here. We should really check for it... *)
+let test (x:int) =
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x ^
+ to_string x ^ to_string x ^ to_string x ^ to_string x
diff --git a/tests/typeclasses/Makefile b/tests/typeclasses/Makefile
new file mode 100644
index 00000000000..b0d903477bd
--- /dev/null
+++ b/tests/typeclasses/Makefile
@@ -0,0 +1,15 @@
+FSTAR_HOME=../..
+
+FSTAR_FILES=$(wildcard *.fst)
+
+all: verify-all
+
+include $(FSTAR_HOME)/examples/Makefile.common
+
+verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
+
+clean:
+ $(call msg, "CLEAN")
+ $(Q)rm -f .depend
+ $(Q)rm -rf _cache
+ $(Q)rm -rf _output
From 075cfad5b073b2001925eefcb85dc2aedf988879 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 1 Dec 2023 19:42:44 -0800
Subject: [PATCH 3/3] snap
---
ocaml/fstar-lib/generated/FStar_Common.ml | 14 +-
.../fstar-lib/generated/FStar_Syntax_Util.ml | 19 +-
.../generated/FStar_TypeChecker_Rel.ml | 521 ++++++++++--------
3 files changed, 314 insertions(+), 240 deletions(-)
diff --git a/ocaml/fstar-lib/generated/FStar_Common.ml b/ocaml/fstar-lib/generated/FStar_Common.ml
index 3732323554f..c2e5efa5b79 100644
--- a/ocaml/fstar-lib/generated/FStar_Common.ml
+++ b/ocaml/fstar-lib/generated/FStar_Common.ml
@@ -174,4 +174,16 @@ let max_suffix :
FStar_Compiler_Effect.op_Bar_Greater uu___
(fun uu___1 ->
match uu___1 with
- | (xs1, ys) -> ((FStar_Compiler_List.rev ys), xs1))
\ No newline at end of file
+ | (xs1, ys) -> ((FStar_Compiler_List.rev ys), xs1))
+let rec eq_list :
+ 'a .
+ ('a -> 'a -> Prims.bool) -> 'a Prims.list -> 'a Prims.list -> Prims.bool
+ =
+ fun f ->
+ fun l1 ->
+ fun l2 ->
+ match (l1, l2) with
+ | ([], []) -> true
+ | ([], uu___) -> false
+ | (uu___, []) -> false
+ | (x1::t1, x2::t2) -> (f x1 x2) && (eq_list f t1 t2)
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
index 4f73965f002..b12165895a0 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
@@ -5298,4 +5298,21 @@ let (deduplicate_terms :
=
fun l ->
FStar_Compiler_List.deduplicate
- (fun x -> fun y -> let uu___ = eq_tm x y in uu___ = Equal) l
\ No newline at end of file
+ (fun x -> fun y -> let uu___ = eq_tm x y in uu___ = Equal) l
+let (eq_binding :
+ FStar_Syntax_Syntax.binding -> FStar_Syntax_Syntax.binding -> Prims.bool) =
+ fun b1 ->
+ fun b2 ->
+ match (b1, b2) with
+ | (FStar_Syntax_Syntax.Binding_var bv1, FStar_Syntax_Syntax.Binding_var
+ bv2) ->
+ (FStar_Syntax_Syntax.bv_eq bv1 bv2) &&
+ (term_eq bv1.FStar_Syntax_Syntax.sort
+ bv2.FStar_Syntax_Syntax.sort)
+ | (FStar_Syntax_Syntax.Binding_lid (lid1, uu___),
+ FStar_Syntax_Syntax.Binding_lid (lid2, uu___1)) ->
+ FStar_Ident.lid_equals lid1 lid2
+ | (FStar_Syntax_Syntax.Binding_univ u1,
+ FStar_Syntax_Syntax.Binding_univ u2) ->
+ FStar_Ident.ident_equals u1 u2
+ | uu___ -> false
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
index e25560db064..a1078249aef 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
@@ -15205,6 +15205,28 @@ let (resolve_implicits' :
fun is_tac ->
fun is_gen ->
fun implicits ->
+ let cacheable tac =
+ FStar_Syntax_Util.is_fvar FStar_Parser_Const.tcresolve_lid tac in
+ let __meta_arg_cache = FStar_Compiler_Util.mk_ref [] in
+ let meta_arg_cache_result tac e ty res =
+ let uu___ =
+ let uu___1 = FStar_Compiler_Effect.op_Bang __meta_arg_cache in
+ (tac, e, ty, res) :: uu___1 in
+ FStar_Compiler_Effect.op_Colon_Equals __meta_arg_cache uu___ in
+ let meta_arg_cache_lookup tac e ty =
+ let rec aux l =
+ match l with
+ | [] -> FStar_Pervasives_Native.None
+ | (tac', e', ty', res')::l' ->
+ let uu___ =
+ ((FStar_Syntax_Util.term_eq tac tac') &&
+ (FStar_Common.eq_list FStar_Syntax_Util.eq_binding
+ e.FStar_TypeChecker_Env.gamma
+ e'.FStar_TypeChecker_Env.gamma))
+ && (FStar_Syntax_Util.term_eq ty ty') in
+ if uu___ then FStar_Pervasives_Native.Some res' else aux l' in
+ let uu___ = FStar_Compiler_Effect.op_Bang __meta_arg_cache in
+ aux uu___ in
let rec until_fixpoint acc implicits1 =
let uu___ = acc in
match uu___ with
@@ -15279,253 +15301,276 @@ let (resolve_implicits' :
FStar_Class_Show.show
FStar_Syntax_Print.showable_term tm in
let uu___7 =
- FStar_Syntax_Print.ctx_uvar_to_string
- ctx_u in
+ FStar_Class_Show.show
+ FStar_Syntax_Print.showable_ctxu ctx_u in
let uu___8 =
- FStar_Compiler_Util.string_of_bool
+ FStar_Class_Show.show
+ (FStar_Class_Show.printableshow
+ FStar_Class_Printable.printable_bool)
is_tac in
FStar_Compiler_Util.print3
"resolve_implicits' loop, imp_tm = %s and ctx_u = %s, is_tac: %s\n"
uu___6 uu___7 uu___8
else ());
- if
- FStar_Syntax_Syntax.uu___is_Allow_unresolved
- uvar_decoration_should_check
- then until_fixpoint (out, true) tl
- else
- (let uu___6 = unresolved ctx_u in
- if uu___6
- then
- (if flex_uvar_has_meta_tac ctx_u
- then
- let t = run_meta_arg_tac ctx_u in
- let extra =
- let uu___7 = teq_nosmt env t tm in
- match uu___7 with
- | FStar_Pervasives_Native.None ->
- failwith
- "resolve_implicits: unifying with an unresolved uvar failed?"
- | FStar_Pervasives_Native.Some g ->
- g.FStar_TypeChecker_Common.implicits in
- until_fixpoint (out, true)
- (FStar_Compiler_List.op_At extra tl)
- else
- until_fixpoint
- (((hd, Implicit_unresolved) ::
- out), changed) tl)
- else
- if
- ((FStar_Syntax_Syntax.uu___is_Allow_untyped
- uvar_decoration_should_check)
- ||
- (FStar_Syntax_Syntax.uu___is_Already_checked
- uvar_decoration_should_check))
- || is_gen
- then until_fixpoint (out, true) tl
- else
- (let env1 =
- {
- FStar_TypeChecker_Env.solver =
- (env.FStar_TypeChecker_Env.solver);
- FStar_TypeChecker_Env.range =
- (env.FStar_TypeChecker_Env.range);
- FStar_TypeChecker_Env.curmodule =
- (env.FStar_TypeChecker_Env.curmodule);
- FStar_TypeChecker_Env.gamma =
- (ctx_u.FStar_Syntax_Syntax.ctx_uvar_gamma);
- FStar_TypeChecker_Env.gamma_sig =
- (env.FStar_TypeChecker_Env.gamma_sig);
- FStar_TypeChecker_Env.gamma_cache
- =
- (env.FStar_TypeChecker_Env.gamma_cache);
- FStar_TypeChecker_Env.modules =
- (env.FStar_TypeChecker_Env.modules);
- FStar_TypeChecker_Env.expected_typ
- =
- (env.FStar_TypeChecker_Env.expected_typ);
- FStar_TypeChecker_Env.sigtab =
- (env.FStar_TypeChecker_Env.sigtab);
- FStar_TypeChecker_Env.attrtab =
- (env.FStar_TypeChecker_Env.attrtab);
- FStar_TypeChecker_Env.instantiate_imp
- =
- (env.FStar_TypeChecker_Env.instantiate_imp);
- FStar_TypeChecker_Env.effects =
- (env.FStar_TypeChecker_Env.effects);
- FStar_TypeChecker_Env.generalize
- =
- (env.FStar_TypeChecker_Env.generalize);
- FStar_TypeChecker_Env.letrecs =
- (env.FStar_TypeChecker_Env.letrecs);
- FStar_TypeChecker_Env.top_level =
- (env.FStar_TypeChecker_Env.top_level);
- FStar_TypeChecker_Env.check_uvars
- =
- (env.FStar_TypeChecker_Env.check_uvars);
- FStar_TypeChecker_Env.use_eq_strict
- =
- (env.FStar_TypeChecker_Env.use_eq_strict);
- FStar_TypeChecker_Env.is_iface =
- (env.FStar_TypeChecker_Env.is_iface);
- FStar_TypeChecker_Env.admit =
- (env.FStar_TypeChecker_Env.admit);
- FStar_TypeChecker_Env.lax =
- (env.FStar_TypeChecker_Env.lax);
- FStar_TypeChecker_Env.lax_universes
- =
- (env.FStar_TypeChecker_Env.lax_universes);
- FStar_TypeChecker_Env.phase1 =
- (env.FStar_TypeChecker_Env.phase1);
- FStar_TypeChecker_Env.failhard =
- (env.FStar_TypeChecker_Env.failhard);
- FStar_TypeChecker_Env.nosynth =
- (env.FStar_TypeChecker_Env.nosynth);
- FStar_TypeChecker_Env.uvar_subtyping
- =
- (env.FStar_TypeChecker_Env.uvar_subtyping);
- FStar_TypeChecker_Env.intactics =
- (env.FStar_TypeChecker_Env.intactics);
- FStar_TypeChecker_Env.nocoerce =
- (env.FStar_TypeChecker_Env.nocoerce);
- FStar_TypeChecker_Env.tc_term =
- (env.FStar_TypeChecker_Env.tc_term);
- FStar_TypeChecker_Env.typeof_tot_or_gtot_term
- =
- (env.FStar_TypeChecker_Env.typeof_tot_or_gtot_term);
- FStar_TypeChecker_Env.universe_of
- =
- (env.FStar_TypeChecker_Env.universe_of);
- FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term
- =
- (env.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term);
- FStar_TypeChecker_Env.teq_nosmt_force
- =
- (env.FStar_TypeChecker_Env.teq_nosmt_force);
- FStar_TypeChecker_Env.subtype_nosmt_force
- =
- (env.FStar_TypeChecker_Env.subtype_nosmt_force);
- FStar_TypeChecker_Env.qtbl_name_and_index
- =
- (env.FStar_TypeChecker_Env.qtbl_name_and_index);
- FStar_TypeChecker_Env.normalized_eff_names
- =
- (env.FStar_TypeChecker_Env.normalized_eff_names);
- FStar_TypeChecker_Env.fv_delta_depths
- =
- (env.FStar_TypeChecker_Env.fv_delta_depths);
- FStar_TypeChecker_Env.proof_ns =
- (env.FStar_TypeChecker_Env.proof_ns);
- FStar_TypeChecker_Env.synth_hook
- =
- (env.FStar_TypeChecker_Env.synth_hook);
- FStar_TypeChecker_Env.try_solve_implicits_hook
- =
- (env.FStar_TypeChecker_Env.try_solve_implicits_hook);
- FStar_TypeChecker_Env.splice =
- (env.FStar_TypeChecker_Env.splice);
- FStar_TypeChecker_Env.mpreprocess
- =
- (env.FStar_TypeChecker_Env.mpreprocess);
- FStar_TypeChecker_Env.postprocess
- =
- (env.FStar_TypeChecker_Env.postprocess);
- FStar_TypeChecker_Env.identifier_info
- =
- (env.FStar_TypeChecker_Env.identifier_info);
- FStar_TypeChecker_Env.tc_hooks =
- (env.FStar_TypeChecker_Env.tc_hooks);
- FStar_TypeChecker_Env.dsenv =
- (env.FStar_TypeChecker_Env.dsenv);
- FStar_TypeChecker_Env.nbe =
- (env.FStar_TypeChecker_Env.nbe);
- FStar_TypeChecker_Env.strict_args_tab
- =
- (env.FStar_TypeChecker_Env.strict_args_tab);
- FStar_TypeChecker_Env.erasable_types_tab
- =
- (env.FStar_TypeChecker_Env.erasable_types_tab);
- FStar_TypeChecker_Env.enable_defer_to_tac
- =
- (env.FStar_TypeChecker_Env.enable_defer_to_tac);
- FStar_TypeChecker_Env.unif_allow_ref_guards
- =
- (env.FStar_TypeChecker_Env.unif_allow_ref_guards);
- FStar_TypeChecker_Env.erase_erasable_args
- =
- (env.FStar_TypeChecker_Env.erase_erasable_args);
- FStar_TypeChecker_Env.core_check
- =
- (env.FStar_TypeChecker_Env.core_check)
- } in
- let tm1 =
- norm_with_steps
- "FStar.TypeChecker.Rel.norm_with_steps.8"
- [FStar_TypeChecker_Env.Beta] env1
- tm in
- let hd1 =
- {
- FStar_TypeChecker_Common.imp_reason
- =
- (hd.FStar_TypeChecker_Common.imp_reason);
- FStar_TypeChecker_Common.imp_uvar
- =
- (hd.FStar_TypeChecker_Common.imp_uvar);
- FStar_TypeChecker_Common.imp_tm =
- tm1;
- FStar_TypeChecker_Common.imp_range
- =
- (hd.FStar_TypeChecker_Common.imp_range)
- } in
- if is_tac
- then
- ((let uu___10 =
- is_tac_implicit_resolved env1
- hd1 in
- if uu___10
- then
- let force_univ_constraints =
- true in
- let res =
- check_implicit_solution_and_discharge_guard
- env1 hd1 is_tac
- force_univ_constraints in
- (if
- res <>
- (FStar_Pervasives_Native.Some
- [])
- then
- failwith
- "Impossible: check_implicit_solution_and_discharge_guard for tac must return Some []"
- else ())
- else ());
- until_fixpoint (out, true) tl)
- else
- (let force_univ_constraints = false in
- let imps_opt =
+ (match () with
+ | uu___5 when
+ FStar_Syntax_Syntax.uu___is_Allow_unresolved
+ uvar_decoration_should_check
+ -> until_fixpoint (out, true) tl
+ | uu___5 when
+ (unresolved ctx_u) &&
+ (flex_uvar_has_meta_tac ctx_u)
+ ->
+ let uu___6 =
+ ctx_u.FStar_Syntax_Syntax.ctx_uvar_meta in
+ (match uu___6 with
+ | FStar_Pervasives_Native.Some
+ (FStar_Syntax_Syntax.Ctx_uvar_meta_tac
+ meta) ->
+ let m_env =
+ FStar_Compiler_Dyn.undyn
+ (FStar_Pervasives_Native.fst
+ meta) in
+ let tac =
+ FStar_Pervasives_Native.snd meta in
+ let typ =
+ FStar_Syntax_Util.ctx_uvar_typ
+ ctx_u in
+ let solve_with t =
+ let extra =
+ let uu___7 = teq_nosmt env t tm in
+ match uu___7 with
+ | FStar_Pervasives_Native.None
+ ->
+ failwith
+ "resolve_implicits: unifying with an unresolved uvar failed?"
+ | FStar_Pervasives_Native.Some
+ g ->
+ g.FStar_TypeChecker_Common.implicits in
+ until_fixpoint (out, true)
+ (FStar_Compiler_List.op_At
+ extra tl) in
+ let uu___7 = cacheable tac in
+ if uu___7
+ then
+ let uu___8 =
+ meta_arg_cache_lookup tac m_env
+ typ in
+ (match uu___8 with
+ | FStar_Pervasives_Native.Some
+ res -> solve_with res
+ | FStar_Pervasives_Native.None
+ ->
+ let t =
+ run_meta_arg_tac ctx_u in
+ (meta_arg_cache_result tac
+ m_env typ t;
+ solve_with t))
+ else
+ (let t = run_meta_arg_tac ctx_u in
+ solve_with t))
+ | uu___5 when unresolved ctx_u ->
+ until_fixpoint
+ (((hd, Implicit_unresolved) :: out),
+ changed) tl
+ | uu___5 when
+ ((FStar_Syntax_Syntax.uu___is_Allow_untyped
+ uvar_decoration_should_check)
+ ||
+ (FStar_Syntax_Syntax.uu___is_Already_checked
+ uvar_decoration_should_check))
+ || is_gen
+ -> until_fixpoint (out, true) tl
+ | uu___5 ->
+ let env1 =
+ {
+ FStar_TypeChecker_Env.solver =
+ (env.FStar_TypeChecker_Env.solver);
+ FStar_TypeChecker_Env.range =
+ (env.FStar_TypeChecker_Env.range);
+ FStar_TypeChecker_Env.curmodule =
+ (env.FStar_TypeChecker_Env.curmodule);
+ FStar_TypeChecker_Env.gamma =
+ (ctx_u.FStar_Syntax_Syntax.ctx_uvar_gamma);
+ FStar_TypeChecker_Env.gamma_sig =
+ (env.FStar_TypeChecker_Env.gamma_sig);
+ FStar_TypeChecker_Env.gamma_cache =
+ (env.FStar_TypeChecker_Env.gamma_cache);
+ FStar_TypeChecker_Env.modules =
+ (env.FStar_TypeChecker_Env.modules);
+ FStar_TypeChecker_Env.expected_typ =
+ (env.FStar_TypeChecker_Env.expected_typ);
+ FStar_TypeChecker_Env.sigtab =
+ (env.FStar_TypeChecker_Env.sigtab);
+ FStar_TypeChecker_Env.attrtab =
+ (env.FStar_TypeChecker_Env.attrtab);
+ FStar_TypeChecker_Env.instantiate_imp
+ =
+ (env.FStar_TypeChecker_Env.instantiate_imp);
+ FStar_TypeChecker_Env.effects =
+ (env.FStar_TypeChecker_Env.effects);
+ FStar_TypeChecker_Env.generalize =
+ (env.FStar_TypeChecker_Env.generalize);
+ FStar_TypeChecker_Env.letrecs =
+ (env.FStar_TypeChecker_Env.letrecs);
+ FStar_TypeChecker_Env.top_level =
+ (env.FStar_TypeChecker_Env.top_level);
+ FStar_TypeChecker_Env.check_uvars =
+ (env.FStar_TypeChecker_Env.check_uvars);
+ FStar_TypeChecker_Env.use_eq_strict
+ =
+ (env.FStar_TypeChecker_Env.use_eq_strict);
+ FStar_TypeChecker_Env.is_iface =
+ (env.FStar_TypeChecker_Env.is_iface);
+ FStar_TypeChecker_Env.admit =
+ (env.FStar_TypeChecker_Env.admit);
+ FStar_TypeChecker_Env.lax =
+ (env.FStar_TypeChecker_Env.lax);
+ FStar_TypeChecker_Env.lax_universes
+ =
+ (env.FStar_TypeChecker_Env.lax_universes);
+ FStar_TypeChecker_Env.phase1 =
+ (env.FStar_TypeChecker_Env.phase1);
+ FStar_TypeChecker_Env.failhard =
+ (env.FStar_TypeChecker_Env.failhard);
+ FStar_TypeChecker_Env.nosynth =
+ (env.FStar_TypeChecker_Env.nosynth);
+ FStar_TypeChecker_Env.uvar_subtyping
+ =
+ (env.FStar_TypeChecker_Env.uvar_subtyping);
+ FStar_TypeChecker_Env.intactics =
+ (env.FStar_TypeChecker_Env.intactics);
+ FStar_TypeChecker_Env.nocoerce =
+ (env.FStar_TypeChecker_Env.nocoerce);
+ FStar_TypeChecker_Env.tc_term =
+ (env.FStar_TypeChecker_Env.tc_term);
+ FStar_TypeChecker_Env.typeof_tot_or_gtot_term
+ =
+ (env.FStar_TypeChecker_Env.typeof_tot_or_gtot_term);
+ FStar_TypeChecker_Env.universe_of =
+ (env.FStar_TypeChecker_Env.universe_of);
+ FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term
+ =
+ (env.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term);
+ FStar_TypeChecker_Env.teq_nosmt_force
+ =
+ (env.FStar_TypeChecker_Env.teq_nosmt_force);
+ FStar_TypeChecker_Env.subtype_nosmt_force
+ =
+ (env.FStar_TypeChecker_Env.subtype_nosmt_force);
+ FStar_TypeChecker_Env.qtbl_name_and_index
+ =
+ (env.FStar_TypeChecker_Env.qtbl_name_and_index);
+ FStar_TypeChecker_Env.normalized_eff_names
+ =
+ (env.FStar_TypeChecker_Env.normalized_eff_names);
+ FStar_TypeChecker_Env.fv_delta_depths
+ =
+ (env.FStar_TypeChecker_Env.fv_delta_depths);
+ FStar_TypeChecker_Env.proof_ns =
+ (env.FStar_TypeChecker_Env.proof_ns);
+ FStar_TypeChecker_Env.synth_hook =
+ (env.FStar_TypeChecker_Env.synth_hook);
+ FStar_TypeChecker_Env.try_solve_implicits_hook
+ =
+ (env.FStar_TypeChecker_Env.try_solve_implicits_hook);
+ FStar_TypeChecker_Env.splice =
+ (env.FStar_TypeChecker_Env.splice);
+ FStar_TypeChecker_Env.mpreprocess =
+ (env.FStar_TypeChecker_Env.mpreprocess);
+ FStar_TypeChecker_Env.postprocess =
+ (env.FStar_TypeChecker_Env.postprocess);
+ FStar_TypeChecker_Env.identifier_info
+ =
+ (env.FStar_TypeChecker_Env.identifier_info);
+ FStar_TypeChecker_Env.tc_hooks =
+ (env.FStar_TypeChecker_Env.tc_hooks);
+ FStar_TypeChecker_Env.dsenv =
+ (env.FStar_TypeChecker_Env.dsenv);
+ FStar_TypeChecker_Env.nbe =
+ (env.FStar_TypeChecker_Env.nbe);
+ FStar_TypeChecker_Env.strict_args_tab
+ =
+ (env.FStar_TypeChecker_Env.strict_args_tab);
+ FStar_TypeChecker_Env.erasable_types_tab
+ =
+ (env.FStar_TypeChecker_Env.erasable_types_tab);
+ FStar_TypeChecker_Env.enable_defer_to_tac
+ =
+ (env.FStar_TypeChecker_Env.enable_defer_to_tac);
+ FStar_TypeChecker_Env.unif_allow_ref_guards
+ =
+ (env.FStar_TypeChecker_Env.unif_allow_ref_guards);
+ FStar_TypeChecker_Env.erase_erasable_args
+ =
+ (env.FStar_TypeChecker_Env.erase_erasable_args);
+ FStar_TypeChecker_Env.core_check =
+ (env.FStar_TypeChecker_Env.core_check)
+ } in
+ let tm1 =
+ norm_with_steps
+ "FStar.TypeChecker.Rel.norm_with_steps.8"
+ [FStar_TypeChecker_Env.Beta] env1 tm in
+ let hd1 =
+ {
+ FStar_TypeChecker_Common.imp_reason
+ =
+ (hd.FStar_TypeChecker_Common.imp_reason);
+ FStar_TypeChecker_Common.imp_uvar =
+ (hd.FStar_TypeChecker_Common.imp_uvar);
+ FStar_TypeChecker_Common.imp_tm =
+ tm1;
+ FStar_TypeChecker_Common.imp_range =
+ (hd.FStar_TypeChecker_Common.imp_range)
+ } in
+ if is_tac
+ then
+ ((let uu___7 =
+ is_tac_implicit_resolved env1 hd1 in
+ if uu___7
+ then
+ let force_univ_constraints = true in
+ let res =
check_implicit_solution_and_discharge_guard
env1 hd1 is_tac
force_univ_constraints in
- match imps_opt with
- | FStar_Pervasives_Native.None ->
- until_fixpoint
- (((hd1,
- Implicit_checking_defers_univ_constraint)
- :: out), changed) tl
- | FStar_Pervasives_Native.Some
- imps ->
- let uu___10 =
- let uu___11 =
- let uu___12 =
- FStar_Compiler_Effect.op_Bar_Greater
- imps
- (FStar_Compiler_List.map
- (fun i ->
- (i,
- Implicit_unresolved))) in
- FStar_Compiler_List.op_At
- uu___12 out in
- (uu___11, true) in
- until_fixpoint uu___10 tl))))))) in
+ (if
+ res <>
+ (FStar_Pervasives_Native.Some
+ [])
+ then
+ failwith
+ "Impossible: check_implicit_solution_and_discharge_guard for tac must return Some []"
+ else ())
+ else ());
+ until_fixpoint (out, true) tl)
+ else
+ (let force_univ_constraints = false in
+ let imps_opt =
+ check_implicit_solution_and_discharge_guard
+ env1 hd1 is_tac
+ force_univ_constraints in
+ match imps_opt with
+ | FStar_Pervasives_Native.None ->
+ until_fixpoint
+ (((hd1,
+ Implicit_checking_defers_univ_constraint)
+ :: out), changed) tl
+ | FStar_Pervasives_Native.Some imps
+ ->
+ let uu___7 =
+ let uu___8 =
+ let uu___9 =
+ FStar_Compiler_Effect.op_Bar_Greater
+ imps
+ (FStar_Compiler_List.map
+ (fun i ->
+ (i,
+ Implicit_unresolved))) in
+ FStar_Compiler_List.op_At
+ uu___9 out in
+ (uu___8, true) in
+ until_fixpoint uu___7 tl)))))) in
until_fixpoint ([], false) implicits
let (resolve_implicits :
FStar_TypeChecker_Env.env ->