aboutsummaryrefslogtreecommitdiff
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml123
1 files changed, 62 insertions, 61 deletions
diff --git a/library/lib.ml b/library/lib.ml
index f680ecee3c..ddd2ed6afa 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -13,6 +13,9 @@ open Libnames
open Globnames
open Nameops
open Libobject
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
type is_type = bool (* Module Type or just Module *)
type export = bool option (* None for a Module Type *)
@@ -75,7 +78,7 @@ let classify_segment seg =
| (_,ClosedModule _) :: stk -> clean acc stk
| (_,OpenedSection _) :: _ -> error "there are still opened sections"
| (_,OpenedModule (ty,_,_,_)) :: _ ->
- errorlabstrm "Lib.classify_segment"
+ user_err ~hdr:"Lib.classify_segment"
(str "there are still opened " ++ str (module_kind ty) ++ str "s")
| (_,FrozenState _) :: stk -> clean acc stk
in
@@ -94,21 +97,30 @@ let segment_of_objects prefix =
let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty)
-let lib_stk = ref ([] : library_segment)
+type lib_state = {
+ comp_name : Names.DirPath.t option;
+ lib_stk : library_segment;
+ path_prefix : Names.DirPath.t * (Names.module_path * Names.DirPath.t);
+}
+
+let initial_lib_state = {
+ comp_name = None;
+ lib_stk = [];
+ path_prefix = initial_prefix;
+}
-let comp_name = ref None
+let lib_state = ref initial_lib_state
let library_dp () =
- match !comp_name with Some m -> m | None -> default_library
+ match !lib_state.comp_name with Some m -> m | None -> default_library
(* [path_prefix] is a pair of absolute dirpath and a pair of current
module path and relative section path *)
-let path_prefix = ref initial_prefix
-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 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 sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
@@ -129,7 +141,7 @@ let make_kn id =
let mp,dir = current_prefix () in
Names.make_kn mp dir (Names.Label.of_id id)
-let make_oname id = Libnames.make_oname !path_prefix id
+let make_oname id = Libnames.make_oname !lib_state.path_prefix id
let recalc_path_prefix () =
let rec recalc = function
@@ -139,18 +151,18 @@ let recalc_path_prefix () =
| _::l -> recalc l
| [] -> initial_prefix
in
- path_prefix := recalc !lib_stk
+ lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk }
let pop_path_prefix () =
- let dir,(mp,sec) = !path_prefix in
- path_prefix := pop_dirpath dir, (mp, pop_dirpath sec)
+ let dir,(mp,sec) = !lib_state.path_prefix in
+ lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)}
let find_entry_p p =
let rec find = function
| [] -> raise Not_found
| ent::l -> if p ent then ent else find l
in
- find !lib_stk
+ find !lib_state.lib_stk
let split_lib_gen test =
let rec collect after equal = function
@@ -171,7 +183,7 @@ let split_lib_gen test =
| _ -> findeq (hd::after) before)
| [] -> None
in
- match findeq [] !lib_stk with
+ match findeq [] !lib_state.lib_stk with
| None -> error "no such entry"
| Some r -> r
@@ -196,10 +208,10 @@ let split_lib_at_opening sp =
(* Adding operations. *)
let add_entry sp node =
- lib_stk := (sp,node) :: !lib_stk
+ lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk }
let pull_to_head oname =
- lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk
+ lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk }
let anonymous_id =
let n = ref 0 in
@@ -272,9 +284,9 @@ let start_mod is_type export id mp fs =
else Nametab.exists_module dir
in
if exists then
- errorlabstrm "open_module" (pr_id id ++ str " already exists");
+ user_err ~hdr:"open_module" (pr_id id ++ str " already exists");
add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
- path_prefix := prefix;
+ lib_state := { !lib_state with path_prefix = prefix} ;
prefix
let start_module = start_mod false
@@ -282,7 +294,7 @@ let start_modtype = start_mod true None
let error_still_opened string oname =
let id = basename (fst oname) in
- errorlabstrm ""
+ user_err
(str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.")
let end_mod is_type =
@@ -296,16 +308,16 @@ let end_mod is_type =
with Not_found -> error "No opened modules."
in
let (after,mark,before) = split_lib_at_opening oname in
- lib_stk := before;
+ lib_state := { !lib_state with lib_stk = before };
add_entry oname (ClosedModule (List.rev (mark::after)));
- let prefix = !path_prefix in
+ let prefix = !lib_state.path_prefix in
recalc_path_prefix ();
(oname, prefix, fs, after)
let end_module () = end_mod false
let end_modtype () = end_mod true
-let contents () = !lib_stk
+let contents () = !lib_state.lib_stk
let contents_after sp = let (after,_,_) = split_lib sp in after
@@ -313,21 +325,21 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
(* TODO: use check_for_module ? *)
let start_compilation s mp =
- if !comp_name != None then
+ if !lib_state.comp_name != None then
error "compilation unit is already started";
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
- comp_name := Some s;
- path_prefix := prefix
+ lib_state := { !lib_state with comp_name = Some s;
+ path_prefix = prefix }
let end_compilation_checks dir =
let _ =
try match snd (find_entry_p is_opening_node) with
| OpenedSection _ -> error "There are some open sections."
| OpenedModule (ty,_,_,_) ->
- errorlabstrm "Lib.end_compilation_checks"
+ user_err ~hdr:"Lib.end_compilation_checks"
(str "There are some open " ++ str (module_kind ty) ++ str "s.")
| _ -> assert false
with Not_found -> ()
@@ -341,7 +353,7 @@ let end_compilation_checks dir =
with Not_found -> anomaly (Pp.str "No module declared")
in
let _ =
- match !comp_name with
+ match !lib_state.comp_name with
| None -> anomaly (Pp.str "There should be a module name...")
| Some m ->
if not (Names.DirPath.equal m dir) then anomaly
@@ -352,8 +364,8 @@ let end_compilation_checks dir =
let end_compilation oname =
let (after,mark,before) = split_lib_at_opening oname in
- comp_name := None;
- !path_prefix,after
+ lib_state := { !lib_state with comp_name = None };
+ !lib_state.path_prefix,after
(* Returns true if we are inside an opened module or module type *)
@@ -379,7 +391,7 @@ let find_opening_node id =
let oname,entry = find_entry_p is_opening_node in
let id' = basename (fst oname) in
if not (Names.Id.equal id id') then
- errorlabstrm "Lib.find_opening_node"
+ user_err ~hdr:"Lib.find_opening_node"
(str "Last block to end has name " ++ pr_id id' ++ str ".");
entry
with Not_found -> error "There is nothing to end."
@@ -393,7 +405,7 @@ let find_opening_node id =
- the list of substitution to do at section closing
*)
-type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types
+type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
@@ -433,12 +445,10 @@ let add_section_context ctx =
sectab := (Context ctx :: vars,repl,abs)::sl
let extract_hyps (secs,ohyps) =
- let open Context.Named.Declaration in
let rec aux = function
- | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) ->
- let (id',b,t) = to_tuple decl in
+ | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
let l, r = aux (idl,hyps) in
- (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
+ (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
| (Variable (_,_,poly,ctx)::idl,hyps) ->
let l, r = aux (idl,hyps) in
l, if poly then Univ.ContextSet.union r ctx else r
@@ -448,17 +458,11 @@ let extract_hyps (secs,ohyps) =
| [], _ -> [],Univ.ContextSet.empty
in aux (secs,ohyps)
-let instance_from_variable_context sign =
- let rec inst_rec = function
- | (id,b,None,_) :: sign -> id :: inst_rec sign
- | _ :: sign -> inst_rec sign
- | [] -> [] in
- Array.of_list (inst_rec sign)
-
-let named_of_variable_context ctx = let open Context.Named.Declaration in
- List.map (function id,_,None,t -> LocalAssum (id,t)
- | id,_,Some b,t -> LocalDef (id,b,t))
- ctx
+let instance_from_variable_context =
+ List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+
+let named_of_variable_context =
+ List.map fst
let add_section_replacement f g poly hyps =
match !sectab with
@@ -519,16 +523,16 @@ let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
let open_section id =
- let olddir,(mp,oldsec) = !path_prefix in
+ 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
- errorlabstrm "open_section" (pr_id id ++ str " already exists.");
+ user_err ~hdr:"open_section" (pr_id 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);
- path_prefix := prefix;
+ lib_state := { !lib_state with path_prefix = prefix };
if !Flags.xml_export then Hook.get f_xml_open_section id;
add_section ()
@@ -554,8 +558,8 @@ let close_section () =
error "No opened section."
in
let (secdecls,mark,before) = split_lib_at_opening oname in
- lib_stk := before;
- let full_olddir = fst !path_prefix in
+ lib_state := { !lib_state with lib_stk = before };
+ let full_olddir = fst !lib_state.path_prefix in
pop_path_prefix ();
add_entry oname (ClosedSection (List.rev (mark::secdecls)));
if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
@@ -566,7 +570,7 @@ let close_section () =
(* State and initialization. *)
-type frozen = Names.DirPath.t option * library_segment
+type frozen = lib_state
let freeze ~marshallable =
match marshallable with
@@ -583,18 +587,15 @@ let freeze ~marshallable =
Some(n,OpenedSection(op,Summary.empty_frozen))
| n, ClosedSection _ -> Some (n,ClosedSection [])
| _, FrozenState _ -> None)
- !lib_stk in
- !comp_name, lib_stk
+ !lib_state.lib_stk in
+ { !lib_state with lib_stk }
| _ ->
- !comp_name, !lib_stk
+ !lib_state
-let unfreeze (mn,stk) =
- comp_name := mn;
- lib_stk := stk;
- recalc_path_prefix ()
+let unfreeze st = lib_state := st
let init () =
- unfreeze (None,[]);
+ unfreeze initial_lib_state;
Summary.init_summaries ();
add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 08:48:33 +0000