From a8c5846b0cf54a9f183f58b68d24f87f0f4e8ec9 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 11 Sep 2024 02:48:03 +0000 Subject: [PATCH] Add extract_as attribute. --- .../generated/FStar_Extraction_ML_Modul.ml | 151 ++++++++++++------ .../fstar-lib/generated/FStar_Parser_Const.ml | 2 + .../generated/FStar_TypeChecker_Env.ml | 17 +- .../generated/FStar_TypeChecker_Normalize.ml | 64 +++++++- src/extraction/FStar.Extraction.ML.Modul.fst | 10 ++ src/parser/FStar.Parser.Const.fst | 1 + src/typechecker/FStar.TypeChecker.Env.fst | 8 +- src/typechecker/FStar.TypeChecker.Env.fsti | 1 + .../FStar.TypeChecker.Normalize.fst | 28 +++- .../FStar.TypeChecker.Normalize.fsti | 3 + tests/extraction/ExtractAs.fst | 17 ++ tests/extraction/Makefile | 2 +- ulib/FStar.Pervasives.fst | 2 + ulib/FStar.Pervasives.fsti | 14 ++ 14 files changed, 254 insertions(+), 66 deletions(-) create mode 100644 tests/extraction/ExtractAs.fst diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml index 2cc4a72b6dd..90976fb772b 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml @@ -1644,6 +1644,51 @@ let (mark_sigelt_erased : FStar_Syntax_Syntax.lid_as_fv lid FStar_Pervasives_Native.None in FStar_Extraction_ML_UEnv.extend_erased_fv g1 uu___1) (FStar_Syntax_Util.lids_of_sigelt se) g +let (fixup_sigelt_extract_as : + FStar_Syntax_Syntax.sigelt -> FStar_Syntax_Syntax.sigelt) = + fun se -> + let uu___ = + let uu___1 = + FStar_Compiler_Util.find_map se.FStar_Syntax_Syntax.sigattrs + FStar_TypeChecker_Normalize.is_extract_as_attr in + ((se.FStar_Syntax_Syntax.sigel), uu___1) in + match uu___ with + | (FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (uu___1, lb::[]); + FStar_Syntax_Syntax.lids1 = lids;_}, + FStar_Pervasives_Native.Some impl) -> + { + FStar_Syntax_Syntax.sigel = + (FStar_Syntax_Syntax.Sig_let + { + FStar_Syntax_Syntax.lbs1 = + (true, + [{ + FStar_Syntax_Syntax.lbname = + (lb.FStar_Syntax_Syntax.lbname); + FStar_Syntax_Syntax.lbunivs = + (lb.FStar_Syntax_Syntax.lbunivs); + FStar_Syntax_Syntax.lbtyp = + (lb.FStar_Syntax_Syntax.lbtyp); + FStar_Syntax_Syntax.lbeff = + (lb.FStar_Syntax_Syntax.lbeff); + FStar_Syntax_Syntax.lbdef = impl; + FStar_Syntax_Syntax.lbattrs = + (lb.FStar_Syntax_Syntax.lbattrs); + FStar_Syntax_Syntax.lbpos = + (lb.FStar_Syntax_Syntax.lbpos) + }]); + FStar_Syntax_Syntax.lids1 = lids + }); + FStar_Syntax_Syntax.sigrng = (se.FStar_Syntax_Syntax.sigrng); + FStar_Syntax_Syntax.sigquals = (se.FStar_Syntax_Syntax.sigquals); + FStar_Syntax_Syntax.sigmeta = (se.FStar_Syntax_Syntax.sigmeta); + FStar_Syntax_Syntax.sigattrs = (se.FStar_Syntax_Syntax.sigattrs); + FStar_Syntax_Syntax.sigopens_and_abbrevs = + (se.FStar_Syntax_Syntax.sigopens_and_abbrevs); + FStar_Syntax_Syntax.sigopts = (se.FStar_Syntax_Syntax.sigopts) + } + | uu___1 -> se let rec (extract_sigelt_iface : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.sigelt -> (FStar_Extraction_ML_UEnv.uenv * iface)) @@ -1655,21 +1700,22 @@ let rec (extract_sigelt_iface : then let g1 = mark_sigelt_erased se g in (g1, empty_iface) else (let se1 = karamel_fixup_qual se in - match se1.FStar_Syntax_Syntax.sigel with + let se2 = fixup_sigelt_extract_as se1 in + match se2.FStar_Syntax_Syntax.sigel with | FStar_Syntax_Syntax.Sig_bundle uu___2 -> - extract_bundle_iface g se1 + extract_bundle_iface g se2 | FStar_Syntax_Syntax.Sig_inductive_typ uu___2 -> - extract_bundle_iface g se1 + extract_bundle_iface g se2 | FStar_Syntax_Syntax.Sig_datacon uu___2 -> - extract_bundle_iface g se1 + extract_bundle_iface g se2 | FStar_Syntax_Syntax.Sig_declare_typ { FStar_Syntax_Syntax.lid2 = lid; FStar_Syntax_Syntax.us2 = univs; FStar_Syntax_Syntax.t2 = t;_} when FStar_Extraction_ML_Term.is_arity g t -> let uu___2 = extract_type_declaration g true lid - se1.FStar_Syntax_Syntax.sigquals - se1.FStar_Syntax_Syntax.sigattrs univs t in + se2.FStar_Syntax_Syntax.sigquals + se2.FStar_Syntax_Syntax.sigattrs univs t in (match uu___2 with | (env, iface1, uu___3) -> (env, iface1)) | FStar_Syntax_Syntax.Sig_let { FStar_Syntax_Syntax.lbs1 = (false, lb::[]); @@ -1682,19 +1728,19 @@ let rec (extract_sigelt_iface : (fun uu___4 -> match uu___4 with | FStar_Syntax_Syntax.Projector uu___5 -> true - | uu___5 -> false) se1.FStar_Syntax_Syntax.sigquals in + | uu___5 -> false) se2.FStar_Syntax_Syntax.sigquals in if uu___3 then (g, empty_iface) else (let uu___5 = - extract_typ_abbrev g se1.FStar_Syntax_Syntax.sigquals - se1.FStar_Syntax_Syntax.sigattrs lb in + extract_typ_abbrev g se2.FStar_Syntax_Syntax.sigquals + se2.FStar_Syntax_Syntax.sigattrs lb in match uu___5 with | (env, iface1, uu___6) -> (env, iface1)) | FStar_Syntax_Syntax.Sig_let { FStar_Syntax_Syntax.lbs1 = (true, lbs); FStar_Syntax_Syntax.lids1 = uu___2;_} when should_split_let_rec_types_and_terms g lbs -> - let ses = split_let_rec_types_and_terms se1 g lbs in + let ses = split_let_rec_types_and_terms se2 g lbs in let iface1 = let uu___3 = FStar_Extraction_ML_UEnv.current_module_of_uenv g in { @@ -1705,10 +1751,10 @@ let rec (extract_sigelt_iface : } in FStar_Compiler_List.fold_left (fun uu___3 -> - fun se2 -> + fun se3 -> match uu___3 with | (g1, out) -> - let uu___4 = extract_sigelt_iface g1 se2 in + let uu___4 = extract_sigelt_iface g1 se3 in (match uu___4 with | (g2, mls) -> let uu___5 = iface_union out mls in (g2, uu___5))) @@ -1722,14 +1768,14 @@ let rec (extract_sigelt_iface : FStar_Extraction_ML_Term.is_arity g lb.FStar_Syntax_Syntax.lbtyp) lbs -> - let uu___3 = extract_let_rec_types se1 g lbs in + let uu___3 = extract_let_rec_types se2 g lbs in (match uu___3 with | (env, iface1, uu___4) -> (env, iface1)) | FStar_Syntax_Syntax.Sig_declare_typ { FStar_Syntax_Syntax.lid2 = lid; FStar_Syntax_Syntax.us2 = uu___2; FStar_Syntax_Syntax.t2 = t;_} -> - let quals = se1.FStar_Syntax_Syntax.sigquals in + let quals = se2.FStar_Syntax_Syntax.sigquals in let uu___3 = (FStar_Compiler_List.contains FStar_Syntax_Syntax.Assumption quals) @@ -1753,7 +1799,7 @@ let rec (extract_sigelt_iface : FStar_Syntax_Syntax.lids1 = uu___2;_} when Prims.uu___is_Cons - (se1.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data + (se2.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data -> let uu___3 = FStar_Compiler_List.tryPick @@ -1767,7 +1813,7 @@ let rec (extract_sigelt_iface : | FStar_Pervasives_Native.Some extractor -> FStar_Pervasives_Native.Some (ext, blob, extractor))) - (se1.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data in + (se2.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data in (match uu___3 with | FStar_Pervasives_Native.None -> let uu___4 = @@ -1775,7 +1821,7 @@ let rec (extract_sigelt_iface : (match uu___4 with | (g1, bindings) -> (g1, (iface_of_bindings bindings))) | FStar_Pervasives_Native.Some (ext, blob, extractor) -> - let res = extractor.extract_sigelt_iface g se1 blob in + let res = extractor.extract_sigelt_iface g se2 blob in (match res with | FStar_Pervasives.Inl res1 -> res1 | FStar_Pervasives.Inr err -> @@ -1783,7 +1829,7 @@ let rec (extract_sigelt_iface : FStar_Compiler_Util.format2 "Extension %s failed to extract iface: %s" ext err in FStar_Errors.raise_error - FStar_Syntax_Syntax.has_range_sigelt se1 + FStar_Syntax_Syntax.has_range_sigelt se2 FStar_Errors_Codes.Fatal_ExtractionUnsupported () (Obj.magic FStar_Errors_Msg.is_error_message_string) (Obj.magic uu___4))) @@ -1803,7 +1849,7 @@ let rec (extract_sigelt_iface : (g, empty_iface) | FStar_Syntax_Syntax.Sig_pragma p -> (FStar_Syntax_Util.process_pragma p - se1.FStar_Syntax_Syntax.sigrng; + se2.FStar_Syntax_Syntax.sigrng; (g, empty_iface)) | FStar_Syntax_Syntax.Sig_splice uu___2 -> FStar_Compiler_Effect.failwith @@ -2160,35 +2206,36 @@ let rec (extract_sig : then let g1 = mark_sigelt_erased se g in (g1, []) else (let se1 = karamel_fixup_qual se in - match se1.FStar_Syntax_Syntax.sigel with + let se2 = fixup_sigelt_extract_as se1 in + match se2.FStar_Syntax_Syntax.sigel with | FStar_Syntax_Syntax.Sig_bundle uu___5 -> - let uu___6 = extract_bundle g se1 in + let uu___6 = extract_bundle g se2 in (match uu___6 with | (g1, ses) -> let uu___7 = let uu___8 = FStar_Extraction_ML_RegEmb.maybe_register_plugin - g1 se1 in + g1 se2 in FStar_Compiler_List.op_At ses uu___8 in (g1, uu___7)) | FStar_Syntax_Syntax.Sig_inductive_typ uu___5 -> - let uu___6 = extract_bundle g se1 in + let uu___6 = extract_bundle g se2 in (match uu___6 with | (g1, ses) -> let uu___7 = let uu___8 = FStar_Extraction_ML_RegEmb.maybe_register_plugin - g1 se1 in + g1 se2 in FStar_Compiler_List.op_At ses uu___8 in (g1, uu___7)) | FStar_Syntax_Syntax.Sig_datacon uu___5 -> - let uu___6 = extract_bundle g se1 in + let uu___6 = extract_bundle g se2 in (match uu___6 with | (g1, ses) -> let uu___7 = let uu___8 = FStar_Extraction_ML_RegEmb.maybe_register_plugin - g1 se1 in + g1 se2 in FStar_Compiler_List.op_At ses uu___8 in (g1, uu___7)) | FStar_Syntax_Syntax.Sig_new_effect ed when @@ -2217,8 +2264,8 @@ let rec (extract_sig : when FStar_Extraction_ML_Term.is_arity g t -> let uu___5 = extract_type_declaration g false lid - se1.FStar_Syntax_Syntax.sigquals - se1.FStar_Syntax_Syntax.sigattrs univs t in + se2.FStar_Syntax_Syntax.sigquals + se2.FStar_Syntax_Syntax.sigattrs univs t in (match uu___5 with | (env, uu___6, impl) -> (env, impl)) | FStar_Syntax_Syntax.Sig_let { FStar_Syntax_Syntax.lbs1 = (false, lb::[]); @@ -2232,25 +2279,25 @@ let rec (extract_sig : (fun uu___7 -> match uu___7 with | FStar_Syntax_Syntax.Projector uu___8 -> true - | uu___8 -> false) se1.FStar_Syntax_Syntax.sigquals in + | uu___8 -> false) se2.FStar_Syntax_Syntax.sigquals in if uu___6 then (g, []) else (let uu___8 = - extract_typ_abbrev g se1.FStar_Syntax_Syntax.sigquals - se1.FStar_Syntax_Syntax.sigattrs lb in + extract_typ_abbrev g se2.FStar_Syntax_Syntax.sigquals + se2.FStar_Syntax_Syntax.sigattrs lb in match uu___8 with | (env, uu___9, impl) -> (env, impl)) | FStar_Syntax_Syntax.Sig_let { FStar_Syntax_Syntax.lbs1 = (true, lbs); FStar_Syntax_Syntax.lids1 = uu___5;_} when should_split_let_rec_types_and_terms g lbs -> - let ses = split_let_rec_types_and_terms se1 g lbs in + let ses = split_let_rec_types_and_terms se2 g lbs in FStar_Compiler_List.fold_left (fun uu___6 -> - fun se2 -> + fun se3 -> match uu___6 with | (g1, out) -> - let uu___7 = extract_sig g1 se2 in + let uu___7 = extract_sig g1 se3 in (match uu___7 with | (g2, mls) -> (g2, (FStar_Compiler_List.op_At out mls)))) @@ -2264,14 +2311,14 @@ let rec (extract_sig : FStar_Extraction_ML_Term.is_arity g lb.FStar_Syntax_Syntax.lbtyp) lbs -> - let uu___6 = extract_let_rec_types se1 g lbs in + let uu___6 = extract_let_rec_types se2 g lbs in (match uu___6 with | (env, uu___7, impl) -> (env, impl)) | FStar_Syntax_Syntax.Sig_let { FStar_Syntax_Syntax.lbs1 = (false, lb::[]); FStar_Syntax_Syntax.lids1 = uu___5;_} when Prims.uu___is_Cons - (se1.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data + (se2.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data -> let uu___6 = FStar_Compiler_List.tryPick @@ -2285,19 +2332,19 @@ let rec (extract_sig : | FStar_Pervasives_Native.Some extractor -> FStar_Pervasives_Native.Some (ext, blob, extractor))) - (se1.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data in + (se2.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data in (match uu___6 with - | FStar_Pervasives_Native.None -> extract_sig_let g se1 + | FStar_Pervasives_Native.None -> extract_sig_let g se2 | FStar_Pervasives_Native.Some (ext, blob, extractor) -> - let uu___7 = extractor.extract_sigelt g se1 blob in + let uu___7 = extractor.extract_sigelt g se2 blob in (match uu___7 with | FStar_Pervasives.Inl decls -> let meta = extract_metadata - se1.FStar_Syntax_Syntax.sigattrs in + se2.FStar_Syntax_Syntax.sigattrs in let mlattrs = extract_attrs g - se1.FStar_Syntax_Syntax.sigattrs in + se2.FStar_Syntax_Syntax.sigattrs in FStar_Compiler_List.fold_left (fun uu___8 -> fun d -> @@ -2369,19 +2416,19 @@ let rec (extract_sig : "Extension %s failed to extract term: %s" ext err in FStar_Errors.raise_error - FStar_Syntax_Syntax.has_range_sigelt se1 + FStar_Syntax_Syntax.has_range_sigelt se2 FStar_Errors_Codes.Fatal_ExtractionUnsupported () (Obj.magic FStar_Errors_Msg.is_error_message_string) (Obj.magic uu___8))) - | FStar_Syntax_Syntax.Sig_let uu___5 -> extract_sig_let g se1 + | FStar_Syntax_Syntax.Sig_let uu___5 -> extract_sig_let g se2 | FStar_Syntax_Syntax.Sig_declare_typ { FStar_Syntax_Syntax.lid2 = lid; FStar_Syntax_Syntax.us2 = uu___5; FStar_Syntax_Syntax.t2 = t;_} -> - let quals = se1.FStar_Syntax_Syntax.sigquals in + let quals = se2.FStar_Syntax_Syntax.sigquals in let uu___6 = (FStar_Compiler_List.contains FStar_Syntax_Syntax.Assumption quals) @@ -2409,17 +2456,17 @@ let rec (extract_sig : { FStar_Syntax_Syntax.sigel = uu___7; FStar_Syntax_Syntax.sigrng = - (se1.FStar_Syntax_Syntax.sigrng); + (se2.FStar_Syntax_Syntax.sigrng); FStar_Syntax_Syntax.sigquals = - (se1.FStar_Syntax_Syntax.sigquals); + (se2.FStar_Syntax_Syntax.sigquals); FStar_Syntax_Syntax.sigmeta = - (se1.FStar_Syntax_Syntax.sigmeta); + (se2.FStar_Syntax_Syntax.sigmeta); FStar_Syntax_Syntax.sigattrs = - (se1.FStar_Syntax_Syntax.sigattrs); + (se2.FStar_Syntax_Syntax.sigattrs); FStar_Syntax_Syntax.sigopens_and_abbrevs = - (se1.FStar_Syntax_Syntax.sigopens_and_abbrevs); + (se2.FStar_Syntax_Syntax.sigopens_and_abbrevs); FStar_Syntax_Syntax.sigopts = - (se1.FStar_Syntax_Syntax.sigopts) + (se2.FStar_Syntax_Syntax.sigopts) } in let uu___7 = extract_sig g always_fail1 in (match uu___7 with @@ -2438,7 +2485,7 @@ let rec (extract_sig : let uu___11 = let uu___12 = FStar_Extraction_ML_Util.mlloc_of_range - se1.FStar_Syntax_Syntax.sigrng in + se2.FStar_Syntax_Syntax.sigrng in FStar_Extraction_ML_Syntax.MLM_Loc uu___12 in FStar_Extraction_ML_Syntax.mk_mlmodule1 @@ -2473,7 +2520,7 @@ let rec (extract_sig : (g, []) | FStar_Syntax_Syntax.Sig_pragma p -> (FStar_Syntax_Util.process_pragma p - se1.FStar_Syntax_Syntax.sigrng; + se2.FStar_Syntax_Syntax.sigrng; (g, []))))) and (extract_sig_let : FStar_Extraction_ML_UEnv.uenv -> diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index 10006c2add0..defe0ee7e2c 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -661,5 +661,7 @@ let (tref_lid : FStar_Ident.lident) = let (document_lid : FStar_Ident.lident) = p2l ["FStar"; "Stubs"; "Pprint"; "document"] let (issue_lid : FStar_Ident.lident) = p2l ["FStar"; "Issue"; "issue"] +let (extract_as_lid : FStar_Ident.lident) = + p2l ["FStar"; "Pervasives"; "extract_as"] let (extract_as_impure_effect_lid : FStar_Ident.lident) = p2l ["FStar"; "Pervasives"; "extract_as_impure_effect"] \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 306f83b0b5b..8553b2c8f1b 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -3795,6 +3795,15 @@ let (num_datacon_non_injective_ty_params : then FStar_Pervasives_Native.Some Prims.int_zero else FStar_Pervasives_Native.Some num_ty_params | uu___1 -> FStar_Pervasives_Native.None +let (visible_with : + delta_level Prims.list -> + FStar_Syntax_Syntax.qualifier Prims.list -> Prims.bool) + = + fun delta_levels -> + fun quals -> + FStar_Compiler_Util.for_some + (fun dl -> FStar_Compiler_Util.for_some (visible_at dl) quals) + delta_levels let (lookup_definition_qninfo_aux : Prims.bool -> delta_level Prims.list -> @@ -3808,10 +3817,6 @@ let (lookup_definition_qninfo_aux : fun delta_levels -> fun lid -> fun qninfo1 -> - let visible quals = - FStar_Compiler_Util.for_some - (fun dl -> FStar_Compiler_Util.for_some (visible_at dl) quals) - delta_levels in match qninfo1 with | FStar_Pervasives_Native.Some (FStar_Pervasives.Inr (se, FStar_Pervasives_Native.None), @@ -3822,8 +3827,8 @@ let (lookup_definition_qninfo_aux : { FStar_Syntax_Syntax.lbs1 = (is_rec, lbs); FStar_Syntax_Syntax.lids1 = uu___1;_} when - (visible se.FStar_Syntax_Syntax.sigquals) && - ((Prims.op_Negation is_rec) || rec_ok) + (visible_with delta_levels se.FStar_Syntax_Syntax.sigquals) + && ((Prims.op_Negation is_rec) || rec_ok) -> FStar_Compiler_Util.find_map lbs (fun lb -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml index 4180b8465e5..5ef1da8d471 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml @@ -2063,6 +2063,43 @@ let (is_forall_const : uu___4)))) | uu___1 -> Obj.magic (Obj.repr FStar_Pervasives_Native.None)) uu___1 uu___ +let (is_extract_as_attr : + FStar_Syntax_Syntax.attribute -> + FStar_Syntax_Syntax.term FStar_Pervasives_Native.option) + = + fun attr -> + let uu___ = FStar_Syntax_Util.head_and_args attr in + match uu___ with + | (head, args) -> + let uu___1 = + let uu___2 = + let uu___3 = FStar_Syntax_Subst.compress head in + uu___3.FStar_Syntax_Syntax.n in + (uu___2, args) in + (match uu___1 with + | (FStar_Syntax_Syntax.Tm_uinst + ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_fvar fv; + FStar_Syntax_Syntax.pos = uu___2; + FStar_Syntax_Syntax.vars = uu___3; + FStar_Syntax_Syntax.hash_code = uu___4;_}, + u::[]), + uu___5::(t, uu___6)::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.extract_as_lid + -> FStar_Pervasives_Native.Some t + | uu___2 -> FStar_Pervasives_Native.None) +let (has_extract_as_attr : + FStar_TypeChecker_Env.env -> + FStar_Ident.lid -> + FStar_Syntax_Syntax.term FStar_Pervasives_Native.option) + = + fun g -> + fun lid -> + let uu___ = FStar_TypeChecker_Env.lookup_attrs_of_lid g lid in + match uu___ with + | FStar_Pervasives_Native.Some attrs -> + FStar_Compiler_Util.find_map attrs is_extract_as_attr + | FStar_Pervasives_Native.None -> FStar_Pervasives_Native.None let rec (norm : FStar_TypeChecker_Cfg.cfg -> env -> stack -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) @@ -3826,10 +3863,33 @@ and (do_unfold_fv : fun t0 -> fun qninfo -> fun f -> - let uu___ = + let defn uu___ = FStar_TypeChecker_Env.lookup_definition_qninfo cfg.FStar_TypeChecker_Cfg.delta_level (f.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v qninfo in + let defn1 uu___ = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + match qninfo with + | FStar_Pervasives_Native.Some + (FStar_Pervasives.Inr (se, FStar_Pervasives_Native.None), + uu___1) + when + FStar_TypeChecker_Env.visible_with + cfg.FStar_TypeChecker_Cfg.delta_level + se.FStar_Syntax_Syntax.sigquals + -> + let uu___2 = + FStar_Compiler_Util.find_map + se.FStar_Syntax_Syntax.sigattrs is_extract_as_attr in + (match uu___2 with + | FStar_Pervasives_Native.Some impl -> + FStar_Pervasives_Native.Some ([], impl) + | FStar_Pervasives_Native.None -> defn ()) + | uu___1 -> defn () + else defn () in + let uu___ = defn1 () in match uu___ with | FStar_Pervasives_Native.None -> (FStar_TypeChecker_Cfg.log_unfolding cfg @@ -9154,7 +9214,7 @@ let (get_n_binders : FStar_Syntax_Syntax.term -> (FStar_Syntax_Syntax.binder Prims.list * FStar_Syntax_Syntax.comp)) = fun env1 -> fun n -> fun t -> get_n_binders' env1 [] n t -let (uu___3455 : unit) = +let (uu___3497 : unit) = FStar_Compiler_Effect.op_Colon_Equals __get_n_binders get_n_binders' let (maybe_unfold_head_fv : FStar_TypeChecker_Env.env -> diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst index fc2f7529713..8554a846f6d 100644 --- a/src/extraction/FStar.Extraction.ML.Modul.fst +++ b/src/extraction/FStar.Extraction.ML.Modul.fst @@ -751,6 +751,14 @@ let mark_sigelt_erased (se:sigelt) (g:uenv) : uenv = List.fold_right (fun lid g -> extend_erased_fv g (S.lid_as_fv lid None)) (U.lids_of_sigelt se) g +// If the definition has an [@@extract_as impl] attribute, +// replace the lbdef with the specified impl: +let fixup_sigelt_extract_as se = + match se.sigel, find_map se.sigattrs N.is_extract_as_attr with + | Sig_let {lids; lbs=(_, [lb])}, Some impl -> + {se with sigel = Sig_let {lids; lbs=(true, [{lb with lbdef = impl}])}} + | _ -> se + (* The top-level extraction of a sigelt to an interface *) let rec extract_sigelt_iface (g:uenv) (se:sigelt) : uenv & iface = if sigelt_has_noextract se then @@ -758,6 +766,7 @@ let rec extract_sigelt_iface (g:uenv) (se:sigelt) : uenv & iface = g, empty_iface else let se = karamel_fixup_qual se in + let se = fixup_sigelt_extract_as se in match se.sigel with | Sig_bundle _ @@ -997,6 +1006,7 @@ let rec extract_sig (g:env_t) (se:sigelt) : env_t & list mlmodule1 = g, [] else begin let se = karamel_fixup_qual se in + let se = fixup_sigelt_extract_as se in match se.sigel with | Sig_bundle _ diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index a091a3d7748..cd393c8e02b 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/src/parser/FStar.Parser.Const.fst @@ -598,4 +598,5 @@ let tref_lid = p2l ["FStar"; "Stubs"; "Tactics"; "Types"; "tref"] let document_lid = p2l ["FStar"; "Stubs"; "Pprint"; "document"] let issue_lid = p2l ["FStar"; "Issue"; "issue"] +let extract_as_lid = p2l ["FStar"; "Pervasives"; "extract_as"] let extract_as_impure_effect_lid = p2l ["FStar"; "Pervasives"; "extract_as_impure_effect"] diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index 0446758b780..891f7bef53e 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -768,15 +768,15 @@ let num_datacon_non_injective_ty_params env lid = if injective_type_params then Some 0 else Some num_ty_params | _ -> None +let visible_with delta_levels quals = + delta_levels |> BU.for_some (fun dl -> quals |> BU.for_some (visible_at dl)) + let lookup_definition_qninfo_aux rec_ok delta_levels lid (qninfo : qninfo) = - let visible quals = - delta_levels |> BU.for_some (fun dl -> quals |> BU.for_some (visible_at dl)) - in match qninfo with | Some (Inr (se, None), _) -> begin match se.sigel with | Sig_let {lbs=(is_rec, lbs)} - when visible se.sigquals + when visible_with delta_levels se.sigquals && (not is_rec || rec_ok) -> BU.find_map lbs (fun lb -> let fv = right lb.lbname in diff --git a/src/typechecker/FStar.TypeChecker.Env.fsti b/src/typechecker/FStar.TypeChecker.Env.fsti index 59d71f23b1a..c3d130e6933 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fsti +++ b/src/typechecker/FStar.TypeChecker.Env.fsti @@ -330,6 +330,7 @@ val lookup_and_inst_datacon: env -> universes -> lident -> typ (* the boolean tells if the lident was actually a inductive *) val datacons_of_typ : env -> lident -> (bool & list lident) val typ_of_datacon : env -> lident -> lident +val visible_with : list delta_level -> list qualifier -> bool val lookup_definition_qninfo : list delta_level -> lident -> qninfo -> option (univ_names & term) val lookup_definition : list delta_level -> env -> lident -> option (univ_names & term) val lookup_nonrec_definition: list delta_level -> env -> lident -> option (univ_names & term) diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index 2c61dba7fb3..44f488eda83 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/src/typechecker/FStar.TypeChecker.Normalize.fst @@ -863,6 +863,19 @@ let is_forall_const cfg (phi : term) : option term = | _ -> None +let is_extract_as_attr (attr: attribute) : option term = + let head, args = head_and_args attr in + match (Subst.compress head).n, args with + | Tm_uinst({n=Tm_fvar fv}, [u]), [_; (t, _)] + when Syntax.fv_eq_lid fv PC.extract_as_lid -> + Some t + | _ -> None + +let has_extract_as_attr (g: Env.env) (lid: I.lid) : option term = + match Env.lookup_attrs_of_lid g lid with + | Some attrs -> find_map attrs is_extract_as_attr + | None -> None + (* GM: Please consider this function private outside of this recursive * group, and call `normalize` instead. `normalize` will print timing * information when --debug NormTop is given, which makes it a @@ -1498,7 +1511,20 @@ let rec norm : cfg -> env -> stack -> term -> term = (* NOTE: we do not need any environment here, since an fv does not * have any free indices. Hence, we use empty_env as environment when needed. *) and do_unfold_fv (cfg:Cfg.cfg) stack (t0:term) (qninfo : qninfo) (f:fv) : term = - match Env.lookup_definition_qninfo cfg.delta_level f.fv_name.v qninfo with + // Second, try to unfold to the definition itself. + let defn () = Env.lookup_definition_qninfo cfg.delta_level f.fv_name.v qninfo in + // First, try to unfold to the implementation specified in the extract_as attribute (when doing extraction) + let defn () = + if cfg.steps.for_extraction then + match qninfo with + | Some (Inr (se, None), _) when Env.visible_with cfg.delta_level se.sigquals -> + (match find_map se.sigattrs is_extract_as_attr with + | Some impl -> Some ([], impl) + | None -> defn ()) + | _ -> defn () + else + defn () in + match defn () with | None -> log_unfolding cfg (fun () -> BU.print2 " >> No definition found for %s (delta_level = %s)\n" diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fsti b/src/typechecker/FStar.TypeChecker.Normalize.fsti index 8a065847407..c81195059ea 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fsti +++ b/src/typechecker/FStar.TypeChecker.Normalize.fsti @@ -66,6 +66,9 @@ val remove_uvar_solutions: Env.env -> term -> term val unfold_head_once: Env.env -> term -> option term val unembed_binder_knot : ref (option (FStar.Syntax.Embeddings.embedding binder)) +val is_extract_as_attr : attribute -> option term +val has_extract_as_attr : Env.env -> Ident.lid -> option term + val reflection_env_hook : ref (option Env.env) (* Destructs the term as an arrow type and returns its binders and diff --git a/tests/extraction/ExtractAs.fst b/tests/extraction/ExtractAs.fst new file mode 100644 index 00000000000..5df61055da8 --- /dev/null +++ b/tests/extraction/ExtractAs.fst @@ -0,0 +1,17 @@ +module ExtractAs +let fail_unless (b: bool) = if b then "ok" else magic () + +// Test that extract_as works when extracting the definition itself. + +[@@extract_as (fun x -> x + 10)] +let frob y = 2 + y + +let _ = fail_unless (frob 1 = 11) + +// Test that extract_as works when inlining the definition. + +inline_for_extraction noextract [@@extract_as (fun x -> x + 10)] +let bar_2 y = 2 + y +let bar z = bar_2 z + +let _ = fail_unless (bar 1 = 11) diff --git a/tests/extraction/Makefile b/tests/extraction/Makefile index 84952c9372c..9d601ca8897 100644 --- a/tests/extraction/Makefile +++ b/tests/extraction/Makefile @@ -2,7 +2,7 @@ FSTAR_EXAMPLES=$(realpath ../../examples) include $(FSTAR_EXAMPLES)/Makefile.include include $(FSTAR_ULIB)/ml/Makefile.include -all: inline_let all_cmi Eta_expand.test Div.test +all: inline_let all_cmi Eta_expand.test Div.test ExtractAs.test %.exe: %.fst | out $(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml $< diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst index 42987e0cdc6..86a91a47232 100644 --- a/ulib/FStar.Pervasives.fst +++ b/ulib/FStar.Pervasives.fst @@ -185,6 +185,8 @@ let primitive_extraction = () let extract_as_impure_effect = () +let extract_as _ = () + let strictly_positive = () let unused = () diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index 6bb8b1076a3..8d6459e1b8f 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -1146,6 +1146,20 @@ val primitive_extraction : unit *) val extract_as_impure_effect : unit +(** Replaces the annotated definition + by the specified implementation during extraction. + There are no checks whether the implementation + has the same semantics, or even the same type. + + For example, if you have: + + [@@extract_as (fun (x: nat) -> "not a number")] + let add_one (x: nat) : nat = x + 42 + + Then `add_one` will extract to `let add_one x = "not a number"`, + and most likely cause the extracted program to crash. + *) +val extract_as (#t: Type u#a) (impl: t) : unit (** A binder in a definition/declaration may optionally be annotated as strictly_positive When the let definition is used in a data constructor type in an inductive