diff options
Diffstat (limited to 'contrib/extraction/common.ml')
-rw-r--r-- | contrib/extraction/common.ml | 610 |
1 files changed, 283 insertions, 327 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 5ad4a288..02173c1f 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.ml 10596 2008-02-27 15:30:11Z letouzey $ i*) +(*i $Id: common.ml 11559 2008-11-07 22:03:34Z letouzey $ i*) open Pp open Util @@ -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 (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 (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 (id_of_global r)) (global_ids_list ()) - else id_of_string (modular_rename upper (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 + |