From 1f0fb1fde70c2bb48d087846b054d5da2f96cb9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 1 Aug 2023 11:38:05 -0700 Subject: [PATCH] snap --- ocaml/fstar-lib/generated/FStar_Errors.ml | 52 +- .../generated/FStar_SMTEncoding_Solver.ml | 12 +- .../generated/FStar_Tactics_V1_Basic.ml | 1167 +---------------- .../generated/FStar_Tactics_V1_Interpreter.ml | 608 +-------- 4 files changed, 58 insertions(+), 1781 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Errors.ml b/ocaml/fstar-lib/generated/FStar_Errors.ml index 3e09a6991a6..41ba23efa4b 100644 --- a/ocaml/fstar-lib/generated/FStar_Errors.ml +++ b/ocaml/fstar-lib/generated/FStar_Errors.ml @@ -519,6 +519,52 @@ let (diag : FStar_Compiler_Range_Type.range -> Prims.string -> unit) = (mk_issue EInfo (FStar_Pervasives_Native.Some r) msg FStar_Pervasives_Native.None []) else () +let (diag0 : Prims.string -> unit) = + fun msg -> + let uu___ = FStar_Options.debug_any () in + if uu___ + then + add_one + (mk_issue EInfo FStar_Pervasives_Native.None msg + FStar_Pervasives_Native.None []) + else () +let (diag1 : Prims.string -> Prims.string -> unit) = + fun f -> + fun a -> let uu___ = FStar_Compiler_Util.format1 f a in diag0 uu___ +let (diag2 : Prims.string -> Prims.string -> Prims.string -> unit) = + fun f -> + fun a -> + fun b -> let uu___ = FStar_Compiler_Util.format2 f a b in diag0 uu___ +let (diag3 : + Prims.string -> Prims.string -> Prims.string -> Prims.string -> unit) = + fun f -> + fun a -> + fun b -> + fun c -> + let uu___ = FStar_Compiler_Util.format3 f a b c in diag0 uu___ +let (diag4 : + Prims.string -> + Prims.string -> Prims.string -> Prims.string -> Prims.string -> unit) + = + fun f -> + fun a -> + fun b -> + fun c -> + fun d -> + let uu___ = FStar_Compiler_Util.format4 f a b c d in diag0 uu___ +let (diag5 : + Prims.string -> + Prims.string -> + Prims.string -> Prims.string -> Prims.string -> Prims.string -> unit) + = + fun f -> + fun a -> + fun b -> + fun c -> + fun d -> + fun e -> + let uu___ = FStar_Compiler_Util.format5 f a b c d e in + diag0 uu___ let (warn_unsafe_options : FStar_Compiler_Range_Type.range FStar_Pervasives_Native.option -> Prims.string -> unit) @@ -548,7 +594,7 @@ let (set_option_warning_callback_range : FStar_Compiler_Range_Type.range FStar_Pervasives_Native.option -> unit) = fun ropt -> FStar_Options.set_option_warning_callback (warn_unsafe_options ropt) -let (uu___299 : +let (uu___342 : (((Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) * (unit -> FStar_Errors_Codes.error_setting Prims.list))) = @@ -594,10 +640,10 @@ let (uu___299 : (set_callbacks, get_error_flags) let (t_set_parse_warn_error : (Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) = - match uu___299 with + match uu___342 with | (t_set_parse_warn_error1, error_flags) -> t_set_parse_warn_error1 let (error_flags : unit -> FStar_Errors_Codes.error_setting Prims.list) = - match uu___299 with + match uu___342 with | (t_set_parse_warn_error1, error_flags1) -> error_flags1 let (set_parse_warn_error : (Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) = diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml index a78ec1063af..e1154d8bce0 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml @@ -855,6 +855,7 @@ let (report_errors : query_settings -> unit) = fun qry_settings -> let uu___ = errors_to_report qry_settings in FStar_Errors.add_errors uu___ +let (rlimit_conversion_factor : Prims.int) = (Prims.parse_int "544656") let (query_info : query_settings -> FStar_SMTEncoding_Z3.z3result -> unit) = fun settings -> fun z3result -> @@ -1047,7 +1048,8 @@ let (query_info : query_settings -> FStar_SMTEncoding_Z3.z3result -> unit) = let uu___16 = let uu___17 = FStar_Compiler_Util.string_of_int - settings.query_rlimit in + (settings.query_rlimit / + rlimit_conversion_factor) in [uu___17; stats] in uu___15 :: uu___16 in uu___13 :: uu___14 in @@ -1277,11 +1279,11 @@ let (make_solver_configs : match uu___1 with | (qname, index) -> let rlimit = - let uu___2 = FStar_Options.z3_rlimit_factor () in - let uu___3 = + let uu___2 = + let uu___3 = FStar_Options.z3_rlimit_factor () in let uu___4 = FStar_Options.z3_rlimit () in - uu___4 * (Prims.parse_int "544656") in - uu___2 * uu___3 in + FStar_Mul.op_Star uu___3 uu___4 in + FStar_Mul.op_Star uu___2 rlimit_conversion_factor in let next_hint = get_hint_for qname index in let default_settings = let uu___2 = FStar_TypeChecker_Env.get_range env in diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml index 6a7e862c243..c77b310d06e 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml @@ -7253,1169 +7253,4 @@ let (unexpected_uvars_issue : FStar_Errors.issue_number = uu___; FStar_Errors.issue_ctx = [] } in - i -let (refl_check_relation : - env -> - FStar_Syntax_Syntax.typ -> - FStar_Syntax_Syntax.typ -> - relation -> - (unit FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = - fun g -> - fun t0 -> - fun t1 -> - fun rel -> - let uu___ = - ((no_uvars_in_g g) && (no_uvars_in_term t0)) && - (no_uvars_in_term t1) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string t0 in - let uu___5 = FStar_Syntax_Print.term_to_string t1 in - FStar_Compiler_Util.format3 - "refl_check_relation: %s %s %s\n" uu___4 - (if rel = Subtyping then "<:?" else "=?=") uu___5); - (let f = - if rel = Subtyping - then FStar_TypeChecker_Core.check_term_subtyping - else FStar_TypeChecker_Core.check_term_equality in - let uu___3 = f g t0 t1 in - match uu___3 with - | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) -> - dbg_refl g - (fun uu___5 -> - "refl_check_relation: succeeded (no guard)") - | FStar_Pervasives.Inl (FStar_Pervasives_Native.Some - guard_f) -> - (FStar_TypeChecker_Rel.force_trivial_guard g - { - FStar_TypeChecker_Common.guard_f = - (FStar_TypeChecker_Common.NonTrivial guard_f); - FStar_TypeChecker_Common.deferred_to_tac = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) - }; - dbg_refl g - (fun uu___5 -> "refl_check_relation: succeeded")) - | FStar_Pervasives.Inr err -> - (dbg_refl g - (fun uu___5 -> - let uu___6 = - FStar_TypeChecker_Core.print_error err in - FStar_Compiler_Util.format1 - "refl_check_relation failed: %s\n" uu___6); - (let uu___5 = - let uu___6 = - let uu___7 = - FStar_TypeChecker_Core.print_error err in - Prims.op_Hat "check_relation failed: " uu___7 in - (FStar_Errors_Codes.Fatal_IllTyped, uu___6) in - FStar_Errors.raise_error uu___5 - FStar_Compiler_Range_Type.dummyRange)))) - else - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2) -let (refl_check_subtyping : - env -> - FStar_Syntax_Syntax.typ -> - FStar_Syntax_Syntax.typ -> - (unit FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = fun g -> fun t0 -> fun t1 -> refl_check_relation g t0 t1 Subtyping -let (refl_check_equiv : - env -> - FStar_Syntax_Syntax.typ -> - FStar_Syntax_Syntax.typ -> - (unit FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = fun g -> fun t0 -> fun t1 -> refl_check_relation g t0 t1 Equality -let (to_must_tot : FStar_Tactics_Types.tot_or_ghost -> Prims.bool) = - fun eff -> - match eff with - | FStar_Tactics_Types.E_Total -> true - | FStar_Tactics_Types.E_Ghost -> false -let (refl_norm_type : - env -> FStar_Syntax_Syntax.typ -> FStar_Syntax_Syntax.typ) = - fun g -> - fun t -> - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Exclude FStar_TypeChecker_Env.Zeta] g t -let (refl_core_compute_term_type : - env -> - FStar_Syntax_Syntax.term -> - FStar_Tactics_Types.tot_or_ghost -> - (FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = - fun g -> - fun e -> - fun eff -> - let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - FStar_Compiler_Util.format1 - "refl_core_compute_term_type: %s\n" uu___4); - (let must_tot = to_must_tot eff in - let gh g1 guard = - FStar_TypeChecker_Rel.force_trivial_guard g1 - { - FStar_TypeChecker_Common.guard_f = - (FStar_TypeChecker_Common.NonTrivial guard); - FStar_TypeChecker_Common.deferred_to_tac = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) - }; - true in - let uu___3 = - FStar_TypeChecker_Core.compute_term_type_handle_guards g e - must_tot gh in - match uu___3 with - | FStar_Pervasives.Inl t -> - let t1 = refl_norm_type g t in - (dbg_refl g - (fun uu___5 -> - let uu___6 = FStar_Syntax_Print.term_to_string e in - let uu___7 = FStar_Syntax_Print.term_to_string t1 in - FStar_Compiler_Util.format2 - "refl_core_compute_term_type for %s computed type %s\n" - uu___6 uu___7); - t1) - | FStar_Pervasives.Inr err -> - (dbg_refl g - (fun uu___5 -> - let uu___6 = FStar_TypeChecker_Core.print_error err in - FStar_Compiler_Util.format1 - "refl_core_compute_term_type: %s\n" uu___6); - (let uu___5 = - let uu___6 = - let uu___7 = FStar_TypeChecker_Core.print_error err in - Prims.op_Hat "core_compute_term_type failed: " - uu___7 in - (FStar_Errors_Codes.Fatal_IllTyped, uu___6) in - FStar_Errors.raise_error uu___5 - FStar_Compiler_Range_Type.dummyRange)))) - else - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2) -let (refl_core_check_term : - env -> - FStar_Syntax_Syntax.term -> - FStar_Syntax_Syntax.typ -> - FStar_Tactics_Types.tot_or_ghost -> - (unit FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = - fun g -> - fun e -> - fun t -> - fun eff -> - let uu___ = - ((no_uvars_in_g g) && (no_uvars_in_term e)) && - (no_uvars_in_term t) in - if uu___ - then - Obj.magic - (Obj.repr - (refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - let uu___5 = FStar_Syntax_Print.term_to_string t in - FStar_Compiler_Util.format2 - "refl_core_check_term: term: %s, type: %s\n" - uu___4 uu___5); - (let must_tot = to_must_tot eff in - let uu___3 = - FStar_TypeChecker_Core.check_term g e t must_tot in - match uu___3 with - | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) - -> - (dbg_refl g - (fun uu___5 -> - "refl_core_check_term: succeeded with no guard\n"); - FStar_Tactics_Monad.ret ()) - | FStar_Pervasives.Inl (FStar_Pervasives_Native.Some - guard) -> - (dbg_refl g - (fun uu___5 -> - "refl_core_check_term: succeeded with guard\n"); - FStar_TypeChecker_Rel.force_trivial_guard g - { - FStar_TypeChecker_Common.guard_f = - (FStar_TypeChecker_Common.NonTrivial guard); - FStar_TypeChecker_Common.deferred_to_tac = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) - }; - FStar_Tactics_Monad.ret ()) - | FStar_Pervasives.Inr err -> - (dbg_refl g - (fun uu___5 -> - let uu___6 = - FStar_TypeChecker_Core.print_error err in - FStar_Compiler_Util.format1 - "refl_core_check_term failed: %s\n" - uu___6); - (let uu___5 = - let uu___6 = - let uu___7 = - FStar_TypeChecker_Core.print_error err in - Prims.op_Hat - "refl_core_check_term failed: " uu___7 in - (FStar_Errors_Codes.Fatal_IllTyped, uu___6) in - FStar_Errors.raise_error uu___5 - FStar_Compiler_Range_Type.dummyRange)))))) - else - Obj.magic - (Obj.repr - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2)) -let (refl_tc_term : - env -> - FStar_Syntax_Syntax.term -> - FStar_Tactics_Types.tot_or_ghost -> - ((FStar_Syntax_Syntax.term * FStar_Syntax_Syntax.typ) - FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) - = - fun g -> - fun e -> - fun eff -> - let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - FStar_Compiler_Util.format1 "refl_tc_term: %s\n" uu___4); - dbg_refl g (fun uu___4 -> "refl_tc_term: starting tc {\n"); - (let must_tot = to_must_tot eff in - let g1 = - { - FStar_TypeChecker_Env.solver = - (g.FStar_TypeChecker_Env.solver); - FStar_TypeChecker_Env.range = - (g.FStar_TypeChecker_Env.range); - FStar_TypeChecker_Env.curmodule = - (g.FStar_TypeChecker_Env.curmodule); - FStar_TypeChecker_Env.gamma = - (g.FStar_TypeChecker_Env.gamma); - FStar_TypeChecker_Env.gamma_sig = - (g.FStar_TypeChecker_Env.gamma_sig); - FStar_TypeChecker_Env.gamma_cache = - (g.FStar_TypeChecker_Env.gamma_cache); - FStar_TypeChecker_Env.modules = - (g.FStar_TypeChecker_Env.modules); - FStar_TypeChecker_Env.expected_typ = - (g.FStar_TypeChecker_Env.expected_typ); - FStar_TypeChecker_Env.sigtab = - (g.FStar_TypeChecker_Env.sigtab); - FStar_TypeChecker_Env.attrtab = - (g.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = false; - FStar_TypeChecker_Env.effects = - (g.FStar_TypeChecker_Env.effects); - FStar_TypeChecker_Env.generalize = - (g.FStar_TypeChecker_Env.generalize); - FStar_TypeChecker_Env.letrecs = - (g.FStar_TypeChecker_Env.letrecs); - FStar_TypeChecker_Env.top_level = - (g.FStar_TypeChecker_Env.top_level); - FStar_TypeChecker_Env.check_uvars = - (g.FStar_TypeChecker_Env.check_uvars); - FStar_TypeChecker_Env.use_eq_strict = - (g.FStar_TypeChecker_Env.use_eq_strict); - FStar_TypeChecker_Env.is_iface = - (g.FStar_TypeChecker_Env.is_iface); - FStar_TypeChecker_Env.admit = - (g.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = (g.FStar_TypeChecker_Env.lax); - FStar_TypeChecker_Env.lax_universes = - (g.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = - (g.FStar_TypeChecker_Env.phase1); - FStar_TypeChecker_Env.failhard = - (g.FStar_TypeChecker_Env.failhard); - FStar_TypeChecker_Env.nosynth = - (g.FStar_TypeChecker_Env.nosynth); - FStar_TypeChecker_Env.uvar_subtyping = - (g.FStar_TypeChecker_Env.uvar_subtyping); - FStar_TypeChecker_Env.intactics = - (g.FStar_TypeChecker_Env.intactics); - FStar_TypeChecker_Env.tc_term = - (g.FStar_TypeChecker_Env.tc_term); - FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (g.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); - FStar_TypeChecker_Env.universe_of = - (g.FStar_TypeChecker_Env.universe_of); - FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term - = - (g.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); - FStar_TypeChecker_Env.teq_nosmt_force = - (g.FStar_TypeChecker_Env.teq_nosmt_force); - FStar_TypeChecker_Env.subtype_nosmt_force = - (g.FStar_TypeChecker_Env.subtype_nosmt_force); - FStar_TypeChecker_Env.qtbl_name_and_index = - (g.FStar_TypeChecker_Env.qtbl_name_and_index); - FStar_TypeChecker_Env.normalized_eff_names = - (g.FStar_TypeChecker_Env.normalized_eff_names); - FStar_TypeChecker_Env.fv_delta_depths = - (g.FStar_TypeChecker_Env.fv_delta_depths); - FStar_TypeChecker_Env.proof_ns = - (g.FStar_TypeChecker_Env.proof_ns); - FStar_TypeChecker_Env.synth_hook = - (g.FStar_TypeChecker_Env.synth_hook); - FStar_TypeChecker_Env.try_solve_implicits_hook = - (g.FStar_TypeChecker_Env.try_solve_implicits_hook); - FStar_TypeChecker_Env.splice = - (g.FStar_TypeChecker_Env.splice); - FStar_TypeChecker_Env.mpreprocess = - (g.FStar_TypeChecker_Env.mpreprocess); - FStar_TypeChecker_Env.postprocess = - (g.FStar_TypeChecker_Env.postprocess); - FStar_TypeChecker_Env.identifier_info = - (g.FStar_TypeChecker_Env.identifier_info); - FStar_TypeChecker_Env.tc_hooks = - (g.FStar_TypeChecker_Env.tc_hooks); - FStar_TypeChecker_Env.dsenv = - (g.FStar_TypeChecker_Env.dsenv); - FStar_TypeChecker_Env.nbe = (g.FStar_TypeChecker_Env.nbe); - FStar_TypeChecker_Env.strict_args_tab = - (g.FStar_TypeChecker_Env.strict_args_tab); - FStar_TypeChecker_Env.erasable_types_tab = - (g.FStar_TypeChecker_Env.erasable_types_tab); - FStar_TypeChecker_Env.enable_defer_to_tac = - (g.FStar_TypeChecker_Env.enable_defer_to_tac); - FStar_TypeChecker_Env.unif_allow_ref_guards = - (g.FStar_TypeChecker_Env.unif_allow_ref_guards); - FStar_TypeChecker_Env.erase_erasable_args = - (g.FStar_TypeChecker_Env.erase_erasable_args); - FStar_TypeChecker_Env.core_check = - (g.FStar_TypeChecker_Env.core_check) - } in - let e1 = - let g2 = - { - FStar_TypeChecker_Env.solver = - (g1.FStar_TypeChecker_Env.solver); - FStar_TypeChecker_Env.range = - (g1.FStar_TypeChecker_Env.range); - FStar_TypeChecker_Env.curmodule = - (g1.FStar_TypeChecker_Env.curmodule); - FStar_TypeChecker_Env.gamma = - (g1.FStar_TypeChecker_Env.gamma); - FStar_TypeChecker_Env.gamma_sig = - (g1.FStar_TypeChecker_Env.gamma_sig); - FStar_TypeChecker_Env.gamma_cache = - (g1.FStar_TypeChecker_Env.gamma_cache); - FStar_TypeChecker_Env.modules = - (g1.FStar_TypeChecker_Env.modules); - FStar_TypeChecker_Env.expected_typ = - (g1.FStar_TypeChecker_Env.expected_typ); - FStar_TypeChecker_Env.sigtab = - (g1.FStar_TypeChecker_Env.sigtab); - FStar_TypeChecker_Env.attrtab = - (g1.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = - (g1.FStar_TypeChecker_Env.instantiate_imp); - FStar_TypeChecker_Env.effects = - (g1.FStar_TypeChecker_Env.effects); - FStar_TypeChecker_Env.generalize = - (g1.FStar_TypeChecker_Env.generalize); - FStar_TypeChecker_Env.letrecs = - (g1.FStar_TypeChecker_Env.letrecs); - FStar_TypeChecker_Env.top_level = - (g1.FStar_TypeChecker_Env.top_level); - FStar_TypeChecker_Env.check_uvars = - (g1.FStar_TypeChecker_Env.check_uvars); - FStar_TypeChecker_Env.use_eq_strict = - (g1.FStar_TypeChecker_Env.use_eq_strict); - FStar_TypeChecker_Env.is_iface = - (g1.FStar_TypeChecker_Env.is_iface); - FStar_TypeChecker_Env.admit = - (g1.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = true; - FStar_TypeChecker_Env.lax_universes = - (g1.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = true; - FStar_TypeChecker_Env.failhard = - (g1.FStar_TypeChecker_Env.failhard); - FStar_TypeChecker_Env.nosynth = - (g1.FStar_TypeChecker_Env.nosynth); - FStar_TypeChecker_Env.uvar_subtyping = - (g1.FStar_TypeChecker_Env.uvar_subtyping); - FStar_TypeChecker_Env.intactics = - (g1.FStar_TypeChecker_Env.intactics); - FStar_TypeChecker_Env.tc_term = - (g1.FStar_TypeChecker_Env.tc_term); - FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (g1.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); - FStar_TypeChecker_Env.universe_of = - (g1.FStar_TypeChecker_Env.universe_of); - FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term - = - (g1.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); - FStar_TypeChecker_Env.teq_nosmt_force = - (g1.FStar_TypeChecker_Env.teq_nosmt_force); - FStar_TypeChecker_Env.subtype_nosmt_force = - (g1.FStar_TypeChecker_Env.subtype_nosmt_force); - FStar_TypeChecker_Env.qtbl_name_and_index = - (g1.FStar_TypeChecker_Env.qtbl_name_and_index); - FStar_TypeChecker_Env.normalized_eff_names = - (g1.FStar_TypeChecker_Env.normalized_eff_names); - FStar_TypeChecker_Env.fv_delta_depths = - (g1.FStar_TypeChecker_Env.fv_delta_depths); - FStar_TypeChecker_Env.proof_ns = - (g1.FStar_TypeChecker_Env.proof_ns); - FStar_TypeChecker_Env.synth_hook = - (g1.FStar_TypeChecker_Env.synth_hook); - FStar_TypeChecker_Env.try_solve_implicits_hook = - (g1.FStar_TypeChecker_Env.try_solve_implicits_hook); - FStar_TypeChecker_Env.splice = - (g1.FStar_TypeChecker_Env.splice); - FStar_TypeChecker_Env.mpreprocess = - (g1.FStar_TypeChecker_Env.mpreprocess); - FStar_TypeChecker_Env.postprocess = - (g1.FStar_TypeChecker_Env.postprocess); - FStar_TypeChecker_Env.identifier_info = - (g1.FStar_TypeChecker_Env.identifier_info); - FStar_TypeChecker_Env.tc_hooks = - (g1.FStar_TypeChecker_Env.tc_hooks); - FStar_TypeChecker_Env.dsenv = - (g1.FStar_TypeChecker_Env.dsenv); - FStar_TypeChecker_Env.nbe = - (g1.FStar_TypeChecker_Env.nbe); - FStar_TypeChecker_Env.strict_args_tab = - (g1.FStar_TypeChecker_Env.strict_args_tab); - FStar_TypeChecker_Env.erasable_types_tab = - (g1.FStar_TypeChecker_Env.erasable_types_tab); - FStar_TypeChecker_Env.enable_defer_to_tac = - (g1.FStar_TypeChecker_Env.enable_defer_to_tac); - FStar_TypeChecker_Env.unif_allow_ref_guards = - (g1.FStar_TypeChecker_Env.unif_allow_ref_guards); - FStar_TypeChecker_Env.erase_erasable_args = - (g1.FStar_TypeChecker_Env.erase_erasable_args); - FStar_TypeChecker_Env.core_check = - (g1.FStar_TypeChecker_Env.core_check) - } in - let uu___4 = - g2.FStar_TypeChecker_Env.typeof_tot_or_gtot_term g2 e - must_tot in - match uu___4 with - | (e2, uu___5, guard) -> - (FStar_TypeChecker_Rel.force_trivial_guard g2 guard; e2) in - try - (fun uu___4 -> - match () with - | () -> - let e2 = - FStar_Syntax_Compress.deep_compress false e1 in - (dbg_refl g1 - (fun uu___6 -> - let uu___7 = - FStar_Syntax_Print.term_to_string e2 in - FStar_Compiler_Util.format1 - "} finished tc with e = %s\n" uu___7); - (let gh g2 guard = - FStar_TypeChecker_Rel.force_trivial_guard g2 - { - FStar_TypeChecker_Common.guard_f = - (FStar_TypeChecker_Common.NonTrivial guard); - FStar_TypeChecker_Common.deferred_to_tac = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) - }; - true in - let uu___6 = - FStar_TypeChecker_Core.compute_term_type_handle_guards - g1 e2 must_tot gh in - match uu___6 with - | FStar_Pervasives.Inl t -> - let t1 = refl_norm_type g1 t in - (dbg_refl g1 - (fun uu___8 -> - let uu___9 = - FStar_Syntax_Print.term_to_string e2 in - let uu___10 = - FStar_Syntax_Print.term_to_string t1 in - FStar_Compiler_Util.format2 - "refl_tc_term for %s computed type %s\n" - uu___9 uu___10); - (e2, t1)) - | FStar_Pervasives.Inr err -> - (dbg_refl g1 - (fun uu___8 -> - let uu___9 = - FStar_TypeChecker_Core.print_error err in - FStar_Compiler_Util.format1 - "refl_tc_term failed: %s\n" uu___9); - (let uu___8 = - let uu___9 = - let uu___10 = - FStar_TypeChecker_Core.print_error err in - Prims.op_Hat "tc_term callback failed: " - uu___10 in - (FStar_Errors_Codes.Fatal_IllTyped, - uu___9) in - FStar_Errors.raise_error uu___8 - e2.FStar_Syntax_Syntax.pos))))) () - with - | FStar_Errors.Error - (FStar_Errors_Codes.Error_UnexpectedUnresolvedUvar, - uu___5, uu___6, uu___7) - -> - FStar_Errors.raise_error - (FStar_Errors_Codes.Fatal_IllTyped, - "UVars remaing in term after tc_term callback") - e1.FStar_Syntax_Syntax.pos)) - else - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2) -let (refl_universe_of : - env -> - FStar_Syntax_Syntax.term -> - (FStar_Syntax_Syntax.universe FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = - fun g -> - fun e -> - let check_univ_var_resolved u = - let uu___ = FStar_Syntax_Subst.compress_univ u in - match uu___ with - | FStar_Syntax_Syntax.U_unif uu___1 -> - FStar_Errors.raise_error - (FStar_Errors_Codes.Fatal_IllTyped, - "Unresolved variable in universe_of callback") - FStar_Compiler_Range_Type.dummyRange - | u1 -> u1 in - let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - let uu___2 = FStar_Syntax_Util.type_u () in - match uu___2 with - | (t, u) -> - let must_tot = false in - let uu___3 = - FStar_TypeChecker_Core.check_term g e t must_tot in - (match uu___3 with - | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) -> - check_univ_var_resolved u - | FStar_Pervasives.Inl (FStar_Pervasives_Native.Some guard) - -> - (FStar_TypeChecker_Rel.force_trivial_guard g - { - FStar_TypeChecker_Common.guard_f = - (FStar_TypeChecker_Common.NonTrivial guard); - FStar_TypeChecker_Common.deferred_to_tac = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) - }; - check_univ_var_resolved u) - | FStar_Pervasives.Inr err -> - let msg = - let uu___4 = FStar_TypeChecker_Core.print_error err in - FStar_Compiler_Util.format1 - "refl_universe_of failed: %s\n" uu___4 in - (dbg_refl g (fun uu___5 -> msg); - (let uu___5 = - let uu___6 = - let uu___7 = - FStar_TypeChecker_Core.print_error err in - Prims.op_Hat "universe_of failed: " uu___7 in - (FStar_Errors_Codes.Fatal_IllTyped, uu___6) in - FStar_Errors.raise_error uu___5 - FStar_Compiler_Range_Type.dummyRange)))) - else - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2) -let (refl_check_prop_validity : - env -> - FStar_Syntax_Syntax.term -> - (unit FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) - = - fun g -> - fun e -> - let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - FStar_Compiler_Util.format1 - "refl_check_prop_validity: %s\n" uu___4); - (let must_tot = false in - (let uu___4 = - let uu___5 = - FStar_Syntax_Util.fvar_const FStar_Parser_Const.prop_lid in - FStar_TypeChecker_Core.check_term g e uu___5 must_tot in - match uu___4 with - | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) -> () - | FStar_Pervasives.Inl (FStar_Pervasives_Native.Some guard) -> - FStar_TypeChecker_Rel.force_trivial_guard g - { - FStar_TypeChecker_Common.guard_f = - (FStar_TypeChecker_Common.NonTrivial guard); - FStar_TypeChecker_Common.deferred_to_tac = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) - } - | FStar_Pervasives.Inr err -> - let msg = - let uu___5 = FStar_TypeChecker_Core.print_error err in - FStar_Compiler_Util.format1 - "refl_check_prop_validity failed (not a prop): %s\n" - uu___5 in - (dbg_refl g (fun uu___6 -> msg); - FStar_Errors.raise_error - (FStar_Errors_Codes.Fatal_IllTyped, msg) - FStar_Compiler_Range_Type.dummyRange)); - FStar_TypeChecker_Rel.force_trivial_guard g - { - FStar_TypeChecker_Common.guard_f = - (FStar_TypeChecker_Common.NonTrivial e); - FStar_TypeChecker_Common.deferred_to_tac = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) - })) - else - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2) -let (refl_instantiate_implicits : - env -> - FStar_Syntax_Syntax.term -> - ((FStar_Syntax_Syntax.term * FStar_Syntax_Syntax.typ) - FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) - = - fun g -> - fun e -> - let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - FStar_Compiler_Util.format1 - "refl_instantiate_implicits: %s\n" uu___4); - dbg_refl g - (fun uu___4 -> "refl_instantiate_implicits: starting tc {\n"); - (let must_tot = true in - let g1 = - { - FStar_TypeChecker_Env.solver = - (g.FStar_TypeChecker_Env.solver); - FStar_TypeChecker_Env.range = - (g.FStar_TypeChecker_Env.range); - FStar_TypeChecker_Env.curmodule = - (g.FStar_TypeChecker_Env.curmodule); - FStar_TypeChecker_Env.gamma = - (g.FStar_TypeChecker_Env.gamma); - FStar_TypeChecker_Env.gamma_sig = - (g.FStar_TypeChecker_Env.gamma_sig); - FStar_TypeChecker_Env.gamma_cache = - (g.FStar_TypeChecker_Env.gamma_cache); - FStar_TypeChecker_Env.modules = - (g.FStar_TypeChecker_Env.modules); - FStar_TypeChecker_Env.expected_typ = - (g.FStar_TypeChecker_Env.expected_typ); - FStar_TypeChecker_Env.sigtab = - (g.FStar_TypeChecker_Env.sigtab); - FStar_TypeChecker_Env.attrtab = - (g.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = false; - FStar_TypeChecker_Env.effects = - (g.FStar_TypeChecker_Env.effects); - FStar_TypeChecker_Env.generalize = - (g.FStar_TypeChecker_Env.generalize); - FStar_TypeChecker_Env.letrecs = - (g.FStar_TypeChecker_Env.letrecs); - FStar_TypeChecker_Env.top_level = - (g.FStar_TypeChecker_Env.top_level); - FStar_TypeChecker_Env.check_uvars = - (g.FStar_TypeChecker_Env.check_uvars); - FStar_TypeChecker_Env.use_eq_strict = - (g.FStar_TypeChecker_Env.use_eq_strict); - FStar_TypeChecker_Env.is_iface = - (g.FStar_TypeChecker_Env.is_iface); - FStar_TypeChecker_Env.admit = - (g.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = true; - FStar_TypeChecker_Env.lax_universes = - (g.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = true; - FStar_TypeChecker_Env.failhard = - (g.FStar_TypeChecker_Env.failhard); - FStar_TypeChecker_Env.nosynth = - (g.FStar_TypeChecker_Env.nosynth); - FStar_TypeChecker_Env.uvar_subtyping = - (g.FStar_TypeChecker_Env.uvar_subtyping); - FStar_TypeChecker_Env.intactics = - (g.FStar_TypeChecker_Env.intactics); - FStar_TypeChecker_Env.tc_term = - (g.FStar_TypeChecker_Env.tc_term); - FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (g.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); - FStar_TypeChecker_Env.universe_of = - (g.FStar_TypeChecker_Env.universe_of); - FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term = - (g.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); - FStar_TypeChecker_Env.teq_nosmt_force = - (g.FStar_TypeChecker_Env.teq_nosmt_force); - FStar_TypeChecker_Env.subtype_nosmt_force = - (g.FStar_TypeChecker_Env.subtype_nosmt_force); - FStar_TypeChecker_Env.qtbl_name_and_index = - (g.FStar_TypeChecker_Env.qtbl_name_and_index); - FStar_TypeChecker_Env.normalized_eff_names = - (g.FStar_TypeChecker_Env.normalized_eff_names); - FStar_TypeChecker_Env.fv_delta_depths = - (g.FStar_TypeChecker_Env.fv_delta_depths); - FStar_TypeChecker_Env.proof_ns = - (g.FStar_TypeChecker_Env.proof_ns); - FStar_TypeChecker_Env.synth_hook = - (g.FStar_TypeChecker_Env.synth_hook); - FStar_TypeChecker_Env.try_solve_implicits_hook = - (g.FStar_TypeChecker_Env.try_solve_implicits_hook); - FStar_TypeChecker_Env.splice = - (g.FStar_TypeChecker_Env.splice); - FStar_TypeChecker_Env.mpreprocess = - (g.FStar_TypeChecker_Env.mpreprocess); - FStar_TypeChecker_Env.postprocess = - (g.FStar_TypeChecker_Env.postprocess); - FStar_TypeChecker_Env.identifier_info = - (g.FStar_TypeChecker_Env.identifier_info); - FStar_TypeChecker_Env.tc_hooks = - (g.FStar_TypeChecker_Env.tc_hooks); - FStar_TypeChecker_Env.dsenv = - (g.FStar_TypeChecker_Env.dsenv); - FStar_TypeChecker_Env.nbe = (g.FStar_TypeChecker_Env.nbe); - FStar_TypeChecker_Env.strict_args_tab = - (g.FStar_TypeChecker_Env.strict_args_tab); - FStar_TypeChecker_Env.erasable_types_tab = - (g.FStar_TypeChecker_Env.erasable_types_tab); - FStar_TypeChecker_Env.enable_defer_to_tac = - (g.FStar_TypeChecker_Env.enable_defer_to_tac); - FStar_TypeChecker_Env.unif_allow_ref_guards = - (g.FStar_TypeChecker_Env.unif_allow_ref_guards); - FStar_TypeChecker_Env.erase_erasable_args = - (g.FStar_TypeChecker_Env.erase_erasable_args); - FStar_TypeChecker_Env.core_check = - (g.FStar_TypeChecker_Env.core_check) - } in - let uu___4 = - g1.FStar_TypeChecker_Env.typeof_tot_or_gtot_term g1 e - must_tot in - match uu___4 with - | (e1, t, guard) -> - (FStar_TypeChecker_Rel.force_trivial_guard g1 guard; - (let e2 = FStar_Syntax_Compress.deep_compress false e1 in - let t1 = - let uu___6 = - FStar_Compiler_Effect.op_Bar_Greater t - (refl_norm_type g1) in - FStar_Compiler_Effect.op_Bar_Greater uu___6 - (FStar_Syntax_Compress.deep_compress false) in - dbg_refl g1 - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.term_to_string e2 in - let uu___9 = FStar_Syntax_Print.term_to_string t1 in - FStar_Compiler_Util.format2 - "} finished tc with e = %s and t = %s\n" uu___8 - uu___9); - (e2, t1))))) - else - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2) -let (refl_maybe_relate_after_unfolding : - env -> - FStar_Syntax_Syntax.term -> - FStar_Syntax_Syntax.term -> - (FStar_TypeChecker_Core.side FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = - fun g -> - fun t0 -> - fun t1 -> - let uu___ = - ((no_uvars_in_g g) && (no_uvars_in_term t0)) && - (no_uvars_in_term t1) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string t0 in - let uu___5 = FStar_Syntax_Print.term_to_string t1 in - FStar_Compiler_Util.format2 - "refl_maybe_relate_after_unfolding: %s and %s {\n" - uu___4 uu___5); - (let s = - FStar_TypeChecker_Core.maybe_relate_after_unfolding g t0 t1 in - dbg_refl g - (fun uu___4 -> - let uu___5 = FStar_TypeChecker_Core.side_to_string s in - FStar_Compiler_Util.format1 "} returning side: %s\n" - uu___5); - s)) - else - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2) -let (refl_maybe_unfold_head : - env -> - FStar_Syntax_Syntax.term -> - (FStar_Syntax_Syntax.term FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = - fun g -> - fun e -> - let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - FStar_Compiler_Util.format1 - "refl_maybe_unfold_head: %s {\n" uu___4); - (let eopt = FStar_TypeChecker_Normalize.maybe_unfold_head g e in - dbg_refl g - (fun uu___4 -> - let uu___5 = - match eopt with - | FStar_Pervasives_Native.None -> "none" - | FStar_Pervasives_Native.Some e1 -> - FStar_Syntax_Print.term_to_string e1 in - FStar_Compiler_Util.format1 "} eopt = %s\n" uu___5); - if eopt = FStar_Pervasives_Native.None - then - (let uu___4 = - let uu___5 = - let uu___6 = FStar_Syntax_Print.term_to_string e in - FStar_Compiler_Util.format1 - "Could not unfold head: %s\n" uu___6 in - (FStar_Errors_Codes.Fatal_UnexpectedTerm, uu___5) in - FStar_Errors.raise_error uu___4 e.FStar_Syntax_Syntax.pos) - else - FStar_Compiler_Effect.op_Bar_Greater eopt - FStar_Compiler_Util.must)) - else - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Tactics_Monad.ret uu___2) -let (push_open_namespace : - env -> Prims.string Prims.list -> env FStar_Tactics_Monad.tac) = - fun e -> - fun ns -> - let lid = - FStar_Ident.lid_of_path ns FStar_Compiler_Range_Type.dummyRange in - let uu___ = - let uu___1 = - FStar_Syntax_DsEnv.push_namespace e.FStar_TypeChecker_Env.dsenv lid in - { - FStar_TypeChecker_Env.solver = (e.FStar_TypeChecker_Env.solver); - FStar_TypeChecker_Env.range = (e.FStar_TypeChecker_Env.range); - FStar_TypeChecker_Env.curmodule = - (e.FStar_TypeChecker_Env.curmodule); - FStar_TypeChecker_Env.gamma = (e.FStar_TypeChecker_Env.gamma); - FStar_TypeChecker_Env.gamma_sig = - (e.FStar_TypeChecker_Env.gamma_sig); - FStar_TypeChecker_Env.gamma_cache = - (e.FStar_TypeChecker_Env.gamma_cache); - FStar_TypeChecker_Env.modules = (e.FStar_TypeChecker_Env.modules); - FStar_TypeChecker_Env.expected_typ = - (e.FStar_TypeChecker_Env.expected_typ); - FStar_TypeChecker_Env.sigtab = (e.FStar_TypeChecker_Env.sigtab); - FStar_TypeChecker_Env.attrtab = (e.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = - (e.FStar_TypeChecker_Env.instantiate_imp); - FStar_TypeChecker_Env.effects = (e.FStar_TypeChecker_Env.effects); - FStar_TypeChecker_Env.generalize = - (e.FStar_TypeChecker_Env.generalize); - FStar_TypeChecker_Env.letrecs = (e.FStar_TypeChecker_Env.letrecs); - FStar_TypeChecker_Env.top_level = - (e.FStar_TypeChecker_Env.top_level); - FStar_TypeChecker_Env.check_uvars = - (e.FStar_TypeChecker_Env.check_uvars); - FStar_TypeChecker_Env.use_eq_strict = - (e.FStar_TypeChecker_Env.use_eq_strict); - FStar_TypeChecker_Env.is_iface = (e.FStar_TypeChecker_Env.is_iface); - FStar_TypeChecker_Env.admit = (e.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = (e.FStar_TypeChecker_Env.lax); - FStar_TypeChecker_Env.lax_universes = - (e.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = (e.FStar_TypeChecker_Env.phase1); - FStar_TypeChecker_Env.failhard = (e.FStar_TypeChecker_Env.failhard); - FStar_TypeChecker_Env.nosynth = (e.FStar_TypeChecker_Env.nosynth); - FStar_TypeChecker_Env.uvar_subtyping = - (e.FStar_TypeChecker_Env.uvar_subtyping); - FStar_TypeChecker_Env.intactics = - (e.FStar_TypeChecker_Env.intactics); - FStar_TypeChecker_Env.tc_term = (e.FStar_TypeChecker_Env.tc_term); - FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (e.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); - FStar_TypeChecker_Env.universe_of = - (e.FStar_TypeChecker_Env.universe_of); - FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term = - (e.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); - FStar_TypeChecker_Env.teq_nosmt_force = - (e.FStar_TypeChecker_Env.teq_nosmt_force); - FStar_TypeChecker_Env.subtype_nosmt_force = - (e.FStar_TypeChecker_Env.subtype_nosmt_force); - FStar_TypeChecker_Env.qtbl_name_and_index = - (e.FStar_TypeChecker_Env.qtbl_name_and_index); - FStar_TypeChecker_Env.normalized_eff_names = - (e.FStar_TypeChecker_Env.normalized_eff_names); - FStar_TypeChecker_Env.fv_delta_depths = - (e.FStar_TypeChecker_Env.fv_delta_depths); - FStar_TypeChecker_Env.proof_ns = (e.FStar_TypeChecker_Env.proof_ns); - FStar_TypeChecker_Env.synth_hook = - (e.FStar_TypeChecker_Env.synth_hook); - FStar_TypeChecker_Env.try_solve_implicits_hook = - (e.FStar_TypeChecker_Env.try_solve_implicits_hook); - FStar_TypeChecker_Env.splice = (e.FStar_TypeChecker_Env.splice); - FStar_TypeChecker_Env.mpreprocess = - (e.FStar_TypeChecker_Env.mpreprocess); - FStar_TypeChecker_Env.postprocess = - (e.FStar_TypeChecker_Env.postprocess); - FStar_TypeChecker_Env.identifier_info = - (e.FStar_TypeChecker_Env.identifier_info); - FStar_TypeChecker_Env.tc_hooks = (e.FStar_TypeChecker_Env.tc_hooks); - FStar_TypeChecker_Env.dsenv = uu___1; - FStar_TypeChecker_Env.nbe = (e.FStar_TypeChecker_Env.nbe); - FStar_TypeChecker_Env.strict_args_tab = - (e.FStar_TypeChecker_Env.strict_args_tab); - FStar_TypeChecker_Env.erasable_types_tab = - (e.FStar_TypeChecker_Env.erasable_types_tab); - FStar_TypeChecker_Env.enable_defer_to_tac = - (e.FStar_TypeChecker_Env.enable_defer_to_tac); - FStar_TypeChecker_Env.unif_allow_ref_guards = - (e.FStar_TypeChecker_Env.unif_allow_ref_guards); - FStar_TypeChecker_Env.erase_erasable_args = - (e.FStar_TypeChecker_Env.erase_erasable_args); - FStar_TypeChecker_Env.core_check = - (e.FStar_TypeChecker_Env.core_check) - } in - FStar_Tactics_Monad.ret uu___ -let (push_module_abbrev : - env -> - Prims.string -> Prims.string Prims.list -> env FStar_Tactics_Monad.tac) - = - fun e -> - fun n -> - fun m -> - let mlid = - FStar_Ident.lid_of_path m FStar_Compiler_Range_Type.dummyRange in - let ident = FStar_Ident.id_of_text n in - let uu___ = - let uu___1 = - FStar_Syntax_DsEnv.push_module_abbrev - e.FStar_TypeChecker_Env.dsenv ident mlid in - { - FStar_TypeChecker_Env.solver = (e.FStar_TypeChecker_Env.solver); - FStar_TypeChecker_Env.range = (e.FStar_TypeChecker_Env.range); - FStar_TypeChecker_Env.curmodule = - (e.FStar_TypeChecker_Env.curmodule); - FStar_TypeChecker_Env.gamma = (e.FStar_TypeChecker_Env.gamma); - FStar_TypeChecker_Env.gamma_sig = - (e.FStar_TypeChecker_Env.gamma_sig); - FStar_TypeChecker_Env.gamma_cache = - (e.FStar_TypeChecker_Env.gamma_cache); - FStar_TypeChecker_Env.modules = (e.FStar_TypeChecker_Env.modules); - FStar_TypeChecker_Env.expected_typ = - (e.FStar_TypeChecker_Env.expected_typ); - FStar_TypeChecker_Env.sigtab = (e.FStar_TypeChecker_Env.sigtab); - FStar_TypeChecker_Env.attrtab = (e.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = - (e.FStar_TypeChecker_Env.instantiate_imp); - FStar_TypeChecker_Env.effects = (e.FStar_TypeChecker_Env.effects); - FStar_TypeChecker_Env.generalize = - (e.FStar_TypeChecker_Env.generalize); - FStar_TypeChecker_Env.letrecs = (e.FStar_TypeChecker_Env.letrecs); - FStar_TypeChecker_Env.top_level = - (e.FStar_TypeChecker_Env.top_level); - FStar_TypeChecker_Env.check_uvars = - (e.FStar_TypeChecker_Env.check_uvars); - FStar_TypeChecker_Env.use_eq_strict = - (e.FStar_TypeChecker_Env.use_eq_strict); - FStar_TypeChecker_Env.is_iface = - (e.FStar_TypeChecker_Env.is_iface); - FStar_TypeChecker_Env.admit = (e.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = (e.FStar_TypeChecker_Env.lax); - FStar_TypeChecker_Env.lax_universes = - (e.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = (e.FStar_TypeChecker_Env.phase1); - FStar_TypeChecker_Env.failhard = - (e.FStar_TypeChecker_Env.failhard); - FStar_TypeChecker_Env.nosynth = (e.FStar_TypeChecker_Env.nosynth); - FStar_TypeChecker_Env.uvar_subtyping = - (e.FStar_TypeChecker_Env.uvar_subtyping); - FStar_TypeChecker_Env.intactics = - (e.FStar_TypeChecker_Env.intactics); - FStar_TypeChecker_Env.tc_term = (e.FStar_TypeChecker_Env.tc_term); - FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (e.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); - FStar_TypeChecker_Env.universe_of = - (e.FStar_TypeChecker_Env.universe_of); - FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term = - (e.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); - FStar_TypeChecker_Env.teq_nosmt_force = - (e.FStar_TypeChecker_Env.teq_nosmt_force); - FStar_TypeChecker_Env.subtype_nosmt_force = - (e.FStar_TypeChecker_Env.subtype_nosmt_force); - FStar_TypeChecker_Env.qtbl_name_and_index = - (e.FStar_TypeChecker_Env.qtbl_name_and_index); - FStar_TypeChecker_Env.normalized_eff_names = - (e.FStar_TypeChecker_Env.normalized_eff_names); - FStar_TypeChecker_Env.fv_delta_depths = - (e.FStar_TypeChecker_Env.fv_delta_depths); - FStar_TypeChecker_Env.proof_ns = - (e.FStar_TypeChecker_Env.proof_ns); - FStar_TypeChecker_Env.synth_hook = - (e.FStar_TypeChecker_Env.synth_hook); - FStar_TypeChecker_Env.try_solve_implicits_hook = - (e.FStar_TypeChecker_Env.try_solve_implicits_hook); - FStar_TypeChecker_Env.splice = (e.FStar_TypeChecker_Env.splice); - FStar_TypeChecker_Env.mpreprocess = - (e.FStar_TypeChecker_Env.mpreprocess); - FStar_TypeChecker_Env.postprocess = - (e.FStar_TypeChecker_Env.postprocess); - FStar_TypeChecker_Env.identifier_info = - (e.FStar_TypeChecker_Env.identifier_info); - FStar_TypeChecker_Env.tc_hooks = - (e.FStar_TypeChecker_Env.tc_hooks); - FStar_TypeChecker_Env.dsenv = uu___1; - FStar_TypeChecker_Env.nbe = (e.FStar_TypeChecker_Env.nbe); - FStar_TypeChecker_Env.strict_args_tab = - (e.FStar_TypeChecker_Env.strict_args_tab); - FStar_TypeChecker_Env.erasable_types_tab = - (e.FStar_TypeChecker_Env.erasable_types_tab); - FStar_TypeChecker_Env.enable_defer_to_tac = - (e.FStar_TypeChecker_Env.enable_defer_to_tac); - FStar_TypeChecker_Env.unif_allow_ref_guards = - (e.FStar_TypeChecker_Env.unif_allow_ref_guards); - FStar_TypeChecker_Env.erase_erasable_args = - (e.FStar_TypeChecker_Env.erase_erasable_args); - FStar_TypeChecker_Env.core_check = - (e.FStar_TypeChecker_Env.core_check) - } in - FStar_Tactics_Monad.ret uu___ -let (resolve_name : - env -> - Prims.string Prims.list -> - (FStar_Syntax_Syntax.bv, FStar_Syntax_Syntax.fv) - FStar_Pervasives.either FStar_Pervasives_Native.option - FStar_Tactics_Monad.tac) - = - fun e -> - fun n -> - let l = FStar_Ident.lid_of_path n FStar_Compiler_Range_Type.dummyRange in - let uu___ = - FStar_Syntax_DsEnv.resolve_name e.FStar_TypeChecker_Env.dsenv l in - FStar_Tactics_Monad.ret uu___ \ No newline at end of file + i \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Interpreter.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Interpreter.ml index a5eb547add8..2295592ed89 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Interpreter.ml @@ -1722,613 +1722,7 @@ let (uu___187 : unit) = FStar_Tactics_V1_Basic.free_uvars FStar_Reflection_V1_NBEEmbeddings.e_term uu___167 in - let uu___166 - = - let uu___167 - = - let uu___168 - = - let uu___169 - = - FStar_Syntax_Embeddings.e_option - FStar_Syntax_Embeddings.e_unit in - let uu___170 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___169 - uu___170 in - let uu___169 - = - let uu___170 - = - FStar_TypeChecker_NBETerm.e_option - FStar_TypeChecker_NBETerm.e_unit in - let uu___171 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___170 - uu___171 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_3 - Prims.int_zero - "check_subtyping" - FStar_Tactics_V1_Basic.refl_check_subtyping - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - FStar_Reflection_V1_Embeddings.e_term - uu___168 - FStar_Tactics_V1_Basic.refl_check_subtyping - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Reflection_V1_NBEEmbeddings.e_term - uu___169 in - let uu___168 - = - let uu___169 - = - let uu___170 - = - let uu___171 - = - FStar_Syntax_Embeddings.e_option - FStar_Syntax_Embeddings.e_unit in - let uu___172 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___171 - uu___172 in - let uu___171 - = - let uu___172 - = - FStar_TypeChecker_NBETerm.e_option - FStar_TypeChecker_NBETerm.e_unit in - let uu___173 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___172 - uu___173 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_3 - Prims.int_zero - "check_equiv" - FStar_Tactics_V1_Basic.refl_check_equiv - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - FStar_Reflection_V1_Embeddings.e_term - uu___170 - FStar_Tactics_V1_Basic.refl_check_equiv - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Reflection_V1_NBEEmbeddings.e_term - uu___171 in - let uu___170 - = - let uu___171 - = - let uu___172 - = - let uu___173 - = - FStar_Syntax_Embeddings.e_option - FStar_Reflection_V1_Embeddings.e_term in - let uu___174 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___173 - uu___174 in - let uu___173 - = - let uu___174 - = - FStar_TypeChecker_NBETerm.e_option - FStar_Reflection_V1_NBEEmbeddings.e_term in - let uu___175 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___174 - uu___175 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_3 - Prims.int_zero - "core_compute_term_type" - FStar_Tactics_V1_Basic.refl_core_compute_term_type - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost - uu___172 - FStar_Tactics_V1_Basic.refl_core_compute_term_type - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost_nbe - uu___173 in - let uu___172 - = - let uu___173 - = - let uu___174 - = - let uu___175 - = - FStar_Syntax_Embeddings.e_option - FStar_Syntax_Embeddings.e_unit in - let uu___176 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___175 - uu___176 in - let uu___175 - = - let uu___176 - = - FStar_TypeChecker_NBETerm.e_option - FStar_TypeChecker_NBETerm.e_unit in - let uu___177 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___176 - uu___177 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_4 - Prims.int_zero - "core_check_term" - FStar_Tactics_V1_Basic.refl_core_check_term - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - FStar_Reflection_V1_Embeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost - uu___174 - FStar_Tactics_V1_Basic.refl_core_check_term - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost_nbe - uu___175 in - let uu___174 - = - let uu___175 - = - let uu___176 - = - let uu___177 - = - let uu___178 - = - FStar_Syntax_Embeddings.e_tuple2 - FStar_Reflection_V1_Embeddings.e_term - FStar_Reflection_V1_Embeddings.e_term in - FStar_Syntax_Embeddings.e_option - uu___178 in - let uu___178 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___177 - uu___178 in - let uu___177 - = - let uu___178 - = - let uu___179 - = - FStar_TypeChecker_NBETerm.e_tuple2 - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Reflection_V1_NBEEmbeddings.e_term in - FStar_TypeChecker_NBETerm.e_option - uu___179 in - let uu___179 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___178 - uu___179 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_3 - Prims.int_zero - "tc_term" - FStar_Tactics_V1_Basic.refl_tc_term - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost - uu___176 - FStar_Tactics_V1_Basic.refl_tc_term - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost_nbe - uu___177 in - let uu___176 - = - let uu___177 - = - let uu___178 - = - let uu___179 - = - FStar_Syntax_Embeddings.e_option - FStar_Reflection_V1_Embeddings.e_universe in - let uu___180 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___179 - uu___180 in - let uu___179 - = - let uu___180 - = - FStar_TypeChecker_NBETerm.e_option - FStar_Reflection_V1_NBEEmbeddings.e_universe in - let uu___181 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___180 - uu___181 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_2 - Prims.int_zero - "universe_of" - FStar_Tactics_V1_Basic.refl_universe_of - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - uu___178 - FStar_Tactics_V1_Basic.refl_universe_of - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - uu___179 in - let uu___178 - = - let uu___179 - = - let uu___180 - = - let uu___181 - = - FStar_Syntax_Embeddings.e_option - FStar_Syntax_Embeddings.e_unit in - let uu___182 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___181 - uu___182 in - let uu___181 - = - let uu___182 - = - FStar_TypeChecker_NBETerm.e_option - FStar_TypeChecker_NBETerm.e_unit in - let uu___183 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___182 - uu___183 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_2 - Prims.int_zero - "check_prop_validity" - FStar_Tactics_V1_Basic.refl_check_prop_validity - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - uu___180 - FStar_Tactics_V1_Basic.refl_check_prop_validity - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - uu___181 in - let uu___180 - = - let uu___181 - = - let uu___182 - = - let uu___183 - = - let uu___184 - = - FStar_Syntax_Embeddings.e_tuple2 - FStar_Reflection_V1_Embeddings.e_term - FStar_Reflection_V1_Embeddings.e_term in - FStar_Syntax_Embeddings.e_option - uu___184 in - let uu___184 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___183 - uu___184 in - let uu___183 - = - let uu___184 - = - let uu___185 - = - FStar_TypeChecker_NBETerm.e_tuple2 - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Reflection_V1_NBEEmbeddings.e_term in - FStar_TypeChecker_NBETerm.e_option - uu___185 in - let uu___185 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___184 - uu___185 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_2 - Prims.int_zero - "instantiate_implicits" - FStar_Tactics_V1_Basic.refl_instantiate_implicits - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - uu___182 - FStar_Tactics_V1_Basic.refl_instantiate_implicits - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - uu___183 in - let uu___182 - = - let uu___183 - = - let uu___184 - = - let uu___185 - = - FStar_Syntax_Embeddings.e_option - FStar_Tactics_Embedding.e_unfold_side in - let uu___186 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___185 - uu___186 in - let uu___185 - = - let uu___186 - = - FStar_TypeChecker_NBETerm.e_option - FStar_Tactics_Embedding.e_unfold_side_nbe in - let uu___188 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___186 - uu___188 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_3 - Prims.int_zero - "maybe_relate_after_unfolding" - FStar_Tactics_V1_Basic.refl_maybe_relate_after_unfolding - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - FStar_Reflection_V1_Embeddings.e_term - uu___184 - FStar_Tactics_V1_Basic.refl_maybe_relate_after_unfolding - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - FStar_Reflection_V1_NBEEmbeddings.e_term - uu___185 in - let uu___184 - = - let uu___185 - = - let uu___186 - = - let uu___188 - = - FStar_Syntax_Embeddings.e_option - FStar_Reflection_V1_Embeddings.e_term in - let uu___189 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - FStar_Syntax_Embeddings.e_tuple2 - uu___188 - uu___189 in - let uu___188 - = - let uu___189 - = - FStar_TypeChecker_NBETerm.e_option - FStar_Reflection_V1_NBEEmbeddings.e_term in - let uu___190 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_TypeChecker_NBETerm.e_tuple2 - uu___189 - uu___190 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_2 - Prims.int_zero - "maybe_unfold_head" - FStar_Tactics_V1_Basic.refl_maybe_unfold_head - FStar_Reflection_V1_Embeddings.e_env - FStar_Reflection_V1_Embeddings.e_term - uu___186 - FStar_Tactics_V1_Basic.refl_maybe_unfold_head - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_Reflection_V1_NBEEmbeddings.e_term - uu___188 in - let uu___186 - = - let uu___188 - = - let uu___189 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_string in - let uu___190 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_string in - FStar_Tactics_V1_InterpFuns.mk_tac_step_2 - Prims.int_zero - "push_open_namespace" - FStar_Tactics_V1_Basic.push_open_namespace - FStar_Reflection_V1_Embeddings.e_env - uu___189 - FStar_Reflection_V1_Embeddings.e_env - FStar_Tactics_V1_Basic.push_open_namespace - FStar_Reflection_V1_NBEEmbeddings.e_env - uu___190 - FStar_Reflection_V1_NBEEmbeddings.e_env in - let uu___189 - = - let uu___190 - = - let uu___191 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_string in - let uu___192 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_string in - FStar_Tactics_V1_InterpFuns.mk_tac_step_3 - Prims.int_zero - "push_module_abbrev" - FStar_Tactics_V1_Basic.push_module_abbrev - FStar_Reflection_V1_Embeddings.e_env - FStar_Syntax_Embeddings.e_string - uu___191 - FStar_Reflection_V1_Embeddings.e_env - FStar_Tactics_V1_Basic.push_module_abbrev - FStar_Reflection_V1_NBEEmbeddings.e_env - FStar_TypeChecker_NBETerm.e_string - uu___192 - FStar_Reflection_V1_NBEEmbeddings.e_env in - let uu___191 - = - let uu___192 - = - let uu___193 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_string in - let uu___194 - = - let uu___195 - = - FStar_Syntax_Embeddings.e_either - FStar_Reflection_V1_Embeddings.e_bv - FStar_Reflection_V1_Embeddings.e_fv in - FStar_Syntax_Embeddings.e_option - uu___195 in - let uu___195 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_string in - let uu___196 - = - let uu___197 - = - FStar_TypeChecker_NBETerm.e_either - FStar_Reflection_V1_NBEEmbeddings.e_bv - FStar_Reflection_V1_NBEEmbeddings.e_fv in - FStar_TypeChecker_NBETerm.e_option - uu___197 in - FStar_Tactics_V1_InterpFuns.mk_tac_step_2 - Prims.int_zero - "resolve_name" - FStar_Tactics_V1_Basic.resolve_name - FStar_Reflection_V1_Embeddings.e_env - uu___193 - uu___194 - FStar_Tactics_V1_Basic.resolve_name - FStar_Reflection_V1_NBEEmbeddings.e_env - uu___195 - uu___196 in - let uu___193 - = - let uu___194 - = - let uu___195 - = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_issue in - let uu___196 - = - FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_issue in - FStar_Tactics_V1_InterpFuns.mk_tac_step_1 - Prims.int_zero - "log_issues" - (fun is - -> - FStar_Errors.add_issues - is; - FStar_Tactics_Monad.ret - ()) - uu___195 - FStar_Syntax_Embeddings.e_unit - (fun is - -> - FStar_Errors.add_issues - is; - FStar_Tactics_Monad.ret - ()) - uu___196 - FStar_TypeChecker_NBETerm.e_unit in - [uu___194] in - uu___192 - :: - uu___193 in - uu___190 - :: - uu___191 in - uu___188 - :: - uu___189 in - uu___185 - :: - uu___186 in - uu___183 - :: - uu___184 in - uu___181 - :: - uu___182 in - uu___179 - :: - uu___180 in - uu___177 - :: - uu___178 in - uu___175 - :: - uu___176 in - uu___173 - :: - uu___174 in - uu___171 - :: - uu___172 in - uu___169 - :: - uu___170 in - uu___167 - :: - uu___168 in - uu___165 - :: - uu___166 in + [uu___165] in uu___163 :: uu___164 in