aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--contrib/extraction/common.ml608
-rw-r--r--contrib/extraction/common.mli18
-rw-r--r--contrib/extraction/extract_env.ml58
-rw-r--r--contrib/extraction/haskell.ml7
-rw-r--r--contrib/extraction/modutil.ml59
-rw-r--r--contrib/extraction/modutil.mli8
-rw-r--r--contrib/extraction/ocaml.ml138
-rw-r--r--contrib/extraction/scheme.ml2
-rw-r--r--contrib/extraction/table.ml17
-rw-r--r--contrib/extraction/table.mli1
-rw-r--r--lib/util.ml6
11 files changed, 409 insertions, 513 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 9a06ed49e..b23bbeac4 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -60,14 +60,14 @@ let unquote s =
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 rec dottify = function
+ | [] -> assert false
+ | [s] -> s
+ | s::[""] -> s
+ | s::l -> (dottify l)^"."^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
@@ -75,9 +75,15 @@ 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))
+type kind = Term | Type | Cons | Mod
+
+let upperkind = function
+ | Type -> lang () = Haskell
+ | Term -> false
+ | Cons | Mod -> true
+let kindcase_id k id =
+ if upperkind k then uppercase_id id else lowercase_id id
(*s de Bruijn environments for programs *)
@@ -122,111 +128,109 @@ let get_db_name n (db,_) =
(*s Tables of global renamings *)
-let keywords = ref Idset.empty
-let set_keywords kws = keywords := kws
+let register_cleanup, do_cleanup =
+ let funs = ref [] in
+ (fun f -> funs:=f::!funs), (fun () -> List.iter (fun f -> f ()) !funs)
-let global_ids = ref Idset.empty
-let add_global_ids s = global_ids := Idset.add s !global_ids
-let global_ids_list () = Idset.elements !global_ids
+type phase = Pre | Impl | Intf
-let empty_env () = [], !global_ids
+let set_phase, get_phase =
+ let ph = ref Impl in ((:=) ph), (fun () -> !ph)
-let mktable () =
- let h = Hashtbl.create 97 in
- (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+let set_keywords, get_keywords =
+ let k = ref Idset.empty in
+ ((:=) k), (fun () -> !k)
-let mkset () =
- let h = Hashtbl.create 97 in
- (fun x -> Hashtbl.add h x ()), (Hashtbl.mem h), (fun () -> Hashtbl.clear h)
+let add_global_ids, get_global_ids =
+ let ids = ref Idset.empty in
+ register_cleanup (fun () -> ids := get_keywords ());
+ let add s = ids := Idset.add s !ids
+ and get () = !ids
+ in (add,get)
-let mktriset () =
+let empty_env () = [], get_global_ids ()
+
+let mktable autoclean =
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)
+ if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
+ (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
-(* For each [global_reference], this table will contain the different parts
- of its renaming, in [string list] form. *)
-let add_renaming, get_renaming, clear_renaming = mktable ()
+(* A table recording objects in the first level of all MPfile *)
-(* Idem for [module_path]. *)
-let add_mp_renaming, get_mp_renaming, clear_mp_renaming = mktable ()
+let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
+ mktable false
-(* A table for function modfstlev_rename *)
-let add_modfstlev, get_modfstlev, clear_modfstlev = mktable ()
+(*s The list of external modules that will be opened initially *)
-(* A set of all external objects that will have to be fully qualified *)
-let add_static_clash, static_clash, clear_static_clash = mkset ()
+let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
+ let m = ref MPset.empty in
+ let add mp = m:=MPset.add mp !m
+ and mem mp = MPset.mem mp !m
+ and list () = MPset.elements !m
+ and clear () = m:=MPset.empty
+ in
+ register_cleanup clear;
+ (add,mem,list,clear)
-(* 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 table indicating the visible horizon at a precise moment,
+ i.e. the stack of structures we are inside.
-type kind = Term | Type | Cons | Mod
+ - The sequence of [mp] parts should have the following form:
+ [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either
+ be a [MPdot] over the last entry, or something new, mainly
+ [MPself], or [MPfile] at the beginning.
-let add_ext_mpmem, ext_mpmem, clear_ext_mpmem = mktriset ()
-let add_loc_mpmem, loc_mpmem, clear_loc_mpmem = mktriset ()
-
-(* 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 ()
+ - The [content] part is used to recoard all the names already
+ seen at this level.
+
+ - The [subst] part is here mainly for printing signature
+ (in which names are still short, i.e. relative to a [msid]).
+*)
+
+type visible_layer = { mp : module_path;
+ content : ((kind*string),unit) Hashtbl.t }
+
+let pop_visible, push_visible, get_visible, subst_mp =
+ let vis = ref [] and sub = ref [empty_subst] in
+ register_cleanup (fun () -> vis := []; sub := [empty_subst]);
+ let pop () =
+ let v = List.hd !vis in
+ (* we save the 1st-level-content of MPfile for later use *)
+ if get_phase () = Impl && modular () && is_modfile v.mp
+ then add_mpfiles_content v.mp v.content;
+ vis := List.tl !vis;
+ sub := List.tl !sub
+ and push mp o =
+ vis := { mp = mp; content = Hashtbl.create 97 } :: !vis;
+ let s = List.hd !sub in
+ let s = match o with None -> s | Some msid -> add_msid msid mp s in
+ sub := s :: !sub
+ and get () = !vis
+ and subst mp = subst_mp (List.hd !sub) mp
+ in (pop,push,get,subst)
+
+let get_visible_mps () = List.map (function v -> v.mp) (get_visible ())
+let top_visible () = match get_visible () with [] -> assert false | v::_ -> v
+let top_visible_mp () = (top_visible ()).mp
+let add_visible ks = Hashtbl.add (top_visible ()).content ks ()
+
+(* table of local module wrappers used to provide non-ambiguous names *)
+
+let add_duplicate, check_duplicate =
+ let index = ref 0 and dups = ref Gmap.empty in
+ register_cleanup (fun () -> index := 0; dups := Gmap.empty);
+ let add mp l =
+ incr index;
+ let ren = "Coq__" ^ string_of_int (!index) in
+ dups := Gmap.add (mp,l) ren !dups
+ and check mp l = Gmap.find (subst_mp mp, l) !dups
+ in (add,check)
+
+type reset_kind = AllButExternal | Everything
+
+let reset_renaming_tables flag =
+ do_cleanup ();
+ if flag = Everything then clear_mpfiles_content ()
(*S Renaming functions *)
@@ -235,248 +239,200 @@ let reset_renaming_tables = function
with previous [Coq_id] variable, these prefixes are duplicated if already
existing. *)
-let modular_rename up id =
+let modular_rename k id =
let s = string_of_id id in
- let prefix = if up then "Coq_" else "coq_" in
- let check = if up then is_upper else is_lower in
- if not (check s) ||
- (Idset.mem id !keywords) ||
- (String.length s >= 4 && String.sub s 0 4 = prefix)
+ let prefix,is_ok =
+ if upperkind k then "Coq_",is_upper else "coq_",is_lower
+ in
+ if not (is_ok s) ||
+ (Idset.mem id (get_keywords ())) ||
+ (String.length s >= 4 && String.sub s 0 4 = prefix)
then prefix ^ s
else 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 (safe_id_of_global r))
- in
- 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 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_renaming mp =
- try get_mp_renaming mp
- with Not_found ->
- let ren = match mp with
- | _ when not (modular ()) && at_toplevel mp -> [""]
- | MPdot (mp,l) ->
- 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].
+let modfstlev_rename =
+ let add_prefixes,get_prefixes,_ = mktable true in
+ fun l ->
+ let coqid = id_of_string "Coq" in
+ let id = id_of_label l in
+ try
+ let coqset = get_prefixes id in
+ let nextcoq = next_ident_away coqid coqset in
+ add_prefixes 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_prefixes id [coqid]; "Coq_"^s)
+ else
+ (add_prefixes id []; s)
+
+(*s Creating renaming for a [module_path] : first, the real function ... *)
+
+let rec mp_renaming_fun mp = match mp with
+ | _ when not (modular ()) && at_toplevel mp -> [""]
+ | MPdot (mp,l) ->
+ let lmp = mp_renaming mp in
+ if lmp = [""] then (modfstlev_rename l)::lmp
+ else (modular_rename Mod (id_of_label l))::lmp
+ | MPself msid -> [modular_rename Mod (id_of_msid msid)]
+ | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)]
+ | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *)
+ | MPfile _ ->
+ assert (get_phase () = Pre);
+ let current_mpfile = (list_last (get_visible ())).mp in
+ if mp <> current_mpfile then mpfiles_add mp;
+ [string_of_modfile mp]
+
+(* ... and its version using a cache *)
+
+and mp_renaming =
+ let add,get,_ = mktable true in
+ fun x -> try get x with Not_found -> let y = mp_renaming_fun x in add x y; y
+
+(*s Renamings creation for a [global_reference]: we build its fully-qualified
+ name in a [string list] form (head is the short name). *)
+
+let ref_renaming_fun (k,r) =
+ let mp = subst_mp (modpath_of_r r) in
+ let l = mp_renaming mp in
+ let s =
+ if l = [""] (* this happens only at toplevel of the monolithic case *)
+ then
+ let globs = Idset.elements (get_global_ids ()) in
+ let id = next_ident_away (kindcase_id k (safe_id_of_global r)) globs in
+ string_of_id id
+ else modular_rename k (safe_id_of_global r)
+ in
+ add_global_ids (id_of_string s);
+ s::l
+
+(* Cached version of the last function *)
+
+let ref_renaming =
+ let add,get,_ = mktable true in
+ fun x -> try get x with Not_found -> let y = ref_renaming_fun x in add x y; y
+
+(* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
+ can be printed as [s] in the current context of visible
+ modules. More precisely, we check if there exists a
+ visible [mp] that contains [s].
The verification stops if we encounter [mp=mp0]. *)
-let rec clash mem mp0 s = function
+let rec clash mem mp0 ks = 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 { 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_renaming mp in
- let s = modular_rename upper (safe_id_of_global r) in
- 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 add_mpfiles mp
- with Not_found -> ()
- end;
- in
- Refset.iter (add (lang () = Haskell)) ty;
- Refset.iter (add true) co;
- Refset.iter (add false) tr;
-
- (* 2) determines the opened libraries. *)
- 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 *)
- let needs_qualify k r =
- let mp = modpath_of_r r in
- if (is_modfile mp) && mp <> current_module &&
- (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules)
- then add_static_clash r
- in
- 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 create_mono_renamings struc =
- 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_renaming mp in
- let mycase = if upper then uppercase_id else lowercase_id in
- let id =
- if l = [""] then
- next_ident_away (mycase (safe_id_of_global r)) (global_ids_list ())
- else id_of_string (modular_rename upper (safe_id_of_global r))
- in
- add_global_ids id;
- add_renaming r ((string_of_id id)::l)
- in
- 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
-
-
+ | mp :: _ when mem mp ks -> true
+ | _ :: mpl -> clash mem mp0 ks mpl
+
+let mpfiles_clash mp0 ks =
+ clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks
+ (List.rev (mpfiles_list ()))
+
+let visible_clash mp0 ks =
+ let rec clash = function
+ | [] -> false
+ | v :: _ when v.mp = mp0 -> false
+ | v :: _ when Hashtbl.mem v.content ks -> true
+ | _ :: vis -> clash vis
+ in clash (get_visible ())
+
+(* After the 1st pass, we can decide which modules will be opened initially *)
+
+let opened_libraries () =
+ if not (modular ()) then []
+ else
+ let used = mpfiles_list () in
+ let rec check_elsewhere avoid = function
+ | [] -> []
+ | mp :: mpl ->
+ let clash s = Hashtbl.mem (get_mpfiles_content mp) (Mod,s) in
+ if List.exists clash avoid
+ then check_elsewhere avoid mpl
+ else mp :: check_elsewhere (string_of_modfile mp :: avoid) mpl
+ in
+ let opened = check_elsewhere [] used in
+ mpfiles_clear ();
+ List.iter mpfiles_add opened;
+ opened
+
(*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
+(* First, a function that factorize the printing of both [global_reference]
+ and module names for ocaml. When [k=Mod] then [olab=None], otherwise it
+ contains the label of the reference to print.
+ Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *)
+
+let pp_gen k mp ls olab =
+ try (* what is the largest prefix of [mp] that belongs to [visible]? *)
+ let prefix = common_prefix_from_list mp (get_visible_mps ()) in
+ let delta = mp_length mp - mp_length prefix in
+ assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
+ let ls = list_firstn (delta + if k = Mod then 0 else 1) ls in
+ let s,ls' = list_sep_last ls in
+ (* Reference r / module path mp is of the form [<prefix>.s.<List.rev ls'>].
+ Difficulty: in ocaml the prefix part cannot be used for
+ qualification (we are inside it) and the rest of the long
+ name may be hidden.
+ Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *)
+ let k' = if ls' = [] then k else Mod in
+ if visible_clash prefix (k',s) then
+ let front = if ls' = [] && k <> Mod then [s] else ls' in
+ let lab = (* label associated with s *)
+ if delta = 0 && k <> Mod then Option.get olab
+ else get_nth_label_mp delta mp
+ in
+ try dottify (front @ [check_duplicate prefix lab])
+ with Not_found ->
+ assert (get_phase () = Pre); (* otherwise it's too late *)
+ add_duplicate prefix lab; 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
+ (* [List.rev ls] is [base_s :: s :: List.rev ls2] *)
+ let k' = if ls2 = [] then k else Mod in
+ if modular () && (mpfiles_mem base) &&
+ (not (mpfiles_clash base (k',s))) &&
+ (not (visible_clash base (k',s)))
+ then (* Standard situation of an object in another file: *)
+ (* Thanks to the "open" of this file we remove its name *)
+ dottify ls1
+ else if visible_clash base (Mod,base_s) then
+ error_module_clash base_s
+ else dottify ls
+
+let pp_global k r =
+ let ls = ref_renaming (k,r) in
+ assert (List.length ls > 1);
+ let s = List.hd ls in
+ let mp = subst_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
+ (add_visible (k,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
-
+ | Haskell -> if modular () then dottify ls else s
+ (* for the moment we always qualify in modular Haskell... *)
+ | Ocaml -> pp_gen k mp ls (Some (label_of_r r))
+
(* 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 () ->
+let pp_module mp =
+ let mp = subst_mp mp in
+ let ls = mp_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
+ let s = List.hd ls in
+ add_visible (Mod,s); s
+ | _ -> pp_gen Mod mp ls None
+
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index e17326bc9..38fd863c5 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -24,11 +24,6 @@ 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
@@ -37,9 +32,12 @@ 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
+type phase = Pre | Impl | Intf
-val create_renamings : ml_structure -> module_path list
+val set_phase : phase -> unit
+val get_phase : unit -> phase
+
+val opened_libraries : unit -> module_path list
type kind = Term | Type | Cons | Mod
@@ -47,14 +45,12 @@ 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 push_visible : module_path -> mod_self_id option -> 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
+type reset_kind = AllButExternal | Everything
val reset_renaming_tables : reset_kind -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 8eb7a6b4a..6d2b332ab 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -357,17 +357,18 @@ let module_filename m =
let print_one_decl struc mp decl =
let d = descr () in
reset_renaming_tables AllButExternal;
- ignore (create_renamings struc);
- push_visible mp;
+ set_phase Pre;
+ ignore (d.pp_struct struc);
+ set_phase Impl;
+ push_visible mp None;
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 print_structure_to_file (fn,si,mo) dry 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;
@@ -376,40 +377,42 @@ let print_structure_to_file (fn,si,mo) struc =
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
+ (* First, a dry run, for computing objects to rename or duplicate *)
+ set_phase Pre;
+ msg_with devnull (d.pp_struct struc);
+ let opened = opened_libraries () in
+ (* Print the implementation *)
+ let cout = if dry then None else Option.map open_out fn in
+ let ft = if dry then devnull else
+ match cout with
+ | None -> !Pp_control.std_ft
+ | Some cout -> Pp_control.with_output_to cout in
begin try
- msg_with ft (d.preamble mo used_modules unsafe_needs);
- if lang () = Ocaml then begin
- (* for computing objects to duplicate *)
- let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in
- msg_with devnull (d.pp_struct struc);
- reset_renaming_tables OnlyLocal;
- end;
+ (* The real printing of the implementation *)
+ set_phase Impl;
+ msg_with ft (d.preamble mo opened unsafe_needs);
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 *)
+ (* Now, let's 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;
+ set_phase Intf;
+ msg_with ft (d.sig_preamble mo opened unsafe_needs);
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
+ (if dry then None else si)
(*********************************************)
@@ -454,7 +457,7 @@ let full_extr f (refs,mps) =
List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
let struc = optimize_struct refs (mono_environment refs mps) in
warning_axioms ();
- print_structure_to_file (mono_filename f) struc;
+ print_structure_to_file (mono_filename f) false struc;
reset ()
let full_extraction f lr = full_extr f (locate_ref lr)
@@ -498,15 +501,12 @@ let extraction_library is_rec m =
let struc = List.fold_left select [] l 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 print = function
+ | (MPfile dir, sel) as e ->
+ let dry = not is_rec && dir <> dir_m in
let short_m = snd (split_dirpath dir) in
- print_structure_to_file (module_filename short_m) [e];
- print l
+ print_structure_to_file (module_filename short_m) dry [e]
| _ -> assert false
in
- print struc;
+ List.iter print struc;
reset ()
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index e8ba78903..8cf84cc5b 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -22,6 +22,9 @@ open Common
(*s Haskell renaming issues. *)
+let pr_lower_id id = str (String.uncapitalize (string_of_id id))
+let pr_upper_id id = str (String.capitalize (string_of_id id))
+
let keywords =
List.fold_right (fun s -> Idset.add (id_of_string s))
[ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
@@ -62,8 +65,6 @@ let pp_abst = function
prlist_with_sep (fun () -> (str " ")) pr_id l ++
str " ->" ++ spc ())
-let pr_lower_id id = pr_id (lowercase_id id)
-
(*s The pretty-printer for haskell syntax *)
let pp_global k r =
@@ -313,7 +314,7 @@ let pp_structure_elem = function
let pp_struct =
let pp_sel (mp,sel) =
- push_visible mp;
+ push_visible mp None;
let p = prlist_strict pp_structure_elem sel in
pop_visible (); p
in
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 52d18665f..8173ba9c8 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -19,7 +19,8 @@ open Mlutil
open Mod_subst
(*S Functions upon ML modules. *)
-let rec msid_of_mt = function
+
+let rec msid_of_mt = function
| MTident mp -> begin
match Modops.eval_struct (Global.env()) (SEBident mp) with
| SEBstruct(msid,_) -> MPself msid
@@ -27,12 +28,7 @@ let rec msid_of_mt = function
end
| MTwith(mt,_)-> msid_of_mt mt
| _ -> anomaly "Extraction:the With operator isn't applied to a name"
-
-let make_mp_with mp idl =
- let idl_rev = List.rev idl in
- let idl' = List.rev (List.tl idl_rev) in
- (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
- mp idl')
+
(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
[ml_structure]. *)
@@ -42,13 +38,12 @@ let struct_iter do_decl do_spec s =
| MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
| MTwith (mt,ML_With_type(idl,l,t))->
let mp_mt = msid_of_mt mt in
- let mp = make_mp_with mp_mt idl in
- let gr = ConstRef (
- (make_con mp empty_dirpath
- (label_of_id (
- List.hd (List.rev idl))))) in
- mt_iter mt;do_decl
- (Dtype(gr,l,t))
+ let l',idl' = list_sep_last idl in
+ let mp_w =
+ List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+ in
+ let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
+ mt_iter mt; do_decl (Dtype(r,l,t))
| MTwith (mt,_)->mt_iter mt
| MTsig (_, sign) -> List.iter spec_iter sign
and spec_iter = function
@@ -128,41 +123,6 @@ let spec_iter_references do_term do_cons do_type = function
| Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot
| Sval (r,t) -> do_term r; type_iter_references do_type t
-let struct_iter_references do_term do_cons do_type =
- struct_iter
- (decl_iter_references do_term do_cons do_type)
- (spec_iter_references do_term do_cons do_type)
-
-(*s Get all references used in one [ml_structure], either in [list] or [set]. *)
-
-type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a }
-
-let struct_get_references empty add struc =
- 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
-
-module Orefset = struct
- type t = { set : Refset.t ; list : global_reference list }
- let empty = { set = Refset.empty ; list = [] }
- let add r o =
- if Refset.mem r o.set then o
- else { set = Refset.add r o.set ; list = r :: o.list }
- let set o = o.set
- let list o = o.list
-end
-
-let struct_get_references_list struc =
- let o = struct_get_references Orefset.empty Orefset.add struc in
- { 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). *)
exception Found
@@ -396,6 +356,7 @@ let optimize_struct to_appear struc =
let opt_struc =
List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
in
+ let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
try
if modular () then raise NoDepCheck;
reset_needed ();
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index 670a5a6c2..fdb58e631 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -24,15 +24,11 @@ type do_ref = global_reference -> unit
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 kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a }
-
-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
+val msid_of_mt : ml_module_type -> module_path
+
val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
(* Some transformations of ML terms. [optimize_struct] simplify
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 6038593c1..55fa78c55 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -25,22 +25,6 @@ open Declarations
(*s Some utility functions. *)
-let rec msid_of_mt = function
- | MTident mp -> begin
- match Modops.eval_struct (Global.env()) (SEBident mp) with
- | SEBstruct(msid,_) -> MPself msid
- | _ -> anomaly "Extraction:the With can't be applied to a funsig"
- end
- | MTwith(mt,_)-> msid_of_mt mt
- | _ -> anomaly "Extraction:the With operator isn't applied to a name"
-
-let make_mp_with mp idl =
- let idl_rev = List.rev idl in
- let idl' = List.rev (List.tl idl_rev) in
- (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
- mp idl')
-
-
let pp_tvar id =
let s = string_of_id id in
if String.length s < 2 || s.[1]<>'\''
@@ -107,12 +91,18 @@ let sig_preamble _ used_modules usf =
(*s The pretty-printer for Ocaml syntax*)
-let pp_global k r =
- if is_inline_custom r then str (find_custom r)
+(* Beware of the side-effects of [pp_global] and [pp_modname].
+ They are used to update table of content for modules. Many [let]
+ below should not be altered since they force evaluation order.
+*)
+
+let pp_global k r =
+ if is_inline_custom r then str (find_custom 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 &&
(let s = find_custom r in
@@ -607,52 +597,49 @@ and pp_module_type ol = function
| MTident kn ->
pp_modname kn
| MTfunsig (mbid, mt, mt') ->
- let name = pp_modname (MPbound mbid) in
let typ = pp_module_type None mt in
+ let name = pp_modname (MPbound mbid) in
let def = pp_module_type None mt' in
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (msid, sign) ->
- 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 tvm = top_visible_mp () in
+ let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
+ (* References in [sign] are in short form (relative to [msid]).
+ In push_visible, [msid-->mp] is added to the current subst. *)
+ push_visible mp (Some msid);
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"
| MTwith(mt,ML_With_type(idl,vl,typ)) ->
- let l = rename_tvars keywords vl in
- let ids = pp_parameters l in
+ let ids = pp_parameters (rename_tvars keywords vl) in
let mp_mt = msid_of_mt mt in
- let mp = make_mp_with mp_mt idl in
- let gr = ConstRef (
- (make_con mp empty_dirpath
- (label_of_id (
- List.hd (List.rev idl))))) in
- push_visible mp_mt;
- let s = pp_module_type None mt ++
- str " with type " ++
- pp_global Type gr ++
- ids in
- pop_visible();
- s ++ str "=" ++ spc () ++
- pp_type false vl typ
+ let l,idl' = list_sep_last idl in
+ let mp_w =
+ List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+ in
+ let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l))
+ in
+ push_visible mp_mt None;
+ let s =
+ pp_module_type None mt ++ str " with type " ++
+ pp_global Type r ++ ids
+ in
+ pop_visible();
+ s ++ str "=" ++ spc () ++ pp_type false vl typ
| MTwith(mt,ML_With_module(idl,mp)) ->
- let mp_mt=msid_of_mt mt in
- push_visible mp_mt;
- let s =
- pp_module_type None mt ++
- str " with module " ++
- (pp_modname
- (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
- mp_mt idl))
- ++ str " = "
- in
- pop_visible ();
- s ++ (pp_modname mp)
-
-
+ let mp_mt = msid_of_mt mt in
+ let mp_w =
+ List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
+ in
+ push_visible mp_mt None;
+ let s =
+ pp_module_type None mt ++ str " with module " ++ pp_modname mp_w
+ in
+ pop_visible ();
+ s ++ str " = " ++ pp_modname mp
+
let is_short = function MEident _ | MEapply _ -> true | _ -> false
let rec pp_structure_elem = function
@@ -664,10 +651,16 @@ let rec pp_structure_elem = function
pp_alias_decl ren d
with Not_found -> pp_decl d)
| (l,SEmodule m) ->
+ let typ =
+ (* virtual printing of the type, in order to have a correct mli later*)
+ if Common.get_phase () = Pre then
+ str ": " ++ pp_module_type (Some l) m.ml_mod_type
+ else mt ()
+ in
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 " ++ name ++ str " = " ++
+ (str "module " ++ name ++ typ ++ str " = " ++
(if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++
(try
let ren = Common.check_duplicate (top_visible_mp ()) l in
@@ -694,33 +687,34 @@ and pp_module_expr ol = function
| MEstruct (msid, sel) ->
let tvm = top_visible_mp () in
let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
- push_visible mp;
+ (* No need to update the subst with [Some msid] below : names are
+ already in long form (see [subst_structure] in [Extract_env]). *)
+ push_visible mp None;
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 =
- push_visible mp;
- let p = pp_structure_elem s ++ fnl2 () in
- pop_visible (); p
+let do_struct f s =
+ let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
in
- prlist_strict
- (fun (mp,sel) -> prlist_strict identity (map_succeed (pp mp) sel)) s
-
-let pp_signature s =
- let pp mp s =
- push_visible mp;
- let p = pp_specif s ++ fnl2 () in
- pop_visible (); p
- in
- prlist_strict
- (fun (mp,sign) -> prlist_strict identity (map_succeed (pp mp) sign)) s
+ let ppl (mp,sel) =
+ push_visible mp None;
+ let p = prlist_strict pp sel in
+ (* for monolithic extraction, we try to simulate the unavailability
+ of [MPfile] in names by artificially nesting these [MPfile] *)
+ (if modular () then pop_visible ()); p
+ in
+ let p = prlist_strict ppl s in
+ (if not (modular ()) then repeat (List.length s) pop_visible ());
+ p
+
+let pp_struct s = do_struct pp_structure_elem s
+
+let pp_signature s = do_struct pp_specif s
-let pp_decl d =
- try pp_decl d with Failure "empty phrase" -> mt ()
+let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
let ocaml_descr = {
keywords = keywords;
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index b6724f584..75af1b7bc 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -183,7 +183,7 @@ let pp_structure_elem = function
let pp_struct =
let pp_sel (mp,sel) =
- push_visible mp;
+ push_visible mp None;
let p = prlist_strict pp_structure_elem sel in
pop_visible (); p
in
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 289074b62..66cb8d4e1 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -76,24 +76,15 @@ 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
+let rec get_nth_label_mp n = function
+ | 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 prefixes = prefixes_mp mp0 in
let rec f = function
| [] -> raise Not_found
- | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
+ | mp :: l -> if MPset.mem mp prefixes then mp else f l
in f mpl
let rec parse_labels ll = function
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 628e035bb..dd6e85a9d 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -55,7 +55,6 @@ 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 *)
diff --git a/lib/util.ml b/lib/util.ml
index 7df706393..2ac913607 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1238,11 +1238,13 @@ let rec prlist elem l = match l with
| h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
(* unlike all other functions below, [prlist] works lazily.
- if a strict behavior is needed, use [prlist_strict] instead. *)
+ if a strict behavior is needed, use [prlist_strict] instead.
+ evaluation is done from left to right. *)
let rec prlist_strict elem l = match l with
| [] -> mt ()
- | h::t -> (elem h)++(prlist_strict elem t)
+ | h::t ->
+ let e = elem h in let r = prlist_strict elem t in e++r
(* [prlist_with_sep sep pr [a ; ... ; c]] outputs
[pr a ++ sep() ++ ... ++ sep() ++ pr c] *)