aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml33
-rw-r--r--library/coqlib.mli13
-rw-r--r--library/declaremods.ml3
-rw-r--r--library/decls.ml22
-rw-r--r--library/decls.mli9
-rw-r--r--library/global.ml5
-rw-r--r--library/global.mli5
-rw-r--r--library/globnames.ml50
-rw-r--r--library/globnames.mli12
-rw-r--r--library/keys.ml3
-rw-r--r--library/lib.ml59
-rw-r--r--library/lib.mli8
-rw-r--r--library/libnames.ml4
13 files changed, 60 insertions, 166 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 36a9598f36..e71de4d77e 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -119,29 +119,26 @@ let prelude_module_name = init_dir@["Prelude"]
let prelude_module = make_dir prelude_module_name
let logic_module_name = init_dir@["Logic"]
-let logic_module = make_dir logic_module_name
+let logic_module = MPfile (make_dir logic_module_name)
let logic_type_module_name = init_dir@["Logic_Type"]
let logic_type_module = make_dir logic_type_module_name
let datatypes_module_name = init_dir@["Datatypes"]
-let datatypes_module = make_dir datatypes_module_name
+let datatypes_module = MPfile (make_dir datatypes_module_name)
let jmeq_module_name = [coq;"Logic";"JMeq"]
-let jmeq_module = make_dir jmeq_module_name
-
-(* TODO: temporary hack. Works only if the module isn't an alias *)
-let make_ind dir id = Globnames.encode_mind dir (Id.of_string id)
-let make_con dir id = Globnames.encode_con dir (Id.of_string id)
+let jmeq_library_path = make_dir jmeq_module_name
+let jmeq_module = MPfile jmeq_library_path
(** Identity *)
-let id = make_con datatypes_module "idProp"
-let type_of_id = make_con datatypes_module "IDProp"
+let id = Constant.make2 datatypes_module @@ Label.make "idProp"
+let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp"
(** Natural numbers *)
-let nat_kn = make_ind datatypes_module "nat"
-let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
+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)
@@ -151,7 +148,7 @@ let glob_O = ConstructRef path_of_O
let glob_S = ConstructRef path_of_S
(** Booleans *)
-let bool_kn = make_ind datatypes_module "bool"
+let bool_kn = MutInd.make2 datatypes_module @@ Label.make "bool"
let glob_bool = IndRef (bool_kn,0)
@@ -161,13 +158,13 @@ let glob_true = ConstructRef path_of_true
let glob_false = ConstructRef path_of_false
(** Equality *)
-let eq_kn = make_ind logic_module "eq"
+let eq_kn = MutInd.make2 logic_module @@ Label.make "eq"
let glob_eq = IndRef (eq_kn,0)
-let identity_kn = make_ind datatypes_module "identity"
+let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity"
let glob_identity = IndRef (identity_kn,0)
-let jmeq_kn = make_ind jmeq_module "JMeq"
+let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq"
let glob_jmeq = IndRef (jmeq_kn,0)
type coq_sigma_data = {
@@ -349,6 +346,9 @@ let coq_iff = lazy_init_reference ["Logic"] "iff"
let coq_iff_left_proj = lazy_init_reference ["Logic"] "proj1"
let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2"
+let coq_prod = lazy_init_reference ["Datatypes"] "prod"
+let coq_pair = lazy_init_reference ["Datatypes"] "pair"
+
(* Runtime part *)
let build_coq_True () = Lazy.force coq_True
let build_coq_I () = Lazy.force coq_I
@@ -364,6 +364,9 @@ let build_coq_iff () = Lazy.force coq_iff
let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj
let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
+let build_coq_prod () = Lazy.force coq_prod
+let build_coq_pair () = Lazy.force coq_pair
+
(* The following is less readable but does not depend on parsing *)
let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
diff --git a/library/coqlib.mli b/library/coqlib.mli
index b4bd1b0e06..6a3d0953cd 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -61,12 +61,13 @@ val init_modules : string list list
(** Modules *)
val prelude_module : DirPath.t
-val logic_module : DirPath.t
+val logic_module : ModPath.t
val logic_module_name : string list
val logic_type_module : DirPath.t
-val jmeq_module : DirPath.t
+val jmeq_module : ModPath.t
+val jmeq_library_path : DirPath.t
val jmeq_module_name : string list
val datatypes_module_name : string list
@@ -101,7 +102,7 @@ val glob_jmeq : GlobRef.t
at compile time. Therefore, we can only provide methods to build
them at runtime. This is the purpose of the [constr delayed] and
[constr_pattern delayed] types. Objects of this time needs to be
- forced with [delayed_force] to get the actual constr or pattern
+ forced with [delayed_force] to get the actual constr or pattern
at runtime. *)
type coq_bool_data = {
@@ -167,7 +168,7 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed
val build_coq_sumbool : GlobRef.t delayed
(** {6 ... } *)
-(** Connectives
+(** Connectives
The False proposition *)
val build_coq_False : GlobRef.t delayed
@@ -186,6 +187,10 @@ val build_coq_iff : GlobRef.t delayed
val build_coq_iff_left_proj : GlobRef.t delayed
val build_coq_iff_right_proj : GlobRef.t delayed
+(** Pairs *)
+val build_coq_prod : GlobRef.t delayed
+val build_coq_pair : GlobRef.t delayed
+
(** Disjunction *)
val build_coq_or : GlobRef.t delayed
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0b3b461e6c..e01a99f731 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -164,8 +164,7 @@ module ModObjs :
*)
let mp_of_kn kn =
- let mp,sec,l = KerName.repr kn in
- assert (DirPath.is_empty sec);
+ let mp,l = KerName.repr kn in
MPdot (mp,l)
let dir_of_sp sp =
diff --git a/library/decls.ml b/library/decls.ml
index 12c820fb7d..b766b6e2cb 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -11,13 +11,10 @@
(** This module registers tables for some non-logical informations
associated declarations *)
-open Util
open Names
open Decl_kinds
open Libnames
-module NamedDecl = Context.Named.Declaration
-
(** Datas associated to section variables and local definitions *)
type variable_data =
@@ -47,22 +44,3 @@ let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT"
let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
let constant_kind kn = Cmap.find kn !csttab
-
-(** Miscellaneous functions. *)
-
-let initialize_named_context_for_proof () =
- let sign = Global.named_context () in
- List.fold_right
- (fun d signv ->
- let id = NamedDecl.get_id d in
- let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
- Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-
-let last_section_hyps dir =
- Context.Named.fold_outside
- (fun d sec_ids ->
- let id = NamedDecl.get_id d in
- try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
- with Not_found -> sec_ids)
- (Environ.named_context (Global.env()))
- ~init:[]
diff --git a/library/decls.mli b/library/decls.mli
index d9fc291518..401884736e 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -34,12 +34,3 @@ val variable_exists : variable -> bool
val add_constant_kind : Constant.t -> logical_kind -> unit
val constant_kind : Constant.t -> logical_kind
-
-(* Prepare global named context for proof session: remove proofs of
- opaque section definitions and remove vm-compiled code *)
-
-val initialize_named_context_for_proof : unit -> Environ.named_context_val
-
-(** Miscellaneous functions *)
-
-val last_section_hyps : DirPath.t -> Id.t list
diff --git a/library/global.ml b/library/global.ml
index 5872126a12..0e236e6d34 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -86,14 +86,13 @@ let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
let push_named_def d = globalize0 (Safe_typing.push_named_def d)
let add_constraints c = globalize0 (Safe_typing.add_constraints c)
let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
-let push_context b c = globalize0 (Safe_typing.push_context b c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
let typing_flags () = Environ.typing_flags (env ())
let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
-let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
+let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
+let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
diff --git a/library/global.mli b/library/global.mli
index 6aeae9fd02..fd6c9a60d4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -42,14 +42,13 @@ val export_private_constants : in_section:bool ->
unit Entries.definition_entry * Safe_typing.exported_private_constant list
val add_constant :
- DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t
+ in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t
val add_mind :
- DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t
+ Id.t -> Entries.mutual_inductive_entry -> MutInd.t
(** Extra universe constraints *)
val add_constraints : Univ.Constraint.t -> unit
-val push_context : bool -> Univ.UContext.t -> unit
val push_context_set : bool -> Univ.ContextSet.t -> unit
(** Non-interactive modules and module types *)
diff --git a/library/globnames.ml b/library/globnames.ml
index 6bbdd36489..9aca7788d2 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -8,11 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open CErrors
open Names
open Constr
open Mod_subst
-open Libnames
(*s Global reference is a kernel side type for all references together *)
type global_reference = GlobRef.t =
@@ -137,53 +135,5 @@ type global_reference_or_constr =
| IsGlobal of global_reference
| IsConstr of constr
-(** {6 Temporary function to brutally form kernel names from section paths } *)
-
-let encode_mind dir id = MutInd.make2 (MPfile dir) (Label.of_id id)
-
-let encode_con dir id = Constant.make2 (MPfile dir) (Label.of_id id)
-
-let check_empty_section dp =
- if not (DirPath.is_empty dp) then
- anomaly (Pp.str "Section part should be empty!")
-
-let decode_mind kn =
- let rec dir_of_mp = function
- | MPfile dir -> DirPath.repr dir
- | MPbound mbid ->
- let _,_,dp = MBId.repr mbid in
- let id = MBId.to_id mbid in
- id::(DirPath.repr dp)
- | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
- in
- let mp,sec_dir,l = MutInd.repr3 kn in
- check_empty_section sec_dir;
- (DirPath.make (dir_of_mp mp)),Label.to_id l
-
-let decode_con kn =
- let mp,sec_dir,l = Constant.repr3 kn in
- check_empty_section sec_dir;
- match mp with
- | MPfile dir -> (dir,Label.to_id l)
- | _ -> anomaly (Pp.str "MPfile expected!")
-
-(** Popping one level of section in global names.
- These functions are meant to be used during discharge:
- user and canonical kernel names must be equal. *)
-
-let pop_con con =
- let (mp,dir,l) = Constant.repr3 con in
- Constant.make3 mp (pop_dirpath dir) l
-
-let pop_kn kn =
- let (mp,dir,l) = MutInd.repr3 kn in
- MutInd.make3 mp (pop_dirpath dir) l
-
-let pop_global_reference = function
- | ConstRef con -> ConstRef (pop_con con)
- | IndRef (kn,i) -> IndRef (pop_kn kn,i)
- | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
- | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
-
(* Deprecated *)
let eq_gr = GlobRef.equal
diff --git a/library/globnames.mli b/library/globnames.mli
index 45ee069b06..a96a42ced2 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -82,15 +82,3 @@ end
type global_reference_or_constr =
| IsGlobal of GlobRef.t
| IsConstr of constr
-
-(** {6 Temporary function to brutally form kernel names from section paths } *)
-
-val encode_mind : DirPath.t -> Id.t -> MutInd.t
-val decode_mind : MutInd.t -> DirPath.t * Id.t
-val encode_con : DirPath.t -> Id.t -> Constant.t
-val decode_con : Constant.t -> DirPath.t * Id.t
-
-(** {6 Popping one level of section in global names } *)
-val pop_con : Constant.t -> Constant.t
-val pop_kn : MutInd.t-> MutInd.t
-val pop_global_reference : GlobRef.t -> GlobRef.t
diff --git a/library/keys.ml b/library/keys.ml
index a74d13c600..53447a679a 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -92,8 +92,7 @@ let subst_keys (subst,(k,k')) =
(subst_key subst k, subst_key subst k')
let discharge_key = function
- | KGlob g when Lib.is_in_section g ->
- if isVarRef g then None else Some (KGlob (pop_global_reference g))
+ | KGlob (VarRef _ as g) when Lib.is_in_section g -> None
| x -> Some x
let discharge_keys (_,(k,k')) =
diff --git a/library/lib.ml b/library/lib.ml
index 8ebe44890c..27c5056a7f 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -135,8 +135,8 @@ let make_path_except_section id =
Libnames.make_path (cwd_except_section ()) id
let make_kn id =
- let mp, dir = current_mp (), current_sections () in
- Names.KerName.make mp dir (Names.Label.of_id id)
+ let mp = current_mp () in
+ Names.KerName.make mp (Names.Label.of_id id)
let make_oname id = Libnames.make_oname !lib_state.path_prefix id
@@ -440,6 +440,21 @@ let add_section_context ctx =
check_same_poly true vars;
sectab := (Context ctx :: vars,repl,abs)::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 (function
+ | Variable (_,_,poly,(univs,_)) ->
+ if LSet.mem u univs then raise (PolyFound poly)
+ | Context (univs,_) ->
+ if LSet.mem u univs then raise (PolyFound true)
+ ) vars
+ ) !sectab;
+ false
+ with PolyFound b -> b
+
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) ->
@@ -617,44 +632,12 @@ let library_part = function
|VarRef id -> library_dp ()
|ref -> dp_of_mp (mp_of_global ref)
-(************************)
-(* Discharging names *)
-
-let con_defined_in_sec kn =
- let _,dir,_ = Names.Constant.repr3 kn in
- not (Names.DirPath.is_empty dir) &&
- Names.DirPath.equal (pop_dirpath dir) (current_sections ())
-
-let defined_in_sec kn =
- let _,dir,_ = Names.MutInd.repr3 kn in
- not (Names.DirPath.is_empty dir) &&
- Names.DirPath.equal (pop_dirpath dir) (current_sections ())
-
-let discharge_global = function
- | ConstRef kn when con_defined_in_sec kn ->
- ConstRef (Globnames.pop_con kn)
- | IndRef (kn,i) when defined_in_sec kn ->
- IndRef (Globnames.pop_kn kn,i)
- | ConstructRef ((kn,i),j) when defined_in_sec kn ->
- ConstructRef ((Globnames.pop_kn kn,i),j)
- | r -> r
-
-let discharge_kn kn =
- if defined_in_sec kn then Globnames.pop_kn kn else kn
-
-let discharge_con cst =
- if con_defined_in_sec cst then Globnames.pop_con cst else cst
-
let discharge_proj_repr =
Projection.Repr.map_npars (fun mind npars ->
- if not (defined_in_sec mind) then mind, npars
- else
- let modlist = replacement_context () in
- let _, newpars = Mindmap.find mind (snd modlist) in
- Globnames.pop_kn mind, npars + Array.length newpars)
-
-let discharge_inductive (kn,i) =
- (discharge_kn kn,i)
+ if not (is_in_section (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)
let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx =
let open Univ in
diff --git a/library/lib.mli b/library/lib.mli
index 9933b762ba..686e6a0e2d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -183,12 +183,12 @@ val add_section_kn : Decl_kinds.polymorphic ->
MutInd.t -> Constr.named_context -> unit
val replacement_context : unit -> Opaqueproof.work_list
+val is_polymorphic_univ : Univ.Level.t -> bool
+
(** {6 Discharge: decrease the section level if in the current section } *)
-val discharge_kn : MutInd.t -> MutInd.t
-val discharge_con : Constant.t -> Constant.t
+(* XXX Why can't we use the kernel functions ? *)
+
val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t
-val discharge_global : GlobRef.t -> GlobRef.t
-val discharge_inductive : inductive -> inductive
val discharge_abstract_universe_context :
abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t
diff --git a/library/libnames.ml b/library/libnames.ml
index 23085048a1..bd2ca550b9 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -171,8 +171,8 @@ type object_prefix = {
}
(* 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)
+let make_oname { obj_dir; obj_mp } id =
+ make_path obj_dir id, KerName.make obj_mp (Label.of_id id)
(* to this type are mapped DirPath.t's in the nametab *)
type global_dir_reference =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 18:13:23 +0000