From 7e628f2cdc2dab65c496020b2320ee76211abf0f Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 2 Oct 2024 12:45:52 -0700 Subject: [PATCH] Treat must_erase_for_extraction as an alias for erasable. --- ocaml/fstar-lib/generated/FStar_GSet.ml | 9 +- .../generated/FStar_Monotonic_HyperHeap.ml | 7 +- .../generated/FStar_Monotonic_HyperStack.ml | 5 - .../generated/FStar_TypeChecker_Env.ml | 10 +- .../generated/FStar_TypeChecker_Normalize.ml | 4 + .../generated/FStar_TypeChecker_Quals.ml | 261 ++++++++---------- .../generated/FStar_TypeChecker_Util.ml | 67 +---- .../generated/LowStar_Monotonic_Buffer.ml | 1 - ocaml/fstar-lib/generated/LowStar_Vector.ml | 1 - src/typechecker/FStar.TypeChecker.Env.fst | 9 +- .../FStar.TypeChecker.Normalize.fst | 2 + src/typechecker/FStar.TypeChecker.Quals.fst | 58 ++-- src/typechecker/FStar.TypeChecker.Util.fst | 37 +-- .../MustEraseForExtraction.fst | 3 +- .../MustEraseForExtraction.fsti | 4 +- ulib/FStar.GSet.fsti | 4 +- ulib/FStar.GhostSet.fsti | 2 +- ulib/FStar.Monotonic.HyperHeap.fsti | 4 +- ulib/FStar.Pervasives.fsti | 14 +- ulib/FStar.TSet.fst | 2 +- ulib/FStar.TSet.fsti | 4 +- 21 files changed, 177 insertions(+), 331 deletions(-) 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_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 8553b2c8f1b..65aca445e1d 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 -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml index bec50745032..7e61c84d6b9 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml @@ -7744,6 +7744,10 @@ 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.Zeta; + 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..30f818ebd83 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Quals.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Quals.ml @@ -387,205 +387,177 @@ 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 && + (FStar_TypeChecker_Normalize.non_info_norm 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 +693,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/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_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..2f1a37d4ab2 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 diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index b277bffa941..51171be1854 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; Zeta; 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..339b13566bd 100644 --- a/src/typechecker/FStar.TypeChecker.Quals.fst +++ b/src/typechecker/FStar.TypeChecker.Quals.fst @@ -183,6 +183,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 && N.non_info_norm 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 +237,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 +291,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.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