diff --git a/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml b/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml index 133c0713185..e2efd9060f6 100644 --- a/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml +++ b/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml @@ -60,10 +60,10 @@ let (embed_nat_int : Prims.nat -> Prims.int) = fun n -> n let (uu___0 : (Prims.nat, Prims.int, unit, unit, unit) monoid_morphism) = intro_monoid_morphism embed_nat_int nat_plus_monoid int_plus_monoid type 'p neg = unit -let (uu___1 : (unit, unit, unit neg, unit, unit) monoid_morphism) = +let (uu___1 : (unit, unit, unit, unit, unit) monoid_morphism) = intro_monoid_morphism (fun uu___ -> ()) conjunction_monoid disjunction_monoid -let (uu___2 : (unit, unit, unit neg, unit, unit) monoid_morphism) = +let (uu___2 : (unit, unit, unit, unit, unit) monoid_morphism) = intro_monoid_morphism (fun uu___ -> ()) disjunction_monoid conjunction_monoid type ('m, 'a, 'mult, 'act) mult_act_lemma = unit diff --git a/ocaml/fstar-lib/generated/FStar_GSet.ml b/ocaml/fstar-lib/generated/FStar_GSet.ml index 27aaacec689..a8e11997c67 100644 --- a/ocaml/fstar-lib/generated/FStar_GSet.ml +++ b/ocaml/fstar-lib/generated/FStar_GSet.ml @@ -1,12 +1,5 @@ open Prims type 'a set = unit type ('a, 's1, 's2) equal = unit - - - - - - - type ('a, 's1, 's2) disjoint = unit -type ('a, 's1, 's2) subset = unit +type ('a, 's1, 's2) subset = unit \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Monotonic_HyperHeap.ml b/ocaml/fstar-lib/generated/FStar_Monotonic_HyperHeap.ml index 7c10adf3024..1e52da86ff1 100644 --- a/ocaml/fstar-lib/generated/FStar_Monotonic_HyperHeap.ml +++ b/ocaml/fstar-lib/generated/FStar_Monotonic_HyperHeap.ml @@ -1,9 +1,6 @@ open Prims type rid = unit type hmap = (unit, FStar_Monotonic_Heap.heap) FStar_Map.t - - - let (mod_set : unit FStar_Set.set -> unit FStar_Set.set) = fun uu___ -> Prims.magic () type ('s, 'm0, 'm1) modifies = unit @@ -11,6 +8,4 @@ type ('s, 'm0, 'm1) modifies_just = unit type ('r, 'm0, 'm1) modifies_one = unit type ('s, 'm0, 'm1) equal_on = unit type ('s1, 's2) disjoint_regions = unit -type ('r, 'n, 'c, 'freeable, 's) extend_post = unit - - +type ('r, 'n, 'c, 'freeable, 's) extend_post = unit \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Monotonic_HyperStack.ml b/ocaml/fstar-lib/generated/FStar_Monotonic_HyperStack.ml index b6d1e73fff4..20e7bad6921 100644 --- a/ocaml/fstar-lib/generated/FStar_Monotonic_HyperStack.ml +++ b/ocaml/fstar-lib/generated/FStar_Monotonic_HyperStack.ml @@ -20,13 +20,11 @@ let (__proj__HS__item__rid_ctr : mem' -> Prims.int) = fun projectee -> match projectee with | HS (rid_ctr, h, tip) -> rid_ctr let (__proj__HS__item__h : mem' -> FStar_Monotonic_HyperHeap.hmap) = fun projectee -> match projectee with | HS (rid_ctr, h, tip) -> h - let (mk_mem : Prims.int -> FStar_Monotonic_HyperHeap.hmap -> unit -> mem') = fun rid_ctr -> fun h -> fun tip -> HS (rid_ctr, h, ()) let (get_hmap : mem' -> FStar_Monotonic_HyperHeap.hmap) = fun m -> __proj__HS__item__h m let (get_rid_ctr : mem' -> Prims.int) = fun m -> __proj__HS__item__rid_ctr m - type mem = mem' let (empty_mem : mem) = let empty_map = @@ -51,12 +49,10 @@ type ('a, 'rel) mreference' = | MkRef of unit * ('a, 'rel) FStar_Monotonic_Heap.mref let uu___is_MkRef : 'a 'rel . ('a, 'rel) mreference' -> Prims.bool = fun projectee -> true - let __proj__MkRef__item__ref : 'a 'rel . ('a, 'rel) mreference' -> ('a, 'rel) FStar_Monotonic_Heap.mref = fun projectee -> match projectee with | MkRef (frame, ref) -> ref type ('a, 'rel) mreference = ('a, 'rel) mreference' - let mk_mreference : 'a 'rel . unit -> ('a, 'rel) FStar_Monotonic_Heap.mref -> ('a, 'rel) mreference @@ -187,7 +183,6 @@ type ('rs, 'h0, 'h1) mods = unit type aref = | ARef of unit * FStar_Monotonic_Heap.aref let (uu___is_ARef : aref -> Prims.bool) = fun projectee -> true - let (__proj__ARef__item__aref_aref : aref -> FStar_Monotonic_Heap.aref) = fun projectee -> match projectee with | ARef (aref_region, aref_aref) -> aref_aref diff --git a/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml b/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml index 1f8425ded08..5ee00f0e445 100644 --- a/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml +++ b/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml @@ -9,15 +9,14 @@ let alloc_mref_seq : 'a . unit -> 'a FStar_Seq_Base.seq -> - (unit, 'a FStar_Seq_Base.seq, ('a, unit, unit) grows) - FStar_HyperStack_ST.m_rref + (unit, 'a FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref = fun r -> fun init -> FStar_HyperStack_ST.ralloc () init type ('a, 'i, 'n, 'x, 'r, 'h) at_least = unit let write_at_end : 'a . unit -> - (unit, 'a FStar_Seq_Base.seq, ('a, unit, unit) grows) - FStar_HyperStack_ST.m_rref -> 'a -> unit + (unit, 'a FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref -> + 'a -> unit = fun i -> fun r -> @@ -52,16 +51,15 @@ let i_write_at_end : 'a 'p . unit -> (unit, 'a, 'p) i_seq -> 'a -> unit = type 's invariant = unit let (test0 : unit -> - (unit, Prims.nat FStar_Seq_Base.seq, (Prims.nat, unit, unit) grows) - FStar_HyperStack_ST.m_rref -> Prims.nat -> unit) + (unit, Prims.nat FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref -> + Prims.nat -> unit) = fun r -> fun a -> fun k -> let h0 = FStar_HyperStack_ST.get () in FStar_HyperStack_ST.mr_witness () () () (Obj.magic a) () -let (itest : - unit -> (unit, Prims.nat, unit invariant) i_seq -> Prims.nat -> unit) = +let (itest : unit -> (unit, Prims.nat, unit) i_seq -> Prims.nat -> unit) = fun r -> fun a -> fun k -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 8553b2c8f1b..7ff28a3c68e 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -4150,7 +4150,15 @@ let (fv_has_erasable_attr : env -> FStar_Syntax_Syntax.fv -> Prims.bool) = fv_exists_and_has_attr env1 (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v FStar_Parser_Const.erasable_attr in - match uu___1 with | (ex, erasable) -> (ex, erasable) in + match uu___1 with + | (ex, erasable) -> + let uu___2 = + fv_exists_and_has_attr env1 + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + FStar_Parser_Const.must_erase_for_extraction_attr in + (match uu___2 with + | (ex1, must_erase_for_extraction) -> + (ex1, (erasable || must_erase_for_extraction))) in cache_in_fv_tab env1.erasable_types_tab fv f let (fv_has_strict_args : env -> @@ -4370,6 +4378,10 @@ let rec (non_informative : env -> FStar_Syntax_Syntax.typ -> Prims.bool) = { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = uu___1;_} -> non_informative env1 head + | FStar_Syntax_Syntax.Tm_abs + { FStar_Syntax_Syntax.bs = uu___1; FStar_Syntax_Syntax.body = body; + FStar_Syntax_Syntax.rc_opt = uu___2;_} + -> non_informative env1 body | FStar_Syntax_Syntax.Tm_uinst (t1, uu___1) -> non_informative env1 t1 | FStar_Syntax_Syntax.Tm_arrow { FStar_Syntax_Syntax.bs1 = uu___1; FStar_Syntax_Syntax.comp = c;_} @@ -4378,6 +4390,10 @@ let rec (non_informative : env -> FStar_Syntax_Syntax.typ -> Prims.bool) = (non_informative env1 (FStar_Syntax_Util.comp_result c))) || (is_erasable_effect env1 (FStar_Syntax_Util.comp_effect_name c)) + | FStar_Syntax_Syntax.Tm_meta + { FStar_Syntax_Syntax.tm2 = tm; + FStar_Syntax_Syntax.meta = uu___1;_} + -> non_informative env1 tm | uu___1 -> false let (num_effect_indices : env -> FStar_Ident.lident -> FStar_Compiler_Range_Type.range -> Prims.int) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml index 9644d212b85..2d8b7b05fee 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml @@ -7744,6 +7744,9 @@ let (non_info_norm : [FStar_TypeChecker_Env.UnfoldUntil FStar_Syntax_Syntax.delta_constant; FStar_TypeChecker_Env.AllowUnboundUniverses; FStar_TypeChecker_Env.EraseUniverses; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Iota; FStar_TypeChecker_Env.HNF; FStar_TypeChecker_Env.Unascribe; FStar_TypeChecker_Env.ForExtraction] in diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Quals.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Quals.ml index b4cf1502a43..a8acb8f7bd1 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Quals.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Quals.ml @@ -322,6 +322,23 @@ let (check_sigelt_quals_pre : if uu___5 then err [] else () | uu___4 -> ())) else ()) +let (non_info_norm_weak : + FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> Prims.bool) = + fun env -> + fun t -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.AllowUnboundUniverses; + FStar_TypeChecker_Env.EraseUniverses; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Iota; + FStar_TypeChecker_Env.HNF; + FStar_TypeChecker_Env.Weak; + FStar_TypeChecker_Env.Unascribe; + FStar_TypeChecker_Env.ForExtraction] in + let uu___ = FStar_TypeChecker_Normalize.normalize steps env t in + FStar_TypeChecker_Env.non_informative env uu___ let (check_erasable : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.qualifier Prims.list -> @@ -387,205 +404,176 @@ let (check_erasable : (Obj.magic FStar_Errors_Msg.is_error_message_list_doc) (Obj.magic uu___2)) else (); + (let uu___3 = + (Prims.op_Negation se_has_erasable_attr) && + (let uu___4 = FStar_Options.ide () in Prims.op_Negation uu___4) in + if uu___3 + then + match se.FStar_Syntax_Syntax.sigel with + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (false, lb::[]); + FStar_Syntax_Syntax.lids1 = uu___4;_} + -> + let lbname = + FStar_Compiler_Util.right lb.FStar_Syntax_Syntax.lbname in + let has_iface_val = + let uu___5 = + let uu___6 = FStar_TypeChecker_Env.dsenv env in + let uu___7 = FStar_TypeChecker_Env.current_module env in + FStar_Syntax_DsEnv.iface_decls uu___6 uu___7 in + match uu___5 with + | FStar_Pervasives_Native.Some iface_decls -> + let uu___6 = + let uu___7 = + FStar_Ident.ident_of_lid + (lbname.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + FStar_Parser_AST.decl_is_val uu___7 in + FStar_Compiler_Util.for_some uu___6 iface_decls + | FStar_Pervasives_Native.None -> false in + let uu___5 = + FStar_Syntax_Util.abs_formals lb.FStar_Syntax_Syntax.lbdef in + (match uu___5 with + | (uu___6, body, uu___7) -> + let uu___8 = + has_iface_val && (non_info_norm_weak env body) in + if uu___8 + then + let uu___9 = + let uu___10 = + let uu___11 = + let uu___12 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_fv lbname in + let uu___13 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_fv lbname in + FStar_Compiler_Util.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" + uu___12 uu___13 in + FStar_Errors_Msg.text uu___11 in + [uu___10] in + FStar_Errors.log_issue + FStar_Syntax_Syntax.hasRange_fv lbname + FStar_Errors_Codes.Error_MustEraseMissing () + (Obj.magic + FStar_Errors_Msg.is_error_message_list_doc) + (Obj.magic uu___9) + else ()) + | uu___4 -> () + else ()); if se_has_erasable_attr then (match se.FStar_Syntax_Syntax.sigel with - | FStar_Syntax_Syntax.Sig_bundle uu___2 -> - let uu___3 = - let uu___4 = + | FStar_Syntax_Syntax.Sig_bundle uu___3 -> + let uu___4 = + let uu___5 = FStar_Compiler_Util.for_some - (fun uu___5 -> - match uu___5 with + (fun uu___6 -> + match uu___6 with | FStar_Syntax_Syntax.Noeq -> true - | uu___6 -> false) quals in - Prims.op_Negation uu___4 in - if uu___3 + | uu___7 -> false) quals in + Prims.op_Negation uu___5 in + if uu___4 then - let uu___4 = - let uu___5 = + let uu___5 = + let uu___6 = FStar_Errors_Msg.text "Incompatible attributes and qualifiers: erasable types do not support decidable equality and must be marked `noeq`." in - [uu___5] in + [uu___6] in FStar_Errors.raise_error FStar_Class_HasRange.hasRange_range r FStar_Errors_Codes.Fatal_QulifierListNotPermitted () (Obj.magic FStar_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___4) + (Obj.magic uu___5) else () - | FStar_Syntax_Syntax.Sig_declare_typ uu___2 -> () - | FStar_Syntax_Syntax.Sig_fail uu___2 -> () + | FStar_Syntax_Syntax.Sig_declare_typ uu___3 -> () + | FStar_Syntax_Syntax.Sig_fail uu___3 -> () | FStar_Syntax_Syntax.Sig_let { FStar_Syntax_Syntax.lbs1 = (false, lb::[]); - FStar_Syntax_Syntax.lids1 = uu___2;_} + FStar_Syntax_Syntax.lids1 = uu___3;_} -> - let uu___3 = + let uu___4 = FStar_Syntax_Util.abs_formals lb.FStar_Syntax_Syntax.lbdef in - (match uu___3 with - | (uu___4, body, uu___5) -> - let uu___6 = - let uu___7 = + (match uu___4 with + | (uu___5, body, uu___6) -> + let uu___7 = + let uu___8 = FStar_TypeChecker_Normalize.non_info_norm env body in - Prims.op_Negation uu___7 in - if uu___6 + Prims.op_Negation uu___8 in + if uu___7 then - let uu___7 = - let uu___8 = + let uu___8 = + let uu___9 = FStar_Errors_Msg.text "Illegal attribute: the `erasable` attribute is only permitted on inductive type definitions and abbreviations for non-informative types." in - let uu___9 = - let uu___10 = - let uu___11 = FStar_Errors_Msg.text "The term" in - let uu___12 = - let uu___13 = + let uu___10 = + let uu___11 = + let uu___12 = FStar_Errors_Msg.text "The term" in + let uu___13 = + let uu___14 = FStar_Class_PP.pp FStar_Syntax_Print.pretty_term body in - let uu___14 = + let uu___15 = FStar_Errors_Msg.text "is considered informative." in - FStar_Pprint.op_Hat_Slash_Hat uu___13 uu___14 in - FStar_Pprint.op_Hat_Slash_Hat uu___11 uu___12 in - [uu___10] in - uu___8 :: uu___9 in + FStar_Pprint.op_Hat_Slash_Hat uu___14 uu___15 in + FStar_Pprint.op_Hat_Slash_Hat uu___12 uu___13 in + [uu___11] in + uu___9 :: uu___10 in FStar_Errors.raise_error (FStar_Syntax_Syntax.has_range_syntax ()) body FStar_Errors_Codes.Fatal_QulifierListNotPermitted () (Obj.magic FStar_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___7) + (Obj.magic uu___8) else ()) | FStar_Syntax_Syntax.Sig_new_effect { FStar_Syntax_Syntax.mname = eff_name; - FStar_Syntax_Syntax.cattributes = uu___2; - FStar_Syntax_Syntax.univs = uu___3; - FStar_Syntax_Syntax.binders = uu___4; - FStar_Syntax_Syntax.signature = uu___5; - FStar_Syntax_Syntax.combinators = uu___6; - FStar_Syntax_Syntax.actions = uu___7; - FStar_Syntax_Syntax.eff_attrs = uu___8; - FStar_Syntax_Syntax.extraction_mode = uu___9;_} + FStar_Syntax_Syntax.cattributes = uu___3; + FStar_Syntax_Syntax.univs = uu___4; + FStar_Syntax_Syntax.binders = uu___5; + FStar_Syntax_Syntax.signature = uu___6; + FStar_Syntax_Syntax.combinators = uu___7; + FStar_Syntax_Syntax.actions = uu___8; + FStar_Syntax_Syntax.eff_attrs = uu___9; + FStar_Syntax_Syntax.extraction_mode = uu___10;_} -> if Prims.op_Negation (FStar_Compiler_List.contains FStar_Syntax_Syntax.TotalEffect quals) then - let uu___10 = - let uu___11 = - let uu___12 = FStar_Errors_Msg.text "Effect" in - let uu___13 = - let uu___14 = + let uu___11 = + let uu___12 = + let uu___13 = FStar_Errors_Msg.text "Effect" in + let uu___14 = + let uu___15 = FStar_Class_PP.pp FStar_Ident.pretty_lident eff_name in - let uu___15 = + let uu___16 = FStar_Errors_Msg.text "is marked erasable but only total effects are allowed to be erasable." in - FStar_Pprint.op_Hat_Slash_Hat uu___14 uu___15 in - FStar_Pprint.op_Hat_Slash_Hat uu___12 uu___13 in - [uu___11] in + FStar_Pprint.op_Hat_Slash_Hat uu___15 uu___16 in + FStar_Pprint.op_Hat_Slash_Hat uu___13 uu___14 in + [uu___12] in FStar_Errors.raise_error FStar_Class_HasRange.hasRange_range r FStar_Errors_Codes.Fatal_QulifierListNotPermitted () (Obj.magic FStar_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___10) + (Obj.magic uu___11) else () - | uu___2 -> - let uu___3 = - let uu___4 = + | uu___3 -> + let uu___4 = + let uu___5 = FStar_Errors_Msg.text "Illegal attribute: the `erasable` attribute is only permitted on inductive type definitions and abbreviations for non-informative types." in - [uu___4] in + [uu___5] in FStar_Errors.raise_error FStar_Class_HasRange.hasRange_range r FStar_Errors_Codes.Fatal_QulifierListNotPermitted () (Obj.magic FStar_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___3)) + (Obj.magic uu___4)) else () -let (check_must_erase_attribute : - FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.sigelt -> unit) = - fun env -> - fun se -> - let uu___ = FStar_Options.ide () in - if uu___ - then () - else - (match se.FStar_Syntax_Syntax.sigel with - | FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = lbs; - FStar_Syntax_Syntax.lids1 = l;_} - -> - let uu___2 = - let uu___3 = FStar_TypeChecker_Env.dsenv env in - let uu___4 = FStar_TypeChecker_Env.current_module env in - FStar_Syntax_DsEnv.iface_decls uu___3 uu___4 in - (match uu___2 with - | FStar_Pervasives_Native.None -> () - | FStar_Pervasives_Native.Some iface_decls -> - FStar_Compiler_List.iter - (fun lb -> - let lbname = - FStar_Compiler_Util.right - lb.FStar_Syntax_Syntax.lbname in - let has_iface_val = - let uu___3 = - let uu___4 = - FStar_Ident.ident_of_lid - (lbname.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - FStar_Parser_AST.decl_is_val uu___4 in - FStar_Compiler_Util.for_some uu___3 iface_decls in - if has_iface_val - then - let must_erase = - FStar_TypeChecker_Util.must_erase_for_extraction - env lb.FStar_Syntax_Syntax.lbdef in - let has_attr = - FStar_TypeChecker_Env.fv_has_attr env lbname - FStar_Parser_Const.must_erase_for_extraction_attr in - (if must_erase && (Prims.op_Negation has_attr) - then - let uu___3 = - let uu___4 = - let uu___5 = - let uu___6 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_fv lbname in - let uu___7 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_fv lbname in - FStar_Compiler_Util.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" - uu___6 uu___7 in - FStar_Errors_Msg.text uu___5 in - [uu___4] in - FStar_Errors.log_issue - FStar_Syntax_Syntax.hasRange_fv lbname - FStar_Errors_Codes.Error_MustEraseMissing () - (Obj.magic - FStar_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___3) - else - if has_attr && (Prims.op_Negation must_erase) - then - (let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_fv - lbname in - FStar_Compiler_Util.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." - uu___7 in - FStar_Errors_Msg.text uu___6 in - [uu___5] in - FStar_Errors.log_issue - FStar_Syntax_Syntax.hasRange_fv lbname - FStar_Errors_Codes.Error_MustEraseMissing () - (Obj.magic - FStar_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___4)) - else ()) - else ()) (FStar_Pervasives_Native.snd lbs)) - | uu___2 -> ()) let (check_typeclass_instance_attribute : FStar_TypeChecker_Env.env -> FStar_Compiler_Range_Type.range -> FStar_Syntax_Syntax.sigelt -> unit) @@ -721,5 +709,4 @@ let (check_sigelt_quals_post : let quals = se.FStar_Syntax_Syntax.sigquals in let r = se.FStar_Syntax_Syntax.sigrng in check_erasable env quals r se; - check_must_erase_attribute env se; check_typeclass_instance_attribute env r se \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml index ee46fd88fe6..36cf925a70f 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml @@ -7302,63 +7302,16 @@ let (must_erase_for_extraction : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> Prims.bool) = fun g -> fun t -> - let rec descend env t1 = - let uu___ = - let uu___1 = FStar_Syntax_Subst.compress t1 in - uu___1.FStar_Syntax_Syntax.n in - match uu___ with - | FStar_Syntax_Syntax.Tm_arrow uu___1 -> - let uu___2 = FStar_Syntax_Util.arrow_formals_comp t1 in - (match uu___2 with - | (bs, c) -> - let env1 = FStar_TypeChecker_Env.push_binders env bs in - (FStar_TypeChecker_Env.is_erasable_effect env1 - (FStar_Syntax_Util.comp_effect_name c)) - || - ((FStar_Syntax_Util.is_pure_or_ghost_comp c) && - (aux env1 (FStar_Syntax_Util.comp_result c)))) - | FStar_Syntax_Syntax.Tm_refine - { - FStar_Syntax_Syntax.b = - { FStar_Syntax_Syntax.ppname = uu___1; - FStar_Syntax_Syntax.index = uu___2; - FStar_Syntax_Syntax.sort = t2;_}; - FStar_Syntax_Syntax.phi = uu___3;_} - -> aux env t2 - | FStar_Syntax_Syntax.Tm_app - { FStar_Syntax_Syntax.hd = head; - FStar_Syntax_Syntax.args = uu___1;_} - -> descend env head - | FStar_Syntax_Syntax.Tm_uinst (head, uu___1) -> descend env head - | FStar_Syntax_Syntax.Tm_fvar fv -> - FStar_TypeChecker_Env.fv_has_attr env fv - FStar_Parser_Const.must_erase_for_extraction_attr - | uu___1 -> false - and aux env t1 = - let t2 = - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Weak; - FStar_TypeChecker_Env.HNF; - FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.AllowUnboundUniverses; - FStar_TypeChecker_Env.Zeta; - FStar_TypeChecker_Env.Iota; - FStar_TypeChecker_Env.Unascribe] env t1 in - let res = - (FStar_TypeChecker_Env.non_informative env t2) || (descend env t2) in - (let uu___1 = FStar_Compiler_Effect.op_Bang dbg_Extraction in - if uu___1 - then - let uu___2 = - FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in - FStar_Compiler_Util.print2 "must_erase=%s: %s\n" - (if res then "true" else "false") uu___2 - else ()); - res in - aux g t + let res = FStar_TypeChecker_Normalize.non_info_norm g t in + (let uu___1 = FStar_Compiler_Effect.op_Bang dbg_Extraction in + if uu___1 + then + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in + FStar_Compiler_Util.print2 "must_erase=%s: %s\n" + (if res then "true" else "false") uu___2 + else ()); + res let (effect_extraction_mode : FStar_TypeChecker_Env.env -> FStar_Ident.lident -> FStar_Syntax_Syntax.eff_extraction_mode) diff --git a/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml b/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml index 4aa36833970..43fc68866d2 100644 --- a/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml +++ b/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml @@ -37,8 +37,7 @@ let default_wfr : 'a . unit -> 'a wfr_t = proof = () } type ('a, 'x1, 'x2) empty_relation = unit -let rec empty_decreaser : - 'a . 'a -> ('a, ('a, unit, unit) empty_relation, unit) acc_classical = +let rec empty_decreaser : 'a . 'a -> ('a, unit, unit) acc_classical = fun x -> let smaller y = empty_decreaser y in AccClassicalIntro smaller let empty_wfr : 'a . unit -> 'a wfr_t = fun uu___ -> @@ -48,9 +47,7 @@ let empty_wfr : 'a . unit -> 'a wfr_t = proof = () } type ('a, 'r, 'x1, 'x2) acc_relation = unit -let rec acc_decreaser : - 'a 'r . - unit -> 'a -> ('a, ('a, 'r, unit, unit) acc_relation, unit) acc_classical +let rec acc_decreaser : 'a 'r . unit -> 'a -> ('a, unit, unit) acc_classical = fun f -> fun x -> let smaller y = acc_decreaser () y in AccClassicalIntro smaller diff --git a/ocaml/fstar-lib/generated/LowStar_Buffer.ml b/ocaml/fstar-lib/generated/LowStar_Buffer.ml index 9059a9cc0cc..73d55a5a93f 100644 --- a/ocaml/fstar-lib/generated/LowStar_Buffer.ml +++ b/ocaml/fstar-lib/generated/LowStar_Buffer.ml @@ -8,25 +8,15 @@ type 'a pointer_or_null = 'a buffer let sub : 'a . unit -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer - -> + ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> FStar_UInt32.t -> - unit -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + unit -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.msub let offset : 'a . unit -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer - -> - FStar_UInt32.t -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> + FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.moffset type ('a, 'len) lbuffer = ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer let gcmalloc : @@ -34,45 +24,31 @@ let gcmalloc : unit -> unit -> 'a -> - FStar_UInt32.t -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.mgcmalloc let malloc : 'a . unit -> unit -> 'a -> - FStar_UInt32.t -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.mmalloc let alloca : 'a . unit -> 'a -> - FStar_UInt32.t -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.malloca let alloca_of_list : 'a . unit -> - 'a Prims.list -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer + 'a Prims.list -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.malloca_of_list let gcmalloc_of_list : 'a . unit -> unit -> - 'a Prims.list -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + 'a Prims.list -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.mgcmalloc_of_list type ('a, 'l) assign_list_t = 'a buffer -> unit let rec assign_list : 'a . 'a Prims.list -> 'a buffer -> unit = diff --git a/ocaml/fstar-lib/generated/LowStar_Monotonic_Buffer.ml b/ocaml/fstar-lib/generated/LowStar_Monotonic_Buffer.ml index 3f1f87e182f..4ad15954612 100644 --- a/ocaml/fstar-lib/generated/LowStar_Monotonic_Buffer.ml +++ b/ocaml/fstar-lib/generated/LowStar_Monotonic_Buffer.ml @@ -41,7 +41,6 @@ let mnull : type ('uuuuu, 'uuuuu1, 'uuuuu2, 'b, 'h) unused_in = Obj.t type ('t, 'rrel, 'rel, 'b) buffer_compatible = Obj.t type ('uuuuu, 'rrel, 'rel, 'h, 'b) live = Obj.t - type ('a, 'rrel, 'rel, 'b, 'i, 'len, 'suburel) compatible_sub = unit type ubuffer_ = { diff --git a/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml b/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml index c0a81fdda4e..648a3cef0f8 100644 --- a/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml +++ b/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml @@ -14,10 +14,7 @@ type 'len lbuffer = buffer type ('r, 'len) malloc_pre = unit type ('h0, 'b, 'h1) alloc_post_mem_common = unit let (update_frozen_until_alloc : - (u8, (unit, unit) prefix_freezable_preorder, - (unit, unit) prefix_freezable_preorder) LowStar_Monotonic_Buffer.mbuffer - -> unit) - = + (u8, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> unit) = fun b -> LowStar_Endianness.store32_le_i b Stdint.Uint32.zero (Stdint.Uint32.of_int (4)); diff --git a/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml b/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml index 24e8950e216..9a417b88559 100644 --- a/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml +++ b/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml @@ -10,28 +10,20 @@ type 'a pointer_or_null = 'a ubuffer let usub : 'a . unit -> - ('a FStar_Pervasives_Native.option, - ('a, unit, unit) initialization_preorder, - ('a, unit, unit) initialization_preorder) + ('a FStar_Pervasives_Native.option, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> FStar_UInt32.t -> unit -> - ('a FStar_Pervasives_Native.option, - ('a, unit, unit) initialization_preorder, - ('a, unit, unit) initialization_preorder) + ('a FStar_Pervasives_Native.option, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.msub let uoffset : 'a . unit -> - ('a FStar_Pervasives_Native.option, - ('a, unit, unit) initialization_preorder, - ('a, unit, unit) initialization_preorder) + ('a FStar_Pervasives_Native.option, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> FStar_UInt32.t -> - ('a FStar_Pervasives_Native.option, - ('a, unit, unit) initialization_preorder, - ('a, unit, unit) initialization_preorder) + ('a FStar_Pervasives_Native.option, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.moffset type ('a, 'i, 's) ipred = unit diff --git a/ocaml/fstar-lib/generated/LowStar_Vector.ml b/ocaml/fstar-lib/generated/LowStar_Vector.ml index 022f29b49e0..5b850ecccb2 100644 --- a/ocaml/fstar-lib/generated/LowStar_Vector.ml +++ b/ocaml/fstar-lib/generated/LowStar_Vector.ml @@ -21,7 +21,6 @@ type ('a, 'h, 'vec) live = ('a, unit, unit, unit, unit) LowStar_Monotonic_Buffer.live type ('a, 'vec) freeable = ('a, unit, unit, unit) LowStar_Monotonic_Buffer.freeable - type ('h0, 'h1) hmap_dom_eq = (unit, unit, unit) FStar_Set.equal let alloc_empty : 'a . unit -> 'a vector = fun uu___ -> diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index 891f7bef53e..2ef668f4a0e 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -947,13 +947,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 @@ -1049,10 +1044,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/FStar.TypeChecker.Env.fsti b/src/typechecker/FStar.TypeChecker.Env.fsti index c3d130e6933..e41be424d55 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fsti +++ b/src/typechecker/FStar.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/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index b277bffa941..79444930c02 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/src/typechecker/FStar.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/FStar.TypeChecker.Quals.fst b/src/typechecker/FStar.TypeChecker.Quals.fst index 5c513611314..96dda8f5a3f 100644 --- a/src/typechecker/FStar.TypeChecker.Quals.fst +++ b/src/typechecker/FStar.TypeChecker.Quals.fst @@ -161,6 +161,26 @@ let check_sigelt_quals_pre (env:FStar.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/FStar.TypeChecker.Quals.fsti b/src/typechecker/FStar.TypeChecker.Quals.fsti index d9f11bfc468..62594bd8b3d 100644 --- a/src/typechecker/FStar.TypeChecker.Quals.fsti +++ b/src/typechecker/FStar.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/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst index b08a8f2fec4..8a6768f7815 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fst +++ b/src/typechecker/FStar.TypeChecker.Util.fst @@ -3184,40 +3184,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 = FStar.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