aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/pcic.ml4
-rw-r--r--contrib/correctness/pred.ml4
-rw-r--r--contrib/correctness/preuves.v7
-rw-r--r--contrib/correctness/ptactic.ml12
-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
10 files changed, 127 insertions, 33 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 170a56b28a..cf233a9889 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -89,8 +89,8 @@ let sig_n n =
mind_entry_consnames = [ cname ];
mind_entry_lc = [ lc ] } ] }
-let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "pair",0),1)
-let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "exist",0),1)
+let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1)
+let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1)
let tuple_ref dep n =
if n = 2 & not dep then
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
index d6f9e0e720..c71c91f931 100644
--- a/contrib/correctness/pred.ml
+++ b/contrib/correctness/pred.ml
@@ -29,9 +29,9 @@ let is_eta_redex bl al =
Invalid_argument("List.for_all2") -> false
let rec red = function
- CC_letin (dep, ty, bl, e1, e2) ->
+ | CC_letin (dep, ty, bl, e1, e2) ->
begin match red e2 with
- CC_tuple (false,tl,al) ->
+ | CC_tuple (false,tl,al) ->
if is_eta_redex bl al then
red e1
else
diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v
index 22eccbdbaa..730a25fd48 100644
--- a/contrib/correctness/preuves.v
+++ b/contrib/correctness/preuves.v
@@ -28,10 +28,15 @@ Save.
Global Variable i : Z ref.
Debug on.
-Correctness assign1 { `0 <= i` } begin i := !i + 1 end { `0 < i` }.
+Correctness assign1 { `0 <= i` } (i := !i + 1) { `0 < i` }.
+Omega.
+Save.
(**********************************************************************)
+Global Variable i : Z ref.
+Debug on.
+Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }.
(**********************************************************************)
Correctness echange
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index b8ac085319..45ab72c385 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -105,16 +105,16 @@ let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0)
(* ["(well_founded nat lt)"] *)
let wf_nat_pattern =
PApp (PRef well_founded, [| PRef nat; PRef lt |])
-(* ["((well_founded Z (Zwf ?))"] *)
+(* ["((well_founded Z (Zwf ?1))"] *)
let wf_z_pattern =
let zwf = ConstRef (coq_constant ["correctness";"Zwf"] "Zwf") in
- PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta None |]) |])
-(* ["(and ? ?)"] *)
+ PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta (Some 1) |]) |])
+(* ["(and ?1 ?2)"] *)
let and_pattern =
- PApp (PRef and_, [| PMeta None; PMeta None |])
-(* ["(eq ? ? ?)"] *)
+ PApp (PRef and_, [| PMeta (Some 1); PMeta (Some 2) |])
+(* ["(eq ?1 ?2 ?3)"] *)
let eq_pattern =
- PApp (PRef eq, [| PMeta None; PMeta None; PMeta None |])
+ PApp (PRef eq, [| PMeta (Some 1); PMeta (Some 2); PMeta (Some 3) |])
(* loop_ids: remove loop<i> hypotheses from the context, and rewrite
* using Variant<i> hypotheses when needed. *)
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 472cee1af8..c4c62b3cbe 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 9e87cc9aca..b0bb1ad3a9 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 de77687fbe..4b04c4dec1 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 b68d4a954a..af931b6486 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 a7b96d8e90..2d0518d92a 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 1a0cfec0c7..74d7510514 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.25.1) at 2026-04-23 10:45:22 +0000