aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml67
-rw-r--r--kernel/constr.mli3
-rw-r--r--kernel/entries.ml6
-rw-r--r--kernel/indtypes.ml14
-rw-r--r--kernel/indtypes.mli13
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--kernel/sorts.ml10
-rw-r--r--kernel/sorts.mli4
-rw-r--r--kernel/term_typing.ml10
-rw-r--r--kernel/univ.ml47
-rw-r--r--kernel/univ.mli10
12 files changed, 162 insertions, 30 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index d7f35da10d..704e6de6b8 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1338,3 +1338,70 @@ type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
type rel_context = rel_declaration list
type named_context = named_declaration list
type compacted_context = compacted_declaration list
+
+(* Sorts and sort family *)
+
+let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) =
+ let open Pp in
+ let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
+ hov 1
+ (str"fix " ++ int i ++ spc() ++ str"{" ++
+ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
+ Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
+ str"}")
+
+let pr_puniverses p u =
+ if Univ.Instance.is_empty u then p
+ else Pp.(p ++ str"(*" ++ Univ.Instance.pr Univ.Level.pr u ++ str"*)")
+
+(* Minimalistic constr printer, typically for debugging *)
+
+let rec debug_print c =
+ let open Pp in
+ match kind c with
+ | Rel n -> str "#"++int n
+ | Meta n -> str "Meta(" ++ int n ++ str ")"
+ | Var id -> Id.print id
+ | Sort s -> Sorts.debug_print s
+ | Cast (c,_, t) -> hov 1
+ (str"(" ++ debug_print c ++ cut() ++
+ str":" ++ debug_print t ++ str")")
+ | Prod (Name(id),t,c) -> hov 1
+ (str"forall " ++ Id.print id ++ str":" ++ debug_print t ++ str"," ++
+ spc() ++ debug_print c)
+ | Prod (Anonymous,t,c) -> hov 0
+ (str"(" ++ debug_print t ++ str " ->" ++ spc() ++
+ debug_print c ++ str")")
+ | Lambda (na,t,c) -> hov 1
+ (str"fun " ++ Name.print na ++ str":" ++
+ debug_print t ++ str" =>" ++ spc() ++ debug_print c)
+ | LetIn (na,b,t,c) -> hov 0
+ (str"let " ++ Name.print na ++ str":=" ++ debug_print b ++
+ str":" ++ brk(1,2) ++ debug_print t ++ cut() ++
+ debug_print c)
+ | App (c,l) -> hov 1
+ (str"(" ++ debug_print c ++ spc() ++
+ prlist_with_sep spc debug_print (Array.to_list l) ++ str")")
+ | Evar (e,l) -> hov 1
+ (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
+ prlist_with_sep spc debug_print (Array.to_list l) ++str"}")
+ | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")"
+ | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
+ | Construct (((sp,i),j),u) ->
+ str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
+ | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")"
+ | Case (_ci,p,c,bl) -> v 0
+ (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++
+ debug_print c ++ str"of") ++ cut() ++
+ prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++
+ cut() ++ str"end")
+ | Fix f -> debug_print_fix debug_print f
+ | CoFix(i,(lna,tl,bl)) ->
+ let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
+ hov 1
+ (str"cofix " ++ int i ++ spc() ++ str"{" ++
+ v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
+ Name.print na ++ str":" ++ debug_print ty ++
+ cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++
+ str"}")
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 8753c20eac..1be1f63ff7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -590,3 +590,6 @@ val case_info_hash : case_info -> int
(*********************************************************************)
val hcons : constr -> constr
+
+val debug_print : constr -> Pp.t
+val debug_print_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
diff --git a/kernel/entries.ml b/kernel/entries.ml
index c5bcd74072..58bb782f15 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
type inductive_universes =
| Monomorphic_ind_entry of Univ.ContextSet.t
- | Polymorphic_ind_entry of Univ.UContext.t
- | Cumulative_ind_entry of Univ.CumulativityInfo.t
+ | Polymorphic_ind_entry of Name.t array * Univ.UContext.t
+ | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t
type one_inductive_entry = {
mind_entry_typename : Id.t;
@@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
type constant_universes_entry =
| Monomorphic_const_entry of Univ.ContextSet.t
- | Polymorphic_const_entry of Univ.UContext.t
+ | Polymorphic_const_entry of Name.t array * Univ.UContext.t
type 'a in_constant_universes_entry = 'a * constant_universes_entry
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0346026aa4..20c90bc05a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -268,8 +268,8 @@ let typecheck_inductive env mie =
let env' =
match mie.mind_entry_universes with
| Monomorphic_ind_entry ctx -> push_context_set ctx env
- | Polymorphic_ind_entry ctx -> push_context ctx env
- | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+ | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
+ | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
in
let env_params = check_context env' mie.mind_entry_params in
let paramsctxt = mie.mind_entry_params in
@@ -407,7 +407,7 @@ let typecheck_inductive env mie =
match mie.mind_entry_universes with
| Monomorphic_ind_entry _ -> ()
| Polymorphic_ind_entry _ -> ()
- | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds
+ | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds
in (env_arities, env_ar_par, paramsctxt, inds)
(************************************************************************)
@@ -851,12 +851,12 @@ let compute_projections (kn, i as ind) mib =
let abstract_inductive_universes iu =
match iu with
| Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
- | Polymorphic_ind_entry ctx ->
- let (inst, auctx) = Univ.abstract_universes ctx in
+ | Polymorphic_ind_entry (nas, ctx) ->
+ let (inst, auctx) = Univ.abstract_universes nas ctx in
let inst = Univ.make_instance_subst inst in
(inst, Polymorphic_ind auctx)
- | Cumulative_ind_entry cumi ->
- let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+ | Cumulative_ind_entry (nas, cumi) ->
+ let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
let inst = Univ.make_instance_subst inst in
(inst, Cumulative_ind acumi)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index cb09cfa827..a827c17683 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -34,6 +34,19 @@ type inductive_error =
exception InductiveError of inductive_error
+val infos_and_sort : env -> constr -> Univ.Universe.t
+
+val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit
+
+val check_positivity : chkpos:bool ->
+ Names.MutInd.t ->
+ Environ.env ->
+ (Constr.constr, Constr.types) Context.Rel.pt ->
+ Declarations.recursivity_kind ->
+ ('a * Names.Id.t list * Constr.types array *
+ (('b, 'c) Context.Rel.pt * 'd))
+ array -> Int.t * Declarations.recarg Rtree.t array
+
(** The following function does checks on inductive declarations. *)
val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4b64cc6d11..df10398b2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -682,7 +682,7 @@ let constant_entry_of_side_effect cb u =
| Monomorphic_const uctx ->
Monomorphic_const_entry uctx
| Polymorphic_const auctx ->
- Polymorphic_const_entry (Univ.AUContext.repr auctx)
+ Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
in
let pt =
match cb.const_body, u with
@@ -1061,6 +1061,8 @@ type compiled_library = {
comp_natsymbs : Nativecode.symbols
}
+let module_of_library lib = lib.comp_mod
+
type native_library = Nativecode.global list
let get_library_native_symbols senv dir =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 8fb33b04d4..7af773e3bc 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -141,6 +141,8 @@ val set_share_reduction : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
val set_native_compiler : bool -> safe_transformer0
+val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
+
(** {6 Interactive module functions } *)
val start_module : Label.t -> ModPath.t safe_transformer
@@ -177,6 +179,8 @@ type compiled_library
type native_library = Nativecode.global list
+val module_of_library : compiled_library -> Declarations.module_body
+
val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
val start_library : DirPath.t -> ModPath.t safe_transformer
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index a7bb08f5b6..566dce04c6 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -102,3 +102,13 @@ module Hsorts =
end)
let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
+
+let debug_print = function
+ | Set -> Pp.(str "Set")
+ | Prop -> Pp.(str "Prop")
+ | Type u -> Pp.(str "Type(" ++ Univ.Universe.pr u ++ str ")")
+
+let pr_sort_family = function
+ | InSet -> Pp.(str "Set")
+ | InProp -> Pp.(str "Prop")
+ | InType -> Pp.(str "Type")
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index cac6229b91..6c5ce4df80 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -41,3 +41,7 @@ end
val univ_of_sort : t -> Univ.Universe.t
val sort_of_univ : Univ.Universe.t -> t
+
+val debug_print : t -> Pp.t
+
+val pr_sort_family : family -> Pp.t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index fb1b3e236c..35fa871b4e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,8 +68,8 @@ let feedback_completion_typecheck =
let abstract_constant_universes = function
| Monomorphic_const_entry uctx ->
Univ.empty_level_subst, Monomorphic_const uctx
- | Polymorphic_const_entry uctx ->
- let sbst, auctx = Univ.abstract_universes uctx in
+ | Polymorphic_const_entry (nas, uctx) ->
+ let sbst, auctx = Univ.abstract_universes nas uctx in
let sbst = Univ.make_instance_subst sbst in
sbst, Polymorphic_const auctx
@@ -78,7 +78,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
| ParameterEntry (ctx,(t,uctx),nl) ->
let env = match uctx with
| Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
- | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+ | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
in
let j = infer env t in
let usubst, univs = abstract_constant_universes uctx in
@@ -150,7 +150,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let ctx = Univ.ContextSet.union univs ctx in
let env = push_context_set ~strict:true ctx env in
env, Univ.empty_level_subst, Monomorphic_const ctx
- | Polymorphic_const_entry uctx ->
+ | Polymorphic_const_entry (nas, uctx) ->
(** Ensure not to generate internal constraints in polymorphic mode.
The only way for this to happen would be that either the body
contained deferred universes, or that it contains monomorphic
@@ -160,7 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
i.e. [trust] is always [Pure]. *)
let () = assert (Univ.ContextSet.is_empty ctx) in
let env = push_context ~strict:false uctx env in
- let sbst, auctx = Univ.abstract_universes uctx in
+ let sbst, auctx = Univ.abstract_universes nas uctx in
let sbst = Univ.make_instance_subst sbst in
env, sbst, Polymorphic_const auctx
in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d09b54e7ec..0edf750997 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,17 +937,30 @@ let hcons_universe_context = UContext.hcons
module AUContext =
struct
- include UContext
+ type t = Names.Name.t array constrained
let repr (inst, cst) =
- (Array.mapi (fun i _l -> Level.var i) inst, cst)
+ (Array.init (Array.length inst) (fun i -> Level.var i), cst)
- let pr f ?variance ctx = pr f ?variance (repr ctx)
+ let pr f ?variance ctx = UContext.pr f ?variance (repr ctx)
let instantiate inst (u, cst) =
assert (Array.length u = Array.length inst);
subst_instance_constraints inst cst
+ let names (nas, _) = nas
+
+ let hcons (univs, cst) =
+ (Array.map Names.Name.hcons univs, hcons_constraints cst)
+
+ let empty = ([||], Constraint.empty)
+
+ let is_empty (nas, cst) = Array.is_empty nas && Constraint.is_empty cst
+
+ let union (nas, cst) (nas', cst') = (Array.append nas nas', Constraint.union cst cst')
+
+ let size (nas, _) = Array.length nas
+
end
let hcons_abstract_universe_context = AUContext.hcons
@@ -993,7 +1006,22 @@ end
let hcons_cumulativity_info = CumulativityInfo.hcons
-module ACumulativityInfo = CumulativityInfo
+module ACumulativityInfo =
+struct
+ type t = AUContext.t * Variance.t array
+
+ let pr prl (univs, variance) =
+ AUContext.pr prl ~variance univs
+
+ let hcons (univs, variance) = (* should variance be hconsed? *)
+ (AUContext.hcons univs, variance)
+
+ let univ_context (univs, _subtypcst) = univs
+ let variance (_univs, variance) = variance
+
+ let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
+ let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
+end
let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
@@ -1145,19 +1173,20 @@ let make_inverse_instance_subst i =
LMap.empty arr
let make_abstract_instance (ctx, _) =
- Array.mapi (fun i _l -> Level.var i) ctx
+ Array.init (Array.length ctx) (fun i -> Level.var i)
-let abstract_universes ctx =
+let abstract_universes nas ctx =
let instance = UContext.instance ctx in
+ let () = assert (Int.equal (Array.length nas) (Instance.length instance)) in
let subst = make_instance_subst instance in
let cstrs = subst_univs_level_constraints subst
(UContext.constraints ctx)
in
- let ctx = UContext.make (instance, cstrs) in
+ let ctx = (nas, cstrs) in
instance, ctx
-let abstract_cumulativity_info (univs, variance) =
- let subst, univs = abstract_universes univs in
+let abstract_cumulativity_info nas (univs, variance) =
+ let subst, univs = abstract_universes nas univs in
subst, (univs, variance)
let rec compact_univ s vars i u =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7ac8247ca4..de7b334ae4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -336,9 +336,6 @@ sig
val empty : t
val is_empty : t -> bool
- (** Don't use. *)
- val instance : t -> Instance.t
-
val size : t -> int
(** Keeps the order of the instances *)
@@ -347,6 +344,9 @@ sig
val instantiate : Instance.t -> t -> Constraint.t
(** Generate the set of instantiated Constraint.t **)
+ val names : t -> Names.Name.t array
+ (** Return the names of the bound universe variables *)
+
end
(** Universe info for cumulative inductive types: A context of
@@ -466,8 +466,8 @@ val make_instance_subst : Instance.t -> universe_level_subst
val make_inverse_instance_subst : Instance.t -> universe_level_subst
-val abstract_universes : UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
+val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
(** TODO: move universe abstraction out of the kernel *)
val make_abstract_instance : AUContext.t -> Instance.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 20:31:11 +0000