diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml index b0b9ed58ee3..033d30b3b21 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml @@ -2002,6 +2002,19 @@ let (showable_letbinding : { FStar_Class_Show.show = lb_to_string } let (showable_modul : FStar_Syntax_Syntax.modul FStar_Class_Show.showable) = { FStar_Class_Show.show = modul_to_string } +let (showable_ctx_uvar_meta : + FStar_Syntax_Syntax.ctx_uvar_meta_t FStar_Class_Show.showable) = + { + FStar_Class_Show.show = + (fun uu___ -> + match uu___ with + | FStar_Syntax_Syntax.Ctx_uvar_meta_attr attr -> + let uu___1 = FStar_Class_Show.show showable_term attr in + Prims.strcat "Ctx_uvar_meta_attr " uu___1 + | FStar_Syntax_Syntax.Ctx_uvar_meta_tac r -> + let uu___1 = FStar_Class_Show.show showable_term r in + Prims.strcat "Ctx_uvar_meta_tac " uu___1) + } let (pretty_term : FStar_Syntax_Syntax.term FStar_Class_PP.pretty) = { FStar_Class_PP.pp = term_to_doc } let (pretty_univ : FStar_Syntax_Syntax.universe FStar_Class_PP.pretty) = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_DeferredImplicits.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_DeferredImplicits.ml index c6c6ade4c2f..819bcdf7bc0 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_DeferredImplicits.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_DeferredImplicits.ml @@ -225,7 +225,7 @@ let (should_defer_uvar_to_user_tac : then false else (let uu___1 = find_user_tac_for_uvar env u in - FStar_Compiler_Option.isSome uu___1) + FStar_Pervasives_Native.uu___is_Some uu___1) let solve_goals_with_tac : 'uuuuu . FStar_TypeChecker_Env.env -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 90841d176a1..4382da3afeb 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -7204,6 +7204,26 @@ let (new_implicit_var_aux : fun should_check -> fun meta -> new_tac_implicit_var reason r env1 k should_check [] meta +let (uvar_meta_for_binder : + FStar_Syntax_Syntax.binder -> + FStar_Syntax_Syntax.ctx_uvar_meta_t FStar_Pervasives_Native.option) + = + fun b -> + let uu___ = b in + match uu___ with + | { FStar_Syntax_Syntax.binder_bv = x; + FStar_Syntax_Syntax.binder_qual = qual; + FStar_Syntax_Syntax.binder_positivity = uu___1; + FStar_Syntax_Syntax.binder_attrs = attrs;_} -> + (match (qual, attrs) with + | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta tau), + uu___2) -> + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Ctx_uvar_meta_tac tau) + | (uu___2, attr::uu___3) -> + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Ctx_uvar_meta_attr attr) + | (uu___2, uu___3) -> FStar_Pervasives_Native.None) let (uvars_for_binders : env -> FStar_Syntax_Syntax.binders -> @@ -7226,18 +7246,7 @@ let (uvars_for_binders : let sort = FStar_Syntax_Subst.subst substs1 (b.FStar_Syntax_Syntax.binder_bv).FStar_Syntax_Syntax.sort in - let ctx_uvar_meta_t = - match ((b.FStar_Syntax_Syntax.binder_qual), - (b.FStar_Syntax_Syntax.binder_attrs)) - with - | (FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Meta t), []) -> - FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Ctx_uvar_meta_tac t) - | (uu___2, t::uu___3) -> - FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Ctx_uvar_meta_attr t) - | uu___2 -> FStar_Pervasives_Native.None in + let ctx_uvar_meta = uvar_meta_for_binder b in let uu___2 = let uu___3 = reason b in let uu___4 = @@ -7250,7 +7259,7 @@ let (uvars_for_binders : "indexed effect uvar in compat mode" else FStar_Syntax_Syntax.Strict in new_implicit_var_aux uu___3 r env1 sort uu___4 - ctx_uvar_meta_t in + ctx_uvar_meta in (match uu___2 with | (t, l_ctx_uvars, g_t) -> ((let uu___4 = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml index b3ab2eff5fc..a76db5befc0 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml @@ -2025,24 +2025,22 @@ let (ad_hoc_indexed_bind_substs : | FStar_Syntax_Syntax.Tm_uvar (u, uu___5) -> let uu___6 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in let uu___7 = - match u.FStar_Syntax_Syntax.ctx_uvar_meta - with - | FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Ctx_uvar_meta_attr - a) -> - FStar_Syntax_Print.term_to_string - a - | uu___8 -> "" in + FStar_Class_Show.show + (FStar_Class_Show.show_option + FStar_Syntax_Print.showable_ctx_uvar_meta) + u.FStar_Syntax_Syntax.ctx_uvar_meta in FStar_Compiler_Util.print2 "Generated uvar %s with attribute %s\n" uu___6 uu___7 | uu___5 -> let uu___6 = let uu___7 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in Prims.strcat "Impossible, expected a uvar, got : " @@ -6488,22 +6486,12 @@ let (instantiate_one_binder : let uu___1 = b in match uu___1 with | { FStar_Syntax_Syntax.binder_bv = x; - FStar_Syntax_Syntax.binder_qual = qual; - FStar_Syntax_Syntax.binder_positivity = uu___2; - FStar_Syntax_Syntax.binder_attrs = attrs;_} -> - let ctx_uvar_meta = - match (qual, attrs) with - | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta - tau), uu___3) -> - FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Ctx_uvar_meta_tac tau) - | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Implicit - uu___3), attr::uu___4) -> - FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Ctx_uvar_meta_attr attr) - | (uu___3, uu___4) -> FStar_Pervasives_Native.None in + FStar_Syntax_Syntax.binder_qual = uu___2; + FStar_Syntax_Syntax.binder_positivity = uu___3; + FStar_Syntax_Syntax.binder_attrs = uu___4;_} -> + let ctx_uvar_meta = FStar_TypeChecker_Env.uvar_meta_for_binder b in let t = x.FStar_Syntax_Syntax.sort in - let uu___3 = + let uu___5 = let msg = let is_typeclass = match ctx_uvar_meta with @@ -6511,7 +6499,7 @@ let (instantiate_one_binder : (FStar_Syntax_Syntax.Ctx_uvar_meta_tac tau) -> FStar_Syntax_Util.is_fvar FStar_Parser_Const.tcresolve_lid tau - | uu___4 -> false in + | uu___6 -> false in if is_typeclass then "Typeclass constraint argument" else @@ -6520,15 +6508,15 @@ let (instantiate_one_binder : else "Instantiating implicit argument" in FStar_TypeChecker_Env.new_implicit_var_aux msg r env t FStar_Syntax_Syntax.Strict ctx_uvar_meta in - (match uu___3 with - | (varg, uu___4, implicits) -> + (match uu___5 with + | (varg, uu___6, implicits) -> let aq = FStar_Syntax_Util.aqual_of_binder b in let arg = (varg, aq) in let r1 = (varg, t, aq, implicits) in - ((let uu___6 = FStar_Compiler_Debug.high () in - if uu___6 + ((let uu___8 = FStar_Compiler_Debug.high () in + if uu___8 then - let uu___7 = + let uu___9 = FStar_Class_Show.show (FStar_Class_Show.show_tuple2 FStar_Syntax_Print.showable_term @@ -6538,7 +6526,7 @@ let (instantiate_one_binder : (FStar_Pervasives_Native.__proj__Mktuple4__item___2 r1)) in FStar_Compiler_Util.print1 - "instantiate_one_binder: result = %s\n" uu___7 + "instantiate_one_binder: result = %s\n" uu___9 else ()); r1))) let (maybe_instantiate : diff --git a/src/syntax/FStar.Syntax.Print.fst b/src/syntax/FStar.Syntax.Print.fst index 42549da033c..baf09296f0a 100644 --- a/src/syntax/FStar.Syntax.Print.fst +++ b/src/syntax/FStar.Syntax.Print.fst @@ -1016,6 +1016,11 @@ instance showable_pat = { show = pat_to_string; } instance showable_const = { show = const_to_string; } instance showable_letbinding = { show = lb_to_string; } instance showable_modul = { show = modul_to_string; } +instance showable_ctx_uvar_meta = { + show = (function + | Ctx_uvar_meta_attr attr -> "Ctx_uvar_meta_attr " ^ show attr + | Ctx_uvar_meta_tac r -> "Ctx_uvar_meta_tac " ^ show r); +} instance pretty_term = { pp = term_to_doc; } instance pretty_univ = { pp = univ_to_doc; } diff --git a/src/syntax/FStar.Syntax.Print.fsti b/src/syntax/FStar.Syntax.Print.fsti index 8b2a9a93dd7..62ad4e3d5ea 100644 --- a/src/syntax/FStar.Syntax.Print.fsti +++ b/src/syntax/FStar.Syntax.Print.fsti @@ -107,6 +107,7 @@ instance val showable_pat : showable pat instance val showable_const : showable sconst instance val showable_letbinding : showable letbinding instance val showable_modul : showable modul +instance val showable_ctx_uvar_meta : showable ctx_uvar_meta_t instance val pretty_term : pretty term instance val pretty_univ : pretty universe diff --git a/src/typechecker/FStar.TypeChecker.DeferredImplicits.fst b/src/typechecker/FStar.TypeChecker.DeferredImplicits.fst index 4ebe8fc2c74..f8605b597fd 100644 --- a/src/typechecker/FStar.TypeChecker.DeferredImplicits.fst +++ b/src/typechecker/FStar.TypeChecker.DeferredImplicits.fst @@ -182,9 +182,9 @@ let find_user_tac_for_uvar env (u:ctx_uvar) : option sigelt = | _ -> None let should_defer_uvar_to_user_tac env (u:ctx_uvar) = - if not env.enable_defer_to_tac then false - else Option.isSome (find_user_tac_for_uvar env u) - + if not env.enable_defer_to_tac + then false + else Some? (find_user_tac_for_uvar env u) let solve_goals_with_tac env g (deferred_goals:implicits) (tac:sigelt) = Profiling.profile (fun () -> diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index 56f9d1913b9..0edf6ba1c03 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -2021,6 +2021,21 @@ let new_implicit_var_aux reason r env k should_check meta = (***************************************************) +let uvar_meta_for_binder (b:binder) : option ctx_uvar_meta_t = + let { binder_bv=x; binder_qual=qual; binder_attrs=attrs } = b in + match qual, attrs with + | Some (Meta tau), _ -> + Some (Ctx_uvar_meta_tac tau) + | _, attr::_ -> + (* NB: it does not have to be marked Implicit to get a + Ctx_uvar_meta_attr. In practice most of them are (or + the typechecker will not decide to instantiate) but the + layered effects checking code will sometimes call this + function on regular explicit binders. *) + Some (Ctx_uvar_meta_attr attr) + | _, _ -> + None + // // Perhaps this should not return a guard, // but only a list of implicits, so that callers don't have to @@ -2030,19 +2045,15 @@ let uvars_for_binders env (bs:S.binders) substs reason r = bs |> List.fold_left (fun (substs, uvars, g) b -> let sort = SS.subst substs b.binder_bv.sort in - let ctx_uvar_meta_t = - match b.binder_qual, b.binder_attrs with - | Some (Meta t), [] -> - Some (Ctx_uvar_meta_tac t) - | _, t::_ -> Some (Ctx_uvar_meta_attr t) - | _ -> None in + let ctx_uvar_meta = uvar_meta_for_binder b in let t, l_ctx_uvars, g_t = new_implicit_var_aux (reason b) r env sort (if Options.compat_pre_typed_indexed_effects () then Allow_untyped "indexed effect uvar in compat mode" else Strict) - ctx_uvar_meta_t in + ctx_uvar_meta + in if !dbg_LayeredEffectsEqns then List.iter (fun (ctx_uvar, _) -> diff --git a/src/typechecker/FStar.TypeChecker.Env.fsti b/src/typechecker/FStar.TypeChecker.Env.fsti index 0a0aa153b14..fb07932942c 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fsti +++ b/src/typechecker/FStar.TypeChecker.Env.fsti @@ -512,6 +512,8 @@ val new_implicit_var_aux : string -> option ctx_uvar_meta_t -> (term & list (ctx_uvar & Range.range) & guard_t) +val uvar_meta_for_binder (b:binder) : option ctx_uvar_meta_t + (* layered effect utils *) (* diff --git a/src/typechecker/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst index d1895fe8897..7addda507b7 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fst +++ b/src/typechecker/FStar.TypeChecker.Util.fst @@ -1043,11 +1043,8 @@ let ad_hoc_indexed_bind_substs env match (SS.compress t).n with | Tm_uvar (u, _ ) -> BU.print2 "Generated uvar %s with attribute %s\n" - (Print.term_to_string t) - (match u.ctx_uvar_meta with - | Some (Ctx_uvar_meta_attr a) -> Print.term_to_string a - | _ -> "") - | _ -> failwith ("Impossible, expected a uvar, got : " ^ Print.term_to_string t)); + (show t) (show u.ctx_uvar_meta) + | _ -> failwith ("Impossible, expected a uvar, got : " ^ show t)); let subst = List.map2 (fun b t -> NT (b.binder_bv, t)) @@ -2849,16 +2846,8 @@ let instantiate_one_binder (env:env_t) (r:Range.range) (b:binder) : term & typ & if Debug.high () then BU.print1 "instantiate_one_binder: Instantiating implicit binder %s\n" (show b); let (++) = Env.conj_guard in - let { binder_bv=x; binder_qual=qual; binder_attrs=attrs } = b in - let ctx_uvar_meta = - match qual, attrs with - | Some (Meta tau), _ -> - Some (Ctx_uvar_meta_tac tau) - | Some (Implicit _), attr::_ -> - Some (Ctx_uvar_meta_attr attr) - | _, _ -> - None - in + let { binder_bv=x } = b in + let ctx_uvar_meta = uvar_meta_for_binder b in (* meta/attrs computed here *) let t = x.sort in let varg, _, implicits = let msg =