From f6d8fc17dc9474e4d043cf709d672d9259599354 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 22 Aug 2013 14:30:01 +0000 Subject: Nicer code concerning dirpaths and modpath around Lib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/coqlib.ml | 4 +- library/declaremods.ml | 2 +- library/lib.ml | 123 ++++++++++++++++---------------------- library/lib.mli | 4 +- library/libnames.ml | 23 +++---- library/libnames.mli | 4 +- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/mlutil.ml | 5 +- plugins/extraction/table.ml | 14 ++--- plugins/extraction/table.mli | 1 - plugins/funind/recdef.ml | 2 +- plugins/xml/xmlcommand.ml | 5 +- pretyping/namegen.ml | 18 +++--- printing/printer.ml | 5 +- 14 files changed, 89 insertions(+), 123 deletions(-) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index aac7f9a28..ab4a6a25c 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -69,8 +69,8 @@ let check_required_library d = let dir = make_dir d in if Library.library_is_loaded dir then () else - let in_current_dir = match Lib.current_prefix () with - | MPfile dp, _ -> DirPath.equal dir dp + let in_current_dir = match Lib.current_mp () with + | MPfile dp -> DirPath.equal dir dp | _ -> false in if not in_current_dir then diff --git a/library/declaremods.ml b/library/declaremods.ml index 8d332b7df..dae585d5a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -764,7 +764,7 @@ let declare_one_include interp_modast (me_ast,annot) = let env = Global.env() in let me,kind = interp_modast env ModAny me_ast in let is_mod = (kind == Module) in - let cur_mp = fst (Lib.current_prefix ()) in + let cur_mp = Lib.current_mp () in let inl = inl2intopt annot in let mbids,aobjs = get_module_sobjs is_mod env inl me in let subst_self = diff --git a/library/lib.ml b/library/lib.ml index 159ac2d6d..e8b56de70 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -104,15 +104,13 @@ let library_dp () = module path and relative section path *) let path_prefix = ref initial_prefix -let sections_depth () = - List.length (Names.DirPath.repr (snd (snd !path_prefix))) - -let sections_are_opened () = - match Names.DirPath.repr (snd (snd !path_prefix)) with - [] -> false - | _ -> true - let cwd () = fst !path_prefix +let current_prefix () = snd !path_prefix +let current_mp () = fst (snd !path_prefix) +let current_sections () = snd (snd !path_prefix) + +let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) +let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) let cwd_except_section () = Libnames.pop_dirpath_n (sections_depth ()) (cwd ()) @@ -123,26 +121,14 @@ let current_dirpath sec = let make_path id = Libnames.make_path (cwd ()) id -let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id - -let path_of_include () = - let dir = Names.DirPath.repr (cwd ()) in - let new_dir = List.tl dir in - let id = List.hd dir in - Libnames.make_path (Names.DirPath.make new_dir) id - -let current_prefix () = snd !path_prefix +let make_path_except_section id = + Libnames.make_path (cwd_except_section ()) id let make_kn id = let mp,dir = current_prefix () in - Names.make_kn mp dir (Names.Label.of_id id) + Names.make_kn mp dir (Names.Label.of_id id) -let make_con id = - let mp,dir = current_prefix () in - Names.make_con mp dir (Names.Label.of_id id) - - -let make_oname id = make_path id, make_kn id +let make_oname id = Libnames.make_oname !path_prefix id let recalc_path_prefix () = let rec recalc = function @@ -156,7 +142,7 @@ let recalc_path_prefix () = let pop_path_prefix () = let dir,(mp,sec) = !path_prefix in - path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec)) + path_prefix := pop_dirpath dir, (mp, pop_dirpath sec) let find_entry_p p = let rec find = function @@ -219,8 +205,7 @@ let add_anonymous_entry node = add_entry (make_oname (anonymous_id ())) node let add_leaf id obj = - let (path, _) = current_prefix () in - if Names.ModPath.equal path Names.initial_path then + if Names.ModPath.equal (current_mp ()) Names.initial_path then error ("No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); @@ -271,16 +256,15 @@ let current_mod_id () = let start_mod is_type export id mp fs = - let dir = add_dirpath_suffix (fst !path_prefix) id in + let dir = add_dirpath_suffix (cwd ()) id in let prefix = dir,(mp,Names.DirPath.empty) in - let sp = make_path id in - let oname = sp, make_kn id in let exists = - if is_type then Nametab.exists_cci sp else Nametab.exists_module dir + if is_type then Nametab.exists_cci (make_path id) + else Nametab.exists_module dir in if exists then errorlabstrm "open_module" (pr_id id ++ str " already exists"); - add_entry oname (OpenedModule (is_type,export,prefix,fs)); + add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs)); path_prefix := prefix; prefix @@ -322,7 +306,7 @@ let contents_after sp = let (after,_,_) = split_lib sp in after let start_compilation s mp = if !comp_name != None then error "compilation unit is already started"; - if not (Names.DirPath.equal (snd (snd (!path_prefix))) Names.DirPath.empty) then + if not (Names.DirPath.is_empty (current_sections ())) then error "some sections are already opened"; let prefix = s, (mp, Names.DirPath.empty) in let () = add_anonymous_entry (CompilingLibrary prefix) in @@ -482,11 +466,10 @@ let open_section id = let olddir,(mp,oldsec) = !path_prefix in let dir = add_dirpath_suffix olddir id in let prefix = dir, (mp, add_dirpath_suffix oldsec id) in - let name = make_path id, make_kn id (* this makes little sense however *) in if Nametab.exists_section dir then errorlabstrm "open_section" (pr_id id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:`No in - add_entry name (OpenedSection (prefix, fs)); + add_entry (make_oname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; @@ -545,42 +528,36 @@ let init () = (* Misc *) -let mp_of_global ref = - match ref with - | VarRef id -> fst (current_prefix ()) - | ConstRef cst -> Names.con_modpath cst - | IndRef ind -> Names.ind_modpath ind - | ConstructRef constr -> Names.constr_modpath constr - -let rec dp_of_mp modp = - match modp with - | Names.MPfile dp -> dp - | Names.MPbound _ -> library_dp () - | Names.MPdot (mp,_) -> dp_of_mp mp - -let rec split_mp mp = - match mp with - | Names.MPfile dp -> dp, Names.DirPath.empty - | Names.MPdot (prfx, lbl) -> - let mprec, dprec = split_mp prfx in - mprec, Names.DirPath.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.DirPath.repr dprec)) - | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in library_dp(), Names.DirPath.make [id] - -let split_modpath mp = - let rec aux = function - | Names.MPfile dp -> dp, [] - | Names.MPbound mbid -> - library_dp (), [Names.MBId.to_id mbid] - | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in - (mp', Names.Label.to_id l :: lab) - in - let (mp, l) = aux mp in - mp, l - -let library_part ref = - match ref with - | VarRef id -> library_dp () - | _ -> dp_of_mp (mp_of_global ref) +let mp_of_global = function + |VarRef id -> current_mp () + |ConstRef cst -> Names.con_modpath cst + |IndRef ind -> Names.ind_modpath ind + |ConstructRef constr -> Names.constr_modpath constr + +let rec dp_of_mp = function + |Names.MPfile dp -> dp + |Names.MPbound _ -> library_dp () + |Names.MPdot (mp,_) -> dp_of_mp mp + +let rec split_mp = function + |Names.MPfile dp -> dp, Names.DirPath.empty + |Names.MPdot (prfx, lbl) -> + let mprec, dprec = split_mp prfx in + mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl) + |Names.MPbound mbid -> + let (_,id,dp) = Names.MBId.repr mbid in + library_dp (), Names.DirPath.make [id] + +let rec split_modpath = function + |Names.MPfile dp -> dp, [] + |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid] + |Names.MPdot (mp,l) -> + let (dp,ids) = split_modpath mp in + (dp, Names.Label.to_id l :: ids) + +let library_part = function + |VarRef id -> library_dp () + |ref -> dp_of_mp (mp_of_global ref) let remove_section_part ref = let sp = Nametab.path_of_global ref in @@ -602,12 +579,12 @@ let remove_section_part ref = let con_defined_in_sec kn = let _,dir,_ = Names.repr_con kn in not (Names.DirPath.is_empty dir) && - Names.DirPath.equal (fst (split_dirpath dir)) (snd (current_prefix ())) + Names.DirPath.equal (pop_dirpath dir) (current_sections ()) let defined_in_sec kn = let _,dir,_ = Names.repr_mind kn in not (Names.DirPath.is_empty dir) && - Names.DirPath.equal (fst (split_dirpath dir)) (snd (current_prefix ())) + Names.DirPath.equal (pop_dirpath dir) (current_sections ()) let discharge_global = function | ConstRef kn when con_defined_in_sec kn -> diff --git a/library/lib.mli b/library/lib.mli index 1362fabf8..fa3bd3f48 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -81,12 +81,10 @@ val cwd_except_section : unit -> Names.DirPath.t val current_dirpath : bool -> Names.DirPath.t (* false = except sections *) val make_path : Names.Id.t -> Libnames.full_path val make_path_except_section : Names.Id.t -> Libnames.full_path -val path_of_include : unit -> Libnames.full_path (** Kernel-side names *) -val current_prefix : unit -> Names.module_path * Names.DirPath.t +val current_mp : unit -> Names.module_path val make_kn : Names.Id.t -> Names.kernel_name -val make_con : Names.Id.t -> Names.constant (** Are we inside an opened section *) val sections_are_opened : unit -> bool diff --git a/library/libnames.ml b/library/libnames.ml index bc2406f27..d1bef531a 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -17,33 +17,34 @@ let pr_dirpath sl = (str (DirPath.to_string sl)) (*s Operations on dirpaths *) -(* Pop the last n module idents *) -let pop_dirpath_n n dir = - DirPath.make (List.skipn n (DirPath.repr dir)) +let split_dirpath d = match DirPath.repr d with + | id :: l -> DirPath.make l, id + | _ -> failwith "split_dirpath" let pop_dirpath p = match DirPath.repr p with - | [] -> anomaly (str "dirpath_prefix: empty dirpath") | _::l -> DirPath.make l + | [] -> failwith "pop_dirpath" + +(* Pop the last n module idents *) +let pop_dirpath_n n dir = DirPath.make (List.skipn n (DirPath.repr dir)) let is_dirpath_prefix_of d1 d2 = List.prefix_of (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) let chop_dirpath n d = let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in - DirPath.make (List.rev d1), DirPath.make (List.rev d2) + DirPath.make (List.rev d1), DirPath.make (List.rev d2) let drop_dirpath_prefix d1 d2 = - let d = Util.List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) in - DirPath.make (List.rev d) + let d = + List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) + in + DirPath.make (List.rev d) let append_dirpath d1 d2 = DirPath.make (DirPath.repr d2 @ DirPath.repr d1) -(* To know how qualified a name should be to be understood in the current env*) let add_dirpath_prefix id d = DirPath.make (DirPath.repr d @ [id]) -let split_dirpath d = - let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l) - let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p) (* parsing *) diff --git a/library/libnames.mli b/library/libnames.mli index c44fea543..627b8f013 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -18,13 +18,13 @@ val pr_dirpath : DirPath.t -> Pp.std_ppcmds val dirpath_of_string : string -> DirPath.t val string_of_dirpath : DirPath.t -> string -(** Pop the suffix of a [DirPath.t] *) +(** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *) val pop_dirpath : DirPath.t -> DirPath.t (** Pop the suffix n times *) val pop_dirpath_n : int -> DirPath.t -> DirPath.t -(** Give the immediate prefix and basename of a [DirPath.t] *) +(** Immediate prefix and basename of a [DirPath.t]. May raise [Failure] *) val split_dirpath : DirPath.t -> DirPath.t * Id.t val add_dirpath_suffix : DirPath.t -> module_ident -> DirPath.t diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7fffc960b..f57832d3f 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -52,7 +52,7 @@ let toplevel_env () = let environment_until dir_opt = let rec parse = function - | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()] + | [] when dir_opt = None -> [Lib.current_mp (), toplevel_env ()] | [] -> [] | d :: l -> let meb = diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 659ee4ec4..0903f85a0 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1301,9 +1301,8 @@ let inline_test r t = not (is_fix t2) && ml_size t < 12 && is_not_strict t) let con_of_string s = - match DirPath.repr (dirpath_of_string s) with - | id :: d -> Constant.make2 (MPfile (DirPath.make d)) (Label.of_id id) - | [] -> assert false + let d, id = Libnames.split_dirpath (dirpath_of_string s) in + Constant.make2 (MPfile d) (Label.of_id id) let manual_inline_set = List.fold_right (fun x -> Cset_env.add (con_of_string x)) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2109ba632..66acf23ed 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -58,18 +58,16 @@ let raw_string_of_modfile = function | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f))) | _ -> assert false -let current_toplevel () = fst (Lib.current_prefix ()) - let is_toplevel mp = - mp = initial_path || mp = current_toplevel () + ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ()) let at_toplevel mp = is_modfile mp || is_toplevel mp let mp_length mp = - let mp0 = current_toplevel () in + let mp0 = Lib.current_mp () in let rec len = function - | mp when mp = mp0 -> 1 + | mp when ModPath.equal mp mp0 -> 1 | MPdot (mp,_) -> 1 + len mp | _ -> 1 in len mp @@ -97,7 +95,7 @@ let rec parse_labels2 ll mp1 = function | mp -> mp,ll let labels_of_ref r = - let mp_top = current_toplevel () in + let mp_top = Lib.current_mp () in let mp,_,l = repr_of_r r in parse_labels2 [l] mp_top mp @@ -419,8 +417,8 @@ let error_non_implicit msg = let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> if not (Library.library_is_loaded dp) then begin - match base_mp (current_toplevel ()) with - | MPfile dp' when dp<>dp' -> + match base_mp (Lib.current_mp ()) with + | MPfile dp' when not (DirPath.equal dp dp') -> err (str ("Please load library "^(DirPath.to_string dp^" first."))) | _ -> () end diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index ce6f8e229..91d2531dd 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -49,7 +49,6 @@ val occur_kn_in_ref : mutual_inductive -> global_reference -> bool val repr_of_r : global_reference -> module_path * DirPath.t * Label.t val modpath_of_r : global_reference -> module_path val label_of_r : global_reference -> Label.t -val current_toplevel : unit -> module_path val base_mp : module_path -> module_path val is_modfile : module_path -> bool val string_of_modfile : module_path -> string diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 857e82fc5..7fbc1b981 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1258,7 +1258,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") in - let lemma = mkConst (Lib.make_con na) in + let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in ref_ := Some lemma ; let lid = ref [] in let h_num = ref (-1) in diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 6145548b2..d065ba61a 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -380,10 +380,7 @@ let print internal glob_ref kind xml_library_root = match glob_ref with Gn.VarRef id -> (* this kn is fake since it is not provided by Coq *) - let kn = - let (mod_path,dir_path) = Lib.current_prefix () in - N.make_kn mod_path dir_path (N.Label.of_id id) - in + let kn = Lib.make_kn id in let (_,body,typ) = G.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ | Gn.ConstRef kn -> diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index a2fa81750..1736bcff2 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -26,16 +26,14 @@ open Termops (**********************************************************************) (* Globality of identifiers *) -let is_imported_modpath mp = - let current_mp,_ = Lib.current_prefix() in - match mp with - | MPfile dp -> - let rec find_prefix = function - |MPfile dp1 -> not (DirPath.equal dp1 dp) - |MPdot(mp,_) -> find_prefix mp - |MPbound(_) -> false - in find_prefix current_mp - | p -> false +let is_imported_modpath = function + | MPfile dp -> + let rec find_prefix = function + |MPfile dp1 -> not (DirPath.equal dp1 dp) + |MPdot(mp,_) -> find_prefix mp + |MPbound(_) -> false + in find_prefix (Lib.current_mp ()) + | _ -> false let is_imported_ref = function | VarRef _ -> false diff --git a/printing/printer.ml b/printing/printer.ml index cc9356cda..05037a150 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -144,12 +144,11 @@ let id_of_global env = function (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1) | VarRef v -> v -let cons_dirpath id dp = DirPath.make (id :: DirPath.repr dp) - let rec dirpath_of_mp = function | MPfile sl -> sl | MPbound uid -> DirPath.make [MBId.to_id uid] - | MPdot (mp,l) -> cons_dirpath (Label.to_id l) (dirpath_of_mp mp) + | MPdot (mp,l) -> + Libnames.add_dirpath_suffix (dirpath_of_mp mp) (Label.to_id l) let dirpath_of_global = function | ConstRef kn -> dirpath_of_mp (Constant.modpath kn) -- cgit v1.2.3