From dd5911294cdca30137d733f1ea375daba0e10f02 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 3 Oct 2024 09:34:53 -0700 Subject: [PATCH] Replace must_erase_during_extraction with erasable. --- src/typechecker/FStarC.TypeChecker.Env.fst | 11 +-- src/typechecker/FStarC.TypeChecker.Env.fsti | 4 + .../FStarC.TypeChecker.Normalize.fst | 2 + src/typechecker/FStarC.TypeChecker.Quals.fst | 78 +++++++++---------- src/typechecker/FStarC.TypeChecker.Quals.fsti | 1 - src/typechecker/FStarC.TypeChecker.Util.fst | 37 +-------- .../MustEraseForExtraction.fst | 3 +- .../MustEraseForExtraction.fsti | 4 +- ulib/FStar.GSet.fsti | 4 +- ulib/FStar.GhostSet.fsti | 2 +- ulib/FStar.Monotonic.HyperHeap.fsti | 4 +- ulib/FStar.Pervasives.fsti | 14 +--- ulib/FStar.TSet.fst | 2 +- ulib/FStar.TSet.fsti | 4 +- 14 files changed, 62 insertions(+), 108 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Env.fst b/src/typechecker/FStarC.TypeChecker.Env.fst index a8ebf4d6dd9..87f7a1a9687 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fst +++ b/src/typechecker/FStarC.TypeChecker.Env.fst @@ -932,13 +932,8 @@ let cache_in_fv_tab (tab:BU.smap 'a) (fv:fv) (f:unit -> (bool & 'a)) : 'a = let fv_has_erasable_attr env fv = let f () = let ex, erasable = fv_exists_and_has_attr env fv.fv_name.v Const.erasable_attr in - ex,erasable - //unfortunately, treating the Const.must_erase_for_extraction_attr - //in the same way here as erasable_attr leads to regressions in fragile proofs, - //notably in FStar.ModifiesGen, since this expands the class of computation types - //that can be promoted from ghost to tot. That in turn results in slightly different - //smt encodings, leading to breakages. So, sadly, I'm not including must_erase_for_extraction - //here. In any case, must_erase_for_extraction is transitionary and should be removed + let ex, must_erase_for_extraction = fv_exists_and_has_attr env fv.fv_name.v Const.must_erase_for_extraction_attr in + ex, erasable || must_erase_for_extraction in cache_in_fv_tab env.erasable_types_tab fv f @@ -1034,10 +1029,12 @@ let rec non_informative env t = || fv_eq_lid fv Const.erased_lid || fv_has_erasable_attr env fv | Tm_app {hd=head} -> non_informative env head + | Tm_abs {body} -> non_informative env body | Tm_uinst (t, _) -> non_informative env t | Tm_arrow {comp=c} -> (is_pure_or_ghost_comp c && non_informative env (comp_result c)) || is_erasable_effect env (comp_effect_name c) + | Tm_meta {tm} -> non_informative env tm | _ -> false let num_effect_indices env name r = diff --git a/src/typechecker/FStarC.TypeChecker.Env.fsti b/src/typechecker/FStarC.TypeChecker.Env.fsti index fdc48da5081..bd550ef07a8 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fsti +++ b/src/typechecker/FStarC.TypeChecker.Env.fsti @@ -341,7 +341,11 @@ val fv_with_lid_has_attr : env -> fv_lid:lid -> attr_lid:lid -> bool val fv_has_attr : env -> fv -> attr_lid:lid -> bool val fv_has_strict_args : env -> fv -> option (list int) val fv_has_erasable_attr : env -> fv -> bool + +(* `non_informative env t` is true if the type family `t: (... -> Type) is noninformative, + i.e., any `x: t ...` can be erased to `()`. *) val non_informative : env -> typ -> bool + val try_lookup_effect_lid : env -> lident -> option term val lookup_effect_lid : env -> lident -> term val lookup_effect_abbrev : env -> universes -> lident -> option (binders & comp) diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst index 0432f64f2ef..6ce884b3cf2 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fst @@ -2808,6 +2808,8 @@ let non_info_norm env t = let steps = [UnfoldUntil delta_constant; AllowUnboundUniverses; EraseUniverses; + Primops; + Beta; Iota; HNF; (* We could use Weak too were it not that we need * to descend in the codomain of arrows. *) diff --git a/src/typechecker/FStarC.TypeChecker.Quals.fst b/src/typechecker/FStarC.TypeChecker.Quals.fst index 564e89cf344..5935db49972 100644 --- a/src/typechecker/FStarC.TypeChecker.Quals.fst +++ b/src/typechecker/FStarC.TypeChecker.Quals.fst @@ -161,6 +161,26 @@ let check_sigelt_quals_pre (env:FStarC.TypeChecker.Env.env) se = then err [] | _ -> () +// A faster under-approximation of non_info_norm. +// We call this function on every let-binding that has an interface val +// (while non_info_norm is only called on types), +// so it needs to be fast and shouldn't unfold too much. +// The regular non_info_norm doesn't set Weak, +// which makes the normalizer reduce lets. +let non_info_norm_weak env t = + let steps = [UnfoldUntil delta_constant; + AllowUnboundUniverses; + EraseUniverses; + Primops; + Beta; Iota; + HNF; + Weak; + Unascribe; //remove ascriptions + ForExtraction //and refinement types + ] + in + non_informative env (N.normalize steps env t) + let check_erasable env quals (r:Range.range) se = let lids = U.lids_of_sigelt se in let val_exists = @@ -183,6 +203,22 @@ let check_erasable env quals (r:Range.range) se = text "Mismatch of attributes between declaration and definition."; text "Definition is marked `erasable` but the declaration is not."; ]; + if not se_has_erasable_attr && not (Options.ide ()) then begin + match se.sigel with + | Sig_let {lbs=(false, [lb])} -> + let lbname = BU.right lb.lbname in + let has_iface_val = match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with + | Some iface_decls -> iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v)) + | None -> false in + let _, body, _ = U.abs_formals lb.lbdef in + if has_iface_val && non_info_norm_weak env body then log_issue lbname Error_MustEraseMissing [ + text (BU.format2 "Values of type `%s` will be erased during extraction, \ + but its interface hides this fact. Add the `erasable` \ + attribute to the `val %s` declaration for this symbol in the interface" + (show lbname) (show lbname)); + ] + | _ -> () + end; if se_has_erasable_attr then begin match se.sigel with @@ -221,47 +257,6 @@ let check_erasable env quals (r:Range.range) se = ] end -(* - * Given `val t : Type` in an interface - * and `let t = e` in the corresponding implementation - * The val declaration should contains the `must_erase_for_extraction` attribute - * if and only if `e` is a type that's non-informative (e..g., unit, t -> unit, etc.) - *) -let check_must_erase_attribute env se = - if Options.ide() then () else - match se.sigel with - | Sig_let {lbs; lids=l} -> - begin match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with - | None -> - () - - | Some iface_decls -> - snd lbs |> List.iter (fun lb -> - let lbname = BU.right lb.lbname in - let has_iface_val = - iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v)) - in - if has_iface_val - then - let must_erase = TcUtil.must_erase_for_extraction env lb.lbdef in - let has_attr = Env.fv_has_attr env lbname C.must_erase_for_extraction_attr in - if must_erase && not has_attr - then log_issue lbname Error_MustEraseMissing [ - text (BU.format2 "Values of type `%s` will be erased during extraction, \ - but its interface hides this fact. Add the `must_erase_for_extraction` \ - attribute to the `val %s` declaration for this symbol in the interface" - (show lbname) (show lbname)); - ] - else if has_attr && not must_erase - then log_issue lbname Error_MustEraseMissing [ - text (BU.format1 "Values of type `%s` cannot be erased during extraction, \ - but the `must_erase_for_extraction` attribute claims that it can. \ - Please remove the attribute." - (show lbname)); - ]) - end - | _ -> () - let check_typeclass_instance_attribute env (rng:Range.range) se = let is_tc_instance = se.sigattrs |> BU.for_some @@ -316,6 +311,5 @@ let check_sigelt_quals_post env se = let quals = se.sigquals in let r = se.sigrng in check_erasable env quals r se; - check_must_erase_attribute env se; check_typeclass_instance_attribute env r se; () diff --git a/src/typechecker/FStarC.TypeChecker.Quals.fsti b/src/typechecker/FStarC.TypeChecker.Quals.fsti index 9a23f2e8de1..851cc4d6832 100644 --- a/src/typechecker/FStarC.TypeChecker.Quals.fsti +++ b/src/typechecker/FStarC.TypeChecker.Quals.fsti @@ -29,7 +29,6 @@ after the function is typechecked. Currently, the only things that must be checked after the function is typechecked are: - The erasable attribute, since the defn must be elaborated. See #3253. -- The must_erase attribute - The instance attribute for typeclasses *) diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst index d2eca1faae6..e00a75598a4 100644 --- a/src/typechecker/FStarC.TypeChecker.Util.fst +++ b/src/typechecker/FStarC.TypeChecker.Util.fst @@ -3190,40 +3190,9 @@ let maybe_add_implicit_binders (env:env) (bs:binders) : binders = let must_erase_for_extraction (g:env) (t:typ) = - let rec descend env t = //t is expected to b in WHNF - match (SS.compress t).n with - | Tm_arrow _ -> - let bs, c = U.arrow_formals_comp t in - let env = FStarC.TypeChecker.Env.push_binders env bs in - (Env.is_erasable_effect env (U.comp_effect_name c)) //includes GHOST - || (U.is_pure_or_ghost_comp c && aux env (U.comp_result c)) - | Tm_refine {b={sort=t}} -> - aux env t - | Tm_app {hd=head} - | Tm_uinst (head, _) -> - descend env head - | Tm_fvar fv -> - //special treatment for must_erase_for_extraction here - //See Env.type_is_erasable for more explanations - Env.fv_has_attr env fv C.must_erase_for_extraction_attr - | _ -> false - and aux env t = - let t = N.normalize [Env.Primops; - Env.Weak; - Env.HNF; - Env.UnfoldUntil delta_constant; - Env.Beta; - Env.AllowUnboundUniverses; - Env.Zeta; - Env.Iota; - Env.Unascribe] env t in -// debug g (fun () -> BU.print1 "aux %s\n" (show t)); - let res = Env.non_informative env t || descend env t in - if !dbg_Extraction - then BU.print2 "must_erase=%s: %s\n" (if res then "true" else "false") (show t); - res - in - aux g t + let res = N.non_info_norm g t in + if !dbg_Extraction then BU.print2 "must_erase=%s: %s\n" (if res then "true" else "false") (show t); + res let effect_extraction_mode env l = l |> Env.norm_eff_name env diff --git a/tests/micro-benchmarks/MustEraseForExtraction.fst b/tests/micro-benchmarks/MustEraseForExtraction.fst index c7d7c873c3e..554cd54bcd7 100644 --- a/tests/micro-benchmarks/MustEraseForExtraction.fst +++ b/tests/micro-benchmarks/MustEraseForExtraction.fst @@ -17,7 +17,8 @@ module MustEraseForExtraction [@@(expect_failure [318])] let t1 = unit +[@@erasable] let t2 = unit -[@@(expect_failure [318])] +[@@(expect_failure [162])] let t3 = bool diff --git a/tests/micro-benchmarks/MustEraseForExtraction.fsti b/tests/micro-benchmarks/MustEraseForExtraction.fsti index bfd3f977621..e87b4614a03 100644 --- a/tests/micro-benchmarks/MustEraseForExtraction.fsti +++ b/tests/micro-benchmarks/MustEraseForExtraction.fsti @@ -17,8 +17,8 @@ module MustEraseForExtraction val t1 : Type0 -[@@must_erase_for_extraction] +[@@erasable] val t2 : Type0 -[@@must_erase_for_extraction] +[@@erasable] val t3 : Type0 diff --git a/ulib/FStar.GSet.fsti b/ulib/FStar.GSet.fsti index 408496dc2c8..e9ad4c2ea44 100644 --- a/ulib/FStar.GSet.fsti +++ b/ulib/FStar.GSet.fsti @@ -19,9 +19,9 @@ module FStar.GSet #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" (* - * AR: mark it must_erase_for_extraction temporarily until CMI comes in + * AR: mark it erasable temporarily until CMI comes in *) -[@@must_erase_for_extraction] +[@@erasable] val set (a: Type u#a) : Type u#a val equal (#a:Type) (s1:set a) (s2:set a) : Type0 diff --git a/ulib/FStar.GhostSet.fsti b/ulib/FStar.GhostSet.fsti index 239423a4e6c..dd52e6b1214 100644 --- a/ulib/FStar.GhostSet.fsti +++ b/ulib/FStar.GhostSet.fsti @@ -18,7 +18,7 @@ module FStar.GhostSet (** Ghost computational sets: membership is a ghost boolean function *) #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" -[@@must_erase_for_extraction; erasable] +[@@erasable] val set (a: Type u#a) : Type u#a let decide_eq a = x:a -> y:a -> GTot (b:bool { b <==> (x==y) }) diff --git a/ulib/FStar.Monotonic.HyperHeap.fsti b/ulib/FStar.Monotonic.HyperHeap.fsti index 927f269cbaa..0bc9f6ee09e 100644 --- a/ulib/FStar.Monotonic.HyperHeap.fsti +++ b/ulib/FStar.Monotonic.HyperHeap.fsti @@ -28,9 +28,9 @@ open FStar.Ghost *) (* - * AR: mark it must_erase_for_extraction temporarily until CMI comes in + * AR: mark it erasable temporarily until CMI comes in *) -[@@must_erase_for_extraction] +[@@erasable] val rid :eqtype val reveal (r:rid) :GTot (list (int & int)) diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index 6bb8b1076a3..9ef63d35c2d 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -867,19 +867,7 @@ val plugin (x: int) : Tot unit elaborate and typecheck, but unfold before verification. *) val tcnorm : unit -(** We erase all ghost functions and unit-returning pure functions to - [()] at extraction. This creates a small issue with abstract - types. Consider a module that defines an abstract type [t] whose - (internal) definition is [unit] and also defines [f: int -> t]. [f] - would be erased to be just [()] inside the module, while the - client calls to [f] would not, since [t] is abstract. To get - around this, when extracting interfaces, if we encounter an - abstract type, we tag it with this attribute, so that - extraction can treat it specially. - - Note, since the use of cross-module inlining (the [--cmi] option), - this attribute is no longer necessary. We retain it for legacy, - but will remove it in the future. *) +[@@deprecated "use [@@erasable] instead"] val must_erase_for_extraction : unit (** This attribute is used with the Dijkstra Monads for Free diff --git a/ulib/FStar.TSet.fst b/ulib/FStar.TSet.fst index e84f7246884..838a0eaa85d 100644 --- a/ulib/FStar.TSet.fst +++ b/ulib/FStar.TSet.fst @@ -22,7 +22,7 @@ module P = FStar.PropositionalExtensionality module F = FStar.FunctionalExtensionality (* - * AR: mark it must_erase_for_extraction temporarily until CMI comes in + * AR: mark it erasable temporarily until CMI comes in *) [@@erasable] let set a = F.restricted_t a (fun _ -> prop) diff --git a/ulib/FStar.TSet.fsti b/ulib/FStar.TSet.fsti index 47f99d567c9..8bde40c7c42 100644 --- a/ulib/FStar.TSet.fsti +++ b/ulib/FStar.TSet.fsti @@ -20,9 +20,9 @@ module FStar.TSet #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" (* - * AR: mark it must_erase_for_extraction temporarily until CMI comes in + * AR: mark it erasable temporarily until CMI comes in *) -[@@must_erase_for_extraction; erasable] +[@@erasable] val set (a:Type u#a) : Type u#(max 1 a) val equal (#a:Type) (s1:set a) (s2:set a) : prop