From 53ab508daf08418fa7e4904b3d0ba3df689275ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 16:10:28 -0700 Subject: [PATCH 1/3] Extraction: not extracting tactics unless backend is Plugin --- src/extraction/FStar.Extraction.ML.Modul.fst | 24 ++++++++++++++++---- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst index e9bc4f85d8e..085fe0a0e34 100644 --- a/src/extraction/FStar.Extraction.ML.Modul.fst +++ b/src/extraction/FStar.Extraction.ML.Modul.fst @@ -998,10 +998,18 @@ let extract_bundle env se = | _ -> failwith "Unexpected signature element" -let lb_irrelevant (g:env_t) (lb:letbinding) : bool = - Env.non_informative (tcenv_of_uenv g) lb.lbtyp && // result type is non informative - not (Term.is_arity g lb.lbtyp) && // but not a type definition - U.is_pure_or_ghost_effect lb.lbeff // and not top-level effectful +let lb_is_irrelevant (g:env_t) (lb:letbinding) : bool = + Env.non_informative (tcenv_of_uenv g) lb.lbtyp && // result type is non informative + not (Term.is_arity g lb.lbtyp) && // but not a type definition + U.is_pure_or_ghost_effect lb.lbeff // and not top-level effectful + +let lb_is_tactic (g:env_t) (lb:letbinding) : bool = + if U.is_pure_effect lb.lbeff then // not top-level effectful + let bs, c = U.arrow_formals_comp_ln lb.lbtyp in + let c_eff_name = c |> U.comp_effect_name |> Env.norm_eff_name (tcenv_of_uenv g) in + lid_equals c_eff_name PC.effect_TAC_lid + else + false (*****************************************************************************) (* Extracting the top-level definitions in a module *) @@ -1039,7 +1047,13 @@ let rec extract_sig (g:env_t) (se:sigelt) : env_t & list mlmodule1 = g, [] (* Ignore all non-informative sigelts *) - | Sig_let {lbs=(_, lbs)} when List.for_all (lb_irrelevant g) lbs -> + | Sig_let {lbs=(_, lbs)} when List.for_all (lb_is_irrelevant g) lbs -> + g, [] + + (* Ignore tactics whenever we're not extracting plugins *) + | Sig_let {lbs=(_, lbs)} + when Options.codegen () <> Some (Options.Plugin) && + List.for_all (lb_is_tactic g) lbs -> g, [] | Sig_declare_typ {lid; us=univs; t} when Term.is_arity g t -> //lid is a type From 1d7dfefae8aceb9d526143f85d210c06433b603f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 16:28:52 -0700 Subject: [PATCH 2/3] Syntax.Util: remove unused function --- src/syntax/FStar.Syntax.Util.fst | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst index 299cc0c6ec2..85c56cda831 100644 --- a/src/syntax/FStar.Syntax.Util.fst +++ b/src/syntax/FStar.Syntax.Util.fst @@ -951,15 +951,6 @@ let is_fstar_tactics_by_tactic t = | Tm_fvar fv -> fv_eq_lid fv PC.by_tactic_lid | _ -> false -let is_builtin_tactic md = - let path = Ident.path_of_lid md in - if List.length(path) > 2 then - match fst (List.splitAt 2 path) with - | ["FStar"; "Tactics"] - | ["FStar"; "Reflection"] -> true - | _ -> false - else false - (********************************************************************************) (*********************** Constructors of common terms **************************) (********************************************************************************) From 9a4bb7d12ce0b84ac9657105072b52d54724baba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 16:32:29 -0700 Subject: [PATCH 3/3] snap --- .../generated/FStar_Extraction_ML_Modul.ml | 35 +++++++++++++++++-- .../fstar-lib/generated/FStar_Syntax_Util.ml | 13 ------- 2 files changed, 32 insertions(+), 16 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml index d3af331777d..ffd839d8e47 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml @@ -2180,7 +2180,8 @@ let (extract_bundle : (env2, uu___5))) | uu___ -> FStar_Compiler_Effect.failwith "Unexpected signature element" -let (lb_irrelevant : env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = +let (lb_is_irrelevant : + env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = fun g -> fun lb -> ((let uu___ = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in @@ -2193,6 +2194,25 @@ let (lb_irrelevant : env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = && (FStar_Syntax_Util.is_pure_or_ghost_effect lb.FStar_Syntax_Syntax.lbeff) +let (lb_is_tactic : env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = + fun g -> + fun lb -> + let uu___ = + FStar_Syntax_Util.is_pure_effect lb.FStar_Syntax_Syntax.lbeff in + if uu___ + then + let uu___1 = + FStar_Syntax_Util.arrow_formals_comp_ln + lb.FStar_Syntax_Syntax.lbtyp in + match uu___1 with + | (bs, c) -> + let c_eff_name = + let uu___2 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in + FStar_TypeChecker_Env.norm_eff_name uu___2 + (FStar_Syntax_Util.comp_effect_name c) in + FStar_Ident.lid_equals c_eff_name + FStar_Parser_Const.effect_TAC_lid + else false let rec (extract_sig : env_t -> FStar_Syntax_Syntax.sigelt -> @@ -2264,8 +2284,17 @@ let rec (extract_sig : | FStar_Syntax_Syntax.Sig_let { FStar_Syntax_Syntax.lbs1 = (uu___5, lbs); FStar_Syntax_Syntax.lids1 = uu___6;_} - when FStar_Compiler_List.for_all (lb_irrelevant g) lbs -> - (g, []) + when FStar_Compiler_List.for_all (lb_is_irrelevant g) lbs + -> (g, []) + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (uu___5, lbs); + FStar_Syntax_Syntax.lids1 = uu___6;_} + when + (let uu___7 = FStar_Options.codegen () in + uu___7 <> + (FStar_Pervasives_Native.Some FStar_Options.Plugin)) + && (FStar_Compiler_List.for_all (lb_is_tactic g) lbs) + -> (g, []) | FStar_Syntax_Syntax.Sig_declare_typ { FStar_Syntax_Syntax.lid2 = lid; FStar_Syntax_Syntax.us2 = univs; diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml index 1d8e82e9256..9f7bb809e9a 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml @@ -1945,19 +1945,6 @@ let (is_fstar_tactics_by_tactic : FStar_Syntax_Syntax.term -> Prims.bool) = | FStar_Syntax_Syntax.Tm_fvar fv -> FStar_Syntax_Syntax.fv_eq_lid fv FStar_Parser_Const.by_tactic_lid | uu___1 -> false -let (is_builtin_tactic : FStar_Ident.lident -> Prims.bool) = - fun md -> - let path = FStar_Ident.path_of_lid md in - if (FStar_Compiler_List.length path) > (Prims.of_int (2)) - then - let uu___ = - let uu___1 = FStar_Compiler_List.splitAt (Prims.of_int (2)) path in - FStar_Pervasives_Native.fst uu___1 in - match uu___ with - | "FStar"::"Tactics"::[] -> true - | "FStar"::"Reflection"::[] -> true - | uu___1 -> false - else false let (ktype : FStar_Syntax_Syntax.term) = FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_type FStar_Syntax_Syntax.U_unknown)