diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-22 01:14:50 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-29 14:59:29 +0100 |
commit | c408e819ce39b27f0842c84b1b24c585ac5b6086 (patch) | |
tree | a3dac227a23d098e70c7d74bd719f93f3cc6724c /library | |
parent | 437f20f0a1c2717cd7baae52e2ab20750dd9d4fb (diff) |
[lib] [api] Introduce record for `object_prefix`
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
Diffstat (limited to 'library')
-rw-r--r-- | library/declaremods.ml | 34 | ||||
-rw-r--r-- | library/lib.ml | 58 | ||||
-rw-r--r-- | library/libnames.ml | 19 | ||||
-rw-r--r-- | library/libnames.mli | 20 | ||||
-rw-r--r-- | library/nametab.ml | 10 |
5 files changed, 85 insertions, 56 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index db83dafef..41e00a41c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -180,16 +180,16 @@ let compute_visibility exists i = (** Iterate some function [iter_objects] on all components of a module *) -let do_module exists iter_objects i dir mp sobjs kobjs = - let prefix = (dir,(mp,DirPath.empty)) in +let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = + let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in let dirinfo = DirModule prefix in - consistency_checks exists dir dirinfo; - Nametab.push_dir (compute_visibility exists i) dir dirinfo; - ModSubstObjs.set mp sobjs; + consistency_checks exists obj_dir dirinfo; + Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; + ModSubstObjs.set obj_mp sobjs; (* If we're not a functor, let's iter on the internal components *) if sobjs_no_functor sobjs then begin let objs = expand_sobjs sobjs in - ModObjs.set mp (prefix,objs,kobjs); + ModObjs.set obj_mp (prefix,objs,kobjs); iter_objects (i+1) prefix objs; iter_objects (i+1) prefix kobjs end @@ -222,20 +222,20 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!") let load_keep i ((sp,kn),kobjs) = (* Invariant : seg isn't empty *) - let dir = dir_of_sp sp and mp = mp_of_kn kn in - let prefix = (dir,(mp,DirPath.empty)) in + let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in + let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in let prefix',sobjs,kobjs0 = - try ModObjs.get mp + try ModObjs.get obj_mp with Not_found -> assert false (* a substobjs should already be loaded *) in assert (eq_op prefix' prefix); assert (List.is_empty kobjs0); - ModObjs.set mp (prefix,sobjs,kobjs); + ModObjs.set obj_mp (prefix,sobjs,kobjs); Lib.load_objects i prefix kobjs let open_keep i ((sp,kn),kobjs) = - let dir = dir_of_sp sp and mp = mp_of_kn kn in - let prefix = (dir,(mp,DirPath.empty)) in + let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in + let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in Lib.open_objects i prefix kobjs let in_modkeep : Lib.lib_objects -> obj = @@ -284,9 +284,9 @@ let (in_modtype : substitutive_objects -> obj), (** {6 Declaration of substitutive objects for Include} *) let do_include do_load do_open i ((sp,kn),aobjs) = - let dir = Libnames.dirpath sp in - let mp = KerName.modpath kn in - let prefix = (dir,(mp,DirPath.empty)) in + let obj_dir = Libnames.dirpath sp in + let obj_mp = KerName.modpath kn in + let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in let o = expand_aobjs aobjs in if do_load then Lib.load_objects i prefix o; if do_open then Lib.open_objects i prefix o @@ -577,7 +577,7 @@ let start_module interp_modast export id args res fs = in openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in - Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); + Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModule prefix); mp let end_module () = @@ -684,7 +684,7 @@ let start_modtype interp_modast id args mtys fs = let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in - Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); + Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix); mp let end_modtype () = diff --git a/library/lib.ml b/library/lib.ml index 3dbb16c7b..499e2ae21 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -93,12 +93,16 @@ let segment_of_objects prefix = sections, but on the contrary there are many constructions of section paths based on the library path. *) -let initial_prefix = default_library,(Names.ModPath.initial,Names.DirPath.empty) +let initial_prefix = { + obj_dir = default_library; + obj_mp = ModPath.initial; + obj_sec = DirPath.empty; +} type lib_state = { - comp_name : Names.DirPath.t option; + comp_name : DirPath.t option; lib_stk : library_segment; - path_prefix : Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t); + path_prefix : object_prefix; } let initial_lib_state = { @@ -115,10 +119,9 @@ let library_dp () = (* [path_prefix] is a pair of absolute dirpath and a pair of current module path and relative section path *) -let cwd () = fst !lib_state.path_prefix -let current_prefix () = snd !lib_state.path_prefix -let current_mp () = fst (snd !lib_state.path_prefix) -let current_sections () = snd (snd !lib_state.path_prefix) +let cwd () = !lib_state.path_prefix.obj_dir +let current_mp () = !lib_state.path_prefix.obj_mp +let current_sections () = !lib_state.path_prefix.obj_sec let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) @@ -136,7 +139,7 @@ let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id let make_kn id = - let mp,dir = current_prefix () in + let mp, dir = current_mp (), current_sections () in Names.KerName.make mp dir (Names.Label.of_id id) let make_oname id = Libnames.make_oname !lib_state.path_prefix id @@ -152,8 +155,11 @@ let recalc_path_prefix () = lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk } let pop_path_prefix () = - let dir,(mp,sec) = !lib_state.path_prefix in - lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)} + let op = !lib_state.path_prefix in + lib_state := { !lib_state + with path_prefix = { op with obj_dir = pop_dirpath op.obj_dir; + obj_sec = pop_dirpath op.obj_sec; + } } let find_entry_p p = let rec find = function @@ -226,7 +232,7 @@ let add_anonymous_entry node = add_entry (make_oname (anonymous_id ())) node let add_leaf id obj = - if Names.ModPath.equal (current_mp ()) Names.ModPath.initial then + if ModPath.equal (current_mp ()) ModPath.initial then user_err Pp.(str "No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); @@ -278,8 +284,8 @@ let current_mod_id () = let start_mod is_type export id mp fs = - let dir = add_dirpath_suffix (cwd ()) id in - let prefix = dir,(mp,Names.DirPath.empty) in + let dir = add_dirpath_suffix (!lib_state.path_prefix.obj_dir) id in + let prefix = { obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in let exists = if is_type then Nametab.exists_cci (make_path id) else Nametab.exists_module dir @@ -328,10 +334,10 @@ let contents_after sp = let (after,_,_) = split_lib sp in after let start_compilation s mp = if !lib_state.comp_name != None then user_err Pp.(str "compilation unit is already started"); - if not (Names.DirPath.is_empty (current_sections ())) then + if not (Names.DirPath.is_empty (!lib_state.path_prefix.obj_sec)) then user_err Pp.(str "some sections are already opened"); - let prefix = s, (mp, Names.DirPath.empty) in - let () = add_anonymous_entry (CompilingLibrary prefix) in + let prefix = Libnames.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in + add_anonymous_entry (CompilingLibrary prefix); lib_state := { !lib_state with comp_name = Some s; path_prefix = prefix } @@ -522,15 +528,15 @@ let is_in_section ref = (*************) (* Sections. *) let open_section id = - let olddir,(mp,oldsec) = !lib_state.path_prefix in - let dir = add_dirpath_suffix olddir id in - let prefix = dir, (mp, add_dirpath_suffix oldsec id) in - if Nametab.exists_section dir then + let opp = !lib_state.path_prefix in + let obj_dir = add_dirpath_suffix opp.obj_dir id in + let prefix = { obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in + if Nametab.exists_section obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:`No in 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); + Nametab.push_dir (Nametab.Until 1) obj_dir (DirOpenSection prefix); lib_state := { !lib_state with path_prefix = prefix }; add_section () @@ -556,7 +562,7 @@ let close_section () = in let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - let full_olddir = fst !lib_state.path_prefix in + let full_olddir = !lib_state.path_prefix.obj_dir in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); let newdecls = List.map discharge_item secdecls in @@ -596,10 +602,10 @@ let init () = (* Misc *) let mp_of_global = function - |VarRef id -> current_mp () - |ConstRef cst -> Names.Constant.modpath cst - |IndRef ind -> Names.ind_modpath ind - |ConstructRef constr -> Names.constr_modpath constr + | VarRef id -> !lib_state.path_prefix.obj_mp + | ConstRef cst -> Names.Constant.modpath cst + | IndRef ind -> Names.ind_modpath ind + | ConstructRef constr -> Names.constr_modpath constr let rec dp_of_mp = function |Names.MPfile dp -> dp diff --git a/library/libnames.ml b/library/libnames.ml index 81878e72f..a471d8396 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -156,10 +156,15 @@ let qualid_of_dirpath dir = type object_name = full_path * KerName.t -type object_prefix = DirPath.t * (ModPath.t * DirPath.t) +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} -let make_oname (dirpath,(mp,dir)) id = - make_path dirpath id, KerName.make mp dir (Label.of_id id) +(* let make_oname (dirpath,(mp,dir)) id = *) +let make_oname { obj_dir; obj_mp; obj_sec } id = + make_path obj_dir id, KerName.make obj_mp obj_sec (Label.of_id id) (* to this type are mapped DirPath.t's in the nametab *) type global_dir_reference = @@ -170,10 +175,10 @@ type global_dir_reference = | DirClosedSection of DirPath.t (* this won't last long I hope! *) -let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) = - DirPath.equal d1 d2 && - DirPath.equal p1 p2 && - ModPath.equal mp1 mp2 +let eq_op op1 op2 = + DirPath.equal op1.obj_dir op2.obj_dir && + DirPath.equal op1.obj_sec op2.obj_sec && + ModPath.equal op1.obj_mp op2.obj_mp let eq_global_dir_reference r1 r2 = match r1, r2 with | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2 diff --git a/library/libnames.mli b/library/libnames.mli index ed01163ee..71f542240 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -94,7 +94,25 @@ val qualid_of_ident : Id.t -> qualid type object_name = full_path * KerName.t -type object_prefix = DirPath.t * (ModPath.t * DirPath.t) +(** Object prefix morally contains the "prefix" naming of an object to + be stored by [library], where [obj_dir] is the "absolute" path, + [obj_mp] is the current "module" prefix and [obj_sec] is the + "section" prefix. + + Thus, for an object living inside [Module A. Section B.] the + prefix would be: + + [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ] + + Note that both [obj_dir] and [obj_sec] are "paths" that is to say, + as opposed to [obj_mp] which is a single module name. + + *) +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} val eq_op : object_prefix -> object_prefix -> bool diff --git a/library/nametab.ml b/library/nametab.ml index 0ec4a37cd..222c4cedc 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -359,8 +359,8 @@ let push_modtype vis sp kn = let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; match dir_ref with - DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab - | _ -> () + | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab + | _ -> () (* Locate functions *******************************************************) @@ -386,17 +386,17 @@ let locate_dir qid = DirTab.locate qid !the_dirtab let locate_module qid = match locate_dir qid with - | DirModule (_,(mp,_)) -> mp + | DirModule { obj_mp ; _} -> obj_mp | _ -> raise Not_found let full_name_module qid = match locate_dir qid with - | DirModule (dir,_) -> dir + | DirModule { obj_dir ; _} -> obj_dir | _ -> raise Not_found let locate_section qid = match locate_dir qid with - | DirOpenSection (dir, _) + | DirOpenSection { obj_dir; _ } -> obj_dir | DirClosedSection dir -> dir | _ -> raise Not_found |