aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/common.ml754
-rw-r--r--contrib/extraction/common.mli48
-rw-r--r--contrib/extraction/extract_env.ml266
-rw-r--r--contrib/extraction/extract_env.mli6
-rw-r--r--contrib/extraction/extraction.ml35
-rw-r--r--contrib/extraction/extraction.mli10
-rw-r--r--contrib/extraction/g_extraction.ml47
-rw-r--r--contrib/extraction/haskell.ml90
-rw-r--r--contrib/extraction/haskell.mli10
-rw-r--r--contrib/extraction/miniml.mli53
-rw-r--r--contrib/extraction/modutil.ml118
-rw-r--r--contrib/extraction/modutil.mli20
-rw-r--r--contrib/extraction/ocaml.ml534
-rw-r--r--contrib/extraction/ocaml.mli44
-rw-r--r--contrib/extraction/scheme.ml55
-rw-r--r--contrib/extraction/scheme.mli18
-rw-r--r--contrib/extraction/table.ml169
-rw-r--r--contrib/extraction/table.mli34
18 files changed, 1179 insertions, 1092 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 6db146b1e..855990d25 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -17,42 +17,218 @@ open Nameops
open Libnames
open Table
open Miniml
+open Mlutil
open Modutil
-open Ocaml
+open Mod_subst
-(*S Renamings. *)
+(*s Some pretty-print utility functions. *)
+
+let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+
+let pp_apply st par args = match args with
+ | [] -> st
+ | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
+
+let pr_binding = function
+ | [] -> mt ()
+ | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+
+let fnl2 () = fnl () ++ fnl ()
+
+let space_if = function true -> str " " | false -> mt ()
+
+let sec_space_if = function true -> spc () | false -> mt ()
+
+let is_digit = function
+ | '0'..'9' -> true
+ | _ -> false
+
+let begins_with_CoqXX s =
+ let n = String.length s in
+ n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
+ let i = ref 3 in
+ try while !i < n do
+ if s.[!i] = '_' then i:=n (*Stop*)
+ else if is_digit s.[!i] then incr i
+ else raise Not_found
+ done; true
+ with Not_found -> false
+
+let unquote s =
+ if lang () <> Scheme then s
+ else
+ let s = String.copy s in
+ for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
+ s
+
+let rec dottify = function
+ | [] -> assert false
+ | [s] -> unquote s
+ | s::[""] -> unquote s
+ | s::l -> (dottify l)^"."^(unquote s)
+
+(*s Uppercase/lowercase renamings. *)
+
+let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
+let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
+
+let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
+let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
+
+(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *)
+let pr_upper_id id = str (String.capitalize (string_of_id id))
+
+
+(*s de Bruijn environments for programs *)
+
+type env = identifier list * Idset.t
+
+(*s Generic renaming issues for local variable names. *)
+
+let rec rename_id id avoid =
+ if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
+
+let rec rename_vars avoid = function
+ | [] ->
+ [], avoid
+ | id :: idl when id == dummy_name ->
+ (* we don't rename dummy binders *)
+ let (idl', avoid') = rename_vars avoid idl in
+ (id :: idl', avoid')
+ | id :: idl ->
+ let (idl, avoid) = rename_vars avoid idl in
+ let id = rename_id (lowercase_id id) avoid in
+ (id :: idl, Idset.add id avoid)
+
+let rename_tvars avoid l =
+ let rec rename avoid = function
+ | [] -> [],avoid
+ | id :: idl ->
+ let id = rename_id (lowercase_id id) avoid in
+ let idl, avoid = rename (Idset.add id avoid) idl in
+ (id :: idl, avoid) in
+ fst (rename avoid l)
+
+let push_vars ids (db,avoid) =
+ let ids',avoid' = rename_vars avoid ids in
+ ids', (ids' @ db, avoid')
+
+let get_db_name n (db,_) =
+ let id = List.nth db (pred n) in
+ if id = dummy_name then id_of_string "__" else id
+
+
+(*S Renamings of global objects. *)
(*s Tables of global renamings *)
let keywords = ref Idset.empty
+let set_keywords kws = keywords := kws
+
let global_ids = ref Idset.empty
-let modular = ref false
+let add_global_ids s = global_ids := Idset.add s !global_ids
+let global_ids_list () = Idset.elements !global_ids
+
+let empty_env () = [], !global_ids
+
+let mktable () =
+ let h = Hashtbl.create 97 in
+ (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+
+let mkset () =
+ let h = Hashtbl.create 97 in
+ (fun x -> Hashtbl.add h x ()), (Hashtbl.mem h), (fun () -> Hashtbl.clear h)
+
+let mktriset () =
+ let h = Hashtbl.create 97 in
+ (fun x y z -> Hashtbl.add h (x,y,z) ()),
+ (fun x y z -> Hashtbl.mem h (x,y,z)),
+ (fun () -> Hashtbl.clear h)
(* For each [global_reference], this table will contain the different parts
- of its renamings, in [string list] form. *)
-let renamings = Hashtbl.create 97
-let rename r l = Hashtbl.add renamings r l
-let get_renamings r = Hashtbl.find renamings r
+ of its renaming, in [string list] form. *)
+let add_renaming, get_renaming, clear_renaming = mktable ()
(* Idem for [module_path]. *)
-let mp_renamings = Hashtbl.create 97
-let mp_rename mp l = Hashtbl.add mp_renamings mp l
-let mp_get_renamings mp = Hashtbl.find mp_renamings mp
+let add_mp_renaming, get_mp_renaming, clear_mp_renaming = mktable ()
-let modvisited = ref MPset.empty
-let modcontents = ref Gset.empty
-let add_module_contents mp s = modcontents := Gset.add (mp,s) !modcontents
-let module_contents mp s = Gset.mem (mp,s) !modcontents
+(* A table for function modfstlev_rename *)
+let add_modfstlev, get_modfstlev, clear_modfstlev = mktable ()
-let to_qualify = ref Refset.empty
+(* A set of all external objects that will have to be fully qualified *)
+let add_static_clash, static_clash, clear_static_clash = mkset ()
-let mod_1st_level = ref Idmap.empty
+(* Two tables of triplets [kind * module_path * string]. The first one
+ will record the first level of all MPfile, not only the current one.
+ The second table will contains local renamings. *)
-(*s Uppercase/lowercase renamings. *)
+type kind = Term | Type | Cons | Mod
-let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
+let add_ext_mpmem, ext_mpmem, clear_ext_mpmem = mktriset ()
+let add_loc_mpmem, loc_mpmem, clear_loc_mpmem = mktriset ()
-let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
+(* The list of external modules that will be opened initially *)
+let add_mpfiles, mem_mpfiles, list_mpfiles, clear_mpfiles =
+ let m = ref MPset.empty in
+ (fun mp -> m:= MPset.add mp !m),
+ (fun mp -> MPset.mem mp !m),
+ (fun () -> MPset.elements !m),
+ (fun () -> m:= MPset.empty)
+
+(*s table containing the visible horizon at a precise moment *)
+
+let visible = ref ([] : module_path list)
+let pop_visible () = visible := List.tl !visible
+let push_visible mp = visible := mp :: !visible
+let top_visible_mp () = List.hd !visible
+
+(*s substitutions for printing signatures *)
+
+let substs = ref empty_subst
+let add_subst msid mp = substs := add_msid msid mp !substs
+let subst_mp mp = subst_mp !substs mp
+let subst_kn kn = subst_kn !substs kn
+let subst_con c = fst (subst_con !substs c)
+let subst_ref = function
+ | ConstRef con -> ConstRef (subst_con con)
+ | IndRef (kn,i) -> IndRef (subst_kn kn,i)
+ | ConstructRef ((kn,i),j) -> ConstructRef ((subst_kn kn,i),j)
+ | _ -> assert false
+
+
+let duplicate_index = ref 0
+let to_duplicate = ref Gmap.empty
+let add_duplicate mp l =
+ incr duplicate_index;
+ let ren = "Coq__" ^ string_of_int (!duplicate_index) in
+ to_duplicate := Gmap.add (mp,l) ren !to_duplicate
+let check_duplicate mp l =
+ let mp' = subst_mp mp in
+ Gmap.find (mp',l) !to_duplicate
+
+type reset_kind = OnlyLocal | AllButExternal | Everything
+
+let reset_allbutext () =
+ clear_loc_mpmem ();
+ global_ids := !keywords;
+ clear_renaming ();
+ clear_mp_renaming ();
+ clear_modfstlev ();
+ clear_static_clash ();
+ clear_mpfiles ();
+ duplicate_index := 0;
+ to_duplicate := Gmap.empty;
+ visible := [];
+ substs := empty_subst
+
+let reset_everything () = reset_allbutext (); clear_ext_mpmem ()
+
+let reset_renaming_tables = function
+ | OnlyLocal -> clear_loc_mpmem ()
+ | AllButExternal -> reset_allbutext ()
+ | Everything -> reset_everything ()
+
+(*S Renaming functions *)
(* This function creates from [id] a correct uppercase/lowercase identifier.
This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes
@@ -69,389 +245,237 @@ let modular_rename up id =
then prefix ^ s
else s
-let rename_module = modular_rename true
-
-(* [clash mp0 l s mpl] checks if [mp0-l-s] can be printed as [l-s] when
- [mpl] is the context of visible modules. More precisely, we check if
- there exists a mp1, module (sub-)path of an element of [mpl], such as
- module [mp1-l] contains [s].
- The verification stops if we encounter [mp1=mp0]. *)
-
-exception Stop
-
-let clash mp0 l s mpl =
- let rec clash_one mp = match mp with
- | _ when mp = mp0 -> raise Stop
- | MPdot (mp',_) ->
- (module_contents (add_labels_mp mp l) s) || (clash_one mp')
- | mp when is_toplevel mp -> false
- | _ -> module_contents (add_labels_mp mp l) s
+(*s [record_contents_fstlev] finds the names of the first-level objects
+ exported by the ground-level modules in [struc]. *)
+
+let rec record_contents_fstlev struc =
+ let upper_type = (lang () = Haskell) in
+ let addtyp mp id = add_ext_mpmem Type mp (modular_rename upper_type id) in
+ let addcons mp id = add_ext_mpmem Cons mp (modular_rename true id) in
+ let addterm mp id = add_ext_mpmem Term mp (modular_rename false id) in
+ let addmod mp id = add_ext_mpmem Mod mp (modular_rename true id) in
+ let addfix mp r =
+ add_ext_mpmem Term mp (modular_rename false (id_of_global r))
in
- let rec clash_list = function
- | [] -> false
- | mp :: mpl -> (clash_one mp) || (clash_list mpl)
- in try clash_list mpl with Stop -> false
-
-(*s [contents_first_level mp] finds the names of the first-level objects
- exported by module [mp]. Nota: it might fail if [mp] isn't a directly
- visible module. Ex: [MPself] under functor, [MPbound], etc ... *)
-
-let contents_first_level mp =
- if not (MPset.mem mp !modvisited) then begin
- modvisited := MPset.add mp !modvisited;
- match (Global.lookup_module mp).mod_type with
- | MTBsig (msid,msb) ->
- let add b id = add_module_contents mp (modular_rename b id) in
- let upper_type = (lang () = Haskell) in
- List.iter
- (function
- | (l, SPBconst cb) ->
- (match Extraction.constant_kind (Global.env ()) cb with
- | Extraction.Logical -> ()
- | Extraction.Type -> add upper_type (id_of_label l)
- | Extraction.Term -> add false (id_of_label l))
- | (_, SPBmind mib) ->
- Array.iter
- (fun mip -> if snd (Inductive.mind_arity mip) <> InProp
- then begin
- add upper_type mip.mind_typename;
- Array.iter (add true) mip.mind_consnames
- end)
- mib.mind_packets
- | _ -> ())
- (Modops.subst_signature_msid msid mp msb)
- | _ -> ()
- end
+ let f mp = function
+ | (l,SEdecl (Dind (_,ind))) ->
+ Array.iter
+ (fun ip ->
+ addtyp mp ip.ip_typename; Array.iter (addcons mp) ip.ip_consnames)
+ ind.ind_packets
+ | (l,SEdecl (Dtype _)) -> addtyp mp (id_of_label l)
+ | (l,SEdecl (Dterm _)) -> addterm mp (id_of_label l)
+ | (l,SEdecl (Dfix (rv,_,_))) -> Array.iter (addfix mp) rv
+ | (l,SEmodule _) -> addmod mp (id_of_label l)
+ | (l,SEmodtype _) -> addmod mp (id_of_label l)
+ in
+ List.iter (fun (mp,sel) -> List.iter (f mp) sel) struc
-(*s Initial renamings creation, for modular extraction. *)
+(*s For monolithic extraction, first-level modules might have to be renamed
+ with unique numbers *)
+
+let modfstlev_rename l =
+ let coqid = id_of_string "Coq" in
+ let id = id_of_label l in
+ try
+ let coqset = get_modfstlev id in
+ let nextcoq = next_ident_away coqid coqset in
+ add_modfstlev id (nextcoq::coqset);
+ (string_of_id nextcoq)^"_"^(string_of_id id)
+ with Not_found ->
+ let s = string_of_id id in
+ if is_lower s || begins_with_CoqXX s then
+ (add_modfstlev id [coqid]; "Coq_"^s)
+ else
+ (add_modfstlev id []; s)
+
+(*s Creating renaming for a [module_path] *)
-let rec mp_create_modular_renamings mp =
- try mp_get_renamings mp
+let rec mp_create_renaming mp =
+ try get_mp_renaming mp
with Not_found ->
let ren = match mp with
+ | _ when not (modular ()) && at_toplevel mp -> [""]
| MPdot (mp,l) ->
- (rename_module (id_of_label l)) :: (mp_create_modular_renamings mp)
- | MPself msid -> [rename_module (id_of_msid msid)]
- | MPbound mbid -> [rename_module (id_of_mbid mbid)]
- | MPfile f -> [String.capitalize (string_of_id (List.hd (repr_dirpath f)))]
- in mp_rename mp ren; ren
+ let lmp = mp_create_renaming mp in
+ if lmp = [""] then (modfstlev_rename l)::lmp
+ else (modular_rename true (id_of_label l))::lmp
+ | MPself msid -> [modular_rename true (id_of_msid msid)]
+ | MPbound mbid -> [modular_rename true (id_of_mbid mbid)]
+ | MPfile _ when not (modular ()) -> assert false
+ | MPfile _ -> [string_of_modfile mp]
+ in add_mp_renaming mp ren; ren
+
+(* [clash mp0 s mpl] checks if [mp0-s] can be printed as [s] when
+ [mpl] is the context of visible modules. More precisely, we check if
+ there exists a [mp] in [mpl] that contains [s].
+ The verification stops if we encounter [mp=mp0]. *)
+let rec clash mem mp0 s = function
+ | [] -> false
+ | mp :: _ when mp = mp0 -> false
+ | mp :: mpl -> mem mp s || clash mem mp0 s mpl
+
+(*s Initial renamings creation, for modular extraction. *)
let create_modular_renamings struc =
let current_module = fst (List.hd struc) in
- let modfiles = ref MPset.empty in
- let { up = u ; down = d } = struct_get_references_set struc
+ let { typ = ty ; trm = tr ; cons = co } = struct_get_references_set struc
in
(* 1) creates renamings of objects *)
let add upper r =
let mp = modpath_of_r r in
- let l = mp_create_modular_renamings mp in
+ let l = mp_create_renaming mp in
let s = modular_rename upper (id_of_global r) in
- global_ids := Idset.add (id_of_string s) !global_ids;
- rename r (s::l);
+ add_global_ids (id_of_string s);
+ add_renaming r (s::l);
begin try
- let mp = modfile_of_mp mp in
- if mp <> current_module then modfiles := MPset.add mp !modfiles
+ let mp = modfile_of_mp mp in if mp <> current_module then add_mpfiles mp
with Not_found -> ()
end;
in
- Refset.iter (add true) u;
- Refset.iter (add false) d;
+ Refset.iter (add (lang () = Haskell)) ty;
+ Refset.iter (add true) co;
+ Refset.iter (add false) tr;
(* 2) determines the opened libraries. *)
- let used_modules = MPset.elements !modfiles in
-
- (* [s] will contain all first-level sub-modules of [cur_mp] *)
- let s = ref Stringset.empty in
- begin
- let add l = s := Stringset.add (rename_module (id_of_label l)) !s in
- match (Global.lookup_module current_module).mod_type with
- | MTBsig (_,msb) ->
- List.iter (function (l,SPBmodule _) -> add l | _ -> ()) msb
- | _ -> ()
- end;
- (* We now compare [s] with the modules coming from [used_modules]. *)
- List.iter
- (function
- | MPfile d ->
- let s_mp =
- String.capitalize (string_of_id (List.hd (repr_dirpath d))) in
- if Stringset.mem s_mp !s then error_module_clash s_mp
- else s:= Stringset.add s_mp !s
- | _ -> assert false)
- used_modules;
+ let used_modules = list_mpfiles () in
+ let used_modules' = List.rev used_modules in
+ let str_list = List.map string_of_modfile used_modules'
+ in
+ let rec check_elsewhere mpl sl = match mpl, sl with
+ | [], [] -> []
+ | mp::mpl, _::sl ->
+ if List.exists (ext_mpmem Mod mp) sl then
+ check_elsewhere mpl sl
+ else mp :: (check_elsewhere mpl sl)
+ | _ -> assert false
+ in
+ let opened_modules = check_elsewhere used_modules' str_list in
+ clear_mpfiles ();
+ List.iter add_mpfiles opened_modules;
(* 3) determines the potential clashes *)
- List.iter contents_first_level used_modules;
- let used_modules' = List.rev used_modules in
- let needs_qualify r =
+ let needs_qualify k r =
let mp = modpath_of_r r in
if (is_modfile mp) && mp <> current_module &&
- (clash mp [] (List.hd (get_renamings r)) used_modules')
- then to_qualify := Refset.add r !to_qualify
+ (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules)
+ then add_static_clash r
in
- Refset.iter needs_qualify u;
- Refset.iter needs_qualify d;
- used_modules
+ Refset.iter (needs_qualify Type) ty;
+ Refset.iter (needs_qualify Term) tr;
+ Refset.iter (needs_qualify Cons) co;
+ List.rev opened_modules
(*s Initial renamings creation, for monolithic extraction. *)
-let begins_with_CoqXX s =
- (String.length s >= 4) &&
- (String.sub s 0 3 = "Coq") &&
- (try
- for i = 4 to (String.index s '_')-1 do
- match s.[i] with
- | '0'..'9' -> ()
- | _ -> raise Not_found
- done;
- true
- with Not_found -> false)
-
-let mod_1st_level_rename l =
- let coqid = id_of_string "Coq" in
- let id = id_of_label l in
- try
- let coqset = Idmap.find id !mod_1st_level in
- let nextcoq = next_ident_away coqid coqset in
- mod_1st_level := Idmap.add id (nextcoq::coqset) !mod_1st_level;
- (string_of_id nextcoq)^"_"^(string_of_id id)
- with Not_found ->
- let s = string_of_id id in
- if is_lower s || begins_with_CoqXX s then
- (mod_1st_level := Idmap.add id [coqid] !mod_1st_level; "Coq_"^s)
- else
- (mod_1st_level := Idmap.add id [] !mod_1st_level; s)
-
-let rec mp_create_mono_renamings mp =
- try mp_get_renamings mp
- with Not_found ->
- let ren = match mp with
- | _ when (at_toplevel mp) -> [""]
- | MPdot (mp,l) ->
- let lmp = mp_create_mono_renamings mp in
- if lmp = [""] then (mod_1st_level_rename l)::lmp
- else (rename_module (id_of_label l))::lmp
- | MPself msid -> [rename_module (id_of_msid msid)]
- | MPbound mbid -> [rename_module (id_of_mbid mbid)]
- | _ -> assert false
- in mp_rename mp ren; ren
-
let create_mono_renamings struc =
- let { up = u ; down = d } = struct_get_references_list struc in
+ let { typ = ty ; trm = tr ; cons = co } = struct_get_references_list struc in
let add upper r =
let mp = modpath_of_r r in
- let l = mp_create_mono_renamings mp in
+ let l = mp_create_renaming mp in
let mycase = if upper then uppercase_id else lowercase_id in
let id =
if l = [""] then
- next_ident_away (mycase (id_of_global r)) (Idset.elements !global_ids)
+ next_ident_away (mycase (id_of_global r)) (global_ids_list ())
else id_of_string (modular_rename upper (id_of_global r))
in
- global_ids := Idset.add id !global_ids;
- rename r ((string_of_id id)::l)
+ add_global_ids id;
+ add_renaming r ((string_of_id id)::l)
in
- List.iter (add true) (List.rev u);
- List.iter (add false) (List.rev d)
-
-(*s Renaming issues at toplevel *)
-
-module TopParams = struct
- let globals () = Idset.empty
- let pp_global _ r = pr_id (id_of_global r)
- let pp_module _ mp = str (string_of_mp mp)
-end
-
-(*s Renaming issues for a monolithic or modular extraction. *)
-
-module StdParams = struct
-
- let globals () = !global_ids
-
- let unquote s =
- if lang () <> Scheme then s
- else
- let s = String.copy s in
- for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
- s
-
- let rec dottify = function
- | [] -> assert false
- | [s] -> unquote s
- | s::[""] -> unquote s
- | s::l -> (dottify l)^"."^(unquote s)
-
- let pp_global mpl r =
- let ls = get_renamings r in
- let s = List.hd ls in
- let mp = modpath_of_r r in
- let ls =
- if mp = List.hd mpl then [s] (* simpliest situation *)
- else match lang () with
- | Scheme -> [s] (* no modular Scheme extraction... *)
- | Toplevel -> [s] (* idem *)
- | Haskell ->
- if !modular then
- ls (* for the moment we always qualify in modular Haskell *)
- else [s]
- | Ocaml ->
- try (* has [mp] something in common with one of those in [mpl] ? *)
- let pref = common_prefix_from_list mp mpl in
- (*i TODO: possibilité de clash i*)
- list_firstn ((mp_length mp)-(mp_length pref)+1) ls
- with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
- let base = base_mp mp in
- if !modular &&
- (at_toplevel mp) &&
- not (Refset.mem r !to_qualify) &&
- not (clash base [] s mpl)
- then snd (list_sep_last ls)
- else ls
- in
- add_module_contents mp s; (* update the visible environment *)
- str (dottify ls)
-
- (* The next function is used only in Ocaml extraction...*)
- let pp_module mpl mp =
- let ls =
- if !modular
- then mp_create_modular_renamings mp
- else mp_create_mono_renamings mp
- in
- let ls =
- try (* has [mp] something in common with one of those in [mpl] ? *)
- let pref = common_prefix_from_list mp mpl in
- (*i TODO: clash possible i*)
- list_firstn ((mp_length mp)-(mp_length pref)) ls
- with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
- if !modular && (at_toplevel mp)
- then snd (list_sep_last ls)
- else ls
- in str (dottify ls)
-
-end
-
-module ToplevelPp = Ocaml.Make(TopParams)
-module OcamlPp = Ocaml.Make(StdParams)
-module HaskellPp = Haskell.Make(StdParams)
-module SchemePp = Scheme.Make(StdParams)
-
-let pp_decl mp d = match lang () with
- | Ocaml -> OcamlPp.pp_decl mp d
- | Haskell -> HaskellPp.pp_decl mp d
- | Scheme -> SchemePp.pp_decl mp d
- | Toplevel -> ToplevelPp.pp_decl mp d
-
-let pp_struct s = match lang () with
- | Ocaml -> OcamlPp.pp_struct s
- | Haskell -> HaskellPp.pp_struct s
- | Scheme -> SchemePp.pp_struct s
- | Toplevel -> ToplevelPp.pp_struct s
-
-let pp_signature s = match lang () with
- | Ocaml -> OcamlPp.pp_signature s
- | Haskell -> HaskellPp.pp_signature s
- | _ -> assert false
-
-let set_keywords () =
- (match lang () with
- | Ocaml -> keywords := Ocaml.keywords
- | Haskell -> keywords := Haskell.keywords
- | Scheme -> keywords := Scheme.keywords
- | Toplevel -> keywords := Idset.empty);
- global_ids := !keywords;
- to_qualify := Refset.empty
+ List.iter (add (lang () = Haskell)) (List.rev ty);
+ List.iter (add false) (List.rev tr);
+ List.iter (add true) (List.rev co);
+ []
+
+let create_renamings struc =
+ if modular () then create_modular_renamings struc
+ else create_mono_renamings struc
-let preamble prm = match lang () with
- | Ocaml -> Ocaml.preamble prm
- | Haskell -> Haskell.preamble prm
- | Scheme -> Scheme.preamble prm
- | Toplevel -> (fun _ _ _ -> mt ())
-
-let preamble_sig prm = match lang () with
- | Ocaml -> Ocaml.preamble_sig prm
- | _ -> assert false
-
-(*S Extraction of one decl to stdout. *)
-
-let print_one_decl struc mp decl =
- set_keywords ();
- modular := false;
- create_mono_renamings struc;
- msgnl (pp_decl [mp] decl)
-
-(*S Extraction to a file. *)
-
-let info f =
- Options.if_verbose msgnl
- (str ("The file "^f^" has been created by extraction."))
-
-let print_structure_to_file f prm struc =
- Hashtbl.clear renamings;
- mod_1st_level := Idmap.empty;
- modcontents := Gset.empty;
- modvisited := MPset.empty;
- set_keywords ();
- modular := prm.modular;
- let used_modules =
- if lang () = Toplevel then []
- else if prm.modular then create_modular_renamings struc
- else (create_mono_renamings struc; [])
- in
- let print_dummys =
- (struct_ast_search ((=) MLdummy) struc,
- struct_type_search Mlutil.isDummy struc,
- struct_type_search ((=) Tunknown) struc)
- in
- let print_magic =
- if lang () <> Haskell then false
- else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
- in
- (* print the implementation *)
- let cout = option_map (fun (f,_) -> open_out f) f in
- let ft = match cout with
- | None -> !Pp_control.std_ft
- | Some cout -> Pp_control.with_output_to cout in
- begin try
- msg_with ft (preamble prm used_modules print_dummys print_magic);
- msg_with ft (pp_struct struc);
- option_iter close_out cout;
- with e ->
- option_iter close_out cout; raise e
- end;
- option_iter (fun (f,_) -> info f) f;
- (* print the signature *)
- match f with
- | Some (_,f) when lang () = Ocaml ->
- let cout = open_out f in
- let ft = Pp_control.with_output_to cout in
- begin try
- msg_with ft (preamble_sig prm used_modules print_dummys);
- msg_with ft (pp_signature (signature_of_structure struc));
- close_out cout;
- with e ->
- close_out cout; raise e
- end;
- info f
- | _ -> ()
-
-
-(*i
- (* DO NOT REMOVE: used when making names resolution *)
- let cout = open_out (f^".ren") in
- let ft = Pp_control.with_output_to cout in
- Hashtbl.iter
- (fun r id ->
- if short_module r = !current_module then
- msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r)))
- renamings;
- pp_flush_with ft ();
- close_out cout;
-i*)
-
-
-
-
-
-
+
+(*s On-the-fly qualification issues for both monolithic or modular extraction. *)
+
+let pp_global k r =
+ let ls = get_renaming r in
+ assert (List.length ls > 1);
+ let s = List.hd ls in
+ let mp = modpath_of_r r in
+ if mp = top_visible_mp () then
+ (* simpliest situation: definition of r (or use in the same context) *)
+ (* we update the visible environment *)
+ (add_loc_mpmem k mp s; unquote s)
+ else match lang () with
+ | Scheme -> unquote s (* no modular Scheme extraction... *)
+ | Haskell ->
+ (* for the moment we always qualify in modular Haskell *)
+ if modular () then dottify ls else s
+ | Ocaml ->
+ try (* has [mp] something in common with one of [!visible] ? *)
+ let prefix = common_prefix_from_list mp !visible in
+ let delta = mp_length mp - mp_length prefix in
+ let ls = list_firstn (delta+1) ls in
+ (* Difficulty: in ocaml we cannot qualify more than [ls],
+ but this (not-so-long) name can in fact be hidden. Solution:
+ duplication of the _definition_ of r in a Coq__XXX module *)
+ let s,ls' = list_sep_last ls in
+ let k' = if ls' = [] then k else Mod in
+ if clash (loc_mpmem k') prefix s !visible then
+ let front = if ls' = [] then [s] else ls' in
+ let l = get_nth_label delta r in
+ try dottify (front @ [check_duplicate prefix l])
+ with Not_found -> add_duplicate prefix l; dottify ls
+ else dottify ls
+ with Not_found ->
+ (* [mp] belongs to a closed module, not one of [!visible]. *)
+ let base = base_mp mp in
+ let base_s,ls1 = list_sep_last ls in
+ let s,ls2 = list_sep_last ls1 in
+ let k' = if ls2 = [] then k else Mod in
+ if modular () && (mem_mpfiles base) &&
+ not (static_clash r) &&
+ (* k' = Mod can't clash in an opened module, see earlier check *)
+ not (clash (loc_mpmem k') base s !visible)
+ then (* Standard situation of an object in another file: *)
+ (* Thanks to the "open" of this file we remove its name *)
+ dottify ls1
+ else if clash (loc_mpmem Mod) base base_s !visible then
+ error_module_clash base_s
+ else dottify ls
+
+(* The next function is used only in Ocaml extraction...*)
+let pp_module mp =
+ let ls = mp_create_renaming mp in
+ if List.length ls = 1 then dottify ls
+ else match mp with
+ | MPdot (mp0,_) when mp0 = top_visible_mp () ->
+ (* simpliest situation: definition of mp (or use in the same context) *)
+ (* we update the visible environment *)
+ let s = List.hd ls in
+ add_loc_mpmem Mod mp0 s; s
+ | _ ->
+ try (* has [mp] something in common with one of those in [!visible] ? *)
+ let prefix = common_prefix_from_list mp !visible in
+ assert (mp <> prefix); (* no use of mp as whole module from itself *)
+ let delta = mp_length mp - mp_length prefix in
+ let ls = list_firstn delta ls in
+ (* Difficulty: in ocaml we cannot qualify more than [ls],
+ but this (not-so-long) name can in fact be hidden. Solution:
+ duplication of the _definition_ of mp via a Coq__XXX module *)
+ let s,ls' = list_sep_last ls in
+ if clash (loc_mpmem Mod) prefix s !visible then
+ let l = get_nth_label_mp delta mp in
+ try dottify (ls' @ [check_duplicate prefix l])
+ with Not_found -> add_duplicate prefix l; dottify ls
+ else dottify ls
+ with Not_found ->
+ (* [mp] belongs to a closed module, not one of [!visible]. *)
+ let base = base_mp mp in
+ let base_s,ls' = list_sep_last ls in
+ let s = fst (list_sep_last ls) in
+ if modular () && (mem_mpfiles base) &&
+ not (clash (loc_mpmem Mod) base s !visible)
+ then dottify ls'
+ else if clash (loc_mpmem Mod) base base_s !visible then
+ error_module_clash base_s
+ else dottify ls
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index f35c0dea5..e17326bc9 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -9,13 +9,53 @@
(*i $Id$ i*)
open Names
+open Libnames
open Miniml
open Mlutil
+open Pp
-val print_one_decl :
- ml_structure -> module_path -> ml_decl -> unit
+val fnl2 : unit -> std_ppcmds
+val space_if : bool -> std_ppcmds
+val sec_space_if : bool -> std_ppcmds
-val print_structure_to_file :
- (string * string) option -> extraction_params -> ml_structure -> unit
+val pp_par : bool -> std_ppcmds -> std_ppcmds
+val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+val pr_binding : identifier list -> std_ppcmds
+val rename_id : identifier -> Idset.t -> identifier
+val lowercase_id : identifier -> identifier
+val uppercase_id : identifier -> identifier
+
+val pr_upper_id : identifier -> std_ppcmds
+
+type env = identifier list * Idset.t
+val empty_env : unit -> env
+
+val rename_vars: Idset.t -> identifier list -> env
+val rename_tvars: Idset.t -> identifier list -> identifier list
+val push_vars : identifier list -> env -> identifier list * env
+val get_db_name : int -> env -> identifier
+
+val record_contents_fstlev : ml_structure -> unit
+
+val create_renamings : ml_structure -> module_path list
+
+type kind = Term | Type | Cons | Mod
+
+val pp_global : kind -> global_reference -> string
+val pp_module : module_path -> string
+
+val top_visible_mp : unit -> module_path
+val push_visible : module_path -> unit
+val pop_visible : unit -> unit
+
+val add_subst : mod_self_id -> module_path -> unit
+
+val check_duplicate : module_path -> label -> string
+
+type reset_kind = OnlyLocal | AllButExternal | Everything
+
+val reset_renaming_tables : reset_kind -> unit
+
+val set_keywords : Idset.t -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 0ef993057..953e4930b 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -21,7 +21,9 @@ open Modutil
open Common
open Mod_subst
-(*s Obtaining Coq environment. *)
+(***************************************)
+(*S Part I: computing Coq environment. *)
+(***************************************)
let toplevel_env () =
let seg = Lib.contents_after None in
@@ -156,22 +158,19 @@ let rec extract_msig env mp = function
(l,Spec s) :: (extract_msig env mp msig)
end
| (l,SPBmodule {msb_modtype=mtb}) :: msig ->
- (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig)
+ (l,Smodule (extract_mtb env mtb)) :: (extract_msig env mp msig)
| (l,SPBmodtype mtb) :: msig ->
- (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig)
+ (l,Smodtype (extract_mtb env mtb)) :: (extract_msig env mp msig)
-and extract_mtb env mpo = function
+and extract_mtb env = function
| MTBident kn -> Visit.add_kn kn; MTident kn
| MTBfunsig (mbid, mtb, mtb') ->
let mp = MPbound mbid in
let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in
- MTfunsig (mbid, extract_mtb env None mtb,
- extract_mtb env' None mtb')
+ MTfunsig (mbid, extract_mtb env mtb,
+ extract_mtb env' mtb')
| MTBsig (msid, msig) ->
- let mp, msig = match mpo with
- | None -> MPself msid, msig
- | Some mp -> mp, Modops.subst_signature_msid msid mp msig
- in
+ let mp = MPself msid in
let env' = Modops.add_signature mp msig env in
MTsig (msid, extract_msig env' mp msig)
@@ -216,19 +215,20 @@ let rec extract_msb env mp all = function
let ms = extract_msb env mp all msb in
let kn = make_kn mp empty_dirpath l in
if all || Visit.needed_kn kn then
- (l,SEmodtype (extract_mtb env None mtb)) :: ms
+ (l,SEmodtype (extract_mtb env mtb)) :: ms
else ms
and extract_meb env mpo all = function
- | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *)
- | MEBident mp -> Visit.add_mp mp; MEident mp
+ | MEBident mp ->
+ if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp;
+ Visit.add_mp mp; MEident mp
| MEBapply (meb, meb',_) ->
MEapply (extract_meb env None true meb,
extract_meb env None true meb')
| MEBfunctor (mbid, mtb, meb) ->
let mp = MPbound mbid in
let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in
- MEfunctor (mbid, extract_mtb env None mtb,
+ MEfunctor (mbid, extract_mtb env mtb,
extract_meb env' None true meb)
| MEBstruct (msid, msb) ->
let mp,msb = match mpo with
@@ -247,7 +247,7 @@ and extract_module env mp all mb =
(* a msid different from the one of the module. Here is the patch. *)
let mtb = replicate_msid meb mtb in
{ ml_mod_expr = extract_meb env (Some mp) all meb;
- ml_mod_type = extract_mtb env None mtb }
+ ml_mod_type = extract_mtb env mtb }
let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
@@ -260,14 +260,118 @@ let mono_environment refs mpl =
List.rev_map
(fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l
-
+(**************************************)
+(*S Part II : Input/Output primitives *)
+(**************************************)
+
+let descr () = match lang () with
+ | Ocaml -> Ocaml.ocaml_descr
+ | Haskell -> Haskell.haskell_descr
+ | Scheme -> Scheme.scheme_descr
+
+(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
+ Works similarly for the other languages. *)
+
+let mono_filename f =
+ let d = descr () in
+ match f with
+ | None -> None, None, id_of_string "Main"
+ | Some f ->
+ let f =
+ if Filename.check_suffix f d.file_suffix then
+ Filename.chop_suffix f d.file_suffix
+ else f
+ in
+ Some (f^d.file_suffix), option_map ((^) f) d.sig_suffix, id_of_string f
+
+(* Builds a suitable filename from a module id *)
+
+let module_filename m =
+ let d = descr () in
+ let f = if d.capital_file then String.capitalize else String.uncapitalize in
+ let fn = f (string_of_id m) in
+ Some (fn^d.file_suffix), option_map ((^) fn) d.sig_suffix, m
+
+(*s Extraction of one decl to stdout. *)
+
+let print_one_decl struc mp decl =
+ let d = descr () in
+ reset_renaming_tables AllButExternal;
+ ignore (create_renamings struc);
+ push_visible mp;
+ msgnl (d.pp_decl decl);
+ pop_visible ()
+
+(*s Extraction of a ml struct to a file. *)
+
+let print_structure_to_file (fn,si,mo) struc =
+ let d = descr () in
+ reset_renaming_tables AllButExternal;
+ let used_modules = create_renamings struc in
+ let unsafe_needs = {
+ mldummy = struct_ast_search ((=) MLdummy) struc;
+ tdummy = struct_type_search Mlutil.isDummy struc;
+ tunknown = struct_type_search ((=) Tunknown) struc;
+ magic =
+ if lang () <> Haskell then false
+ else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
+ in
+ (* print the implementation *)
+ let cout = option_map open_out fn in
+ let ft = match cout with
+ | None -> !Pp_control.std_ft
+ | Some cout -> Pp_control.with_output_to cout in
+ let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in
+ begin try
+ msg_with ft (d.preamble mo used_modules unsafe_needs);
+ msg_with devnull (d.pp_struct struc); (* for computing objects to duplicate *)
+ reset_renaming_tables OnlyLocal;
+ msg_with ft (d.pp_struct struc);
+ option_iter close_out cout;
+ with e ->
+ option_iter close_out cout; raise e
+ end;
+ option_iter info_file fn;
+ (* print the signature *)
+ option_iter
+ (fun si ->
+ let cout = open_out si in
+ let ft = Pp_control.with_output_to cout in
+ begin try
+ msg_with ft (d.sig_preamble mo used_modules unsafe_needs);
+ reset_renaming_tables OnlyLocal;
+ msg_with ft (d.pp_sig (signature_of_structure struc));
+ close_out cout;
+ with e ->
+ close_out cout; raise e
+ end;
+ info_file si)
+ si
+
+
+(*********************************************)
+(*s Part III: the actual extraction commands *)
+(*********************************************)
+
+
+let reset () =
+ Visit.reset (); reset_tables (); reset_renaming_tables Everything
+
+let init modular =
+ check_inside_section (); check_inside_module ();
+ set_keywords (descr ()).keywords;
+ set_modular modular;
+ reset ();
+ if modular && lang () = Scheme then error_scheme ()
+
+
(*s Recursive extraction in the Coq toplevel. The vernacular command is
- \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
- to get the saturated environment to extract. *)
+ \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when
+ extracting to a file with the command:
+ \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
-let mono_extraction (f,m) qualids =
- check_inside_section ();
- check_inside_module ();
+let full_extraction f qualids =
+ init false;
let rec find = function
| [] -> [],[]
| q::l ->
@@ -276,116 +380,44 @@ let mono_extraction (f,m) qualids =
let mp = Nametab.locate_module (snd (qualid_of_reference q))
in refs,(mp::mps)
with Not_found -> (Nametab.global q)::refs, mps
- in
+ in
let refs,mps = find qualids in
- let prm = {modular=false; mod_name = m; to_appear= refs} in
- let struc = optimize_struct prm None (mono_environment refs mps) in
- print_structure_to_file f prm struc;
- Visit.reset ();
- reset_tables ()
+ let struc = optimize_struct refs (mono_environment refs mps) in
+ warning_axioms ();
+ print_structure_to_file (mono_filename f) struc;
+ reset ()
-let extraction_rec = mono_extraction (None,id_of_string "Main")
-(*s Extraction in the Coq toplevel. We display the extracted term in
- Ocaml syntax and we use the Coq printers for globals. The
- vernacular command is \verb!Extraction! [qualid]. *)
+(*s Simple extraction in the Coq toplevel. The vernacular command
+ is \verb!Extraction! [qualid]. *)
-let extraction qid =
- check_inside_section ();
- check_inside_module ();
+let simple_extraction qid =
+ init false;
try
let _ = Nametab.locate_module (snd (qualid_of_reference qid)) in
- extraction_rec [qid]
+ full_extraction None [qid]
with Not_found ->
let r = Nametab.global qid in
if is_custom r then
msgnl (str "User defined extraction:" ++ spc () ++
str (find_custom r) ++ fnl ())
else
- let prm =
- { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
- let struc = optimize_struct prm None (mono_environment [r] []) in
+ let struc = optimize_struct [r] (mono_environment [r] []) in
let d = get_decl_in_structure r struc in
+ warning_axioms ();
print_one_decl struc (modpath_of_r r) d;
- Visit.reset ();
- reset_tables ()
-
-(*s Extraction to a file (necessarily recursive).
- The vernacular command is
- \verb!Extraction "file"! [qualid1] ... [qualidn].*)
-
-let lang_suffix () = match lang () with
- | Ocaml -> ".ml",".mli"
- | Haskell -> ".hs",".hi"
- | Scheme -> ".scm",".scm"
- | Toplevel -> assert false
-
-let filename f =
- let s,s' = lang_suffix () in
- if Filename.check_suffix f s then
- let f' = Filename.chop_suffix f s in
- Some (f,f'^s'),id_of_string f'
- else Some (f^s,f^s'),id_of_string f
-
-let extraction_file f vl =
- if lang () = Toplevel then error_toplevel ()
- else mono_extraction (filename f) vl
-
-(*s Extraction of a module at the toplevel. *)
-
-let extraction_module m =
- check_inside_section ();
- check_inside_module ();
- begin match lang () with
- | Toplevel -> error_toplevel ()
- | Scheme -> error_scheme ()
- | _ -> ()
- end;
- let q = snd (qualid_of_reference m) in
- let mp =
- try Nametab.locate_module q with Not_found -> error_unknown_module q
- in
- let b = is_modfile mp in
- let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
- Visit.reset ();
- Visit.add_mp mp;
- let env = Global.env () in
- let l = List.rev (environment_until None) in
- let struc =
- List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) b m)) l
- in
- let struc = optimize_struct prm None struc in
- let struc =
- let bmp = base_mp mp in
- try [bmp, List.assoc bmp struc] with Not_found -> assert false
- in
- print_structure_to_file None prm struc;
- Visit.reset ();
- reset_tables ()
+ reset ()
(*s (Recursive) Extraction of a library. The vernacular command is
\verb!(Recursive) Extraction Library! [M]. *)
-let module_file_name m = match lang () with
- | Ocaml -> let f = String.uncapitalize (string_of_id m) in f^".ml", f^".mli"
- | Haskell -> let f = String.capitalize (string_of_id m) in f^".hs", f^".hi"
- | _ -> assert false
-
-let dir_module_of_id m =
- let q = make_short_qualid m in
- try Nametab.full_name_module q with Not_found -> error_unknown_module q
-
let extraction_library is_rec m =
- check_inside_section ();
- check_inside_module ();
- begin match lang () with
- | Toplevel -> error_toplevel ()
- | Scheme -> error_scheme ()
- | _ -> ()
- end;
- let dir_m = dir_module_of_id m in
- Visit.reset ();
+ init true;
+ let dir_m =
+ let q = make_short_qualid m in
+ try Nametab.full_name_module q with Not_found -> error_unknown_module q
+ in
Visit.add_mp (MPfile dir_m);
let env = Global.env () in
let l = List.rev (environment_until (Some dir_m)) in
@@ -395,22 +427,20 @@ let extraction_library is_rec m =
else l
in
let struc = List.fold_left select [] l in
- let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
- let struc = optimize_struct dummy_prm None struc in
+ let struc = optimize_struct [] struc in
+ warning_axioms ();
+ record_contents_fstlev struc;
let rec print = function
| [] -> ()
| (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l
| (MPfile dir, sel) as e :: l ->
let short_m = snd (split_dirpath dir) in
- let f = module_file_name short_m in
- let prm = {modular=true;mod_name=short_m;to_appear=[]} in
- print_structure_to_file (Some f) prm [e];
+ print_structure_to_file (module_filename short_m) [e];
print l
| _ -> assert false
in
print struc;
- Visit.reset ();
- reset_tables ()
+ reset ()
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 18b106da2..baf79573f 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -13,8 +13,6 @@
open Names
open Libnames
-val extraction : reference -> unit
-val extraction_rec : reference list -> unit
-val extraction_file : string -> reference list -> unit
-val extraction_module : reference -> unit
+val simple_extraction : reference -> unit
+val full_extraction : string option -> reference list -> unit
val extraction_library : bool -> identifier -> unit
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 3fa318e7e..77067b2b4 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -337,7 +337,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
{ind_info = Standard;
ind_nparams = npar;
ind_packets = packets;
- ind_equiv = mib.mind_equiv };
+ ind_equiv = match mib.mind_equiv with
+ | None -> NoEquiv
+ | Some kn -> Equiv kn
+ };
(* Second pass: we extract constructors *)
for i = 0 to mib.mind_ntypes - 1 do
let p = packets.(i) in
@@ -421,7 +424,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let i = {ind_info = ind_info;
ind_nparams = npar;
ind_packets = packets;
- ind_equiv = mib.mind_equiv}
+ ind_equiv = match mib.mind_equiv with
+ | None -> NoEquiv
+ | Some kn -> Equiv kn }
in
add_ind kn mib i;
i
@@ -828,18 +833,18 @@ let extract_constant env kn cb =
| None -> (* A logical axiom is risky, an informative one is fatal. *)
(match flag_of_type env typ with
| (Info,TypeScheme) ->
- if not (is_custom r) then warning_info_ax r;
+ if not (is_custom r) then add_info_axiom r;
let n = type_scheme_nb_args env typ in
let ids = iterate (fun l -> anonymous::l) n [] in
Dtype (r, ids, Taxiom)
| (Info,Default) ->
- if not (is_custom r) then warning_info_ax r;
+ if not (is_custom r) then add_info_axiom r;
let t = snd (record_constant_type env kn (Some typ)) in
Dterm (r, MLaxiom, type_expunge env t)
| (Logic,TypeScheme) ->
- warning_log_ax r; Dtype (r, [], Tdummy Ktype)
+ add_log_axiom r; Dtype (r, [], Tdummy Ktype)
| (Logic,Default) ->
- warning_log_ax r; Dterm (r, MLdummy, Tdummy Kother))
+ add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother))
| Some body ->
(match flag_of_type env typ with
| (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
@@ -880,24 +885,6 @@ let extract_inductive env kn =
ind.ind_packets
in { ind with ind_packets = packets }
-(*s From a global reference to a ML declaration. *)
-
-let extract_declaration env r = match r with
- | ConstRef kn -> extract_constant env kn (Environ.lookup_constant kn env)
- | IndRef (kn,_) -> Dind (kn, extract_inductive env kn)
- | ConstructRef ((kn,_),_) -> Dind (kn, extract_inductive env kn)
- | VarRef kn -> assert false
-
-(*s Without doing complete extraction, just guess what a constant would be. *)
-
-type kind = Logical | Term | Type
-
-let constant_kind env cb =
- match flag_of_type env (Typeops.type_of_constant_type env cb.const_type) with
- | (Logic,_) -> Logical
- | (Info,TypeScheme) -> Type
- | (Info,Default) -> Term
-
(*s Is a [ml_decl] logical ? *)
let logical_decl = function
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index b26a577e2..cb0600d05 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -26,16 +26,6 @@ val extract_fixpoint :
val extract_inductive : env -> kernel_name -> ml_ind
-(*s ML declaration corresponding to a Coq reference. *)
-
-val extract_declaration : env -> global_reference -> ml_decl
-
-(*s Without doing complete extraction, just guess what a constant would be. *)
-
-type kind = Logical | Term | Type
-
-val constant_kind : env -> constant_body -> kind
-
(*s Is a [ml_decl] or a [ml_spec] logical ? *)
val logical_decl : ml_decl -> bool
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 13b29c7b5..cb95808d6 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -31,19 +31,18 @@ VERNAC ARGUMENT EXTEND language
| [ "Ocaml" ] -> [ Ocaml ]
| [ "Haskell" ] -> [ Haskell ]
| [ "Scheme" ] -> [ Scheme ]
-| [ "Toplevel" ] -> [ Toplevel ]
END
(* Extraction commands *)
VERNAC COMMAND EXTEND Extraction
(* Extraction in the Coq toplevel *)
-| [ "Extraction" global(x) ] -> [ extraction x ]
-| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ extraction_rec l ]
+| [ "Extraction" global(x) ] -> [ simple_extraction x ]
+| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ]
(* Monolithic extraction to a file *)
| [ "Extraction" string(f) ne_global_list(l) ]
- -> [ extraction_file f l ]
+ -> [ full_extraction (Some f) l ]
END
(* Modular extraction (one Coq library = one ML module) *)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 1e26f6c75..f55bc6feb 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -18,7 +18,7 @@ open Libnames
open Table
open Miniml
open Mlutil
-open Ocaml
+open Common
(*s Haskell renaming issues. *)
@@ -30,22 +30,22 @@ let keywords =
"as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
Idset.empty
-let preamble prm used_modules (mldummy,tdummy,tunknown) magic =
+let preamble mod_name used_modules usf =
let pp_mp = function
| MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
| _ -> assert false
in
- (if not magic then mt ()
+ (if not usf.magic then mt ()
else
str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
++
- str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl ()
+ str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl ()
++ fnl() ++
str "import qualified Prelude" ++ fnl() ++
prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
++ fnl () ++
- (if not magic then mt ()
+ (if not usf.magic then mt ()
else str "\
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
@@ -58,13 +58,11 @@ unsafeCoerce = IOExts.unsafeCoerce
++
fnl() ++ fnl()
++
- (if not mldummy then mt ()
+ (if not usf.mldummy then mt ()
else
str "__ = Prelude.error \"Logical or arity value used\""
++ fnl () ++ fnl())
-let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO"
-
let pp_abst = function
| [] -> (mt ())
| l -> (str "\\" ++
@@ -73,17 +71,11 @@ let pp_abst = function
let pr_lower_id id = pr_id (lowercase_id id)
-(*s The pretty-printing functor. *)
-
-module Make = functor(P : Mlpp_param) -> struct
-
-let local_mpl = ref ([] : module_path list)
+(*s The pretty-printer for haskell syntax *)
-let pp_global r =
+let pp_global k r =
if is_inline_custom r then str (find_custom r)
- else P.pp_global !local_mpl r
-
-let empty_env () = [], P.globals()
+ else str (Common.pp_global k r)
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
@@ -96,13 +88,14 @@ let rec pp_type par vl t =
let rec pp_rec par = function
| Tmeta _ | Tvar' _ -> assert false
| Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
- | Tglob (r,[]) -> pp_global r
+ | Tglob (r,[]) -> pp_global Type r
| Tglob (r,l) ->
if r = IndRef (kn_sig,0) then
pp_type true vl (List.hd l)
else
pp_par par
- (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
+ (pp_global Type r ++ spc () ++
+ prlist_with_sep spc (pp_type true vl) l)
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
@@ -151,15 +144,15 @@ let rec pp_expr par env args =
spc () ++ str "in") ++
spc () ++ hov 0 pp_a2)))
| MLglob r ->
- apply (pp_global r)
+ apply (pp_global Term r)
| MLcons (_,r,[]) ->
- assert (args=[]); pp_global r
+ assert (args=[]); pp_global Cons r
| MLcons (_,r,[a]) ->
assert (args=[]);
- pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a)
+ pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
| MLcons (_,r,args') ->
assert (args=[]);
- pp_par par (pp_global r ++ spc () ++
+ pp_par par (pp_global Cons r ++ spc () ++
prlist_with_sep spc (pp_expr true env []) args')
| MLcase ((_,factors),t, pv) ->
apply (pp_par par'
@@ -181,7 +174,7 @@ and pp_pat env factors pv =
let pp_one_pat (name,ids,t) =
let ids,env' = push_vars (List.rev ids) env in
let par = expr_needs_par t in
- hov 2 (pp_global name ++
+ hov 2 (pp_global Cons name ++
(match ids with
| [] -> mt ()
| _ -> (str " " ++
@@ -234,7 +227,7 @@ let pp_logical_ind packet =
let pp_singleton kn packet =
let l = rename_tvars keywords packet.ip_vars in
let l' = List.rev l in
- hov 2 (str "type " ++ pp_global (IndRef (kn,0)) ++ spc () ++
+ hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++
prlist_with_sep spc pr_id l ++
(if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -244,7 +237,7 @@ let pp_singleton kn packet =
let pp_one_ind ip pl cv =
let pl = rename_tvars keywords pl in
let pp_constructor (r,l) =
- (pp_global r ++
+ (pp_global Cons r ++
match l with
| [] -> (mt ())
| _ -> (str " " ++
@@ -252,7 +245,7 @@ let pp_one_ind ip pl cv =
(fun () -> (str " ")) (pp_type true pl) l))
in
str (if Array.length cv = 0 then "type " else "data ") ++
- pp_global (IndRef ip) ++ str " " ++
+ pp_global Type (IndRef ip) ++ str " " ++
prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
(if pl = [] then mt () else str " ") ++
if Array.length cv = 0 then str "= () -- empty inductive"
@@ -280,9 +273,7 @@ let rec pp_ind first kn i ind =
let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
-let pp_decl mpl =
- local_mpl := mpl;
- function
+let pp_decl = function
| Dind (kn,i) when i.ind_info = Singleton ->
pp_singleton kn i.ind_packets.(0) ++ fnl ()
| Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
@@ -299,38 +290,49 @@ let pp_decl mpl =
if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
else str "=" ++ spc () ++ pp_type false l t
in
- hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl ()
+ hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
| Dfix (rv, defs, typs) ->
let max = Array.length rv in
let rec iter i =
if i = max then mt ()
else
- let e = pp_global rv.(i) in
+ let e = pp_global Term rv.(i) in
e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl ()
- ++ pp_function (empty_env ()) e defs.(i) ++ fnl () ++ fnl ()
+ ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 ()
++ iter (i+1)
in iter 0
| Dterm (r, a, t) ->
if is_inline_custom r then mt ()
else
- let e = pp_global r in
+ let e = pp_global Term r in
e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
if is_custom r then
- hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl() ++ fnl ())
+ hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
else
- hov 0 (pp_function (empty_env ()) e a ++ fnl () ++ fnl ())
+ hov 0 (pp_function (empty_env ()) e a ++ fnl2 ())
-let pp_structure_elem mpl = function
- | (l,SEdecl d) -> pp_decl mpl d
+let pp_structure_elem = function
+ | (l,SEdecl d) -> pp_decl d
| (l,SEmodule m) ->
failwith "TODO: Haskell extraction of modules not implemented yet"
| (l,SEmodtype m) ->
failwith "TODO: Haskell extraction of modules not implemented yet"
let pp_struct =
- prlist (fun (mp,sel) -> prlist (pp_structure_elem [mp]) sel)
-
-let pp_signature s = failwith "TODO"
-
-end
-
+ let pp_sel (mp,sel) =
+ push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p
+ in
+ prlist pp_sel
+
+
+let haskell_descr = {
+ keywords = keywords;
+ file_suffix = ".hs";
+ capital_file = true;
+ preamble = preamble;
+ pp_struct = pp_struct;
+ sig_suffix = None;
+ sig_preamble = (fun _ _ _ -> mt ());
+ pp_sig = (fun _ -> mt ());
+ pp_decl = pp_decl;
+}
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 430ec1fce..1b5dbc711 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -8,13 +8,5 @@
(*i $Id$ i*)
-open Pp
-open Names
-open Miniml
+val haskell_descr : Miniml.language_descr
-val keywords : Idset.t
-
-val preamble :
- extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
-
-module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index d728a8a14..ef963cc90 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -78,11 +78,16 @@ type ml_ind_packet = {
(* [ip_nparams] contains the number of parameters. *)
+type equiv =
+ | NoEquiv
+ | Equiv of kernel_name
+ | RenEquiv of string
+
type ml_ind = {
ind_info : inductive_info;
ind_nparams : int;
ind_packets : ml_ind_packet array;
- ind_equiv : kernel_name option
+ ind_equiv : equiv
}
(*s ML terms. *)
@@ -151,24 +156,28 @@ type ml_structure = (module_path * ml_module_structure) list
type ml_signature = (module_path * ml_module_sig) list
-(*s Pretty-printing of MiniML in a given concrete syntax is parameterized
- by a function [pp_global] that pretty-prints global references.
- The resulting pretty-printer is a module of type [Mlpp] providing
- functions to print types, terms and declarations. *)
-
-module type Mlpp_param = sig
- val globals : unit -> Idset.t
- val pp_global : module_path list -> global_reference -> std_ppcmds
- val pp_module : module_path list -> module_path -> std_ppcmds
-end
-
-module type Mlpp = sig
- val pp_decl : module_path list -> ml_decl -> std_ppcmds
- val pp_struct : ml_structure -> std_ppcmds
- val pp_signature : ml_signature -> std_ppcmds
-end
-
-type extraction_params =
- { modular : bool;
- mod_name : identifier;
- to_appear : global_reference list }
+type unsafe_needs = {
+ mldummy : bool;
+ tdummy : bool;
+ tunknown : bool;
+ magic : bool
+}
+
+type language_descr = {
+ keywords : Idset.t;
+
+ (* Concerning the source file *)
+ file_suffix : string;
+ capital_file : bool; (* should we capitalize filenames ? *)
+ preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+ pp_struct : ml_structure -> std_ppcmds;
+
+ (* Concerning a possible interface file *)
+ sig_suffix : string option;
+ sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+ pp_sig : ml_signature -> std_ppcmds;
+
+ (* for an isolated declaration print *)
+ pp_decl : ml_decl -> std_ppcmds;
+
+}
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 87713e4d5..760f76c9a 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -86,56 +86,6 @@ let rec replicate_msid meb mtb = match meb,mtb with
if msig' == msig then MTBsig (msid, msig) else MTBsig (msid, msig')
| _ -> mtb
-
-(*S More functions concerning [module_path]. *)
-
-let rec mp_length = function
- | MPdot (mp, _) -> 1 + (mp_length mp)
- | _ -> 1
-
-let rec prefixes_mp mp = match mp with
- | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
- | _ -> MPset.singleton mp
-
-let rec common_prefix prefixes_mp1 mp2 =
- if MPset.mem mp2 prefixes_mp1 then mp2
- else match mp2 with
- | MPdot (mp,_) -> common_prefix prefixes_mp1 mp
- | _ -> raise Not_found
-
-let common_prefix_from_list mp0 mpl =
- let prefixes_mp0 = prefixes_mp mp0 in
- let rec f = function
- | [] -> raise Not_found
- | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
- in f mpl
-
-let rec modfile_of_mp mp = match mp with
- | MPfile _ -> mp
- | MPdot (mp,_) -> modfile_of_mp mp
- | _ -> raise Not_found
-
-let rec parse_labels ll = function
- | MPdot (mp,l) -> parse_labels (l::ll) mp
- | mp -> mp,ll
-
-let labels_of_mp mp = parse_labels [] mp
-
-let labels_of_ref r =
- let mp,_,l =
- match r with
- ConstRef con -> repr_con con
- | IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> repr_kn kn
- | VarRef _ -> assert false
- in
- parse_labels [l] mp
-
-let rec add_labels_mp mp = function
- | [] -> mp
- | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
-
-
(*S Functions upon ML modules. *)
(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
@@ -200,7 +150,9 @@ let ind_iter_references do_term do_cons do_type kn ind =
let packet_iter ip p =
do_type (IndRef ip);
if lang () = Ocaml then
- option_iter (fun kne -> do_type (IndRef (kne,snd ip))) ind.ind_equiv;
+ (match ind.ind_equiv with
+ | Equiv kne -> do_type (IndRef (kne, snd ip));
+ | _ -> ());
Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
in
if lang () = Ocaml then record_iter_references do_term ind.ind_info;
@@ -228,13 +180,13 @@ let struct_iter_references do_term do_cons do_type =
(*s Get all references used in one [ml_structure], either in [list] or [set]. *)
-type 'a updown = { mutable up : 'a ; mutable down : 'a }
+type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a }
let struct_get_references empty add struc =
- let o = { up = empty ; down = empty } in
- let do_term r = o.down <- add r o.down in
- let do_cons r = o.up <- add r o.up in
- let do_type = if lang () = Haskell then do_cons else do_term in
+ let o = { typ = empty ; trm = empty ; cons = empty } in
+ let do_type r = o.typ <- add r o.typ in
+ let do_term r = o.trm <- add r o.trm in
+ let do_cons r = o.cons <- add r o.cons in
struct_iter_references do_term do_cons do_type struc; o
let struct_get_references_set = struct_get_references Refset.empty Refset.add
@@ -251,7 +203,9 @@ end
let struct_get_references_list struc =
let o = struct_get_references Orefset.empty Orefset.add struc in
- { up = Orefset.list o.up; down = Orefset.list o.down }
+ { typ = Orefset.list o.typ;
+ trm = Orefset.list o.trm;
+ cons = Orefset.list o.cons }
(*s Searching occurrences of a particular term (no lifting done). *)
@@ -363,38 +317,40 @@ let dfix_to_mlfix rv av i =
let c = Array.map (subst 0) av
in MLfix(i, ids, c)
-let rec optim prm s = function
+let rec optim to_appear s = function
| [] -> []
| (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
- if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l
+ if List.mem r to_appear
+ then d :: (optim to_appear s l)
+ else optim to_appear s l
| Dterm (r,t,typ) :: l ->
let t = normalize (ast_glob_subst !s t) in
let i = inline r t in
if i then s := Refmap.add r t !s;
- if not i || prm.modular || List.mem r prm.to_appear
+ if not i || modular () || List.mem r to_appear
then
let d = match optimize_fix t with
| MLfix (0, _, [|c|]) ->
Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|])
| t -> Dterm (r, t, typ)
- in d :: (optim prm s l)
- else optim prm s l
- | d :: l -> d :: (optim prm s l)
+ in d :: (optim to_appear s l)
+ else optim to_appear s l
+ | d :: l -> d :: (optim to_appear s l)
-let rec optim_se top prm s = function
+let rec optim_se top to_appear s = function
| [] -> []
| (l,SEdecl (Dterm (r,a,t))) :: lse ->
let a = normalize (ast_glob_subst !s a) in
let i = inline r a in
if i then s := Refmap.add r a !s;
- if top && i && not prm.modular && not (List.mem r prm.to_appear)
- then optim_se top prm s lse
+ if top && i && not (modular ()) && not (List.mem r to_appear)
+ then optim_se top to_appear s lse
else
let d = match optimize_fix a with
| MLfix (0, _, [|c|]) ->
Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
| a -> Dterm (r, a, t)
- in (l,SEdecl d) :: (optim_se top prm s lse)
+ in (l,SEdecl d) :: (optim_se top to_appear s lse)
| (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
let all = ref true in
@@ -405,22 +361,22 @@ let rec optim_se top prm s = function
then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
else all := false
done;
- if !all && top && not prm.modular
- && (array_for_all (fun r -> not (List.mem r prm.to_appear)) rv)
- then optim_se top prm s lse
- else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top prm s lse)
+ if !all && top && not (modular ())
+ && (array_for_all (fun r -> not (List.mem r to_appear)) rv)
+ then optim_se top to_appear s lse
+ else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
| (l,SEmodule m) :: lse ->
- let m = { m with ml_mod_expr = optim_me prm s m.ml_mod_expr}
- in (l,SEmodule m) :: (optim_se top prm s lse)
- | se :: lse -> se :: (optim_se top prm s lse)
+ let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
+ in (l,SEmodule m) :: (optim_se top to_appear s lse)
+ | se :: lse -> se :: (optim_se top to_appear s lse)
-and optim_me prm s = function
- | MEstruct (msid, lse) -> MEstruct (msid, optim_se false prm s lse)
+and optim_me to_appear s = function
+ | MEstruct (msid, lse) -> MEstruct (msid, optim_se false to_appear s lse)
| MEident mp as me -> me
- | MEapply (me, me') -> MEapply (optim_me prm s me, optim_me prm s me')
- | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me)
+ | MEapply (me, me') ->
+ MEapply (optim_me to_appear s me, optim_me to_appear s me')
+ | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me)
-let optimize_struct prm before struc =
+let optimize_struct to_appear struc =
let subst = ref (Refmap.empty : ml_ast Refmap.t) in
- option_iter (fun l -> ignore (optim prm subst l)) before;
- List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc
+ List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index 46c7dbc3f..c89590daa 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -33,14 +33,6 @@ val subst_msb : substitution -> module_structure_body -> module_structure_body
val replicate_msid : module_expr_body -> module_type_body -> module_type_body
-(*s More utilities concerning [module_path]. *)
-
-val mp_length : module_path -> int
-val prefixes_mp : module_path -> MPset.t
-val modfile_of_mp : module_path -> module_path
-val common_prefix_from_list : module_path -> module_path list -> module_path
-val add_labels_mp : module_path -> label list -> module_path
-
(*s Functions upon ML modules. *)
val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
@@ -52,10 +44,10 @@ val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
val struct_iter_references : do_ref -> do_ref -> do_ref -> ml_structure -> unit
-type 'a updown = { mutable up : 'a ; mutable down : 'a }
+type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a }
-val struct_get_references_set : ml_structure -> Refset.t updown
-val struct_get_references_list : ml_structure -> global_reference list updown
+val struct_get_references_set : ml_structure -> Refset.t kinds
+val struct_get_references_list : ml_structure -> global_reference list kinds
val signature_of_structure : ml_structure -> ml_signature
@@ -65,7 +57,7 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
all beta redexes (when the argument does not occur, it is just
thrown away; when it occurs exactly once it is substituted; otherwise
a let-in redex is created for clarity) and iota redexes, plus some other
- optimizations. *)
+ optimizations. The first argument is the list of objects we want to appear.
+*)
-val optimize_struct :
- extraction_params -> ml_decl list option -> ml_structure -> ml_structure
+val optimize_struct : global_reference list -> ml_structure -> ml_structure
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 600e6ebca..7548c1487 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -19,10 +19,7 @@ open Table
open Miniml
open Mlutil
open Modutil
-
-(*s Some utility functions. *)
-
-let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+open Common
let pp_tvar id =
let s = string_of_id id in
@@ -52,70 +49,12 @@ let pp_abst = function
str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
str " ->" ++ spc ()
-let pp_apply st par args = match args with
- | [] -> st
- | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
-
-let pr_binding = function
- | [] -> mt ()
- | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
-
-let space_if = function true -> str " " | false -> mt ()
-
-let sec_space_if = function true -> spc () | false -> mt ()
-
-let fnl2 () = fnl () ++ fnl ()
-
let pp_parameters l =
(pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
let pp_string_parameters l =
(pp_boxed_tuple str l ++ space_if (l<>[]))
-(*s Generic renaming issues. *)
-
-let rec rename_id id avoid =
- if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
-
-let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
-let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
-
-(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *)
-let pr_upper_id id = str (String.capitalize (string_of_id id))
-
-(*s de Bruijn environments for programs *)
-
-type env = identifier list * Idset.t
-
-let rec rename_vars avoid = function
- | [] ->
- [], avoid
- | id :: idl when id == dummy_name ->
- (* we don't rename dummy binders *)
- let (idl', avoid') = rename_vars avoid idl in
- (id :: idl', avoid')
- | id :: idl ->
- let (idl, avoid) = rename_vars avoid idl in
- let id = rename_id (lowercase_id id) avoid in
- (id :: idl, Idset.add id avoid)
-
-let rename_tvars avoid l =
- let rec rename avoid = function
- | [] -> [],avoid
- | id :: idl ->
- let id = rename_id (lowercase_id id) avoid in
- let idl, avoid = rename (Idset.add id avoid) idl in
- (id :: idl, avoid) in
- fst (rename avoid l)
-
-let push_vars ids (db,avoid) =
- let ids',avoid' = rename_vars avoid ids in
- ids', (ids' @ db, avoid')
-
-let get_db_name n (db,_) =
- let id = List.nth db (pred n) in
- if id = dummy_name then id_of_string "__" else id
-
(*s Ocaml renaming issues. *)
let keywords =
@@ -130,7 +69,7 @@ let keywords =
"land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
Idset.empty
-let preamble _ used_modules (mldummy,tdummy,tunknown) _ =
+let preamble _ used_modules usf =
let pp_mp = function
| MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
| _ -> assert false
@@ -139,15 +78,15 @@ let preamble _ used_modules (mldummy,tdummy,tunknown) _ =
++
(if used_modules = [] then mt () else fnl ())
++
- (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt())
+ (if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl() else mt())
++
- (if mldummy then
+ (if usf.mldummy then
str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl ()
else mt ())
++
- (if tdummy || tunknown || mldummy then fnl () else mt ())
+ (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
-let preamble_sig _ used_modules (_,tdummy,tunknown) =
+let sig_preamble _ used_modules usf =
let pp_mp = function
| MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
| _ -> assert false
@@ -156,18 +95,16 @@ let preamble_sig _ used_modules (_,tdummy,tunknown) =
++
(if used_modules = [] then mt () else fnl ())
++
- (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl ()
+ (if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl ()
else mt())
-(*s The pretty-printing functor. *)
-
-module Make = functor(P : Mlpp_param) -> struct
+(*s The pretty-printer for Ocaml syntax*)
-let local_mpl = ref ([] : module_path list)
-
-let pp_global r =
+let pp_global k r =
if is_inline_custom r then str (find_custom r)
- else P.pp_global !local_mpl r
+ else str (Common.pp_global k r)
+
+let pp_modname mp = str (Common.pp_module mp)
let is_infix r =
is_inline_custom r &&
@@ -177,8 +114,6 @@ let get_infix r =
let s = find_custom r in
String.sub s 1 (String.length s - 2)
-let empty_env () = [], P.globals ()
-
exception NoRecord
let find_projections = function Record l -> l | _ -> raise NoRecord
@@ -199,12 +134,12 @@ let rec pp_type par vl t =
pp_par par
(pp_rec true a1 ++ spc () ++ str (get_infix r) ++ spc () ++
pp_rec true a2)
- | Tglob (r,[]) -> pp_global r
+ | Tglob (r,[]) -> pp_global Type r
| Tglob (r,l) ->
if r = IndRef (kn_sig,0) then
pp_tuple_light pp_rec l
else
- pp_tuple_light pp_rec l ++ spc () ++ pp_global r
+ pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
@@ -256,18 +191,18 @@ let rec pp_expr par env args =
(try
let args = list_skipn (projection_arity r) args in
let record = List.hd args in
- pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
- with _ -> apply (pp_global r))
+ pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
+ with _ -> apply (pp_global Term r))
| MLcons (Coinductive,r,[]) ->
assert (args=[]);
- pp_par par (str "lazy " ++ pp_global r)
+ pp_par par (str "lazy " ++ pp_global Cons r)
| MLcons (Coinductive,r,args') ->
assert (args=[]);
let tuple = pp_tuple (pp_expr true env []) args' in
- pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
+ pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
| MLcons (_,r,[]) ->
assert (args=[]);
- pp_global r
+ pp_global Cons r
| MLcons (Record projs, r, args') ->
assert (args=[]);
pp_record_pat (projs, List.map (pp_expr true env []) args')
@@ -279,7 +214,7 @@ let rec pp_expr par env args =
| MLcons (_,r,args') ->
assert (args=[]);
let tuple = pp_tuple (pp_expr true env []) args' in
- pp_par par (pp_global r ++ spc () ++ tuple)
+ pp_par par (pp_global Cons r ++ spc () ++ tuple)
| MLcase ((i,factors), t, pv) ->
let expr = if i = Coinductive then
(str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
@@ -293,7 +228,7 @@ let rec pp_expr par env args =
match c with
| MLrel i when i <= n ->
apply (pp_par par' (pp_expr true env [] t ++ str "." ++
- pp_global (List.nth projs (n-i))))
+ pp_global Term (List.nth projs (n-i))))
| MLapp (MLrel i, a) when i <= n ->
if List.exists (ast_occurs_itvl 1 n) a
then raise NoRecord
@@ -301,7 +236,7 @@ let rec pp_expr par env args =
let ids,env' = push_vars (List.rev ids) env in
(pp_apply
(pp_expr true env [] t ++ str "." ++
- pp_global (List.nth projs (n-i)))
+ pp_global Term (List.nth projs (n-i)))
par ((List.map (pp_expr true env' []) a) @ args))
| _ -> raise NoRecord
with NoRecord ->
@@ -336,7 +271,7 @@ let rec pp_expr par env args =
and pp_record_pat (projs, args) =
str "{ " ++
prlist_with_sep (fun () -> str ";" ++ spc ())
- (fun (r,a) -> pp_global r ++ str " =" ++ spc () ++ a)
+ (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a)
(List.combine projs args) ++
str " }"
@@ -350,8 +285,8 @@ and pp_one_pat env i (r,ids,t) =
(match List.rev ids with
| [i1;i2] when is_infix r ->
pr_id i1 ++ str " " ++ str (get_infix r) ++ str " " ++ pr_id i2
- | [] -> pp_global r
- | ids -> pp_global r ++ str " " ++ pp_boxed_tuple pr_id ids),
+ | [] -> pp_global Cons r
+ | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids),
expr
and pp_pat env (info,factors) pv =
@@ -369,23 +304,23 @@ and pp_pat env (info,factors) pv =
let t = ast_lift (-List.length ids) t in
hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t)
-and pp_function env f t =
+and pp_function env t =
let bl,t' = collect_lams t in
let bl,env' = push_vars bl env in
match t' with
| MLcase(i,MLrel 1,pv) when fst i=Standard ->
if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
- (f ++ pr_binding (List.rev (List.tl bl)) ++
- str " = function" ++ fnl () ++
- v 0 (str " | " ++ pp_pat env' i pv))
+ pr_binding (List.rev (List.tl bl)) ++
+ str " = function" ++ fnl () ++
+ v 0 (str " | " ++ pp_pat env' i pv)
else
- (f ++ pr_binding (List.rev bl) ++
- str " = match " ++
- pr_id (List.hd bl) ++ str " with" ++ fnl () ++
- v 0 (str " | " ++ pp_pat env' i pv))
- | _ -> (f ++ pr_binding (List.rev bl) ++
- str " =" ++ fnl () ++ str " " ++
- hov 2 (pp_expr false env' [] t'))
+ pr_binding (List.rev bl) ++
+ str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
+ v 0 (str " | " ++ pp_pat env' i pv)
+ | _ ->
+ pr_binding (List.rev bl) ++
+ str " =" ++ fnl () ++ str " " ++
+ hov 2 (pp_expr false env' [] t')
(*s names of the functions ([ids]) are already pushed in [env],
and passed here just for convenience. *)
@@ -395,54 +330,57 @@ and pp_fix par env i (ids,bl) args =
(v 0 (str "let rec " ++
prvect_with_sep
(fun () -> fnl () ++ str "and ")
- (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+ (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
(array_map2 (fun id b -> (id,b)) ids bl) ++
fnl () ++
hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
let pp_val e typ =
- str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++
- str " **)" ++ fnl2 ()
+ hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++
+ str " **)") ++ fnl2 ()
(*s Pretty-printing of [Dfix] *)
-let rec pp_Dfix init i ((rv,c,t) as fix) =
- if i >= Array.length rv then mt ()
- else
- if is_inline_custom rv.(i) then pp_Dfix init (i+1) fix
+let pp_Dfix (rv,c,t) =
+ let names = Array.map
+ (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+ in
+ let rec pp sep letand i =
+ if i >= Array.length rv then mt ()
+ else if is_inline_custom rv.(i) then pp sep letand (i+1)
else
- let e = pp_global rv.(i) in
- (if init then mt () else fnl2 ()) ++
- pp_val e t.(i) ++
- str (if init then "let rec " else "and ") ++
- (if is_custom rv.(i) then e ++ str " = " ++ str (find_custom rv.(i))
- else pp_function (empty_env ()) e c.(i)) ++
- pp_Dfix false (i+1) fix
-
+ let def =
+ if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
+ else pp_function (empty_env ()) c.(i)
+ in
+ sep () ++ pp_val names.(i) t.(i) ++
+ str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1)
+ in pp mt "let rec " 0
+
(*s Pretty-printing of inductive types declaration. *)
-let pp_equiv param_list = function
- | None -> mt ()
- | Some ip_equiv ->
- str " = " ++ pp_parameters param_list ++ pp_global (IndRef ip_equiv)
+let pp_equiv param_list name = function
+ | NoEquiv, _ -> mt ()
+ | Equiv kn, i ->
+ str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i))
+ | RenEquiv ren, _ ->
+ str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
let pp_comment s = str "(* " ++ s ++ str " *)"
-let pp_one_ind prefix ip ip_equiv pl cv =
+let pp_one_ind prefix ip_equiv pl name cnames ctyps =
let pl = rename_tvars keywords pl in
- let pp_constructor (r,l) =
- hov 2 (str " | " ++ pp_global r ++
- match l with
- | [] -> mt ()
- | _ -> (str " of " ++
- prlist_with_sep
- (fun () -> spc () ++ str "* ") (pp_type true pl) l))
+ let pp_constructor i typs =
+ (if i=0 then mt () else fnl ()) ++
+ hov 5 (str " | " ++ cnames.(i) ++
+ (if typs = [] then mt () else str " of ") ++
+ prlist_with_sep
+ (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
in
- pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++
- pp_equiv pl ip_equiv ++ str " =" ++
- if Array.length cv = 0 then str " unit (* empty inductive *)"
- else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor
- (Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv))
+ pp_parameters pl ++ str prefix ++ name ++
+ pp_equiv pl name ip_equiv ++ str " =" ++
+ if Array.length ctyps = 0 then str " unit (* empty inductive *)"
+ else fnl () ++ v 0 (prvecti pp_constructor ctyps)
let pp_logical_ind packet =
pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
@@ -452,38 +390,51 @@ let pp_logical_ind packet =
fnl ()
let pp_singleton kn packet =
+ let name = pp_global Type (IndRef (kn,0)) in
let l = rename_tvars keywords packet.ip_vars in
- hov 2 (str "type " ++ pp_parameters l ++
- pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++
+ hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
pp_comment (str "singleton inductive, whose constructor was " ++
pr_id packet.ip_consnames.(0)))
let pp_record kn projs ip_equiv packet =
- let l = List.combine projs packet.ip_types.(0) in
+ let name = pp_global Type (IndRef (kn,0)) in
+ let projnames = List.map (pp_global Term) projs in
+ let l = List.combine projnames packet.ip_types.(0) in
let pl = rename_tvars keywords packet.ip_vars in
- str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++
- pp_equiv pl ip_equiv ++ str " = { "++
+ str "type " ++ pp_parameters pl ++ name ++
+ pp_equiv pl name ip_equiv ++ str " = { "++
hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ())
- (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l)
+ (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l)
++ str " }"
-let pp_coind ip pl =
- let r = IndRef ip in
+let pp_coind pl name =
let pl = rename_tvars keywords pl in
- pp_parameters pl ++ pp_global r ++ str " = " ++
- pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" ++
+ pp_parameters pl ++ name ++ str " = " ++
+ pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++
fnl() ++ str "and "
let pp_ind co kn ind =
let prefix = if co then "__" else "" in
let some = ref false in
let init= ref (str "type ") in
+ let names =
+ Array.mapi (fun i p -> if p.ip_logical then mt () else
+ pp_global Type (IndRef (kn,i)))
+ ind.ind_packets
+ in
+ let cnames =
+ Array.mapi
+ (fun i p -> if p.ip_logical then [||] else
+ Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1)))
+ p.ip_types)
+ ind.ind_packets
+ in
let rec pp i =
if i >= Array.length ind.ind_packets then mt ()
else
let ip = (kn,i) in
- let ip_equiv = option_map (fun kn -> (kn,i)) ind.ind_equiv in
+ let ip_equiv = ind.ind_equiv, 0 in
let p = ind.ind_packets.(i) in
if is_custom (IndRef ip) then pp (i+1)
else begin
@@ -494,8 +445,9 @@ let pp_ind co kn ind =
begin
init := (fnl () ++ str "and ");
s ++
- (if co then pp_coind ip p.ip_vars else mt ())
- ++ pp_one_ind prefix ip ip_equiv p.ip_vars p.ip_types ++
+ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
+ pp_one_ind
+ prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
pp (i+1)
end
end
@@ -510,159 +462,215 @@ let pp_mind kn i =
| Singleton -> pp_singleton kn i.ind_packets.(0)
| Coinductive -> pp_ind true kn i
| Record projs ->
- let ip_equiv = option_map (fun kn -> (kn,0)) i.ind_equiv in
- pp_record kn projs ip_equiv i.ind_packets.(0)
+ pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0)
| Standard -> pp_ind false kn i
-let pp_decl mpl =
- local_mpl := mpl;
- function
+let pp_decl = function
+ | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
+ | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"
| Dind (kn,i) -> pp_mind kn i
- | Dtype (r, l, t) ->
- if is_inline_custom r then failwith "empty phrase"
- else
- let pp_r = pp_global r in
- let l = rename_tvars keywords l in
- let ids, def = try
+ | Dtype (r, l, t) ->
+ let name = pp_global Type r in
+ let l = rename_tvars keywords l in
+ let ids, def =
+ try
let ids,s = find_type_custom r in
pp_string_parameters ids, str "=" ++ spc () ++ str s
- with not_found ->
+ with Not_found ->
pp_parameters l,
if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
else str "=" ++ spc () ++ pp_type false l t
- in
- hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++
- spc () ++ def)
+ in
+ hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
| Dterm (r, a, t) ->
- if is_inline_custom r then failwith "empty phrase"
- else
- let e = pp_global r in
- pp_val e t ++
- hov 0
- (str "let " ++
- if is_custom r then
- e ++ str " = " ++ str (find_custom r)
- else if is_projection r then
- let s = prvecti (fun _ -> str)
- (Array.make (projection_arity r) " _") in
- e ++ s ++ str " x = x." ++ e
- else pp_function (empty_env ()) e a)
+ let def =
+ if is_custom r then str (" = " ^ find_custom r)
+ else if is_projection r then
+ (prvect str (Array.make (projection_arity r) " _")) ++
+ str " x = x."
+ else pp_function (empty_env ()) a
+ in
+ let name = pp_global Term r in
+ let postdef = if is_projection r then name else mt () in
+ pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef)
| Dfix (rv,defs,typs) ->
- pp_Dfix true 0 (rv,defs,typs)
-
-let pp_spec mpl =
- local_mpl := mpl;
- function
- | Sind (kn,i) -> pp_mind kn i
- | Sval (r,t) ->
- if is_inline_custom r then failwith "empty phrase"
- else
- hov 2 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++
- pp_type false [] t)
- | Stype (r,vl,ot) ->
- if is_inline_custom r then failwith "empty phrase"
- else
- let l = rename_tvars keywords vl in
- let ids, def =
- try
- let ids, s = find_type_custom r in
- pp_string_parameters ids, str "= " ++ str s
- with not_found ->
- let ids = pp_parameters l in
- match ot with
- | None -> ids, mt ()
- | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)"
- | Some t -> ids, str "=" ++ spc () ++ pp_type false l t
- in
- hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def)
-
-let rec pp_specif mpl = function
- | (_,Spec s) -> pp_spec mpl s
+ pp_Dfix (rv,defs,typs)
+
+let pp_alias_decl ren = function
+ | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
+ | Dtype (r, l, _) ->
+ let name = pp_global Type r in
+ let l = rename_tvars keywords l in
+ let ids = pp_parameters l in
+ hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
+ str (ren^".") ++ name)
+ | Dterm (r, a, t) ->
+ let name = pp_global Term r in
+ hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
+ | Dfix (rv, _, _) ->
+ prvecti (fun i r -> if is_inline_custom r then mt () else
+ let name = pp_global Term r in
+ hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
+ fnl ())
+ rv
+
+let pp_spec = function
+ | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
+ | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
+ | Sind (kn,i) -> pp_mind kn i
+ | Sval (r,t) ->
+ let def = pp_type false [] t in
+ let name = pp_global Term r in
+ hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
+ | Stype (r,vl,ot) ->
+ let name = pp_global Type r in
+ let l = rename_tvars keywords vl in
+ let ids, def =
+ try
+ let ids, s = find_type_custom r in
+ pp_string_parameters ids, str "= " ++ str s
+ with Not_found ->
+ let ids = pp_parameters l in
+ match ot with
+ | None -> ids, mt ()
+ | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)"
+ | Some t -> ids, str "=" ++ spc () ++ pp_type false l t
+ in
+ hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
+
+let pp_alias_spec ren = function
+ | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
+ | Stype (r,l,_) ->
+ let name = pp_global Type r in
+ let l = rename_tvars keywords l in
+ let ids = pp_parameters l in
+ hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
+ str (ren^".") ++ name)
+ | Sval _ -> assert false
+
+let rec pp_specif = function
+ | (_,Spec (Sval _ as s)) -> pp_spec s
+ | (l,Spec s) ->
+ (try
+ let ren = Common.check_duplicate (top_visible_mp ()) l in
+ hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++
+ fnl () ++ str "end" ++ fnl () ++
+ pp_alias_spec ren s
+ with Not_found -> pp_spec s)
| (l,Smodule mt) ->
- hov 1
- (str "module " ++
- P.pp_module mpl (MPdot (List.hd mpl, l)) ++
- str " : " ++ fnl () ++ pp_module_type mpl None (* (Some l) *) mt)
+ let def = pp_module_type (Some l) mt in
+ let def' = pp_module_type (Some l) mt in
+ let name = pp_modname (MPdot (top_visible_mp (), l)) in
+ hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
+ (try
+ let ren = Common.check_duplicate (top_visible_mp ()) l in
+ fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
+ with Not_found -> Pp.mt ())
| (l,Smodtype mt) ->
- hov 1
- (str "module type " ++
- P.pp_module mpl (MPdot (List.hd mpl, l)) ++
- str " = " ++ fnl () ++ pp_module_type mpl None mt)
-
-and pp_module_type mpl ol = function
+ let def = pp_module_type None mt in
+ let name = pp_modname (MPdot (top_visible_mp (), l)) in
+ hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
+ (try
+ let ren = Common.check_duplicate (top_visible_mp ()) l in
+ fnl () ++ str ("module type "^ren^" = ") ++ name
+ with Not_found -> Pp.mt ())
+
+and pp_module_type ol = function
| MTident kn ->
- let mp,_,l = repr_kn kn in P.pp_module mpl (MPdot (mp,l))
+ let mp,_,l = repr_kn kn in pp_modname (MPdot (mp,l))
| MTfunsig (mbid, mt, mt') ->
- str "functor (" ++
- P.pp_module mpl (MPbound mbid) ++
- str ":" ++
- pp_module_type mpl None mt ++
- str ") ->" ++ fnl () ++
- pp_module_type mpl None mt'
+ let name = pp_modname (MPbound mbid) in
+ let typ = pp_module_type None mt in
+ let def = pp_module_type None mt' in
+ str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (msid, sign) ->
- let mpl = match ol, mpl with
- | None, _ -> (MPself msid) :: mpl
- | Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl
- | _ -> assert false
- in
- let l = map_succeed (pp_specif mpl) sign in
+ let tvm = top_visible_mp () in
+ option_iter (fun l -> add_subst msid (MPdot (tvm, l))) ol;
+ let mp = MPself msid in
+ push_visible mp;
+ let l = map_succeed pp_specif sign in
+ pop_visible ();
str "sig " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
fnl () ++ str "end"
let is_short = function MEident _ | MEapply _ -> true | _ -> false
-let rec pp_structure_elem mpl = function
- | (_,SEdecl d) -> pp_decl mpl d
+let rec pp_structure_elem = function
+ | (l,SEdecl d) ->
+ (try
+ let ren = Common.check_duplicate (top_visible_mp ()) l in
+ hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++
+ fnl () ++ str "end" ++ fnl () ++
+ pp_alias_decl ren d
+ with Not_found -> pp_decl d)
| (l,SEmodule m) ->
+ let def = pp_module_expr (Some l) m.ml_mod_expr in
+ let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1
- (str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++
- (*i if you want signatures everywhere: i*)
- (*i str " :" ++ fnl () ++ i*)
- (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*)
- str " = " ++
- (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++
- pp_module_expr mpl (Some l) m.ml_mod_expr)
+ (str "module " ++ name ++ str " = " ++
+ (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++
+ (try
+ let ren = Common.check_duplicate (top_visible_mp ()) l in
+ fnl () ++ str ("module "^ren^" = ") ++ name
+ with Not_found -> mt ())
| (l,SEmodtype m) ->
- hov 1
- (str "module type " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++
- str " = " ++ fnl () ++ pp_module_type mpl None m)
-
-and pp_module_expr mpl ol = function
- | MEident mp' -> P.pp_module mpl mp'
+ let def = pp_module_type None m in
+ let name = pp_modname (MPdot (top_visible_mp (), l)) in
+ hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
+ (try
+ let ren = Common.check_duplicate (top_visible_mp ()) l in
+ fnl () ++ str ("module type "^ren^" = ") ++ name
+ with Not_found -> mt ())
+
+and pp_module_expr ol = function
+ | MEident mp' -> pp_modname mp'
| MEfunctor (mbid, mt, me) ->
- str "functor (" ++
- P.pp_module mpl (MPbound mbid) ++
- str ":" ++
- pp_module_type mpl None mt ++
- str ") ->" ++ fnl () ++
- pp_module_expr mpl None me
+ let name = pp_modname (MPbound mbid) in
+ let typ = pp_module_type None mt in
+ let def = pp_module_expr None me in
+ str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MEapply (me, me') ->
- pp_module_expr mpl None me ++ str "(" ++
- pp_module_expr mpl None me' ++ str ")"
+ pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")"
| MEstruct (msid, sel) ->
- let mpl = match ol, mpl with
- | None, _ -> (MPself msid) :: mpl
- | Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl
- | _ -> assert false
- in
- let l = map_succeed (pp_structure_elem mpl) sel in
+ let tvm = top_visible_mp () in
+ let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
+ push_visible mp;
+ let l = map_succeed pp_structure_elem sel in
+ pop_visible ();
str "struct " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
fnl () ++ str "end"
let pp_struct s =
- let pp mp s = pp_structure_elem [mp] s ++ fnl2 () in
+ let pp mp s =
+ push_visible mp;
+ let p = pp_structure_elem s ++ fnl2 () in
+ pop_visible (); p
+ in
prlist (fun (mp,sel) -> prlist identity (map_succeed (pp mp) sel)) s
let pp_signature s =
- let pp mp s = pp_specif [mp] s ++ fnl2 () in
+ let pp mp s =
+ push_visible mp;
+ let p = pp_specif s ++ fnl2 () in
+ pop_visible (); p
+ in
prlist (fun (mp,sign) -> prlist identity (map_succeed (pp mp) sign)) s
-let pp_decl mpl d =
- try pp_decl mpl d with Failure "empty phrase" -> mt ()
-
-end
-
+let pp_decl d =
+ try pp_decl d with Failure "empty phrase" -> mt ()
+
+let ocaml_descr = {
+ keywords = keywords;
+ file_suffix = ".ml";
+ capital_file = false;
+ preamble = preamble;
+ pp_struct = pp_struct;
+ sig_suffix = Some ".mli";
+ sig_preamble = sig_preamble;
+ pp_sig = pp_signature;
+ pp_decl = pp_decl;
+}
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 7a13590e2..c127fc1d1 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -8,47 +8,5 @@
(*i $Id$ i*)
-(*s Some utility functions to be reused in module [Haskell]. *)
-
-open Pp
-open Names
-open Libnames
-open Miniml
-
-val pp_par : bool -> std_ppcmds -> std_ppcmds
-val pp_abst : identifier list -> std_ppcmds
-val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
-val pr_binding : identifier list -> std_ppcmds
-
-val rename_id : identifier -> Idset.t -> identifier
-
-val lowercase_id : identifier -> identifier
-val uppercase_id : identifier -> identifier
-
-val pr_upper_id : identifier -> std_ppcmds
-
-type env = identifier list * Idset.t
-
-val rename_vars: Idset.t -> identifier list -> env
-val rename_tvars: Idset.t -> identifier list -> identifier list
-val push_vars : identifier list -> env -> identifier list * env
-val get_db_name : int -> env -> identifier
-
-val keywords : Idset.t
-
-val preamble :
- extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
-
-val preamble_sig :
- extraction_params -> module_path list -> bool*bool*bool -> std_ppcmds
-
-(*s Production of Ocaml syntax. We export both a functor to be used for
- extraction in the Coq toplevel and a function to extract some
- declarations to a file. *)
-
-module Make : functor(P : Mlpp_param) -> Mlpp
-
-
-
-
+val ocaml_descr : Miniml.language_descr
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 0b358f77d..5048002d0 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -18,7 +18,7 @@ open Libnames
open Miniml
open Mlutil
open Table
-open Ocaml
+open Common
(*s Scheme renaming issues. *)
@@ -29,14 +29,14 @@ let keywords =
"error"; "delay"; "force"; "_"; "__"]
Idset.empty
-let preamble _ _ (mldummy,_,_) _ =
+let preamble _ _ usf =
str ";; This extracted scheme code relies on some additional macros" ++
fnl () ++
str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++
fnl () ++
str "(load \"macros_extr.scm\")" ++
fnl () ++ fnl () ++
- (if mldummy then
+ (if usf.mldummy then
str "(define __ (lambda (_) __))"
++ fnl () ++ fnl()
else mt ())
@@ -62,12 +62,9 @@ let pp_apply st _ = function
| args -> hov 2 (paren (str "@ " ++ st ++
(prlist (fun x -> spc () ++ x) args)))
-(*s The pretty-printing functor. *)
+(*s The pretty-printer for Scheme syntax *)
-module Make = functor(P : Mlpp_param) -> struct
-
-let pp_global r = P.pp_global [initial_path] r
-let empty_env () = [], P.globals()
+let pp_global k r = str (Common.pp_global k r)
(*s Pretty-printing of expressions. *)
@@ -95,12 +92,12 @@ let rec pp_expr env args =
(pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1))
++ spc () ++ hov 0 (pp_expr env' [] a2)))))
| MLglob r ->
- apply (pp_global r)
+ apply (pp_global Term r)
| MLcons (i,r,args') ->
assert (args=[]);
let st =
str "`" ++
- paren (pp_global r ++
+ paren (pp_global Cons r ++
(if args' = [] then mt () else spc ()) ++
prlist_with_sep spc (pp_cons_args env) args')
in
@@ -125,7 +122,7 @@ let rec pp_expr env args =
and pp_cons_args env = function
| MLcons (i,r,args) when i<>Coinductive ->
- paren (pp_global r ++
+ paren (pp_global Cons r ++
(if args = [] then mt () else spc ()) ++
prlist_with_sep spc (pp_cons_args env) args)
| e -> str "," ++ pp_expr env [] e
@@ -137,7 +134,7 @@ and pp_one_pat env (r,ids,t) =
if ids = [] then mt ()
else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
in
- (pp_global r ++ args), (pp_expr env' [] t)
+ (pp_global Cons r ++ args), (pp_expr env' [] t)
and pp_pat env pv =
prvect_with_sep fnl
@@ -160,11 +157,11 @@ and pp_fix env j (ids,bl) args =
(*s Pretty-printing of a declaration. *)
-let pp_decl _ = function
+let pp_decl = function
| Dind _ -> mt ()
| Dtype _ -> mt ()
| Dfix (rv, defs,_) ->
- let ppv = Array.map pp_global rv in
+ let ppv = Array.map (pp_global Term) rv in
prvect_with_sep fnl
(fun (pi,ti) ->
hov 2
@@ -177,23 +174,33 @@ let pp_decl _ = function
if is_inline_custom r then mt ()
else
if is_custom r then
- hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+ hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
str (find_custom r))) ++ fnl () ++ fnl ()
else
- hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+ hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
-let pp_structure_elem mp = function
- | (l,SEdecl d) -> pp_decl mp d
+let pp_structure_elem = function
+ | (l,SEdecl d) -> pp_decl d
| (l,SEmodule m) ->
failwith "TODO: Scheme extraction of modules not implemented yet"
| (l,SEmodtype m) ->
failwith "TODO: Scheme extraction of modules not implemented yet"
let pp_struct =
- prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel)
-
-let pp_signature s = assert false
-
-end
-
+ let pp_sel (mp,sel) =
+ push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p
+ in
+ prlist pp_sel
+
+let scheme_descr = {
+ keywords = keywords;
+ file_suffix = ".scm";
+ capital_file = false;
+ preamble = preamble;
+ pp_struct = pp_struct;
+ sig_suffix = None;
+ sig_preamble = (fun _ _ _ -> mt ());
+ pp_sig = (fun _ -> mt ());
+ pp_decl = pp_decl;
+}
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index bded1a8a8..573bb9cef 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -8,20 +8,4 @@
(*i $Id$ i*)
-(*s Some utility functions to be reused in module [Haskell]. *)
-
-open Pp
-open Miniml
-open Names
-
-val keywords : Idset.t
-
-val preamble :
- extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
-
-module Make : functor(P : Mlpp_param) -> Mlpp
-
-
-
-
-
+val scheme_descr : Miniml.language_descr
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 204319099..7a8ff95ed 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -20,37 +20,49 @@ open Util
open Pp
open Miniml
-(*S Utilities concerning [module_path] and [kernel_names] *)
+(*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
-let occur_kn_in_ref kn =
- function
+let occur_kn_in_ref kn = function
| IndRef (kn',_)
| ConstructRef ((kn',_),_) -> kn = kn'
| ConstRef _ -> false
| VarRef _ -> assert false
-
-let modpath_of_r r = match r with
- | ConstRef kn -> con_modpath kn
- | IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> modpath kn
- | VarRef _ -> assert false
-
-let label_of_r r = match r with
- | ConstRef kn -> con_label kn
- | IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> label kn
- | VarRef _ -> assert false
-
-let current_toplevel () = fst (Lib.current_prefix ())
+
+let modpath_of_r = function
+ | ConstRef kn -> con_modpath kn
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> modpath kn
+ | VarRef _ -> assert false
+
+let label_of_r = function
+ | ConstRef kn -> con_label kn
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> label kn
+ | VarRef _ -> assert false
let rec base_mp = function
| MPdot (mp,l) -> base_mp mp
| mp -> mp
+let rec mp_length = function
+ | MPdot (mp, _) -> 1 + (mp_length mp)
+ | _ -> 1
+
let is_modfile = function
| MPfile _ -> true
| _ -> false
+let string_of_modfile = function
+ | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
+ | _ -> assert false
+
+let rec modfile_of_mp = function
+ | (MPfile _) as mp -> mp
+ | MPdot (mp,_) -> modfile_of_mp mp
+ | _ -> raise Not_found
+
+let current_toplevel () = fst (Lib.current_prefix ())
+
let is_toplevel mp =
mp = initial_path || mp = current_toplevel ()
@@ -60,8 +72,56 @@ let at_toplevel mp =
let visible_kn kn = at_toplevel (base_mp (modpath kn))
let visible_con kn = at_toplevel (base_mp (con_modpath kn))
+let rec prefixes_mp mp = match mp with
+ | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
+ | _ -> MPset.singleton mp
+
+let rec get_nth_label_mp n mp = match mp with
+ | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
+ | _ -> failwith "get_nth_label: not enough MPdot"
+
+let get_nth_label n r =
+ if n=0 then label_of_r r else get_nth_label_mp n (modpath_of_r r)
+
+let rec common_prefix prefixes_mp1 mp2 =
+ if MPset.mem mp2 prefixes_mp1 then mp2
+ else match mp2 with
+ | MPdot (mp,_) -> common_prefix prefixes_mp1 mp
+ | _ -> raise Not_found
+
+let common_prefix_from_list mp0 mpl =
+ let prefixes_mp0 = prefixes_mp mp0 in
+ let rec f = function
+ | [] -> raise Not_found
+ | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
+ in f mpl
+
+let rec parse_labels ll = function
+ | MPdot (mp,l) -> parse_labels (l::ll) mp
+ | mp -> mp,ll
+
+let labels_of_mp mp = parse_labels [] mp
+
+let labels_of_ref r =
+ let mp,_,l =
+ match r with
+ ConstRef con -> repr_con con
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> repr_kn kn
+ | VarRef _ -> assert false
+ in
+ parse_labels [l] mp
+
+let rec add_labels_mp mp = function
+ | [] -> mp
+ | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
+
+
(*S The main tables: constants, inductives, records, ... *)
+(* Theses tables are not registered within coq save/undo mechanism
+ since we reset their contents at each run of Extraction *)
+
(*s Constants tables. *)
let terms = ref (Cmap.empty : ml_decl Cmap.t)
@@ -109,11 +169,26 @@ let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
let is_projection r = Refmap.mem r !projs
let projection_arity r = Refmap.find r !projs
+(*s Table of used axioms *)
+
+let info_axioms = ref Refset.empty
+let log_axioms = ref Refset.empty
+let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty
+let add_info_axiom r = info_axioms := Refset.add r !info_axioms
+let add_log_axiom r = log_axioms := Refset.add r !log_axioms
+
+(*s Extraction mode: modular or monolithic *)
+
+let modular_ref = ref false
+
+let set_modular b = modular_ref := b
+let modular () = !modular_ref
+
(*s Tables synchronization. *)
let reset_tables () =
init_terms (); init_types (); init_inductives (); init_recursors ();
- init_projs ()
+ init_projs (); init_axioms ()
(*s Printing. *)
@@ -146,21 +221,34 @@ let pr_long_global r =
let err s = errorlabstrm "Extraction" s
+let warning_axioms () =
+ let info_axioms = Refset.elements !info_axioms in
+ if info_axioms = [] then ()
+ else begin
+ let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
+ msg_warning
+ (str ("The following "^s^" must be realized in the extracted code:")
+ ++ hov 1 (spc () ++ prlist_with_sep spc pr_global info_axioms)
+ ++ str "." ++ fnl ())
+ end;
+ let log_axioms = Refset.elements !log_axioms in
+ if log_axioms = [] then ()
+ else begin
+ let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
+ in
+ msg_warning
+ (str ("The following logical "^s^" encountered:") ++
+ hov 1 (spc () ++ prlist_with_sep spc pr_global log_axioms ++ str ".\n") ++
+ str "Having invalid logical axiom in the environment when extracting" ++
+ spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
+ fnl ())
+ end
+
let error_axiom_scheme r i =
err (str "The type scheme axiom " ++ spc () ++
pr_global r ++ spc () ++ str "needs " ++ pr_int i ++
str " type variable(s).")
-let warning_info_ax r =
- msg_warning (str "You must realize axiom " ++
- pr_global r ++ str " in the extracted code.")
-
-let warning_log_ax r =
- msg_warning (str "This extraction depends on logical axiom" ++ spc () ++
- pr_global r ++ str "." ++ spc() ++
- str "Having false logical axiom in the environment when extracting" ++
- spc () ++ str "may lead to incorrect or non-terminating ML terms.")
-
let check_inside_module () =
if Lib.is_modtype () then
err (str "You can't do that within a Module Type." ++ fnl () ++
@@ -186,15 +274,11 @@ let error_nb_cons () =
let error_module_clash s =
err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++
- str "This is not allowed in ML. Please do some renaming first.")
+ str "This is not supported yet. Please do some renaming first.")
let error_unknown_module m =
err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
-let error_toplevel () =
- err (str "Toplevel pseudo-ML language can be used only at Coq toplevel.\n" ++
- str "You should use Extraction Language Ocaml or Haskell before.")
-
let error_scheme () =
err (str "No Scheme modular extraction available yet.")
@@ -203,9 +287,11 @@ let error_not_visible r =
str "For example, it may be inside an applied functor." ++
str "Use Recursive Extraction to get the whole environment.")
-let error_MPfile_as_mod d =
- err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
- "Extraction cannot currently deal with this situation.\n"))
+let error_MPfile_as_mod mp =
+ err (str ("The whole file "^(string_of_modfile mp)^
+ ".v is used somewhere as a module.\n"^
+ "Monolithic Extraction cannot deal with this situation.\n"^
+ "Please use (Recursive) Extraction Library instead.\n"))
let error_record r =
err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
@@ -216,8 +302,16 @@ let check_loaded_modfile mp = match base_mp mp with
err (str ("Please load library "^(string_of_dirpath dp^" first.")))
| _ -> ()
+let info_file f =
+ Options.if_verbose message
+ ("The file "^f^" has been created by extraction.")
+
+
(*S The Extraction auxiliary commands *)
+(* The objects defined below should survive an arbitrary time,
+ so we register them to coq save/undo mechanism. *)
+
(*s Extraction AutoInline *)
let auto_inline_ref = ref true
@@ -305,7 +399,7 @@ let _ = declare_int_option
(*s Extraction Lang *)
-type lang = Ocaml | Haskell | Scheme | Toplevel
+type lang = Ocaml | Haskell | Scheme
let lang_ref = ref Ocaml
@@ -327,7 +421,6 @@ let _ = declare_summary "Extraction Lang"
let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
-
(*s Extraction Inline/NoInline *)
let empty_inline_table = (Refset.empty,Refset.empty)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 55402d94a..304e374b5 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -14,39 +14,49 @@ open Miniml
open Declarations
val id_of_global : global_reference -> identifier
+val pr_long_global : global_reference -> Pp.std_ppcmds
+
(*s Warning and Error messages. *)
+val warning_axioms : unit -> unit
val error_axiom_scheme : global_reference -> int -> 'a
-val warning_info_ax : global_reference -> unit
-val warning_log_ax : global_reference -> unit
val error_constant : global_reference -> 'a
val error_inductive : global_reference -> 'a
val error_nb_cons : unit -> 'a
val error_module_clash : string -> 'a
val error_unknown_module : qualid -> 'a
-val error_toplevel : unit -> 'a
val error_scheme : unit -> 'a
val error_not_visible : global_reference -> 'a
-val error_MPfile_as_mod : dir_path -> 'a
+val error_MPfile_as_mod : module_path -> 'a
val error_record : global_reference -> 'a
val check_inside_module : unit -> unit
val check_inside_section : unit -> unit
val check_loaded_modfile : module_path -> unit
-(*s utilities concerning [module_path]. *)
+val info_file : string -> unit
+
+(*s utilities about [module_path] and [kernel_names] and [global_reference] *)
val occur_kn_in_ref : kernel_name -> global_reference -> bool
val modpath_of_r : global_reference -> module_path
val label_of_r : global_reference -> label
-
val current_toplevel : unit -> module_path
val base_mp : module_path -> module_path
-val is_modfile : module_path -> bool
+val is_modfile : module_path -> bool
+val string_of_modfile : module_path -> string
val is_toplevel : module_path -> bool
val at_toplevel : module_path -> bool
val visible_kn : kernel_name -> bool
val visible_con : constant -> bool
+val mp_length : module_path -> int
+val prefixes_mp : module_path -> MPset.t
+val modfile_of_mp : module_path -> module_path
+val common_prefix_from_list : module_path -> module_path list -> module_path
+val add_labels_mp : module_path -> label list -> module_path
+val get_nth_label_mp : int -> module_path -> label
+val get_nth_label : int -> global_reference -> label
+val labels_of_ref : global_reference -> module_path * label list
(*s Some table-related operations *)
@@ -66,6 +76,9 @@ val add_projection : int -> constant -> unit
val is_projection : global_reference -> bool
val projection_arity : global_reference -> int
+val add_info_axiom : global_reference -> unit
+val add_log_axiom : global_reference -> unit
+
val reset_tables : unit -> unit
(*s AutoInline parameter *)
@@ -95,9 +108,14 @@ val optims : unit -> opt_flag
(*s Target language. *)
-type lang = Ocaml | Haskell | Scheme | Toplevel
+type lang = Ocaml | Haskell | Scheme
val lang : unit -> lang
+(*s Extraction mode: modular or monolithic *)
+
+val set_modular : bool -> unit
+val modular : unit -> bool
+
(*s Table for custom inlining *)
val to_inline : global_reference -> bool
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-03 04:12:11 +0000