aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/Extraction.v20
-rw-r--r--contrib/extraction/extract_env.ml38
-rw-r--r--contrib/extraction/mlutil.ml52
-rw-r--r--contrib/extraction/mlutil.mli13
-rw-r--r--contrib/extraction/ocaml.ml5
-rw-r--r--contrib/extraction/ocaml.mli5
6 files changed, 111 insertions, 22 deletions
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 472cee1af..c4c62b3cb 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -6,17 +6,17 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-Declare ML Module "mlutil" "ocaml" "extraction" "extract_env".
-
Grammar vernac vernac : ast :=
extr_constr [ "Extraction" constrarg($c) "." ] ->
[ (Extraction $c) ]
| extr_list [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
[ (ExtractionRec ($LIST $l)) ]
-| extr_list [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] ->
- [ (ExtractionFile $f ($LIST $l)) ]
-| extr_module [ "Extraction" "Module" identarg($m) "." ] ->
- [ (ExtractionModule $m) ]
+| extr_list
+ [ "Extraction" options($o) stringarg($f) ne_qualidarg_list($l) "." ]
+ -> [ (ExtractionFile $o $f ($LIST $l)) ]
+| extr_module
+ [ "Extraction" options($o) "Module" identarg($m) "." ]
+ -> [ (ExtractionModule $o $m) ]
| extract_constant
[ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
@@ -36,4 +36,10 @@ with idorstring_list: List :=
with idorstring : ast :=
ids_ident [ identarg($id) ] -> [ $id ]
-| ids_string [ stringarg($s) ] -> [ $s ].
+| ids_string [ stringarg($s) ] -> [ $s ]
+
+with options : ast :=
+| ext_opt_noopt [ "noopt" ] -> [ (VERNACARGLIST "noopt") ]
+| ext_op_expand [ "expand" "[" ne_qualidarg_list($l) "]" ] ->
+ [ (VERNACARGLIST "expand" ($LIST $l)) ]
+| ext_opt_none [ ] -> [ (VERNACARGLIST "nooption") ].
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 9e87cc9ac..b0bb1ad3a 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -144,16 +144,35 @@ let reference_of_varg = function
(try Nametab.locate q with Not_found -> no_such_reference q)
| _ -> assert false
-let decl_of_vargl vl =
- let rl = List.map reference_of_varg vl in
- List.map extract_declaration (extract_env rl)
+let refs_of_vargl = List.map reference_of_varg
+
+let refs_set_of_list l = List.fold_right Refset.add l Refset.empty
+
+let decl_of_refs refs =
+ List.map extract_declaration (extract_env refs)
let _ =
vinterp_add "ExtractionRec"
(fun vl () ->
- let rl' = decl_of_vargl vl in
+ let rl' = decl_of_refs (refs_of_vargl vl) in
List.iter (fun d -> mSGNL (Pp.pp_decl d)) rl')
+(*s Extraction parameters. *)
+
+let interp_options keep modular = function
+ | [VARG_STRING "noopt"] ->
+ { no_opt = true; modular = modular;
+ to_keep = refs_set_of_list keep; to_expand = Refset.empty }
+ | [VARG_STRING "nooption"] ->
+ { no_opt = false; modular = modular;
+ to_keep = refs_set_of_list keep; to_expand = Refset.empty }
+ | VARG_STRING "expand" :: l ->
+ { no_opt = false; modular = modular;
+ to_keep = refs_set_of_list keep;
+ to_expand = refs_set_of_list (refs_of_vargl l) }
+ | _ ->
+ assert false
+
(*s Extraction to a file (necessarily recursive).
The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
We just call [extract_to_file] on the saturated environment. *)
@@ -161,8 +180,10 @@ let _ =
let _ =
vinterp_add "ExtractionFile"
(function
- | VARG_STRING f :: vl ->
- (fun () -> Ocaml.extract_to_file f false (decl_of_vargl vl))
+ | VARG_VARGLIST o :: VARG_STRING f :: vl ->
+ let refs = refs_of_vargl vl in
+ let prm = interp_options refs false o in
+ (fun () -> Ocaml.extract_to_file f prm (decl_of_refs refs))
| _ -> assert false)
(*s Extraction of a module. The vernacular command is \verb!Extraction Module!
@@ -190,10 +211,11 @@ let extract_module m =
let _ =
vinterp_add "ExtractionModule"
(function
- | [VARG_IDENTIFIER m] ->
+ | [VARG_VARGLIST o; VARG_IDENTIFIER m] ->
(fun () ->
let m = Names.string_of_id m in
Ocaml.current_module := m;
let f = (String.uncapitalize m) ^ ".ml" in
- Ocaml.extract_to_file f true (extract_module m))
+ let prm = interp_options [] true o in
+ Ocaml.extract_to_file f prm (extract_module m))
| _ -> assert false)
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index de77687fb..4b04c4dec 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -195,11 +195,61 @@ let uncurrify_decl = function
| d -> d
-(*s Table for direct ML extractions. *)
+(*s Optimization. *)
module Refset =
Set.Make(struct type t = global_reference let compare = compare end)
+type extraction_params = {
+ modular : bool; (* modular extraction *)
+ no_opt : bool; (* no optimization at all *)
+ to_keep : Refset.t; (* globals to keep *)
+ to_expand : Refset.t; (* globals to expand *)
+}
+
+let ml_subst_glob r m =
+ let rec substrec = function
+ | MLglob r' as t -> if r = r' then m else t
+ | t -> ast_map substrec t
+ in
+ substrec
+
+let expand r m = function
+ | Dglob(r',t') -> Dglob(r', ml_subst_glob r m t')
+ | d -> d
+
+let normalize = betared_ast
+
+let keep prm r t' = true
+ (* prm.no_opt || Refset.mem r prm.to_keep *)
+
+let warning_expansion r =
+ wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
+ Printer.pr_global r; 'sPC; 'sTR "is expanded." >])
+
+let rec optimize prm = function
+ | [] ->
+ []
+ | (Dtype _ | Dabbrev _) as d :: l ->
+ d :: (optimize prm l)
+ (*i
+ | Dglob(id,(MLexn _ as t)) as d :: l ->
+ let l' = List.map (expand (id,t)) l in optimize prm l'
+ i*)
+ | [ Dglob(r,t) ] ->
+ let t' = normalize t in [ Dglob(r,t') ]
+ | Dglob(r,t) as d :: l ->
+ let t' = normalize t in
+ if keep prm r t' then
+ (Dglob(r,t')) :: (optimize prm l)
+ else begin
+ warning_expansion r;
+ let l' = List.map (expand r t') l in
+ optimize prm l'
+ end
+
+(*s Table for direct ML extractions. *)
+
module Refmap =
Map.Make(struct type t = global_reference let compare = compare end)
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index b68d4a954..af931b648 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -39,10 +39,21 @@ val betared_decl : ml_decl -> ml_decl
val uncurrify_ast : ml_ast -> ml_ast
val uncurrify_decl : ml_decl -> ml_decl
-(*s Table for direct extractions to ML values. *)
+(*s Optimization. *)
module Refset : Set.S with type elt = global_reference
+type extraction_params = {
+ modular : bool; (* modular extraction *)
+ no_opt : bool; (* no optimization at all *)
+ to_keep : Refset.t; (* globals to keep *)
+ to_expand : Refset.t; (* globals to expand *)
+}
+
+val optimize : extraction_params -> ml_decl list -> ml_decl list
+
+(*s Table for direct extractions to ML values. *)
+
val is_ml_extraction : global_reference -> bool
val find_ml_extraction : global_reference -> string
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index a7b96d8e9..2d0518d92 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -438,8 +438,9 @@ let ocaml_preamble () =
'sTR "type arity = unit"; 'fNL;
'sTR "let arity = ()"; 'fNL; 'fNL >]
-let extract_to_file f modular decls =
- let pp_decl = if modular then ModularPp.pp_decl else MonoPp.pp_decl in
+let extract_to_file f prm decls =
+ let decls = optimize prm decls in
+ let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in
let cout = open_out f in
let ft = Pp_control.with_output_to cout in
pP_with ft (hV 0 (ocaml_preamble ()));
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 1a0cfec0c..74d751051 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -13,12 +13,11 @@
declarations to a file. *)
open Miniml
+open Mlutil
module Make : functor(P : Mlpp_param) -> Mlpp
-(* The boolean indicates if the extraction is modular. *)
-
val current_module : string ref
-val extract_to_file : string -> bool -> ml_decl list -> unit
+val extract_to_file : string -> extraction_params -> ml_decl list -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:14:22 +0000