From 6d7c92b1dfc17db8d8d4bd1701378cfd05419aa8 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 9 Oct 2024 11:12:09 -0700 Subject: [PATCH] Erase functions to functions instead of unit. This only works if extraction can see through the type definitions, in general this requires `--cmi`. Fixes #3366 --- src/extraction/FStarC.Extraction.ML.Modul.fst | 6 +-- src/extraction/FStarC.Extraction.ML.Term.fst | 41 +++++++++++----- src/typechecker/FStarC.TypeChecker.Core.fst | 2 +- src/typechecker/FStarC.TypeChecker.Env.fst | 38 ++++++++++----- src/typechecker/FStarC.TypeChecker.Env.fsti | 6 +-- .../FStarC.TypeChecker.Normalize.fst | 46 ++++++++++-------- .../FStarC.TypeChecker.Normalize.fsti | 2 +- src/typechecker/FStarC.TypeChecker.Quals.fst | 4 +- src/typechecker/FStarC.TypeChecker.Rel.fst | 4 +- .../FStarC.TypeChecker.TcEffect.fst | 2 +- src/typechecker/FStarC.TypeChecker.TcTerm.fst | 10 ++-- src/typechecker/FStarC.TypeChecker.Util.fst | 8 ++-- src/typechecker/FStarC.TypeChecker.Util.fsti | 2 +- tests/error-messages/Monoid.fst.expected | 48 +++++++++---------- tests/error-messages/Monoid.fst.json_expected | 48 +++++++++---------- tests/extraction/Bug3366.fst | 13 +++++ tests/extraction/Makefile | 2 +- ulib/legacy/FStar.Buffer.fst | 4 +- 18 files changed, 169 insertions(+), 117 deletions(-) create mode 100644 tests/extraction/Bug3366.fst diff --git a/src/extraction/FStarC.Extraction.ML.Modul.fst b/src/extraction/FStarC.Extraction.ML.Modul.fst index 4c58c3625e9..96205919519 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 2a5ae75a2ea..e301f3fd773 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 + let rec translate_term_to_mlty (g:uenv) (t0:term) : mlty = let arg_as_mlty (g:uenv) (a, _) : mlty = if is_type g a //This is just an optimization; we could in principle always emit MLTY_Erased, at the expense of more magics @@ -743,6 +752,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*) @@ -801,12 +813,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 = @@ -1207,7 +1221,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 @@ -1485,13 +1499,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 f1f355e0808..cd4c07e331a 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 87f7a1a9687..578bc18f6a9 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fst +++ b/src/typechecker/FStarC.TypeChecker.Env.fst @@ -1022,20 +1022,36 @@ 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_abs {body} -> non_informative env body + // | 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_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 a non-function. + Some unit_const + 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 + // (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 + | _ -> None 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 bd550ef07a8..18977ca95e8 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fsti +++ b/src/typechecker/FStarC.TypeChecker.Env.fsti @@ -342,9 +342,9 @@ 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 +(* `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 val try_lookup_effect_lid : env -> lident -> option term val lookup_effect_lid : env -> lident -> term diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst index 6ce884b3cf2..4dc07aa188a 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fst @@ -1426,38 +1426,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 @@ -2832,7 +2836,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 8a66b5062ae..163e0770339 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fsti +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fsti @@ -34,7 +34,7 @@ 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 (* * 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 5935db49972..7fb7b02a8de 100644 --- a/src/typechecker/FStarC.TypeChecker.Quals.fst +++ b/src/typechecker/FStarC.TypeChecker.Quals.fst @@ -211,7 +211,7 @@ let check_erasable env quals (r:Range.range) se = | 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 [ + if has_iface_val && Some? (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" @@ -235,7 +235,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 \ diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index 3487afbafd2..da908dec9cc 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 152c5110ef0..5912afaad36 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 19a73ddfd62..eeb267b7b94 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 = @@ -4732,7 +4732,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 _ @@ -4822,7 +4822,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 e00a75598a4..98c71af7671 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." @@ -3191,7 +3191,7 @@ let maybe_add_implicit_binders (env:env) (bs:binders) : binders = let must_erase_for_extraction (g:env) (t:typ) = 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); + if !dbg_Extraction then BU.print2 "must_erase=%s: %s\n" (show res) (show t); res let effect_extraction_mode env l = @@ -3267,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 af2e8733647..5c77f2e9b3b 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/error-messages/Monoid.fst.expected b/tests/error-messages/Monoid.fst.expected index e276faba323..1997ea79d94 100644 --- a/tests/error-messages/Monoid.fst.expected +++ b/tests/error-messages/Monoid.fst.expected @@ -345,8 +345,8 @@ let left_action_morphism f mf la lb = forall (g: ma) (x: a). lb.act (mf g) (f x) Module after type checking: module Monoid Declarations: [ -let right_unitality_lemma m u466 mult = forall (x: m). mult x u466 == x -let left_unitality_lemma m u466 mult = forall (x: m). mult u466 x == x +let right_unitality_lemma m u476 mult = forall (x: m). mult x u476 == x +let left_unitality_lemma m u476 mult = forall (x: m). mult u476 x == x let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z) unopteq type monoid (m: Type) = @@ -382,25 +382,25 @@ val monoid__uu___haseq: Prims.l_True /\ -let intro_monoid m u466 mult = Monoid.Monoid u466 mult () () () <: Prims.Pure (Monoid.monoid m) +let intro_monoid m u476 mult = Monoid.Monoid u476 mult () () () <: Prims.Pure (Monoid.monoid m) let nat_plus_monoid = let add x y = x + y <: Prims.nat in Monoid.intro_monoid Prims.nat 0 add let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition let conjunction_monoid = - let u464 = FStar.Pervasives.singleton Prims.l_True in + let u474 = FStar.Pervasives.singleton Prims.l_True in let mult p q = p /\ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u464 p <==> p); - FStar.PropositionalExtensionality.apply (mult u464 p) p) + (assert (mult u474 p <==> p); + FStar.PropositionalExtensionality.apply (mult u474 p) p) <: - FStar.Pervasives.Lemma (ensures mult u464 p == p) + FStar.Pervasives.Lemma (ensures mult u474 p == p) in let right_unitality_helper p = - (assert (mult p u464 <==> p); - FStar.PropositionalExtensionality.apply (mult p u464) p) + (assert (mult p u474 <==> p); + FStar.PropositionalExtensionality.apply (mult p u474) p) <: - FStar.Pervasives.Lemma (ensures mult p u464 == p) + FStar.Pervasives.Lemma (ensures mult p u474 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -409,26 +409,26 @@ let conjunction_monoid = FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u464 mult); + assert (Monoid.right_unitality_lemma Prims.prop u474 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u464 mult); + assert (Monoid.left_unitality_lemma Prims.prop u474 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u464 mult + Monoid.intro_monoid Prims.prop u474 mult let disjunction_monoid = - let u464 = FStar.Pervasives.singleton Prims.l_False in + let u474 = FStar.Pervasives.singleton Prims.l_False in let mult p q = p \/ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u464 p <==> p); - FStar.PropositionalExtensionality.apply (mult u464 p) p) + (assert (mult u474 p <==> p); + FStar.PropositionalExtensionality.apply (mult u474 p) p) <: - FStar.Pervasives.Lemma (ensures mult u464 p == p) + FStar.Pervasives.Lemma (ensures mult u474 p == p) in let right_unitality_helper p = - (assert (mult p u464 <==> p); - FStar.PropositionalExtensionality.apply (mult p u464) p) + (assert (mult p u474 <==> p); + FStar.PropositionalExtensionality.apply (mult p u474) p) <: - FStar.Pervasives.Lemma (ensures mult p u464 == p) + FStar.Pervasives.Lemma (ensures mult p u474 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -437,12 +437,12 @@ let disjunction_monoid = FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u464 mult); + assert (Monoid.right_unitality_lemma Prims.prop u474 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u464 mult); + assert (Monoid.left_unitality_lemma Prims.prop u474 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u464 mult + Monoid.intro_monoid Prims.prop u474 mult let bool_and_monoid = let and_ b1 b2 = b1 && b2 in Monoid.intro_monoid Prims.bool true and_ @@ -520,7 +520,7 @@ let _ = Monoid.intro_monoid_morphism Monoid.neg Monoid.disjunction_monoid Monoid.conjunction_monoid let mult_act_lemma m a mult act = forall (x: m) (x': m) (y: a). act (mult x x') y == act x (act x' y) -let unit_act_lemma m a u468 act = forall (y: a). act u468 y == y +let unit_act_lemma m a u478 act = forall (y: a). act u478 y == y unopteq type left_action (mm: Monoid.monoid m) (a: Type) = | LAct : diff --git a/tests/error-messages/Monoid.fst.json_expected b/tests/error-messages/Monoid.fst.json_expected index e276faba323..1997ea79d94 100644 --- a/tests/error-messages/Monoid.fst.json_expected +++ b/tests/error-messages/Monoid.fst.json_expected @@ -345,8 +345,8 @@ let left_action_morphism f mf la lb = forall (g: ma) (x: a). lb.act (mf g) (f x) Module after type checking: module Monoid Declarations: [ -let right_unitality_lemma m u466 mult = forall (x: m). mult x u466 == x -let left_unitality_lemma m u466 mult = forall (x: m). mult u466 x == x +let right_unitality_lemma m u476 mult = forall (x: m). mult x u476 == x +let left_unitality_lemma m u476 mult = forall (x: m). mult u476 x == x let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z) unopteq type monoid (m: Type) = @@ -382,25 +382,25 @@ val monoid__uu___haseq: Prims.l_True /\ -let intro_monoid m u466 mult = Monoid.Monoid u466 mult () () () <: Prims.Pure (Monoid.monoid m) +let intro_monoid m u476 mult = Monoid.Monoid u476 mult () () () <: Prims.Pure (Monoid.monoid m) let nat_plus_monoid = let add x y = x + y <: Prims.nat in Monoid.intro_monoid Prims.nat 0 add let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition let conjunction_monoid = - let u464 = FStar.Pervasives.singleton Prims.l_True in + let u474 = FStar.Pervasives.singleton Prims.l_True in let mult p q = p /\ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u464 p <==> p); - FStar.PropositionalExtensionality.apply (mult u464 p) p) + (assert (mult u474 p <==> p); + FStar.PropositionalExtensionality.apply (mult u474 p) p) <: - FStar.Pervasives.Lemma (ensures mult u464 p == p) + FStar.Pervasives.Lemma (ensures mult u474 p == p) in let right_unitality_helper p = - (assert (mult p u464 <==> p); - FStar.PropositionalExtensionality.apply (mult p u464) p) + (assert (mult p u474 <==> p); + FStar.PropositionalExtensionality.apply (mult p u474) p) <: - FStar.Pervasives.Lemma (ensures mult p u464 == p) + FStar.Pervasives.Lemma (ensures mult p u474 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -409,26 +409,26 @@ let conjunction_monoid = FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u464 mult); + assert (Monoid.right_unitality_lemma Prims.prop u474 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u464 mult); + assert (Monoid.left_unitality_lemma Prims.prop u474 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u464 mult + Monoid.intro_monoid Prims.prop u474 mult let disjunction_monoid = - let u464 = FStar.Pervasives.singleton Prims.l_False in + let u474 = FStar.Pervasives.singleton Prims.l_False in let mult p q = p \/ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u464 p <==> p); - FStar.PropositionalExtensionality.apply (mult u464 p) p) + (assert (mult u474 p <==> p); + FStar.PropositionalExtensionality.apply (mult u474 p) p) <: - FStar.Pervasives.Lemma (ensures mult u464 p == p) + FStar.Pervasives.Lemma (ensures mult u474 p == p) in let right_unitality_helper p = - (assert (mult p u464 <==> p); - FStar.PropositionalExtensionality.apply (mult p u464) p) + (assert (mult p u474 <==> p); + FStar.PropositionalExtensionality.apply (mult p u474) p) <: - FStar.Pervasives.Lemma (ensures mult p u464 == p) + FStar.Pervasives.Lemma (ensures mult p u474 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -437,12 +437,12 @@ let disjunction_monoid = FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u464 mult); + assert (Monoid.right_unitality_lemma Prims.prop u474 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u464 mult); + assert (Monoid.left_unitality_lemma Prims.prop u474 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u464 mult + Monoid.intro_monoid Prims.prop u474 mult let bool_and_monoid = let and_ b1 b2 = b1 && b2 in Monoid.intro_monoid Prims.bool true and_ @@ -520,7 +520,7 @@ let _ = Monoid.intro_monoid_morphism Monoid.neg Monoid.disjunction_monoid Monoid.conjunction_monoid let mult_act_lemma m a mult act = forall (x: m) (x': m) (y: a). act (mult x x') y == act x (act x' y) -let unit_act_lemma m a u468 act = forall (y: a). act u468 y == y +let unit_act_lemma m a u478 act = forall (y: a). act u478 y == y unopteq type left_action (mm: Monoid.monoid m) (a: Type) = | LAct : 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 705eff93f83..660e89785e8 100644 --- a/tests/extraction/Makefile +++ b/tests/extraction/Makefile @@ -2,7 +2,7 @@ FSTAR_ROOT ?= ../.. NODEPEND=1 include $(FSTAR_ROOT)/mk/test.mk -all: inline_let all_cmi Eta_expand.test Div.test ExtractAs.test +all: inline_let all_cmi Eta_expand.test Div.test ExtractAs.test Bug3366.test %.exe: %.fst $(FSTAR) --codegen OCaml $< diff --git a/ulib/legacy/FStar.Buffer.fst b/ulib/legacy/FStar.Buffer.fst index 1911536b625..0ea2e284380 100644 --- a/ulib/legacy/FStar.Buffer.fst +++ b/ulib/legacy/FStar.Buffer.fst @@ -1152,8 +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)] = () -#reset-options "--z3rlimit 100 --max_fuel 0 --max_ifuel 0 --initial_fuel 0 --initial_ifuel 0" - (** Corresponds to memcpy *) val blit: #t:Type -> a:buffer t @@ -1170,7 +1168,9 @@ val blit: #t:Type Seq.slice (as_seq h0 b) 0 (v idx_b) /\ Seq.slice (as_seq h1 b) (v idx_b+v len) (length b) == Seq.slice (as_seq h0 b) (v idx_b+v len) (length b) )) + #restart-solver +#reset-options "--z3rlimit 200 --split_queries always" let rec blit #t a idx_a b idx_b len = let h0 = HST.get () in if len =^ 0ul then ()