aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/extraction/common.ml41
-rw-r--r--contrib/extraction/common.mli6
-rw-r--r--contrib/extraction/extract_env.ml112
-rw-r--r--contrib/extraction/mlutil.ml19
-rw-r--r--contrib/extraction/ocaml.ml10
-rw-r--r--contrib/extraction/test/Makefile1
-rw-r--r--contrib/extraction/test/custom/Reals.v6
7 files changed, 145 insertions, 50 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 637a30bd7..9b111bbf4 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -16,6 +16,7 @@ open Table
open Mlutil
open Ocaml
open Nametab
+open Util
(*s Modules considerations *)
@@ -27,11 +28,43 @@ let sp_of_r r = match r with
| ConstructRef ((sp,_),_) -> sp
| _ -> assert false
-let module_of_r r =
- snd (split_dirpath (dirpath (sp_of_r r)))
+let qualid_of_dirpath d =
+ let dir,id = split_dirpath d in
+ make_qualid dir id
+
+(* [long_module r] computes the dirpath of the module of the global
+ reference [r]. The difficulty comes from the possible section names
+ at the beginning of the dirpath (due to Remark). *)
+
+let long_module r =
+ let rec check_module d =
+ try
+ locate_loaded_library (qualid_of_dirpath d)
+ with Not_found ->
+ let d' =
+ try
+ dirpath_prefix d
+ with _ -> errorlabstrm "long_module_message"
+ [< 'sTR "Can't find the module of"; 'sPC;
+ Printer.pr_global r >]
+ in check_module d'
+ in check_module (dirpath (sp_of_r r))
+
+(* From a valid module dirpath [d], we check if [r] belongs to this module. *)
+
+let is_long_module d r =
+ let dir = repr_dirpath d
+ and dir' = repr_dirpath (dirpath (sp_of_r r)) in
+ let l = List.length dir
+ and l' = List.length dir' in
+ if l' < l then false
+ else dir = snd (list_chop (l'-l) dir')
+
+let short_module r =
+ snd (split_dirpath (long_module r))
let module_option r =
- let m = module_of_r r in
+ let m = short_module r in
if Some m = !current_module then ""
else (String.capitalize (string_of_id m)) ^ "."
@@ -42,7 +75,7 @@ let check_ml r d =
with Not_found -> d
else d
-(*s tables of global renamings *)
+(*s Tables of global renamings *)
let keywords = ref Idset.empty
let global_ids = ref Idset.empty
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index c9b41a4ef..e196fd852 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -17,7 +17,11 @@ module ToplevelPp : Mlpp
val sp_of_r : global_reference -> section_path
-val module_of_r : global_reference -> identifier
+val long_module : global_reference -> dir_path
+
+val is_long_module : dir_path -> global_reference -> bool
+
+val short_module : global_reference -> identifier
val extract_to_file :
string -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 77e20c785..8ce82a45b 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -22,18 +22,62 @@ open Nametab
open Vernacinterp
open Common
+(*s Auxiliary functions dealing with modules. *)
+
+module Dirset =
+ Set.Make(struct type t = dir_path let compare = compare end)
+
+let module_of_id m =
+ try
+ locate_loaded_library (make_short_qualid m)
+ with Not_found ->
+ errorlabstrm "module_message"
+ [< 'sTR "Module"; 'sPC;pr_id m; 'sPC; 'sTR "not found." >]
+
+(*s Module name clash verification. *)
+
+let clash_error sn n1 n2 =
+ errorlabstrm "clash_module_message"
+ [< 'sTR ("There are two Coq modules with ML name " ^ sn ^" :");
+ 'fNL ; 'sTR (" "^(string_of_dirpath n1)) ;
+ 'fNL ; 'sTR (" "^(string_of_dirpath n2)) ;
+ 'fNL ; 'sTR "This is not allowed in ML. Please do some renaming first." >]
+
+let check_r m sm r =
+ let rm = String.capitalize (string_of_id (short_module r)) in
+ if rm = sm && not (is_long_module m r)
+ then clash_error sm m (long_module r)
+
+let check_decl m sm = function
+ | Dglob (r,_) -> check_r m sm r
+ | Dabbrev (r,_,_) -> check_r m sm r
+ | Dtype ((_,r,_)::_, _) -> check_r m sm r
+ | Dtype ([],_) -> ()
+ | Dcustom (r,_) -> check_r m sm r
+
+(* [check_one_module m l] checks that no module names in [l] clashes with [m]. *)
+
+let check_one_module m l =
+ let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in
+ List.iter (check_decl m sm) l
+
+(* [check_modules m] checks if there are conflicts within the set [m] of modules dirpath. *)
+
+let check_modules m =
+ let map = ref Idmap.empty in
+ Dirset.iter
+ (fun m ->
+ let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in
+ let idm = id_of_string sm in
+ try
+ let m' = Idmap.find idm !map in clash_error sm m m'
+ with Not_found -> map := Idmap.add idm m !map) m
+
(*s [extract_module m] returns all the global reference declared
- in a module. This is done by traversing the segment of module [M].
+ in a module. This is done by traversing the segment of module [m].
We just keep constants and inductives. *)
let extract_module m =
- let m =
- try
- Nametab.locate_loaded_library (Nametab.make_short_qualid m)
- with Not_found ->
- errorlabstrm "module_message"
- [< 'sTR "Module"; 'sPC;pr_id m; 'sPC; 'sTR "not found." >]
- in
let seg = Library.module_segment (Some m) in
let get_reference = function
| sp, Leaf o ->
@@ -59,11 +103,13 @@ let extract_module m =
type extracted_env = {
mutable visited : Refset.t;
mutable to_extract : global_reference list;
- mutable modules : Idset.t
+ mutable modules : Dirset.t
}
let empty () =
- { visited = ml_extractions (); to_extract = []; modules = Idset.empty }
+ { visited = ml_extractions ();
+ to_extract = [];
+ modules = Dirset.empty }
let rec visit_reference m eenv r =
let r' = match r with
@@ -76,12 +122,10 @@ let rec visit_reference m eenv r =
and in module extraction *)
eenv.visited <- Refset.add r' eenv.visited;
if m then begin
- let m_name = module_of_r r' in
- if not (Idset.mem m_name eenv.modules) then begin
- eenv.modules <- Idset.add m_name eenv.modules;
- try (* HACK temporaire pour eviter les m_name qui sont des sections *)
- List.iter (visit_reference m eenv) (extract_module m_name)
- with _ -> ()
+ let m_name = long_module r' in
+ if not (Dirset.mem m_name eenv.modules) then begin
+ eenv.modules <- Dirset.add m_name eenv.modules;
+ List.iter (visit_reference m eenv) (extract_module m_name)
end
end;
visit_decl m eenv (extract_declaration r);
@@ -141,7 +185,7 @@ let extract_env rl =
let modules_extract_env m =
let eenv = empty () in
- eenv.modules <- Idset.singleton m;
+ eenv.modules <- Dirset.singleton m;
List.iter (visit_reference true eenv) (extract_module m);
eenv.modules, List.rev eenv.to_extract
@@ -158,7 +202,6 @@ let local_optimize refs =
let prm =
{ lang = "ocaml" ; toplevel = true;
mod_name = None; to_appear = refs} in
- clear_singletons ();
optimize prm (decl_of_refs refs)
let print_user_extract r =
@@ -223,7 +266,6 @@ let _ =
(function
| VARG_STRING lang :: VARG_STRING f :: vl ->
(fun () ->
- clear_singletons ();
let refs = refs_of_vargl vl in
let prm = {lang=lang;
toplevel=false;
@@ -239,11 +281,11 @@ let _ =
\verb!Extraction Module! [M]. *)
let decl_in_m m = function
- | Dglob (r,_) -> m = module_of_r r
- | Dabbrev (r,_,_) -> m = module_of_r r
- | Dtype ((_,r,_)::_, _) -> m = module_of_r r
+ | Dglob (r,_) -> is_long_module m r
+ | Dabbrev (r,_,_) -> is_long_module m r
+ | Dtype ((_,r,_)::_, _) -> is_long_module m r
| Dtype ([],_) -> false
- | Dcustom (r,_) -> m = module_of_r r
+ | Dcustom (r,_) -> is_long_module m r
let file_suffix = function
| "ocaml" -> ".ml"
@@ -255,21 +297,22 @@ let _ =
(function
| [VARG_STRING lang; VARG_IDENTIFIER m] ->
(fun () ->
- clear_singletons ();
+ let dir_m = module_of_id m in
let f = (String.uncapitalize (string_of_id m))
^ (file_suffix lang) in
let prm = {lang=lang;
toplevel=false;
mod_name= Some m;
to_appear= []} in
- let rl = extract_module m in
+ let rl = extract_module dir_m in
let decls = optimize prm (decl_of_refs rl) in
let decls = add_ml_decls prm decls in
- let decls = List.filter (decl_in_m m) decls in
+ check_one_module dir_m decls;
+ let decls = List.filter (decl_in_m dir_m) decls in
extract_to_file f prm decls)
| _ -> assert false)
-(*s Recusrive Extraction of all the modules [M] depends on.
+(*s Recursive Extraction of all the modules [M] depends on.
The vernacular command is \verb!Recursive Extraction Module! [M]. *)
let _ =
@@ -277,23 +320,26 @@ let _ =
(function
| [VARG_STRING lang; VARG_IDENTIFIER m] ->
(fun () ->
- clear_singletons ();
- let modules,refs = modules_extract_env m in
+ let dir_m = module_of_id m in
+ let modules,refs =
+ modules_extract_env dir_m in
+ check_modules modules;
let dummy_prm = {lang=lang;
toplevel=false;
mod_name= Some m;
to_appear= []} in
let decls = optimize dummy_prm (decl_of_refs refs) in
let decls = add_ml_decls dummy_prm decls in
- Idset.iter
+ Dirset.iter
(fun m ->
- let f = (String.uncapitalize (string_of_id m))
+ let short_m = snd (split_dirpath m) in
+ let f = (String.uncapitalize (string_of_id short_m))
^ (file_suffix lang) in
let prm = {lang=lang;
toplevel=false;
- mod_name= Some m;
+ mod_name= Some short_m;
to_appear= []} in
let decls = List.filter (decl_in_m m) decls in
- extract_to_file f prm decls)
+ if decls <> [] then extract_to_file f prm decls)
modules)
| _ -> assert false)
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 0ae088384..32ad5053b 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -616,7 +616,7 @@ let is_exn = function
| MLexn _ -> true
| _ -> false
-let rec optimize prm = function
+let rec optim prm = function
| [] ->
[]
| ( Dabbrev (r,_,Tarity) |
@@ -624,8 +624,8 @@ let rec optimize prm = function
Dglob(r,MLarity) |
Dglob(r,MLprop) ) as d :: l ->
if List.mem r prm.to_appear then
- d :: (optimize prm l)
- else optimize prm l
+ d :: (optim prm l)
+ else optim prm l
| Dglob (r,t) :: l ->
let t = normalize t in
let b = expand (strict_language prm.lang) r t
@@ -644,19 +644,20 @@ let rec optimize prm = function
if not b' &&
(not b || prm.mod_name <> None || List.mem r prm.to_appear) then
let t = optimize_fix t in
- Dglob (r,t) :: (optimize prm l)
+ Dglob (r,t) :: (optim prm l)
else
- optimize prm l
+ optim prm l
| (Dtype ([],_) | Dabbrev _ | Dcustom _) as d :: l ->
- d :: (optimize prm l)
+ d :: (optim prm l)
| Dtype ([ids,r,[r0,[t0]]],false) :: l when not (type_mem r t0) ->
(* Detection of informative singleton. *)
add_singleton r0;
- Dabbrev (r, ids, t0) :: (optimize prm l)
+ Dabbrev (r, ids, t0) :: (optim prm l)
| Dtype(il,b) :: l ->
(* Detection of empty inductives. *)
let l1,l2 = empty_ind il in
- if l2 = [] then l1 @ (optimize prm l)
- else l1 @ (Dtype(l2,b) :: (optimize prm l))
+ if l2 = [] then l1 @ (optim prm l)
+ else l1 @ (Dtype(l2,b) :: (optim prm l))
+let optimize prm l = clear_singletons(); optim prm l
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 391bf7350..778683646 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -35,6 +35,12 @@ let open_par = function true -> string "(" | false -> [< >]
let close_par = function true -> string ")" | false -> [< >]
+let pp_tvar id =
+ let s = string_of_id id in
+ if String.length s < 2 || s.[1]<>'\''
+ then string ("'"^s)
+ else string ("' "^s)
+
let pp_tuple f = function
| [] -> [< >]
| [x] -> f x
@@ -129,7 +135,7 @@ let empty_env () = [], P.globals()
let rec pp_type par t =
let rec pp_rec par = function
| Tvar id ->
- string ("'" ^ string_of_id id)
+ pp_tvar id
| Tapp l ->
(match collapse_type_app l with
| [] -> assert false
@@ -295,7 +301,7 @@ let pp_ast a = hOV 0 (pp_expr false (empty_env ()) [] a)
(*s Pretty-printing of inductive types declaration. *)
let pp_parameters l =
- [< pp_tuple (fun id -> string ("'" ^ string_of_id id)) l; space_if (l<>[]) >]
+ [< pp_tuple pp_tvar l; space_if (l<>[]) >]
let pp_one_inductive (pl,name,cl) =
let pp_constructor (id,l) =
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 1db621f18..90598daa4 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -9,6 +9,7 @@ TOPDIR=../../..
AXIOMSVO:= \
theories/Arith/Arith.vo \
theories/Lists/List.vo \
+theories/Reals/% \
theories/Reals/Rsyntax.vo \
theories/Num/% \
theories/ZArith/Zsyntax.vo
diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v
index d42fe0a53..b817c3600 100644
--- a/contrib/extraction/test/custom/Reals.v
+++ b/contrib/extraction/test/custom/Reals.v
@@ -9,4 +9,8 @@ Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)".
Extract Inlined Constant Rlt => "(<)".
Extract Inlined Constant up => "AddReals.my_ceil".
Extract Inlined Constant total_order_T => "AddReals.total_order_T".
-
+Extract Inlined Constant sqrt => "sqrt".
+Extract Inlined Constant sigma => "(fun l h -> sigma_aux l h (Minus.minus h l))".
+Extract Inlined Constant PI => "3.141593".
+Extract Inlined Constant cos => cos.
+Extract Inlined Constant sin => sin.
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-03 09:50:22 +0000