aboutsummaryrefslogtreecommitdiff
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml91
1 files changed, 57 insertions, 34 deletions
diff --git a/library/lib.ml b/library/lib.ml
index daa41eca65..576e23c4f5 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -28,7 +28,7 @@ let make_oname Nametab.{ obj_dir; obj_mp } id =
(* let make_oname (dirpath,(mp,dir)) id = *)
type node =
- | Leaf of obj
+ | Leaf of Libobject.t
| CompilingLibrary of Nametab.object_prefix
| OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
| OpenedSection of Nametab.object_prefix * Summary.frozen
@@ -37,7 +37,8 @@ type library_entry = object_name * node
type library_segment = library_entry list
-type lib_objects = (Names.Id.t * obj) list
+type lib_atomic_objects = (Id.t * Libobject.obj) list
+type lib_objects = (Names.Id.t * Libobject.t) list
let module_kind is_type =
if is_type then "module type" else "module"
@@ -45,10 +46,10 @@ let module_kind is_type =
let iter_objects f i prefix =
List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
-let load_objects i pr = iter_objects load_object i pr
-let open_objects i pr = iter_objects open_object i pr
+let load_atomic_objects i pr = iter_objects load_object i pr
+let open_atomic_objects i pr = iter_objects open_object i pr
-let subst_objects subst seg =
+let subst_atomic_objects subst seg =
let subst_one = fun (id,obj as node) ->
let obj' = subst_object (subst,obj) in
if obj' == obj then node else
@@ -67,15 +68,28 @@ let classify_segment seg =
let rec clean ((substl,keepl,anticipl) as acc) = function
| (_,CompilingLibrary _) :: _ | [] -> acc
| ((sp,kn),Leaf o) :: stk ->
- let id = Names.Label.to_id (Names.KerName.label kn) in
- (match classify_object o with
- | Dispose -> clean acc stk
- | Keep o' ->
- clean (substl, (id,o')::keepl, anticipl) stk
- | Substitute o' ->
- clean ((id,o')::substl, keepl, anticipl) stk
- | Anticipate o' ->
- clean (substl, keepl, o'::anticipl) stk)
+ let id = Names.Label.to_id (Names.KerName.label kn) in
+ begin match o with
+ | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ ->
+ clean ((id,o)::substl, keepl, anticipl) stk
+ | KeepObject _ ->
+ clean (substl, (id,o)::keepl, anticipl) stk
+ | ImportObject { export } ->
+ if export then
+ clean ((id,o)::substl, keepl, anticipl) stk
+ else
+ clean acc stk
+ | AtomicObject obj ->
+ begin match classify_object obj with
+ | Dispose -> clean acc stk
+ | Keep o' ->
+ clean (substl, (id,AtomicObject o')::keepl, anticipl) stk
+ | Substitute o' ->
+ clean ((id,AtomicObject o')::substl, keepl, anticipl) stk
+ | Anticipate o' ->
+ clean (substl, keepl, AtomicObject o'::anticipl) stk
+ end
+ end
| (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
| (_,OpenedModule (ty,_,_,_)) :: _ ->
user_err ~hdr:"Lib.classify_segment"
@@ -223,19 +237,19 @@ let add_leaf id obj =
user_err Pp.(str "No session module started (use -top dir)");
let oname = make_foname id in
cache_object (oname,obj);
- add_entry oname (Leaf obj);
+ add_entry oname (Leaf (AtomicObject obj));
oname
let add_discharged_leaf id obj =
let oname = make_foname id in
let newobj = rebuild_object obj in
cache_object (oname,newobj);
- add_entry oname (Leaf newobj)
+ add_entry oname (Leaf (AtomicObject newobj))
let add_leaves id objs =
let oname = make_foname id in
let add_obj obj =
- add_entry oname (Leaf obj);
+ add_entry oname (Leaf (AtomicObject obj));
load_object 1 (oname,obj)
in
List.iter add_obj objs;
@@ -246,9 +260,9 @@ let add_anonymous_leaf ?(cache_first = true) obj =
let oname = make_foname id in
if cache_first then begin
cache_object (oname,obj);
- add_entry oname (Leaf obj)
+ add_entry oname (Leaf (AtomicObject obj))
end else begin
- add_entry oname (Leaf obj);
+ add_entry oname (Leaf (AtomicObject obj));
cache_object (oname,obj)
end
@@ -411,8 +425,12 @@ type abstr_info = {
type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
type secentry =
- | Variable of (Names.Id.t * Decl_kinds.binding_kind *
- Decl_kinds.polymorphic * Univ.ContextSet.t)
+ | Variable of {
+ id:Names.Id.t;
+ kind:Decl_kinds.binding_kind;
+ poly:bool;
+ univs:Univ.ContextSet.t;
+ }
| Context of Univ.ContextSet.t
let sectab =
@@ -424,16 +442,16 @@ let add_section () =
(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
let check_same_poly p vars =
- let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
+ let pred = function Context _ -> p = false | Variable {poly} -> p != poly in
if List.exists pred vars then
user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
-let add_section_variable id impl poly ctx =
+let add_section_variable ~name ~kind ~poly univs =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| (vars,repl,abs)::sl ->
List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
- sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+ sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl
let add_section_context ctx =
match !sectab with
@@ -448,7 +466,7 @@ let is_polymorphic_univ u =
let open Univ in
List.iter (fun (vars,_,_) ->
List.iter (function
- | Variable (_,_,poly,(univs,_)) ->
+ | Variable {poly;univs=(univs,_)} ->
if LSet.mem u univs then raise (PolyFound poly)
| Context (univs,_) ->
if LSet.mem u univs then raise (PolyFound true)
@@ -459,12 +477,12 @@ let is_polymorphic_univ u =
let extract_hyps (secs,ohyps) =
let rec aux = function
- | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+ | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
let l, r = aux (idl,hyps) in
- (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
- | (Variable (_,_,poly,ctx)::idl,hyps) ->
+ (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
+ | (Variable {poly;univs}::idl,hyps) ->
let l, r = aux (idl,hyps) in
- l, if poly then Univ.ContextSet.union r ctx else r
+ l, if poly then Univ.ContextSet.union r univs else r
| (Context ctx :: idl, hyps) ->
let l, r = aux (idl, hyps) in
l, Univ.ContextSet.union r ctx
@@ -509,11 +527,11 @@ let add_section_replacement f g poly hyps =
} in
sectab := (vars,f (inst,args) exps, g info abs) :: sl
-let add_section_kn poly kn =
+let add_section_kn ~poly kn =
let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
add_section_replacement f f poly
-let add_section_constant poly kn =
+let add_section_constant ~poly kn =
let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
add_section_replacement f f poly
@@ -543,7 +561,7 @@ let variable_section_segment_of_reference gr =
let section_instance = function
| VarRef id ->
let eq = function
- | Variable (id',_,_,_) -> Names.Id.equal id id'
+ | Variable {id=id'} -> Names.Id.equal id id'
| Context _ -> false
in
if List.exists eq (pi1 (List.hd !sectab))
@@ -579,7 +597,12 @@ let open_section id =
let discharge_item ((sp,_ as oname),e) =
match e with
| Leaf lobj ->
- Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+ begin match lobj with
+ | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _
+ | ImportObject _ -> None
+ | AtomicObject obj ->
+ Option.map (fun o -> (basename sp,o)) (discharge_object (oname,obj))
+ end
| OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
anomaly (Pp.str "discharge_item.")
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 22:29:57 +0000