diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Compress.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Compress.ml index 1f1b6ba0255..a9a1f0a6be4 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Compress.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Compress.ml @@ -1,70 +1,77 @@ open Prims let (compress1_t : - Prims.bool -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) = + Prims.bool -> + Prims.bool -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) + = fun allow_uvars -> - fun t -> - let mk x = FStar_Syntax_Syntax.mk x t.FStar_Syntax_Syntax.pos in - match t.FStar_Syntax_Syntax.n with - | FStar_Syntax_Syntax.Tm_uvar (uv, s) when - Prims.op_Negation allow_uvars -> - let uu___ = - let uu___1 = - let uu___2 = - let uu___3 = - FStar_Syntax_Unionfind.uvar_id - uv.FStar_Syntax_Syntax.ctx_uvar_head in - FStar_Compiler_Util.string_of_int uu___3 in - FStar_Compiler_Util.format1 - "Internal error: unexpected unresolved uvar in deep_compress: %s" - uu___2 in - (FStar_Errors_Codes.Error_UnexpectedUnresolvedUvar, uu___1) in - FStar_Errors.raise_err uu___ - | FStar_Syntax_Syntax.Tm_name bv when Prims.op_Negation allow_uvars -> - ((let uu___1 = FStar_Options.debug_any () in - if uu___1 - then - let uu___2 = - let uu___3 = - let uu___4 = FStar_Syntax_Print.bv_to_string bv in - FStar_Compiler_Util.format1 "Tm_name %s in deep compress" - uu___4 in - (FStar_Errors_Codes.Warning_NameEscape, uu___3) in - FStar_Errors.log_issue t.FStar_Syntax_Syntax.pos uu___2 - else ()); - (let uu___1 = - let uu___2 = - let uu___3 = mk FStar_Syntax_Syntax.Tm_unknown in + fun allow_names -> + fun t -> + let mk x = FStar_Syntax_Syntax.mk x t.FStar_Syntax_Syntax.pos in + match t.FStar_Syntax_Syntax.n with + | FStar_Syntax_Syntax.Tm_uvar (uv, s) when + Prims.op_Negation allow_uvars -> + let uu___ = + let uu___1 = + let uu___2 = + let uu___3 = + FStar_Syntax_Unionfind.uvar_id + uv.FStar_Syntax_Syntax.ctx_uvar_head in + FStar_Compiler_Util.string_of_int uu___3 in + FStar_Compiler_Util.format1 + "Internal error: unexpected unresolved uvar in deep_compress: %s" + uu___2 in + (FStar_Errors_Codes.Error_UnexpectedUnresolvedUvar, uu___1) in + FStar_Errors.raise_err uu___ + | FStar_Syntax_Syntax.Tm_name bv when Prims.op_Negation allow_names + -> + ((let uu___1 = FStar_Options.debug_any () in + if uu___1 + then + let uu___2 = + let uu___3 = + let uu___4 = FStar_Syntax_Print.bv_to_string bv in + FStar_Compiler_Util.format1 "Tm_name %s in deep compress" + uu___4 in + (FStar_Errors_Codes.Warning_NameEscape, uu___3) in + FStar_Errors.log_issue t.FStar_Syntax_Syntax.pos uu___2 + else ()); + (let uu___1 = + let uu___2 = + let uu___3 = mk FStar_Syntax_Syntax.Tm_unknown in + { + FStar_Syntax_Syntax.ppname = + (bv.FStar_Syntax_Syntax.ppname); + FStar_Syntax_Syntax.index = + (bv.FStar_Syntax_Syntax.index); + FStar_Syntax_Syntax.sort = uu___3 + } in + FStar_Syntax_Syntax.Tm_name uu___2 in + mk uu___1)) + | FStar_Syntax_Syntax.Tm_bvar bv -> + let uu___ = + let uu___1 = + let uu___2 = mk FStar_Syntax_Syntax.Tm_unknown in { FStar_Syntax_Syntax.ppname = (bv.FStar_Syntax_Syntax.ppname); FStar_Syntax_Syntax.index = (bv.FStar_Syntax_Syntax.index); - FStar_Syntax_Syntax.sort = uu___3 + FStar_Syntax_Syntax.sort = uu___2 } in - FStar_Syntax_Syntax.Tm_name uu___2 in - mk uu___1)) - | FStar_Syntax_Syntax.Tm_bvar bv -> - let uu___ = - let uu___1 = - let uu___2 = mk FStar_Syntax_Syntax.Tm_unknown in - { - FStar_Syntax_Syntax.ppname = (bv.FStar_Syntax_Syntax.ppname); - FStar_Syntax_Syntax.index = (bv.FStar_Syntax_Syntax.index); - FStar_Syntax_Syntax.sort = uu___2 - } in - FStar_Syntax_Syntax.Tm_bvar uu___1 in - mk uu___ - | FStar_Syntax_Syntax.Tm_name bv -> - let uu___ = - let uu___1 = - let uu___2 = mk FStar_Syntax_Syntax.Tm_unknown in - { - FStar_Syntax_Syntax.ppname = (bv.FStar_Syntax_Syntax.ppname); - FStar_Syntax_Syntax.index = (bv.FStar_Syntax_Syntax.index); - FStar_Syntax_Syntax.sort = uu___2 - } in - FStar_Syntax_Syntax.Tm_name uu___1 in - mk uu___ - | uu___ -> t + FStar_Syntax_Syntax.Tm_bvar uu___1 in + mk uu___ + | FStar_Syntax_Syntax.Tm_name bv -> + let uu___ = + let uu___1 = + let uu___2 = mk FStar_Syntax_Syntax.Tm_unknown in + { + FStar_Syntax_Syntax.ppname = + (bv.FStar_Syntax_Syntax.ppname); + FStar_Syntax_Syntax.index = (bv.FStar_Syntax_Syntax.index); + FStar_Syntax_Syntax.sort = uu___2 + } in + FStar_Syntax_Syntax.Tm_name uu___1 in + mk uu___ + | uu___ -> t let (compress1_u : Prims.bool -> FStar_Syntax_Syntax.universe -> FStar_Syntax_Syntax.universe) = @@ -84,16 +91,22 @@ let (compress1_u : FStar_Errors.raise_err uu___ | uu___ -> u let (deep_compress : - Prims.bool -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) = + Prims.bool -> + Prims.bool -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) + = fun allow_uvars -> - fun tm -> - FStar_Errors.with_ctx "While deep-compressing a term" - (fun uu___ -> - let uu___1 = - let uu___2 = compress1_t allow_uvars in - let uu___3 = compress1_u allow_uvars in - FStar_Syntax_Visit.visit_term_univs uu___2 uu___3 in - uu___1 tm) + fun allow_names -> + fun tm -> + FStar_Errors.with_ctx "While deep-compressing a term" + (fun uu___ -> + let uu___1 = + let uu___2 = compress1_t allow_uvars allow_names in + let uu___3 = compress1_u allow_uvars in + FStar_Syntax_Visit.visit_term_univs uu___2 uu___3 in + uu___1 tm) +let (deep_compress_uvars : + FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) = + deep_compress false true let (deep_compress_if_no_uvars : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term FStar_Pervasives_Native.option) @@ -107,7 +120,7 @@ let (deep_compress_if_no_uvars : | () -> let uu___2 = let uu___3 = - let uu___4 = compress1_t false in + let uu___4 = compress1_t false true in let uu___5 = compress1_u false in FStar_Syntax_Visit.visit_term_univs uu___4 uu___5 in uu___3 tm in @@ -118,16 +131,19 @@ let (deep_compress_if_no_uvars : uu___3) -> FStar_Pervasives_Native.None) let (deep_compress_se : - Prims.bool -> FStar_Syntax_Syntax.sigelt -> FStar_Syntax_Syntax.sigelt) = + Prims.bool -> + Prims.bool -> FStar_Syntax_Syntax.sigelt -> FStar_Syntax_Syntax.sigelt) + = fun allow_uvars -> - fun se -> - let uu___ = - let uu___1 = FStar_Syntax_Print.sigelt_to_string_short se in - FStar_Compiler_Util.format1 "While deep-compressing %s" uu___1 in - FStar_Errors.with_ctx uu___ - (fun uu___1 -> - let uu___2 = - let uu___3 = compress1_t allow_uvars in - let uu___4 = compress1_u allow_uvars in - FStar_Syntax_Visit.visit_sigelt uu___3 uu___4 in - uu___2 se) \ No newline at end of file + fun allow_names -> + fun se -> + let uu___ = + let uu___1 = FStar_Syntax_Print.sigelt_to_string_short se in + FStar_Compiler_Util.format1 "While deep-compressing %s" uu___1 in + FStar_Errors.with_ctx uu___ + (fun uu___1 -> + let uu___2 = + let uu___3 = compress1_t allow_uvars allow_names in + let uu___4 = compress1_u allow_uvars in + FStar_Syntax_Visit.visit_sigelt uu___3 uu___4 in + uu___2 se) \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml index 1af7c1b45a1..b6882a5e7fb 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -6840,12 +6840,14 @@ let __refl_typing_builtin_wrapper : if FStar_Pervasives_Native.uu___is_Some r then let allow_uvars = false in + let allow_names = true in FStar_Compiler_List.map (fun uu___1 -> match uu___1 with | (e, g) -> let uu___2 = - FStar_Syntax_Compress.deep_compress allow_uvars g in + FStar_Syntax_Compress.deep_compress allow_uvars + allow_names g in (e, uu___2)) (FStar_Pervasives_Native.snd (FStar_Pervasives_Native.__proj__Some__item__v r)) @@ -7436,7 +7438,11 @@ let (refl_tc_term : (fun uu___4 -> match () with | () -> - let e2 = FStar_Syntax_Compress.deep_compress false e1 in + let allow_uvars = false in + let allow_names = true in + let e2 = + FStar_Syntax_Compress.deep_compress allow_uvars + allow_names e1 in (dbg_refl g1 (fun uu___6 -> let uu___7 = @@ -7856,13 +7862,18 @@ let (refl_instantiate_implicits : 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 allow_uvars = false in + let allow_names = true in + let e2 = + FStar_Syntax_Compress.deep_compress allow_uvars + allow_names 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 + (FStar_Syntax_Compress.deep_compress allow_uvars + allow_names) in dbg_refl g1 (fun uu___7 -> let uu___8 = FStar_Syntax_Print.term_to_string e2 in diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml index 7f6bbbea0fc..c2bdafe86d8 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml @@ -4543,7 +4543,7 @@ let (compute_term_type_handle_guards : fun g -> fun e -> fun gh -> - let e1 = FStar_Syntax_Compress.deep_compress true e in + let e1 = FStar_Syntax_Compress.deep_compress true true e in let must_tot = false in let uu___ = check_term_top_gh g e1 FStar_Pervasives_Native.None must_tot diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml index ca0861ba687..78a42733463 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml @@ -4783,7 +4783,8 @@ let (tc_decls : (let ses'2 = FStar_Compiler_Effect.op_Bar_Greater ses'1 (FStar_Compiler_List.map - (FStar_Syntax_Compress.deep_compress_se false)) in + (FStar_Syntax_Compress.deep_compress_se false + false)) in let env3 = FStar_Compiler_Effect.op_Bar_Greater ses'2 (FStar_Compiler_List.fold_left @@ -5100,7 +5101,8 @@ let (deep_compress_modul : FStar_Syntax_Syntax.modul -> FStar_Syntax_Syntax.modul) = fun m -> let uu___ = - FStar_Compiler_List.map (FStar_Syntax_Compress.deep_compress_se false) + FStar_Compiler_List.map + (FStar_Syntax_Compress.deep_compress_se false false) m.FStar_Syntax_Syntax.declarations in { FStar_Syntax_Syntax.name = (m.FStar_Syntax_Syntax.name); diff --git a/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml b/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml index 0f6ccebc172..f78e3f52d7d 100644 --- a/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml +++ b/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml @@ -454,7 +454,7 @@ let (tc' : match uu___ with | (tm1, uu___1, g) -> (FStar_TypeChecker_Rel.force_trivial_guard tcenv1 g; - (let tm2 = FStar_Syntax_Compress.deep_compress false tm1 in + (let tm2 = FStar_Syntax_Compress.deep_compress false false tm1 in (tm2, tcenv1))) let (tc : Prims.string -> FStar_Syntax_Syntax.term) = fun s -> let uu___ = tc' s in match uu___ with | (tm, uu___1) -> tm @@ -553,7 +553,8 @@ let (tc_term : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) = match uu___ with | (tm1, uu___1, g) -> (FStar_TypeChecker_Rel.force_trivial_guard tcenv1 g; - (let tm2 = FStar_Syntax_Compress.deep_compress false tm1 in tm2)) + (let tm2 = FStar_Syntax_Compress.deep_compress false false tm1 in + tm2)) let (pars_and_tc_fragment : Prims.string -> unit) = fun s -> FStar_Options.set_option "trace_error" (FStar_Options.Bool true); diff --git a/src/syntax/FStar.Syntax.Compress.fst b/src/syntax/FStar.Syntax.Compress.fst index 54ebb333f4d..98929e54e08 100644 --- a/src/syntax/FStar.Syntax.Compress.fst +++ b/src/syntax/FStar.Syntax.Compress.fst @@ -13,7 +13,7 @@ module Err = FStar.Errors (* This function really just checks for bad(tm) things happening, the actual `compress` call is done by the visitor, so no need to repeat it here. Morally, `deep_compress` is just `visit id` with some checks. *) -let compress1_t (allow_uvars:bool) : term -> term = +let compress1_t (allow_uvars: bool) (allow_names: bool) : term -> term = fun t -> let mk x = Syntax.mk x t.pos in match t.n with @@ -21,7 +21,7 @@ let compress1_t (allow_uvars:bool) : term -> term = Err.raise_err (Err.Error_UnexpectedUnresolvedUvar, format1 "Internal error: unexpected unresolved uvar in deep_compress: %s" (string_of_int (Unionfind.uvar_id uv.ctx_uvar_head))) - | Tm_name bv when not allow_uvars -> + | Tm_name bv when not allow_names -> (* This currently happens, and often, but it should not! *) if Options.debug_any () then Errors.log_issue t.pos (Err.Warning_NameEscape, format1 "Tm_name %s in deep compress" (Syntax.Print.bv_to_string bv)); @@ -63,29 +63,31 @@ function. [1] OCaml's Marshal module can actually serialize closures, but this makes .checked files more brittle, so we don't do it. *) -let deep_compress (allow_uvars:bool) (tm : term) : term = +let deep_compress (allow_uvars:bool) (allow_names: bool) (tm : term) : term = Err.with_ctx ("While deep-compressing a term") (fun () -> Visit.visit_term_univs - (compress1_t allow_uvars) + (compress1_t allow_uvars allow_names) (compress1_u allow_uvars) tm ) +let deep_compress_uvars = deep_compress false true + let deep_compress_if_no_uvars (tm : term) : option term = Err.with_ctx ("While deep-compressing a term") (fun () -> try Some (Visit.visit_term_univs - (compress1_t false) + (compress1_t false true) (compress1_u false) tm) with | FStar.Errors.Err (Err.Error_UnexpectedUnresolvedUvar, _, _) -> None ) -let deep_compress_se (allow_uvars:bool) (se : sigelt) : sigelt = +let deep_compress_se (allow_uvars:bool) (allow_names:bool) (se : sigelt) : sigelt = Err.with_ctx (format1 "While deep-compressing %s" (Syntax.Print.sigelt_to_string_short se)) (fun () -> Visit.visit_sigelt - (compress1_t allow_uvars) + (compress1_t allow_uvars allow_names) (compress1_u allow_uvars) se ) diff --git a/src/syntax/FStar.Syntax.Compress.fsti b/src/syntax/FStar.Syntax.Compress.fsti index c4d6a1bd691..b829a34203f 100644 --- a/src/syntax/FStar.Syntax.Compress.fsti +++ b/src/syntax/FStar.Syntax.Compress.fsti @@ -6,10 +6,14 @@ open FStar.Syntax.Syntax if allow_uvars is false, it raises a hard error if an *unresolved* uvar (term or universe) remains. Resolved uvars are replaced by their solutions, as in compress. *) -val deep_compress (allow_uvars: bool) (t:term) : term +val deep_compress (allow_uvars: bool) (allow_names: bool) (t:term) : term -(* Similar to `deep_compress false t`, except instead of a hard error +(* Alias for deep_compress false true. i.e. allows names but not uvars, +useful to check that a potentially open term does not have any uvars. *) +val deep_compress_uvars (t:term) : term + +(* Similar to `deep_compress false false t`, except instead of a hard error this returns None in case an unresolved uvar is found. *) val deep_compress_if_no_uvars (t:term) : option term -val deep_compress_se (allow_uvars: bool) (se:sigelt) : sigelt +val deep_compress_se (allow_uvars: bool) (allow_names: bool) (se:sigelt) : sigelt diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index ae9910533f6..0dcd1c0e634 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -2138,7 +2138,8 @@ let __refl_typing_builtin_wrapper (f:unit -> 'a & list (env & typ)) : tac (optio let gs = if Some? r then let allow_uvars = false in - List.map (fun (e,g) -> e, SC.deep_compress allow_uvars g) (snd (Some?.v r)) + let allow_names = true in (* terms are potentially open, names are OK *) + List.map (fun (e,g) -> e, SC.deep_compress allow_uvars allow_names g) (snd (Some?.v r)) else [] in @@ -2344,7 +2345,9 @@ let refl_tc_term (g:env) (e:term) : tac (option (term & (Core.tot_or_ghost & typ e in try begin - let e = SC.deep_compress false e in + let allow_uvars = false in + let allow_names = true in (* terms are potentially open, names are OK *) + let e = SC.deep_compress allow_uvars allow_names e in // TODO: may be should we check here that e has no unresolved implicits? dbg_refl g (fun _ -> BU.format1 "} finished tc with e = %s\n" @@ -2464,8 +2467,10 @@ let refl_instantiate_implicits (g:env) (e:term) : tac (option (term & typ) & iss will return this term and it MUST be compressed. It's logical part should be trivial too, as we only lax-typechecked the term. *) Rel.force_trivial_guard g guard; - let e = SC.deep_compress false e in - let t = t |> refl_norm_type g |> SC.deep_compress false in + let allow_uvars = false in + let allow_names = true in (* terms are potentially open, names are OK *) + let e = SC.deep_compress allow_uvars allow_names e in + let t = t |> refl_norm_type g |> SC.deep_compress allow_uvars allow_names in dbg_refl g (fun _ -> BU.format2 "} finished tc with e = %s and t = %s\n" (Print.term_to_string e) diff --git a/src/tests/FStar.Tests.Pars.fst b/src/tests/FStar.Tests.Pars.fst index 4f2b168e626..73bf5ab7226 100644 --- a/src/tests/FStar.Tests.Pars.fst +++ b/src/tests/FStar.Tests.Pars.fst @@ -142,7 +142,7 @@ let tc' s = let tcenv = {tcenv with top_level=false} in let tm, _, g = TcTerm.tc_tot_or_gtot_term tcenv tm in Rel.force_trivial_guard tcenv g; - let tm = FStar.Syntax.Compress.deep_compress false tm in + let tm = FStar.Syntax.Compress.deep_compress false false tm in tm, tcenv let tc s = @@ -154,7 +154,7 @@ let tc_term tm = let tcenv = {tcenv with top_level=false} in let tm, _, g = TcTerm.tc_tot_or_gtot_term tcenv tm in Rel.force_trivial_guard tcenv g; - let tm = FStar.Syntax.Compress.deep_compress false tm in + let tm = FStar.Syntax.Compress.deep_compress false false tm in tm let pars_and_tc_fragment (s:string) = diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst index e4c079d32ca..92ed4ca596e 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fst +++ b/src/typechecker/FStar.TypeChecker.Core.fst @@ -1908,7 +1908,7 @@ let check_term g e t must_tot = | Inr err -> Inr err let compute_term_type_handle_guards g e gh = - let e = FStar.Syntax.Compress.deep_compress true e in + let e = FStar.Syntax.Compress.deep_compress true true e in let must_tot = false in match check_term_top_gh g e None must_tot (Some gh) with | Inl (Some r, None) -> Inl r diff --git a/src/typechecker/FStar.TypeChecker.Tc.fst b/src/typechecker/FStar.TypeChecker.Tc.fst index dde70218a25..a34e71a58d2 100644 --- a/src/typechecker/FStar.TypeChecker.Tc.fst +++ b/src/typechecker/FStar.TypeChecker.Tc.fst @@ -1074,8 +1074,8 @@ let tc_decls env ses = Env.promote_id_info env (compress_and_norm env); - // Compress all checked sigelts - let ses' = ses' |> List.map (Compress.deep_compress_se false) in + // Compress all checked sigelts. Uvars and names are not OK after a full typecheck + let ses' = ses' |> List.map (Compress.deep_compress_se false false) in // Add to the environment let env = ses' |> List.fold_left (fun env se -> add_sigelt_to_env env se false) env in @@ -1175,7 +1175,7 @@ let finish_partial_modul (loading_from_cache:bool) (iface_exists:bool) (en:env) m, env let deep_compress_modul (m:modul) : modul = - { m with declarations = List.map (Compress.deep_compress_se false) m.declarations } + { m with declarations = List.map (Compress.deep_compress_se false false) m.declarations } let tc_modul (env0:env) (m:modul) (iface_exists:bool) :(modul * env) = let msg = "Internals for " ^ string_of_lid m.name in