diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml index b107db9a02d..6285c480803 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml @@ -1868,6 +1868,20 @@ let (__proj__Mkdebug_switches__item__erase_erasable_args : | { gen; top; cfg; primop; unfolding; b380; wpe; norm_delayed; print_normalized; debug_nbe; erase_erasable_args;_} -> erase_erasable_args +let (no_debug_switches : debug_switches) = + { + gen = false; + top = false; + cfg = false; + primop = false; + unfolding = false; + b380 = false; + wpe = false; + norm_delayed = false; + print_normalized = false; + debug_nbe = false; + erase_erasable_args = false + } type cfg = { steps: fsteps ; @@ -1942,20 +1956,6 @@ let (__proj__Mkcfg__item__compat_memo_ignore_cfg : cfg -> Prims.bool) = | { steps; tcenv; debug; delta_level; primitive_steps; strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> compat_memo_ignore_cfg -let (no_debug_switches : debug_switches) = - { - gen = false; - top = false; - cfg = false; - primop = false; - unfolding = false; - b380 = false; - wpe = false; - norm_delayed = false; - print_normalized = false; - debug_nbe = false; - erase_erasable_args = false - } type prim_step_set = primitive_step FStar_Compiler_Util.psmap let (empty_prim_steps : unit -> prim_step_set) = fun uu___ -> FStar_Compiler_Util.psmap_empty () @@ -4629,7 +4629,8 @@ let (config' : (FStar_TypeChecker_Env.debug e (FStar_Options.Other "Norm")) || dbg_flag in let uu___3 = - FStar_TypeChecker_Env.debug e (FStar_Options.Other "NormTop") in + (FStar_TypeChecker_Env.debug e (FStar_Options.Other "NormTop")) + || dbg_flag in let uu___4 = FStar_TypeChecker_Env.debug e (FStar_Options.Other "NormCfg") in let uu___5 = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml index 0d762306efe..f1a58e816c5 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml @@ -696,85 +696,97 @@ let (check_expected_effect : FStar_Pervasives_Native.None))))) in (match uu___1 with | (expected_c_opt, c1, gopt) -> - let c2 = norm_c env c1 in - (match expected_c_opt with - | FStar_Pervasives_Native.None -> - (e, c2, + (FStar_TypeChecker_Env.def_check_comp_closed_in_env + c1.FStar_Syntax_Syntax.pos + "check_expected_effect.c.before_norm" env c1; + (let c2 = norm_c env c1 in + FStar_TypeChecker_Env.def_check_comp_closed_in_env + c2.FStar_Syntax_Syntax.pos + "check_expected_effect.c.after_norm" env c2; + (match expected_c_opt with + | FStar_Pervasives_Native.None -> + (e, c2, + ((match gopt with + | FStar_Pervasives_Native.None -> + FStar_TypeChecker_Env.trivial_guard + | FStar_Pervasives_Native.Some g -> g))) + | FStar_Pervasives_Native.Some expected_c -> ((match gopt with - | FStar_Pervasives_Native.None -> - FStar_TypeChecker_Env.trivial_guard - | FStar_Pervasives_Native.Some g -> g))) - | FStar_Pervasives_Native.Some expected_c -> - ((match gopt with - | FStar_Pervasives_Native.None -> () - | FStar_Pervasives_Native.Some uu___3 -> - failwith - "Impossible! check_expected_effect, gopt should have been None"); - (let c3 = - let uu___3 = - FStar_TypeChecker_Common.lcomp_of_comp c2 in - FStar_TypeChecker_Util.maybe_assume_result_eq_pure_term - env e uu___3 in - let uu___3 = FStar_TypeChecker_Common.lcomp_comp c3 in - match uu___3 with - | (c4, g_c) -> - ((let uu___5 = - FStar_Compiler_Effect.op_Less_Bar - (FStar_TypeChecker_Env.debug env) - FStar_Options.Medium in - if uu___5 - then - let uu___6 = - FStar_Syntax_Print.term_to_string e in - let uu___7 = - FStar_Syntax_Print.comp_to_string c4 in - let uu___8 = - FStar_Syntax_Print.comp_to_string - expected_c in - let uu___9 = - FStar_Compiler_Util.string_of_bool use_eq in - FStar_Compiler_Util.print4 - "In check_expected_effect, asking rel to solve the problem on e=(%s) and c=(%s), expected_c=(%s), and use_eq=%s\n" - uu___6 uu___7 uu___8 uu___9 - else ()); - (let uu___5 = - FStar_TypeChecker_Util.check_comp env - use_eq e c4 expected_c in - match uu___5 with - | (e1, uu___6, g) -> - let g1 = - let uu___7 = - FStar_TypeChecker_Env.get_range env in - FStar_TypeChecker_Util.label_guard - uu___7 - "Could not prove post-condition" g in - ((let uu___8 = - FStar_TypeChecker_Env.debug env - FStar_Options.Medium in - if uu___8 - then - let uu___9 = - FStar_Compiler_Range_Ops.string_of_range - e1.FStar_Syntax_Syntax.pos in + | FStar_Pervasives_Native.None -> () + | FStar_Pervasives_Native.Some uu___5 -> + failwith + "Impossible! check_expected_effect, gopt should have been None"); + (let c3 = + let uu___5 = + FStar_TypeChecker_Common.lcomp_of_comp c2 in + FStar_TypeChecker_Util.maybe_assume_result_eq_pure_term + env e uu___5 in + let uu___5 = + FStar_TypeChecker_Common.lcomp_comp c3 in + match uu___5 with + | (c4, g_c) -> + (FStar_TypeChecker_Env.def_check_comp_closed_in_env + c4.FStar_Syntax_Syntax.pos + "check_expected_effect.c.after_assume" env + c4; + (let uu___8 = + FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug env) + FStar_Options.Medium in + if uu___8 + then + let uu___9 = + FStar_Syntax_Print.term_to_string e in + let uu___10 = + FStar_Syntax_Print.comp_to_string c4 in + let uu___11 = + FStar_Syntax_Print.comp_to_string + expected_c in + let uu___12 = + FStar_Compiler_Util.string_of_bool + use_eq in + FStar_Compiler_Util.print4 + "In check_expected_effect, asking rel to solve the problem on e=(%s) and c=(%s), expected_c=(%s), and use_eq=%s\n" + uu___9 uu___10 uu___11 uu___12 + else ()); + (let uu___8 = + FStar_TypeChecker_Util.check_comp env + use_eq e c4 expected_c in + match uu___8 with + | (e1, uu___9, g) -> + let g1 = let uu___10 = - FStar_TypeChecker_Rel.guard_to_string - env g1 in - FStar_Compiler_Util.print2 - "(%s) DONE check_expected_effect;\n\tguard is: %s\n" - uu___9 uu___10 - else ()); - (let e2 = - FStar_TypeChecker_Util.maybe_lift env - e1 - (FStar_Syntax_Util.comp_effect_name - c4) - (FStar_Syntax_Util.comp_effect_name - expected_c) - (FStar_Syntax_Util.comp_result c4) in - let uu___8 = - FStar_TypeChecker_Env.conj_guard g_c - g1 in - (e2, expected_c, uu___8))))))))) + FStar_TypeChecker_Env.get_range env in + FStar_TypeChecker_Util.label_guard + uu___10 + "Could not prove post-condition" g in + ((let uu___11 = + FStar_TypeChecker_Env.debug env + FStar_Options.Medium in + if uu___11 + then + let uu___12 = + FStar_Compiler_Range_Ops.string_of_range + e1.FStar_Syntax_Syntax.pos in + let uu___13 = + FStar_TypeChecker_Rel.guard_to_string + env g1 in + FStar_Compiler_Util.print2 + "(%s) DONE check_expected_effect;\n\tguard is: %s\n" + uu___12 uu___13 + else ()); + (let e2 = + FStar_TypeChecker_Util.maybe_lift + env e1 + (FStar_Syntax_Util.comp_effect_name + c4) + (FStar_Syntax_Util.comp_effect_name + expected_c) + (FStar_Syntax_Util.comp_result c4) in + let uu___11 = + FStar_TypeChecker_Env.conj_guard + g_c g1 in + (e2, expected_c, uu___11))))))))))) let no_logical_guard : 'uuuuu 'uuuuu1 . FStar_TypeChecker_Env.env -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml index 90f6a773259..ff253f7cbb2 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml @@ -4861,38 +4861,42 @@ let (check_comp : fun e -> fun c -> fun c' -> - (let uu___1 = + FStar_TypeChecker_Env.def_check_comp_closed_in_env + c.FStar_Syntax_Syntax.pos "check_comp.c" env c; + FStar_TypeChecker_Env.def_check_comp_closed_in_env + c'.FStar_Syntax_Syntax.pos "check_comp.c'" env c'; + (let uu___3 = FStar_Compiler_Effect.op_Less_Bar (FStar_TypeChecker_Env.debug env) FStar_Options.Extreme in - if uu___1 + if uu___3 then - let uu___2 = FStar_Syntax_Print.term_to_string e in - let uu___3 = FStar_Syntax_Print.comp_to_string c in - let uu___4 = FStar_Syntax_Print.comp_to_string c' in + let uu___4 = FStar_Syntax_Print.term_to_string e in + let uu___5 = FStar_Syntax_Print.comp_to_string c in + let uu___6 = FStar_Syntax_Print.comp_to_string c' in FStar_Compiler_Util.print4 "Checking comp relation:\n%s has type %s\n\t %s \n%s\n" - uu___2 uu___3 (if use_eq then "$:" else "<:") uu___4 + uu___4 uu___5 (if use_eq then "$:" else "<:") uu___6 else ()); (let f = if use_eq then FStar_TypeChecker_Rel.eq_comp else FStar_TypeChecker_Rel.sub_comp in - let uu___1 = f env c c' in - match uu___1 with + let uu___3 = f env c c' in + match uu___3 with | FStar_Pervasives_Native.None -> if use_eq then - let uu___2 = + let uu___4 = FStar_TypeChecker_Err.computed_computation_type_does_not_match_annotation_eq env e c c' in - let uu___3 = FStar_TypeChecker_Env.get_range env in - FStar_Errors.raise_error uu___2 uu___3 + let uu___5 = FStar_TypeChecker_Env.get_range env in + FStar_Errors.raise_error uu___4 uu___5 else - (let uu___3 = + (let uu___5 = FStar_TypeChecker_Err.computed_computation_type_does_not_match_annotation env e c c' in - let uu___4 = FStar_TypeChecker_Env.get_range env in - FStar_Errors.raise_error uu___3 uu___4) + let uu___6 = FStar_TypeChecker_Env.get_range env in + FStar_Errors.raise_error uu___5 uu___6) | FStar_Pervasives_Native.Some g -> (e, c', g)) let (universe_of_comp : FStar_TypeChecker_Env.env -> @@ -8850,28 +8854,9 @@ let (try_lookup_record_type : is_rec } in FStar_Pervasives_Native.Some r) - else - ((let uu___16 = - FStar_Compiler_Util.string_of_int nparms in - let uu___17 = - FStar_Syntax_Print.term_to_string t in - let uu___18 = - FStar_Syntax_Print.binders_to_string ", " - formals in - FStar_Compiler_Util.print3 - "Not enough formals; nparms=%s; type = %s; formals=%s\n" - uu___16 uu___17 uu___18); - FStar_Pervasives_Native.None)) - | uu___3 -> - ((let uu___5 = FStar_Ident.string_of_lid dc in - FStar_Compiler_Util.print1 "Could not find %s\n" - uu___5); - FStar_Pervasives_Native.None)) - | (uu___2, dcs) -> - ((let uu___4 = FStar_Ident.string_of_lid typename in - FStar_Compiler_Util.print1 - "Could not find type %s ... Got %s\n" uu___4); - FStar_Pervasives_Native.None))) () + else FStar_Pervasives_Native.None) + | uu___3 -> FStar_Pervasives_Native.None) + | (uu___2, dcs) -> FStar_Pervasives_Native.None)) () with | uu___ -> FStar_Pervasives_Native.None let (find_record_or_dc_from_typ : FStar_TypeChecker_Env.env -> diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst index 0ae303a14fe..fa6059cf793 100644 --- a/src/typechecker/FStar.TypeChecker.Cfg.fst +++ b/src/typechecker/FStar.TypeChecker.Cfg.fst @@ -1559,7 +1559,7 @@ let config' psteps s e = {tcenv = e; debug = if dbg_flag || Options.debug_any () then { gen = Env.debug e (Options.Other "Norm") || dbg_flag - ; top = Env.debug e (Options.Other "NormTop") + ; top = Env.debug e (Options.Other "NormTop") || dbg_flag ; cfg = Env.debug e (Options.Other "NormCfg") ; primop = Env.debug e (Options.Other "Primops") ; unfolding = Env.debug e (Options.Other "Unfolding") diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fsti b/src/typechecker/FStar.TypeChecker.Cfg.fsti index 9ab766f9165..9963d9e80d7 100644 --- a/src/typechecker/FStar.TypeChecker.Cfg.fsti +++ b/src/typechecker/FStar.TypeChecker.Cfg.fsti @@ -113,6 +113,8 @@ type debug_switches = { erase_erasable_args: bool; } +val no_debug_switches : debug_switches + type cfg = { steps: fsteps; tcenv: Env.env; diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index b912ccc1a8b..16f4b64f1ce 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/src/typechecker/FStar.TypeChecker.Normalize.fst @@ -100,7 +100,7 @@ type branches = list (pat * option term * term) type stack_elt = | Arg of closure * aqual * Range.range - | UnivArgs of list universe * Range.range + | UnivArgs of list universe * Range.range // NB: universes must be values already, no bvars allowed | MemoLazy of cfg_memo (env * term) | Match of env * option match_returns_ascription * branches * option residual_comp * cfg * Range.range | Abs of env * binders * env * option residual_comp * Range.range //the second env is the first one extended with the binders, for reducing the option lcomp diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst index e6034d1af1d..7f913cb6802 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst @@ -298,7 +298,9 @@ let check_expected_effect env (use_eq:bool) (copt:option comp) (ec : term * comp Some g) else None, c, None in + def_check_comp_closed_in_env c.pos "check_expected_effect.c.before_norm" env c; let c = norm_c env c in + def_check_comp_closed_in_env c.pos "check_expected_effect.c.after_norm" env c; match expected_c_opt with | None -> e, c, (match gopt with | None -> Env.trivial_guard | Some g -> g) @@ -310,6 +312,7 @@ let check_expected_effect env (use_eq:bool) (copt:option comp) (ec : term * comp let c = TcUtil.maybe_assume_result_eq_pure_term env e (TcComm.lcomp_of_comp c) in let c, g_c = TcComm.lcomp_comp c in + def_check_comp_closed_in_env c.pos "check_expected_effect.c.after_assume" env c; if debug env <| Options.Medium then BU.print4 "In check_expected_effect, asking rel to solve the problem on e=(%s) and c=(%s), expected_c=(%s), and use_eq=%s\n" (Print.term_to_string e) diff --git a/src/typechecker/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst index 46150678545..325727f84f6 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fst +++ b/src/typechecker/FStar.TypeChecker.Util.fst @@ -2227,6 +2227,8 @@ let bind_cases env0 (res_t:typ) TcComm.mk_lcomp eff res_t bind_cases_flags bind_cases let check_comp env (use_eq:bool) (e:term) (c:comp) (c':comp) : term * comp * guard_t = + def_check_comp_closed_in_env c.pos "check_comp.c" env c; + def_check_comp_closed_in_env c'.pos "check_comp.c'" env c'; if Env.debug env <| Options.Extreme then BU.print4 "Checking comp relation:\n%s has type %s\n\t %s \n%s\n" (Print.term_to_string e) @@ -3750,17 +3752,19 @@ let try_lookup_record_type env (typename:lident) Some r else ( - BU.print3 "Not enough formals; nparms=%s; type = %s; formals=%s\n" - (string_of_int nparms) - (Print.term_to_string t) - (Print.binders_to_string ", " formals); + // BU.print3 "Not enough formals; nparms=%s; type = %s; formals=%s\n" + // (string_of_int nparms) + // (Print.term_to_string t) + // (Print.binders_to_string ", " formals); None ) | _ -> - BU.print1 "Could not find %s\n" (string_of_lid dc); + // BU.print1 "Could not find %s\n" (string_of_lid dc); None) | _, dcs -> - BU.print1 "Could not find type %s ... Got %s\n" (string_of_lid typename); + // BU.print2 "Could not find type %s ... Got %s\n" + // (string_of_lid typename) + // (FStar.Common.string_of_list Ident.string_of_lid dcs); None with | _ -> None