diff --git a/src/extraction/FStarC.Extraction.ML.Modul.fst b/src/extraction/FStarC.Extraction.ML.Modul.fst index 4c80aa0888c..0e2c0791b06 100644 --- a/src/extraction/FStarC.Extraction.ML.Modul.fst +++ b/src/extraction/FStarC.Extraction.ML.Modul.fst @@ -822,7 +822,7 @@ let rec extract_sigelt_iface (g:uenv) (se:sigelt) : uenv & iface = | Sig_declare_typ {lid; t} -> let quals = se.sigquals in if quals |> List.contains Assumption - && not (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t) + && None? (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t) then let g, bindings = Term.extract_lb_iface g (false, [always_fail lid t]) in g, iface_of_bindings bindings else g, empty_iface //it's not assumed, so wait for the corresponding Sig_let to generate code @@ -999,7 +999,7 @@ let extract_bundle env se = | _ -> failwith "Unexpected signature element" let lb_is_irrelevant (g:env_t) (lb:letbinding) : bool = - Env.non_informative (tcenv_of_uenv g) lb.lbtyp && // result type is non informative + Some? (Env.non_informative (tcenv_of_uenv g) lb.lbtyp) && // result type is non informative not (Term.is_arity g lb.lbtyp) && // but not a type definition U.is_pure_or_ghost_effect lb.lbeff // and not top-level effectful @@ -1129,7 +1129,7 @@ let rec extract_sig (g:env_t) (se:sigelt) : env_t & list mlmodule1 = | Sig_declare_typ {lid; t} -> let quals = se.sigquals in if quals |> List.contains Assumption - && not (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t) + && None? (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t) then let always_fail = { se with sigel = Sig_let {lbs=(false, [always_fail lid t]); lids=[]} } in let g, mlm = extract_sig g always_fail in //extend the scope with the new name diff --git a/src/extraction/FStarC.Extraction.ML.Term.fst b/src/extraction/FStarC.Extraction.ML.Term.fst index ad47cbfa828..7c41cd4d0db 100644 --- a/src/extraction/FStarC.Extraction.ML.Term.fst +++ b/src/extraction/FStarC.Extraction.ML.Term.fst @@ -689,6 +689,15 @@ let head_of_type_is_extract_as_impure_effect g t = | Tm_fvar fv -> has_extract_as_impure_effect g fv | _ -> false +let ty_of_must_erase (g: uenv) (t: term) = + let rec go t = + match t.n with + | Tm_abs {bs;body} -> {t with n=Tm_arrow {bs; comp=mk_Total (go body)}} + | Tm_constant Const_unit -> t_unit in + match TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t with + | Some r -> Some (go r) + | None -> None + exception NotSupportedByExtension let translate_typ_t = g:uenv -> t:term -> mlty @@ -762,6 +771,9 @@ let rec translate_term_to_mlty' (g:uenv) (t0:term) : mlty = | Tm_name bv -> bv_as_mlty env bv + | Tm_fvar fv when fv_eq_lid fv PC.unit_lid -> + MLTY_Erased + | Tm_fvar fv -> (* it is not clear whether description in the thesis covers type applications with 0 args. However, this case is needed to translate types like nnat, and so far seems to work as expected*) @@ -820,12 +832,14 @@ let rec translate_term_to_mlty' (g:uenv) (t0:term) : mlty = end | _ -> false in - if TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t0 - then MLTY_Erased - else let mlt = aux g t0 in - if is_top_ty mlt - then MLTY_Top - else mlt + let t0 = + match ty_of_must_erase g t0 with + | Some repl -> repl + | None -> t0 in + let mlt = aux g t0 in + if is_top_ty mlt + then MLTY_Top + else mlt and binders_as_ml_binders (g:uenv) (bs:binders) : list (mlident & mlty) & uenv = @@ -1239,7 +1253,7 @@ let rec extract_lb_sig (g:uenv) (lbs:letbindings) : list lb_sig = let expected_t = term_as_mlty g lbtyp in (lbname_, f_e, (lbtyp, ([], ([],expected_t))), false, has_c_inline, lbdef) in - if TcUtil.must_erase_for_extraction (tcenv_of_uenv g) lbtyp + if Some? (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) lbtyp) then (lbname_, f_e, (lbtyp, ([], ([], MLTY_Erased))), false, has_c_inline, lbdef) else // debug g (fun () -> printfn "Let %s at type %s; expected effect is %A\n" (show lbname) (Print.typ_to_string t) f_e); match lbtyp.n with @@ -1517,13 +1531,18 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = | Tm_uinst(t, _) -> term_as_mlexpr g t + | Tm_constant Const_unit -> + ml_unit, E_PURE, MLTY_Erased + | Tm_constant c -> let tcenv = tcenv_of_uenv g in let _, ty, _ = TcTerm.typeof_tot_or_gtot_term tcenv t true in //AR: TODO: type_of_well_typed? - if TcUtil.must_erase_for_extraction tcenv ty - then ml_unit, E_PURE, MLTY_Erased - else let ml_ty = term_as_mlty g ty in - with_ty ml_ty (mlexpr_of_const t.pos c), E_PURE, ml_ty + (match TcUtil.must_erase_for_extraction tcenv ty with + | Some repl -> + term_as_mlexpr g repl + | None -> + let ml_ty = term_as_mlty g ty in + with_ty ml_ty (mlexpr_of_const t.pos c), E_PURE, ml_ty) | Tm_name _ -> //lookup in g; decide if its in left or right; tag is Pure because it's just a variable if is_type g t //Here, we really need to be certain that g is a type; unclear if level ensures it diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index ead8d527dac..0997fc6acfb 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -670,7 +670,7 @@ let rec iter2 (xs ys:list 'a) (f: 'a -> 'a -> 'b -> result 'b) (b:'b) iter2 xs ys f b | _ -> fail "Lists of differing length" -let is_non_informative g t = N.non_info_norm g t +let is_non_informative g t = Some? (N.non_info_norm g t) let non_informative g t : bool diff --git a/src/typechecker/FStarC.TypeChecker.Env.fst b/src/typechecker/FStarC.TypeChecker.Env.fst index 7a6a62084e9..0530c21941e 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 @@ -1027,18 +1022,46 @@ let is_erasable_effect env l = let rec non_informative env t = match (U.unrefine t).n with - | Tm_type _ -> true - | Tm_fvar fv -> - fv_eq_lid fv Const.unit_lid - || fv_eq_lid fv Const.squash_lid - || fv_eq_lid fv Const.erased_lid - || fv_has_erasable_attr env fv + | Tm_type _ -> Some unit_const + | Tm_fvar fv when + fv_eq_lid fv Const.unit_lid + || fv_eq_lid fv Const.squash_lid + || fv_eq_lid fv Const.erased_lid -> + Some unit_const + | Tm_fvar fv when fv_has_erasable_attr env fv -> + // Note: this is unsound (see #3366), but only happens when we compile without `--cmi`. + Some unit_const | Tm_app {hd=head} -> non_informative env head | 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) - | _ -> false + | Tm_arrow {bs;comp=c} -> + if is_ghost_effect (comp_effect_name c) || is_erasable_effect env (comp_effect_name c) then + // Functions with a ghost effect can only be invoked in a ghost context, + // therefore it is safe to erase them to unit, a non-function. + if List.length bs <= 1 then + Some unit_const + else + // However, this is only true for the full application; + // `a -> b -> GTot c` is equivalent to `a -> Tot (b -> GTot c)` + // and needs to be erased to `fun x -> ()`. + Some (mk (Tm_abs { body = unit_const; rc_opt = None; bs = List.init bs }) t.pos) + else if is_pure_comp c then + // Only the result of a pure computation can be erased; + // a pure function can be still be invoked in non-ghost contexts (see #3366) + match non_informative env (comp_result c) with + | Some body -> Some (mk (Tm_abs { body; rc_opt = None; bs }) t.pos) + | None -> None + else + // Effectful computations may not be erased + None + | Tm_meta {tm} -> non_informative env tm + | _ -> None + +let rec non_informative_sort t = + match (U.unrefine t).n with + | Tm_fvar fv when fv_eq_lid fv Const.prop_lid -> true + | Tm_arrow {comp=c} -> non_informative_sort (comp_result c) + | Tm_meta {tm} -> non_informative_sort tm + | _ -> false let num_effect_indices env name r = let sig_t = name |> lookup_effect_lid env |> SS.compress in diff --git a/src/typechecker/FStarC.TypeChecker.Env.fsti b/src/typechecker/FStarC.TypeChecker.Env.fsti index 4b949d1c8b1..80d188c02d6 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fsti +++ b/src/typechecker/FStarC.TypeChecker.Env.fsti @@ -342,7 +342,16 @@ 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 -val non_informative : env -> typ -> bool + +(* `non_informative env t` is `Some i` if the type `t: Type` is noninformative, + and any `x: t ...` can be erased to `i`. *) +val non_informative : env -> typ -> option term + +(* `non_informative_sort t` is `true` if the type family `t: ... -> Type` only ranges over noninformative types, + i.e., any `x: s ...` such that `s ... : t ...` can be erased. + (practically, this means that `t` is of the form `... -> prop`) *) +val non_informative_sort : 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 a6e4d211347..31c858da772 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fst @@ -1434,38 +1434,42 @@ let rec norm : cfg -> env -> stack -> term -> term = log cfg (fun () -> BU.print1 ">> metadata = %s\n" (show m)); begin match m with | Meta_monadic (m_from, ty) -> + let nonerasable_case () = + reduce_impure_comp cfg env stack head (Inl m_from) ty in if cfg.steps.for_extraction then ( //In Extraction, we want to erase sub-terms with erasable effect - //Or pure terms with non-informative return types - if Env.is_erasable_effect cfg.tcenv m_from - || (U.is_pure_effect m_from && Env.non_informative cfg.tcenv ty) - then ( + if Env.is_erasable_effect cfg.tcenv m_from then rebuild cfg env stack (S.mk (Tm_meta {tm=U.exp_unit; meta=m}) t.pos) - ) - else ( - reduce_impure_comp cfg env stack head (Inl m_from) ty - ) + //Or pure terms with non-informative return types + else if not (U.is_pure_effect m_from) then + nonerasable_case () + else match Env.non_informative cfg.tcenv ty with + | None -> nonerasable_case () + | Some tm -> + rebuild cfg env stack (S.mk (Tm_meta {tm; meta=m}) t.pos) ) - else - reduce_impure_comp cfg env stack head (Inl m_from) ty + else + nonerasable_case () | Meta_monadic_lift (m_from, m_to, ty) -> + let nonerasable_case () = + reduce_impure_comp cfg env stack head (Inr (m_from, m_to)) ty in if cfg.steps.for_extraction then ( //In Extraction, we want to erase sub-terms with erasable effect - //Or pure terms with non-informative return types - if Env.is_erasable_effect cfg.tcenv m_from - || Env.is_erasable_effect cfg.tcenv m_to - || (U.is_pure_effect m_from && Env.non_informative cfg.tcenv ty) - then ( + if Env.is_erasable_effect cfg.tcenv m_from || Env.is_erasable_effect cfg.tcenv m_to then rebuild cfg env stack (S.mk (Tm_meta {tm=U.exp_unit; meta=m}) t.pos) - ) - else ( - reduce_impure_comp cfg env stack head (Inr (m_from, m_to)) ty - ) + //Or pure terms with non-informative return types + else if not (U.is_pure_effect m_from) then + nonerasable_case () + else match Env.non_informative cfg.tcenv ty with + | None -> nonerasable_case () + | Some tm -> + rebuild cfg env stack (S.mk (Tm_meta {tm; meta=m}) t.pos) ) - else reduce_impure_comp cfg env stack head (Inr (m_from, m_to)) ty + else + nonerasable_case () | _ -> if cfg.steps.unmeta @@ -2816,6 +2820,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. *) @@ -2825,6 +2831,21 @@ let non_info_norm env t = in non_informative env (normalize steps env t) +let non_info_sort_norm env t = + let steps = [UnfoldUntil (Env.delta_depth_of_fv env (S.fvconst PC.prop_lid)); // do not unfold prop + AllowUnboundUniverses; + EraseUniverses; + Primops; + Beta; Iota; + HNF; + (* We could use Weak too were it not that we need + * to descend in the codomain of arrows. *) + Unascribe; //remove ascriptions + ForExtraction //and refinement types + ] + in + non_informative_sort (normalize steps env t) + (* * Ghost T to Pure T promotion * @@ -2838,7 +2859,7 @@ let non_info_norm env t = *) let maybe_promote_t env non_informative_only t = - not non_informative_only || non_info_norm env t + not non_informative_only || Some? (non_info_norm env t) let ghost_to_pure_aux env non_informative_only c = match c.n with diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fsti b/src/typechecker/FStarC.TypeChecker.Normalize.fsti index 537da275347..57b3f7ef883 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fsti +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fsti @@ -34,7 +34,8 @@ val whnf_steps: list step val unfold_whnf': steps -> Env.env -> term -> term val unfold_whnf: Env.env -> term -> term val reduce_uvar_solutions:Env.env -> term -> term -val non_info_norm: Env.env -> term -> bool +val non_info_norm: Env.env -> term -> option term +val non_info_sort_norm: Env.env -> term -> bool (* * The maybe versions of ghost_to_pure only promote diff --git a/src/typechecker/FStarC.TypeChecker.Quals.fst b/src/typechecker/FStarC.TypeChecker.Quals.fst index 016ca9e0360..fbfe7ed60d9 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,29 @@ 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 val_decl = Env.try_lookup_val_decl env lbname.fv_name.v in + if has_iface_val && Some? val_decl then + let _, body, _ = U.abs_formals lb.lbdef in + let Some ((us, t), _) = val_decl in + let known_to_be_erasable = + let env = Env.push_univ_vars env us in + N.non_info_sort_norm env t in + if not known_to_be_erasable && Some? (non_info_norm_weak env body) then + log_issue lbname Error_MustEraseMissing [ + text (BU.format1 "Values of type `%s` will be erased during extraction, \ + but its interface hides this fact." (show lbname)); + text (BU.format1 "Add the `erasable` \ + attribute to the `val %s` declaration for this symbol in the interface" (show lbname)); + ] + | _ -> () + end; if se_has_erasable_attr then begin match se.sigel with @@ -199,7 +242,7 @@ let check_erasable env quals (r:Range.range) se = | Sig_let {lbs=(false, [lb])} -> let _, body, _ = U.abs_formals lb.lbdef in - if not (N.non_info_norm env body) + if None? (N.non_info_norm env body) then raise_error body Errors.Fatal_QulifierListNotPermitted [ text "Illegal attribute: \ the `erasable` attribute is only permitted on inductive type definitions \ @@ -221,47 +264,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.format1 "Values of type `%s` will be erased during extraction, \ - but its interface hides this fact." (show lbname)); - text (BU.format1 "Add the `must_erase_for_extraction` \ - attribute to the `val %s` declaration for this symbol in the interface" (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." - (show lbname)); - text "Please remove the attribute."; - ]) - end - | _ -> () - let check_typeclass_instance_attribute env (rng:Range.range) se = let is_tc_instance = se.sigattrs |> BU.for_some @@ -316,6 +318,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 28871759265..f349709fbb8 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.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index b51bb586032..9bed5a088a9 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -4550,7 +4550,7 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = if is_polymonadic && Env.is_erasable_effect env c1.effect_name && not (Env.is_erasable_effect env c2.effect_name) && - not (N.non_info_norm env c1.result_typ) + None? (N.non_info_norm env c1.result_typ) then Errors.raise_error r Errors.Error_TypeError (BU.format3 "Cannot lift erasable expression from %s ~> %s since its type %s is informative" (string_of_lid c1.effect_name) @@ -4729,7 +4729,7 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = else N.ghost_to_pure2 env (c1, c2) in match c1.n, c2.n with - | GTotal t1, Total t2 when (Env.non_informative env t2) -> + | GTotal t1, Total t2 when Some? (Env.non_informative env t2) -> solve_t (problem_using_guard orig t1 problem.relation t2 None "result type") wl | GTotal _, Total _ -> diff --git a/src/typechecker/FStarC.TypeChecker.TcEffect.fst b/src/typechecker/FStarC.TypeChecker.TcEffect.fst index c5e454e69d0..af8a83d62fb 100644 --- a/src/typechecker/FStarC.TypeChecker.TcEffect.fst +++ b/src/typechecker/FStarC.TypeChecker.TcEffect.fst @@ -1928,7 +1928,7 @@ Errors.with_ctx (BU.format1 "While checking layered effect definition `%s`" (str let env = Env.push_univ_vars env0 us in let env = Env.push_binders env [a_b] in let _, r = List.fold_left (fun (env, r) b -> - let r = r && N.non_info_norm env b.binder_bv.sort in + let r = r && Some? (N.non_info_norm env b.binder_bv.sort) in Env.push_binders env [b], r) (env, true) rest_bs in if r && Substitutive_combinator? bind_kind && diff --git a/src/typechecker/FStarC.TypeChecker.TcTerm.fst b/src/typechecker/FStarC.TypeChecker.TcTerm.fst index 9c071ca7689..2b9c70e40ac 100644 --- a/src/typechecker/FStarC.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStarC.TypeChecker.TcTerm.fst @@ -178,7 +178,7 @@ let check_erasable_binder_attributes env attrs (binder_ty:typ) = List.iter (fun attr -> if U.is_fvar Const.erasable_attr attr - && not (N.non_info_norm env binder_ty) + && None? (N.non_info_norm env binder_ty) then raise_error attr Errors.Fatal_QulifierListNotPermitted ("Incompatible attributes: an erasable attribute on a binder must bind a name at an non-informative type")) @@ -2683,7 +2683,7 @@ and check_application_args env head (chead:comp) ghead args expected_topt : term //this argument is effectful, warn if the function would be erased //special casing for ignore, may be use an attribute instead? let warn_effectful_args = - (TcUtil.must_erase_for_extraction env chead.res_typ) && + Some? (TcUtil.must_erase_for_extraction env chead.res_typ) && (not (match (U.un_uinst head).n with | Tm_fvar fv -> S.fv_eq_lid fv (Parser.Const.psconst "ignore") | _ -> true)) @@ -3077,7 +3077,7 @@ and tc_pat env (pat_t:typ) (p0:pat) : //Data constructors are marked with the "erasable" attribute //if their types are; matching on this constructor incurs //a ghost effect - let erasable = Env.non_informative env t in + let erasable = Some? (Env.non_informative env t) in if List.length formals <> List.length args then fail "Pattern is not a fully-applied data constructor"; let rec aux (subst, args_out, bvs, guard) formals args = @@ -4736,7 +4736,7 @@ let tc_tparams env0 (tps:binders) : (binders & Env.env & universes) = let rec __typeof_tot_or_gtot_term_fastpath (env:env) (t:term) (must_tot:bool) : option typ = let mk_tm_type u = S.mk (Tm_type u) t.pos in - let effect_ok k = (not must_tot) || (N.non_info_norm env k) in + let effect_ok k = (not must_tot) || Some? (N.non_info_norm env k) in let t = SS.compress t in match t.n with | Tm_delayed _ @@ -4826,7 +4826,7 @@ let rec __typeof_tot_or_gtot_term_fastpath (env:env) (t:term) (must_tot:bool) : let k = U.comp_result c in if (not must_tot) || (c |> U.comp_effect_name |> Env.norm_eff_name env |> lid_equals Const.effect_PURE_lid) || - (N.non_info_norm env k) + Some? (N.non_info_norm env k) then Some k else None diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst index 05e7e464a56..55f90c1591b 100644 --- a/src/typechecker/FStarC.TypeChecker.Util.fst +++ b/src/typechecker/FStarC.TypeChecker.Util.fst @@ -1188,10 +1188,10 @@ let mk_indexed_bind env if (Env.is_erasable_effect env m && not (Env.is_erasable_effect env p) && - not (N.non_info_norm env ct1.result_typ)) || + None? (N.non_info_norm env ct1.result_typ)) || (Env.is_erasable_effect env n && not (Env.is_erasable_effect env p) && - not (N.non_info_norm env ct2.result_typ)) + None? (N.non_info_norm env ct2.result_typ)) then raise_error r1 Errors.Fatal_UnexpectedEffect [ text "Cannot apply bind" ^/^ doc_of_string (bind_name ()) ^/^ text "since" ^/^ pp p ^/^ text "is not erasable and one of the computations is informative." @@ -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" (show res) (show t); + res let effect_extraction_mode env l = l |> Env.norm_eff_name env @@ -3298,7 +3267,7 @@ let check_non_informative_type_for_lift env m1 m2 t (r:Range.range) : unit = //raise an error if m1 is erasable, m2 is not erasable, and t is informative if Env.is_erasable_effect env m1 && not (Env.is_erasable_effect env m2) && - not (N.non_info_norm env t) + None? (N.non_info_norm env t) then Errors.raise_error r Errors.Error_TypeError (BU.format3 "Cannot lift erasable expression from %s ~> %s since its type %s is informative" (string_of_lid m1) diff --git a/src/typechecker/FStarC.TypeChecker.Util.fsti b/src/typechecker/FStarC.TypeChecker.Util.fsti index c191240052a..09776a66ef2 100644 --- a/src/typechecker/FStarC.TypeChecker.Util.fsti +++ b/src/typechecker/FStarC.TypeChecker.Util.fsti @@ -147,7 +147,7 @@ val remove_reify: term -> term val maybe_lift: env -> term -> lident -> lident -> typ -> term val maybe_monadic: env -> term -> lident -> typ -> term -val must_erase_for_extraction: env -> term -> bool +val must_erase_for_extraction: env -> term -> option term //layered effect utilities diff --git a/tests/extraction/Bug3366.fst b/tests/extraction/Bug3366.fst new file mode 100644 index 00000000000..72d2ab97e42 --- /dev/null +++ b/tests/extraction/Bug3366.fst @@ -0,0 +1,13 @@ +module Bug3366 + +let t = Type0 -> Type0 + +let x = list + +let generic_apply #a #b (f: (a -> b) * nat) (x: a) : b * nat = + (f._1 x, f._2) + +let f (x: t * nat) = + (generic_apply x nat)._2 + +let _ = f (x, 42) // <- crash diff --git a/tests/extraction/Makefile b/tests/extraction/Makefile index 6d58a8cc036..6c4b16ef698 100644 --- a/tests/extraction/Makefile +++ b/tests/extraction/Makefile @@ -13,6 +13,7 @@ endif RUN += ExtractAs.fst RUN += InlineLet.fst +RUN += Bug3366.fst include $(FSTAR_ROOT)/mk/test.mk 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..d6b5c10f943 100644 --- a/ulib/FStar.GSet.fsti +++ b/ulib/FStar.GSet.fsti @@ -18,10 +18,7 @@ module FStar.GSet (** Computational sets (on Types): membership is a boolean function *) #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 - *) -[@@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..f470ef331ba 100644 --- a/ulib/FStar.Monotonic.HyperHeap.fsti +++ b/ulib/FStar.Monotonic.HyperHeap.fsti @@ -27,10 +27,7 @@ open FStar.Ghost * Clients should not open/know about HyperHeap, they should work only with HyperStack *) -(* - * AR: mark it must_erase_for_extraction 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 d9f46f6f97f..68a558c0ae2 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -874,19 +874,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..acb5c044169 100644 --- a/ulib/FStar.TSet.fst +++ b/ulib/FStar.TSet.fst @@ -21,9 +21,6 @@ module FStar.TSet module P = FStar.PropositionalExtensionality module F = FStar.FunctionalExtensionality -(* - * AR: mark it must_erase_for_extraction 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..7771132c2f5 100644 --- a/ulib/FStar.TSet.fsti +++ b/ulib/FStar.TSet.fsti @@ -19,10 +19,7 @@ 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 - *) -[@@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 diff --git a/ulib/legacy/FStar.Buffer.fst b/ulib/legacy/FStar.Buffer.fst index 1bf7092d5db..44a0fedaf54 100644 --- a/ulib/legacy/FStar.Buffer.fst +++ b/ulib/legacy/FStar.Buffer.fst @@ -1152,7 +1152,6 @@ let lemma_modifies_one_trans_1 (#a:Type) (b:buffer a) (h0:mem) (h1:mem) (h2:mem) [SMTPat (modifies_one (frameOf b) h0 h1); SMTPat (modifies_one (frameOf b) h1 h2)] = () - (** Corresponds to memcpy *) val blit: #t:Type -> a:buffer t @@ -1171,7 +1170,6 @@ val blit: #t:Type Seq.slice (as_seq h0 b) (v idx_b+v len) (length b) )) #push-options "--z3rlimit 150 --max_fuel 0 --max_ifuel 0 --initial_fuel 0 --initial_ifuel 0" -#restart-solver let rec blit #t a idx_a b idx_b len = let h0 = HST.get () in if len =^ 0ul then ()