aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml21
-rw-r--r--library/globnames.ml18
-rw-r--r--library/globnames.mli9
-rw-r--r--library/keys.ml17
-rw-r--r--library/lib.ml99
-rw-r--r--library/lib.mli2
-rw-r--r--library/nametab.ml5
7 files changed, 96 insertions, 75 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 7cd2e50274..b1e4ef2b00 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -13,7 +13,6 @@ open Util
open Pp
open Names
open Libnames
-open Globnames
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
@@ -46,7 +45,7 @@ let has_ref s = CString.Map.mem s !table
let check_ind_ref s ind =
match CString.Map.find s !table with
- | IndRef r -> eq_ind r ind
+ | GlobRef.IndRef r -> eq_ind r ind
| _ -> false
| exception Not_found -> false
@@ -157,32 +156,32 @@ let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp"
let nat_kn = MutInd.make2 datatypes_module @@ Label.make "nat"
let nat_path = Libnames.make_path (make_dir datatypes_module_name) (Id.of_string "nat")
-let glob_nat = IndRef (nat_kn,0)
+let glob_nat = GlobRef.IndRef (nat_kn,0)
let path_of_O = ((nat_kn,0),1)
let path_of_S = ((nat_kn,0),2)
-let glob_O = ConstructRef path_of_O
-let glob_S = ConstructRef path_of_S
+let glob_O = GlobRef.ConstructRef path_of_O
+let glob_S = GlobRef.ConstructRef path_of_S
(** Booleans *)
let bool_kn = MutInd.make2 datatypes_module @@ Label.make "bool"
-let glob_bool = IndRef (bool_kn,0)
+let glob_bool = GlobRef.IndRef (bool_kn,0)
let path_of_true = ((bool_kn,0),1)
let path_of_false = ((bool_kn,0),2)
-let glob_true = ConstructRef path_of_true
-let glob_false = ConstructRef path_of_false
+let glob_true = GlobRef.ConstructRef path_of_true
+let glob_false = GlobRef.ConstructRef path_of_false
(** Equality *)
let eq_kn = MutInd.make2 logic_module @@ Label.make "eq"
-let glob_eq = IndRef (eq_kn,0)
+let glob_eq = GlobRef.IndRef (eq_kn,0)
let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity"
-let glob_identity = IndRef (identity_kn,0)
+let glob_identity = GlobRef.IndRef (identity_kn,0)
let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq"
-let glob_jmeq = IndRef (jmeq_kn,0)
+let glob_jmeq = GlobRef.IndRef (jmeq_kn,0)
(* Sigma data *)
type coq_sigma_data = {
diff --git a/library/globnames.ml b/library/globnames.ml
index 71447c4b81..acb05f9ac0 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -12,12 +12,14 @@ open Names
open Constr
open Mod_subst
-(*s Global reference is a kernel side type for all references together *)
type global_reference = GlobRef.t =
- | VarRef of variable (** A reference to the section-context. *)
- | ConstRef of Constant.t (** A reference to the environment. *)
- | IndRef of inductive (** A reference to an inductive type. *)
- | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
+ | VarRef of variable [@ocaml.deprecated "Use Names.GlobRef.VarRef"]
+ | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"]
+ | IndRef of inductive [@ocaml.deprecated "Use Names.GlobRef.IndRef"]
+ | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"]
+[@@ocaml.deprecated "Use Names.GlobRef.t"]
+
+open GlobRef
let isVarRef = function VarRef _ -> true | _ -> false
let isConstRef = function ConstRef _ -> true | _ -> false
@@ -90,7 +92,7 @@ let printable_constr_of_global = function
type syndef_name = KerName.t
type extended_global_reference =
- | TrueGlobal of global_reference
+ | TrueGlobal of GlobRef.t
| SynDef of syndef_name
(* We order [extended_global_reference] via their user part
@@ -122,6 +124,6 @@ module ExtRefOrdered = struct
end
-type global_reference_or_constr =
- | IsGlobal of global_reference
+type global_reference_or_constr =
+ | IsGlobal of GlobRef.t
| IsConstr of constr
diff --git a/library/globnames.mli b/library/globnames.mli
index 547755b088..fc0de96e36 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -12,12 +12,11 @@ open Names
open Constr
open Mod_subst
-(** {6 Global reference is a kernel side type for all references together } *)
type global_reference = GlobRef.t =
- | VarRef of variable (** A reference to the section-context. *)
- | ConstRef of Constant.t (** A reference to the environment. *)
- | IndRef of inductive (** A reference to an inductive type. *)
- | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
+ | VarRef of variable [@ocaml.deprecated "Use Names.GlobRef.VarRef"]
+ | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"]
+ | IndRef of inductive [@ocaml.deprecated "Use Names.GlobRef.IndRef"]
+ | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"]
[@@ocaml.deprecated "Use Names.GlobRef.t"]
val isVarRef : GlobRef.t -> bool
diff --git a/library/keys.ml b/library/keys.ml
index 30ecc9dfdb..9964992433 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -94,7 +94,7 @@ let subst_keys (subst,(k,k')) =
(subst_key subst k, subst_key subst k')
let discharge_key = function
- | KGlob (VarRef _ as g) when Lib.is_in_section g -> None
+ | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None
| x -> Some x
let discharge_keys (_,(k,k')) =
@@ -114,16 +114,15 @@ let declare_equiv_keys ref ref' =
Lib.add_anonymous_leaf (inKeys (ref,ref'))
let constr_key kind c =
- let open Globnames in
- try
- let rec aux k =
+ try
+ let rec aux k =
match kind k with
- | Const (c, _) -> KGlob (ConstRef c)
- | Ind (i, u) -> KGlob (IndRef i)
- | Construct (c,u) -> KGlob (ConstructRef c)
- | Var id -> KGlob (VarRef id)
+ | Const (c, _) -> KGlob (GlobRef.ConstRef c)
+ | Ind (i, u) -> KGlob (GlobRef.IndRef i)
+ | Construct (c,u) -> KGlob (GlobRef.ConstructRef c)
+ | Var id -> KGlob (GlobRef.VarRef id)
| App (f, _) -> aux f
- | Proj (p, _) -> KGlob (ConstRef (Projection.constant p))
+ | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p))
| Cast (p, _, _) -> aux p
| Lambda _ -> KLam
| Prod _ -> KProd
diff --git a/library/lib.ml b/library/lib.ml
index 576e23c4f5..59b55cc16b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -13,7 +13,6 @@ open CErrors
open Util
open Names
open Libnames
-open Globnames
open Libobject
open Context.Named.Declaration
@@ -428,46 +427,60 @@ type secentry =
| Variable of {
id:Names.Id.t;
kind:Decl_kinds.binding_kind;
- poly:bool;
univs:Univ.ContextSet.t;
}
| Context of Univ.ContextSet.t
-let sectab =
- Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list)
- ~name:"section-context"
+type section_data = {
+ sec_entry : secentry list;
+ sec_workl : Opaqueproof.work_list;
+ sec_abstr : abstr_list;
+ sec_poly : bool;
+}
-let add_section () =
- sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),
- (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
+let empty_section_data ~poly = {
+ sec_entry = [];
+ sec_workl = (Names.Cmap.empty,Names.Mindmap.empty);
+ sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
+ sec_poly = poly;
+}
-let check_same_poly p vars =
- let pred = function Context _ -> p = false | Variable {poly} -> p != poly in
- if List.exists pred vars then
+let sectab =
+ Summary.ref ([] : section_data list) ~name:"section-context"
+
+let check_same_poly p sec =
+ if p != sec.sec_poly then
user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
+let add_section ~poly () =
+ List.iter (fun tab -> check_same_poly poly tab) !sectab;
+ sectab := empty_section_data ~poly :: !sectab
+
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=name;kind;poly;univs}::vars,repl,abs)::sl
+ | s :: sl ->
+ List.iter (fun tab -> check_same_poly poly tab) !sectab;
+ let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in
+ sectab := s :: sl
let add_section_context ctx =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
- | (vars,repl,abs)::sl ->
- check_same_poly true vars;
- sectab := (Context ctx :: vars,repl,abs)::sl
+ | s :: sl ->
+ check_same_poly true s;
+ let s = { s with sec_entry = Context ctx :: s.sec_entry } in
+ sectab := s :: sl
exception PolyFound of bool (* make this a let exception once possible *)
let is_polymorphic_univ u =
try
let open Univ in
- List.iter (fun (vars,_,_) ->
+ List.iter (fun s ->
+ let vars = s.sec_entry in
List.iter (function
- | Variable {poly;univs=(univs,_)} ->
- if LSet.mem u univs then raise (PolyFound poly)
+ | Variable {univs=(univs,_)} ->
+ if LSet.mem u univs then raise (PolyFound s.sec_poly)
| Context (univs,_) ->
if LSet.mem u univs then raise (PolyFound true)
) vars
@@ -475,12 +488,12 @@ let is_polymorphic_univ u =
false
with PolyFound b -> b
-let extract_hyps (secs,ohyps) =
+let extract_hyps poly (secs,ohyps) =
let rec aux = function
- | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+ | (Variable {id;kind;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
let l, r = aux (idl,hyps) in
(decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
- | (Variable {poly;univs}::idl,hyps) ->
+ | (Variable {univs}::idl,hyps) ->
let l, r = aux (idl,hyps) in
l, if poly then Univ.ContextSet.union r univs else r
| (Context ctx :: idl, hyps) ->
@@ -512,9 +525,9 @@ let name_instance inst =
let add_section_replacement f g poly hyps =
match !sectab with
| [] -> ()
- | (vars,exps,abs)::sl ->
- let () = check_same_poly poly vars in
- let sechyps,ctx = extract_hyps (vars,hyps) in
+ | s :: sl ->
+ let () = check_same_poly poly s in
+ let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in
let ctx = Univ.ContextSet.to_context ctx in
let inst = Univ.UContext.instance ctx in
let nas = name_instance inst in
@@ -525,7 +538,11 @@ let add_section_replacement f g poly hyps =
abstr_subst = subst;
abstr_uctx = ctx;
} in
- sectab := (vars,f (inst,args) exps, g info abs) :: sl
+ let s = { s with
+ sec_workl = f (inst, args) s.sec_workl;
+ sec_abstr = g info s.sec_abstr;
+ } in
+ sectab := s :: sl
let add_section_kn ~poly kn =
let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -535,13 +552,13 @@ 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
-let replacement_context () = pi2 (List.hd !sectab)
+let replacement_context () = (List.hd !sectab).sec_workl
let section_segment_of_constant con =
- Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
+ Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
let section_segment_of_mutual_inductive kn =
- Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
+ Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr)
let empty_segment = {
abstr_ctx = [];
@@ -549,7 +566,7 @@ let empty_segment = {
abstr_uctx = Univ.AUContext.empty;
}
-let section_segment_of_reference = function
+let section_segment_of_reference = let open GlobRef in function
| ConstRef c -> section_segment_of_constant c
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
section_segment_of_mutual_inductive kn
@@ -558,26 +575,26 @@ let section_segment_of_reference = function
let variable_section_segment_of_reference gr =
(section_segment_of_reference gr).abstr_ctx
-let section_instance = function
+let section_instance = let open GlobRef in function
| VarRef id ->
let eq = function
| Variable {id=id'} -> Names.Id.equal id id'
| Context _ -> false
in
- if List.exists eq (pi1 (List.hd !sectab))
+ if List.exists eq (List.hd !sectab).sec_entry
then Univ.Instance.empty, [||]
else raise Not_found
| ConstRef con ->
- Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
+ Names.Cmap.find con (fst (List.hd !sectab).sec_workl)
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
- Names.Mindmap.find kn (snd (pi2 (List.hd !sectab)))
+ Names.Mindmap.find kn (snd (List.hd !sectab).sec_workl)
let is_in_section ref =
try ignore (section_instance ref); true with Not_found -> false
(*************)
(* Sections. *)
-let open_section id =
+let open_section ~poly id =
let opp = !lib_state.path_prefix in
let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
@@ -588,7 +605,7 @@ let open_section id =
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
lib_state := { !lib_state with path_prefix = prefix };
- add_section ()
+ add_section ~poly ()
(* Restore lib_stk and summaries as before the section opening, and
@@ -647,7 +664,7 @@ let init () =
(* Misc *)
-let mp_of_global = function
+let mp_of_global = let open GlobRef in function
| VarRef id -> !lib_state.path_prefix.Nametab.obj_mp
| ConstRef cst -> Names.Constant.modpath cst
| IndRef ind -> Names.ind_modpath ind
@@ -666,12 +683,12 @@ let rec split_modpath = function
(dp, Names.Label.to_id l :: ids)
let library_part = function
- |VarRef id -> library_dp ()
- |ref -> dp_of_mp (mp_of_global ref)
+ | GlobRef.VarRef id -> library_dp ()
+ | ref -> dp_of_mp (mp_of_global ref)
let discharge_proj_repr =
Projection.Repr.map_npars (fun mind npars ->
- if not (is_in_section (IndRef (mind,0))) then mind, npars
+ if not (is_in_section (GlobRef.IndRef (mind,0))) then mind, npars
else let modlist = replacement_context () in
let _, newpars = Mindmap.find mind (snd modlist) in
mind, npars + Array.length newpars)
diff --git a/library/lib.mli b/library/lib.mli
index 01366ddfd0..fe6bf69ec4 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -147,7 +147,7 @@ val library_part : GlobRef.t -> DirPath.t
(** {6 Sections } *)
-val open_section : Id.t -> unit
+val open_section : poly:bool -> Id.t -> unit
val close_section : unit -> unit
(** {6 We can get and set the state of the operations (used in [States]). } *)
diff --git a/library/nametab.ml b/library/nametab.ml
index 71ee7a6d5a..aed7d08ac1 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -392,6 +392,7 @@ let push_xref visibility sp xref =
| _ ->
begin
if ExtRefTab.exists sp !the_ccitab then
+ let open GlobRef in
match ExtRefTab.find sp !the_ccitab with
| TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
TrueGlobal( ConstructRef _) as xref ->
@@ -483,6 +484,7 @@ let completion_canditates qualid =
(* Derived functions *)
let locate_constant qid =
+ let open GlobRef in
match locate_extended qid with
| TrueGlobal (ConstRef kn) -> kn
| _ -> raise Not_found
@@ -517,6 +519,7 @@ let exists_universe kn = UnivTab.exists kn !the_univtab
(* Reverse locate functions ***********************************************)
let path_of_global ref =
+ let open GlobRef in
match ref with
| VarRef id -> make_path DirPath.empty id
| _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
@@ -542,6 +545,7 @@ let path_of_universe mp =
(* Shortest qualid functions **********************************************)
let shortest_qualid_of_global ?loc ctx ref =
+ let open GlobRef in
match ref with
| VarRef id -> make_qualid ?loc DirPath.empty id
| _ ->
@@ -570,6 +574,7 @@ let pr_global_env env ref =
if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
let global_inductive qid =
+ let open GlobRef in
match global qid with
| IndRef ind -> ind
| ref ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 23:20:41 +0000