aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml15
-rw-r--r--kernel/constr.mli2
-rw-r--r--kernel/context.ml8
-rw-r--r--kernel/context.mli2
-rw-r--r--kernel/cooking.ml22
-rw-r--r--kernel/declarations.ml5
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/environ.ml19
-rw-r--r--kernel/environ.mli24
-rw-r--r--kernel/float64.ml16
-rw-r--r--kernel/indTyping.ml33
-rw-r--r--kernel/indTyping.mli1
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/inductive.ml48
-rw-r--r--kernel/inductive.mli18
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/safe_typing.mli6
-rw-r--r--kernel/subtyping.ml4
-rw-r--r--kernel/term.ml21
-rw-r--r--kernel/term.mli11
-rw-r--r--kernel/type_errors.ml11
-rw-r--r--kernel/type_errors.mli16
-rw-r--r--kernel/typeops.ml28
-rw-r--r--kernel/typeops.mli2
-rw-r--r--kernel/uGraph.ml2
-rw-r--r--kernel/univ.ml34
-rw-r--r--kernel/univ.mli5
27 files changed, 173 insertions, 198 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 15e5c512ed..84eacb196c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -253,7 +253,7 @@ let mkFloat f = Float f
least one argument and the function is not itself an applicative
term *)
-let kind c = c
+let kind (c:t) = c
let rec kind_nocast_gen kind c =
match kind c with
@@ -338,6 +338,19 @@ let isProj c = match kind c with Proj _ -> true | _ -> false
let isFix c = match kind c with Fix _ -> true | _ -> false
let isCoFix c = match kind c with CoFix _ -> true | _ -> false
+let isRef c = match kind c with
+ | Const _ | Ind _ | Construct _ | Var _ -> true
+ | _ -> false
+
+let isRefX x c =
+ let open GlobRef in
+ match x, kind c with
+ | ConstRef c, Const (c', _) -> Constant.equal c c'
+ | IndRef i, Ind (i', _) -> eq_ind i i'
+ | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+ | VarRef id, Var id' -> Id.equal id id'
+ | _ -> false
+
(* Destructs a de Bruijn index *)
let destRel c = match kind c with
| Rel n -> n
diff --git a/kernel/constr.mli b/kernel/constr.mli
index d4af1149c2..159570b5ea 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -256,6 +256,8 @@ val isRel : constr -> bool
val isRelN : int -> constr -> bool
val isVar : constr -> bool
val isVarId : Id.t -> constr -> bool
+val isRef : constr -> bool
+val isRefX : GlobRef.t -> constr -> bool
val isInd : constr -> bool
val isEvar : constr -> bool
val isMeta : constr -> bool
diff --git a/kernel/context.ml b/kernel/context.ml
index 7e394da2ed..500ed20343 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -196,12 +196,10 @@ struct
(** Return a new rel-context enriched by with a given inner-most declaration. *)
let add d ctx = d :: ctx
- (** Return the number of {e local declarations} in a given context. *)
+ (** Return the number of {e local declarations} in a given rel-context. *)
let length = List.length
- (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
- with n = |Δ| and with the local definitions of [Γ] skipped in
- [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+ (** Return the number of {e local assumptions} in a given rel-context. *)
let nhyps ctx =
let open Declaration in
let rec nhyps acc = function
@@ -413,7 +411,7 @@ struct
(** empty named-context *)
let empty = []
- (** empty named-context *)
+ (** Return a new named-context enriched by with a given inner-most declaration. *)
let add d ctx = d :: ctx
(** Return the number of {e local declarations} in a given named-context. *)
diff --git a/kernel/context.mli b/kernel/context.mli
index 8f233613da..04aa039a01 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -129,7 +129,7 @@ sig
(** Return a new rel-context enriched by with a given inner-most declaration. *)
val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
- (** Return the number of {e local declarations} in a given context. *)
+ (** Return the number of {e local declarations} in a given rel-context. *)
val length : ('c, 't) pt -> int
(** Check whether given two rel-contexts are equal. *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cebbfe4986..31dd26d2ba 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -258,17 +258,6 @@ let cook_constant { from = cb; info } =
(********************************)
(* Discharging mutual inductive *)
-let template_level_of_var ~template_check d =
- (* When [template_check], a universe from a section variable may not
- be in the universes from the inductive (it must be pre-declared)
- so always [None]. *)
- if template_check then None
- else
- let c = Term.strip_prod_assum (RelDecl.get_type d) in
- match kind c with
- | Sort (Type u) -> Univ.Universe.level u
- | _ -> None
-
let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
let abstract_rel_ctx (section_decls,subst) ctx =
@@ -305,21 +294,21 @@ let abstract_projection ~params expmod hyps t =
let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in
t
-let cook_one_ind ~template_check ~ntypes
+let cook_one_ind ~ntypes
(section_decls,_ as hyps) expmod mip =
let mind_arity = match mip.mind_arity with
| RegularArity {mind_user_arity=arity;mind_sort=sort} ->
let arity = abstract_as_type (expmod arity) hyps in
let sort = destSort (expmod (mkSort sort)) in
RegularArity {mind_user_arity=arity; mind_sort=sort}
- | TemplateArity {template_param_levels=levels;template_level} ->
+ | TemplateArity {template_param_levels=levels;template_level;template_context} ->
let sec_levels = CList.map_filter (fun d ->
- if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d)
+ if RelDecl.is_local_assum d then Some None
else None)
section_decls
in
let levels = List.rev_append sec_levels levels in
- TemplateArity {template_param_levels=levels;template_level}
+ TemplateArity {template_param_levels=levels;template_level;template_context}
in
let mind_arity_ctxt =
let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
@@ -362,14 +351,13 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
let removed_vars = Context.Named.to_vars section_decls in
let section_decls, _ as hyps = abstract_context section_decls in
let nnewparams = Context.Rel.nhyps section_decls in
- let template_check = mib.mind_typing_flags.check_template in
let mind_params_ctxt =
let ctx = Context.Rel.map expmod mib.mind_params_ctxt in
abstract_rel_ctx hyps ctx
in
let ntypes = mib.mind_ntypes in
let mind_packets =
- Array.map (cook_one_ind ~template_check ~ntypes hyps expmod)
+ Array.map (cook_one_ind ~ntypes hyps expmod)
mib.mind_packets
in
let mind_record = match mib.mind_record with
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0b6e59bd5e..ac130d018d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -32,6 +32,7 @@ type engagement = set_predicativity
type template_arity = {
template_param_levels : Univ.Level.t option list;
template_level : Univ.Universe.t;
+ template_context : Univ.ContextSet.t;
}
type ('a, 'b) declaration_arity =
@@ -88,10 +89,6 @@ type typing_flags = {
indices_matter: bool;
(** The universe of an inductive type must be above that of its indices. *)
- check_template : bool;
- (* If [false] then we don't check that the universes template-polymorphic
- inductive parameterize on are necessarily local and unbounded from below.
- This potentially introduces inconsistencies. *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 27e3f84464..a3adac7a11 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,7 +26,6 @@ let safe_flags oracle = {
enable_VM = true;
enable_native_compiler = true;
indices_matter = true;
- check_template = true;
}
(** {6 Arities } *)
@@ -49,7 +48,8 @@ let map_decl_arity f g = function
let hcons_template_arity ar =
{ template_param_levels = ar.template_param_levels;
(* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
- template_level = Univ.hcons_univ ar.template_level }
+ template_level = Univ.hcons_univ ar.template_level;
+ template_context = Univ.hcons_universe_context_set ar.template_context }
let universes_context = function
| Monomorphic _ -> Univ.AUContext.empty
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f04863386f..501ac99ff3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -275,7 +275,6 @@ let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
let indices_matter env = env.env_typing_flags.indices_matter
-let check_template env = env.env_typing_flags.check_template
let universes env = env.env_stratification.env_universes
let universes_lbound env = env.env_stratification.env_universes_lbound
@@ -399,9 +398,6 @@ let add_constraints c env =
let check_constraints c env =
UGraph.check_constraints c env.env_stratification.env_universes
-let push_constraints_to_env (_,univs) env =
- add_constraints univs env
-
let add_universes ~lbound ~strict ctx g =
let g = Array.fold_left
(fun g v -> UGraph.add_universe ~lbound ~strict v g)
@@ -449,7 +445,6 @@ let same_flags {
share_reduction;
enable_VM;
enable_native_compiler;
- check_template;
} alt =
check_guarded == alt.check_guarded &&
check_positive == alt.check_positive &&
@@ -458,8 +453,7 @@ let same_flags {
indices_matter == alt.indices_matter &&
share_reduction == alt.share_reduction &&
enable_VM == alt.enable_VM &&
- enable_native_compiler == alt.enable_native_compiler &&
- check_template == alt.check_template
+ enable_native_compiler == alt.enable_native_compiler
[@warning "+9"]
let set_typing_flags c env = (* Unsafe *)
@@ -591,9 +585,6 @@ let polymorphic_pind (ind,u) env =
let type_in_type_ind (mind,_i) env =
not (lookup_mind mind env).mind_typing_flags.check_universes
-let template_checked_ind (mind,_i) env =
- (lookup_mind mind env).mind_typing_flags.check_template
-
let template_polymorphic_ind (mind,i) env =
match (lookup_mind mind env).mind_packets.(i).mind_arity with
| TemplateArity _ -> true
@@ -802,14 +793,6 @@ let get_template_polymorphic_variables env r =
| IndRef ind -> template_polymorphic_variables ind env
| ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
-let is_template_checked env r =
- let open Names.GlobRef in
- match r with
- | VarRef _id -> false
- | ConstRef _c -> false
- | IndRef ind -> template_checked_ind ind env
- | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
-
let is_type_in_type env r =
let open Names.GlobRef in
match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index bd5a000c2b..a596584cbe 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -112,7 +112,6 @@ val is_impredicative_set : env -> bool
val type_in_type : env -> bool
val deactivated_guard : env -> bool
val indices_matter : env -> bool
-val check_template : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -274,7 +273,6 @@ val type_in_type_ind : inductive -> env -> bool
val template_polymorphic_ind : inductive -> env -> bool
val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
val template_polymorphic_pind : pinductive -> env -> bool
-val template_checked_ind : inductive -> env -> bool
(** {5 Modules } *)
@@ -288,22 +286,21 @@ val lookup_modtype : ModPath.t -> env -> module_type_body
(** {5 Universe constraints } *)
-(** Add universe constraints to the environment.
- @raise UniverseInconsistency .
-*)
val add_constraints : Univ.Constraint.t -> env -> env
+(** Add universe constraints to the environment.
+ @raise UniverseInconsistency. *)
-(** Check constraints are satifiable in the environment. *)
val check_constraints : Univ.Constraint.t -> env -> bool
+(** Check constraints are satifiable in the environment. *)
+
val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
-(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment.
- @raise UGraph.AlreadyDeclared if one of the universes is already declared.
-*)
-val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
-(* [push_context_set ?(strict=false) ctx env] pushes the universe context set
- to the environment. It does not fail if one of the universes is already declared. *)
+(** [push_context ?(strict=false) ctx env] pushes the universe context to the environment.
+ @raise UGraph.AlreadyDeclared if one of the universes is already declared. *)
-val push_constraints_to_env : 'a Univ.constrained -> env -> env
+val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
+(** [push_context_set ?(strict=false) ctx env] pushes the universe
+ context set to the environment. It does not fail even if one of the
+ universes is already declared. *)
val push_subgraph : Univ.ContextSet.t -> env -> env
(** [push_subgraph univs env] adds the universes and constraints in
@@ -373,7 +370,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
val is_polymorphic : env -> Names.GlobRef.t -> bool
val is_template_polymorphic : env -> GlobRef.t -> bool
val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
-val is_template_checked : env -> GlobRef.t -> bool
val is_type_in_type : env -> GlobRef.t -> bool
(** Native compiler *)
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 3e36373b77..cc661aeba3 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -12,7 +12,10 @@
format *)
type t = float
-let is_nan f = f <> f
+(* The [f : float] type annotation enable the compiler to compile f <> f
+ as comparison on floats rather than the polymorphic OCaml comparison
+ which is much slower. *)
+let is_nan (f : float) = f <> f
let is_infinity f = f = infinity
let is_neg_infinity f = f = neg_infinity
@@ -42,19 +45,20 @@ let abs = abs_float
type float_comparison = FEq | FLt | FGt | FNotComparable
-let eq x y = x = y
+(* See above comment on [is_nan] for the [float] type annotations. *)
+let eq (x : float) (y : float) = x = y
[@@ocaml.inline always]
-let lt x y = x < y
+let lt (x : float) (y : float) = x < y
[@@ocaml.inline always]
-let le x y = x <= y
+let le (x : float) (y : float) = x <= y
[@@ocaml.inline always]
(* inspired by lib/util.ml; see also #10471 *)
-let pervasives_compare = compare
+let pervasives_compare (x : float) (y : float) = compare x y
-let compare x y =
+let compare (x : float) (y : float) =
if x < y then FLt
else
(
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 591cd050a5..cc15109f06 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -66,7 +66,9 @@ let mind_check_names mie =
type univ_info = { ind_squashed : bool; ind_has_relevant_arg : bool;
ind_min_univ : Universe.t option; (* Some for template *)
- ind_univ : Universe.t }
+ ind_univ : Universe.t;
+ missing : Universe.Set.t; (* missing u <= ind_univ constraints *)
+ }
let check_univ_leq ?(is_real_arg=false) env u info =
let ind_univ = info.ind_univ in
@@ -78,9 +80,8 @@ let check_univ_leq ?(is_real_arg=false) env u info =
if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
else if is_impredicative_univ env ind_univ
- then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
- else raise (InductiveError BadUnivs)
- else raise (InductiveError BadUnivs)
+ && Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
+ else {info with missing = Universe.Set.add u info.missing}
let check_context_univs ~ctor env info ctx =
let check_one d (info,env) =
@@ -109,6 +110,7 @@ let check_arity env_params env_ar ind =
ind_has_relevant_arg=false;
ind_min_univ;
ind_univ=Sorts.univ_of_sort ind_sort;
+ missing=Universe.Set.empty;
}
in
let univ_info = check_indices_matter env_params univ_info indices in
@@ -174,7 +176,7 @@ let check_record data =
(* - all_sorts in case of small, unitary Prop (not smashed) *)
(* - logical_sorts in case of large, unitary Prop (smashed) *)
-let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} =
+let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_;missing=_} =
if not ind_squashed then InType
else Sorts.family (Sorts.sort_of_univ ind_univ)
@@ -195,7 +197,7 @@ let unbounded_from_below u cstrs =
(starting from the most recent and ignoring let-definitions) is not
contributing to the inductive type's sort or is Some u_k if its level
is u_k and is contributing. *)
-let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl =
+let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl =
let check_level l =
Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
@@ -203,27 +205,25 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc
in
let univs = Univ.Universe.levels concl in
let univs =
- if template_check then
- Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
- else univs (* Doesn't check the universes can be generalized *)
+ Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
in
let fold acc = function
| (LocalAssum (_, p)) ->
(let c = Term.strip_prod_assum p in
match kind c with
| Sort (Type u) ->
- if template_check then
(match Univ.Universe.level u with
| Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
| None -> None)
- else Univ.Universe.level u
| _ -> None) :: acc
| LocalDef _ -> acc
in
let params = List.fold_left fold [] paramsctxt in
params, univs
-let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+ if not (Universe.Set.is_empty univ_info.missing)
+ then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
let arity = Vars.subst_univs_level_constr usubst arity in
let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
let indices = Vars.subst_univs_level_context usubst indices in
@@ -263,14 +263,14 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
splayed_lc
in
let param_levels, concl_levels =
- template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ
+ template_polymorphic_univs ~ctor_levels ctx params min_univ
in
- if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+ if List.for_all (fun x -> Option.is_empty x) param_levels
&& Univ.LSet.is_empty concl_levels then
CErrors.user_err
Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
else
- TemplateArity {template_param_levels = param_levels; template_level = min_univ}
+ TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
in
let kelim = allowed_sorts univ_info in
@@ -352,8 +352,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
(* Abstract universes *)
let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
let params = Vars.subst_univs_level_context usubst params in
- let template_check = Environ.check_template env in
- let data = List.map (abstract_packets ~template_check univs usubst params) data in
+ let data = List.map (abstract_packets univs usubst params) data in
let env_ar_par =
let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8dea8f046d..723ba5459e 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -40,7 +40,6 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
(* Utility function to compute the actual universe parameters
of a template polymorphic inductive *)
val template_polymorphic_univs :
- template_check:bool ->
ctor_levels:Univ.LSet.t ->
Univ.ContextSet.t ->
Constr.rel_context ->
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 3771454db5..b6b8e5265c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -158,7 +158,7 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
let auxntyp = 1 in
let specif = (lookup_mind_specif env mi, u) in
- let ty = type_of_inductive env specif in
+ let ty = type_of_inductive specif in
let env' =
let r = (snd (fst specif)).mind_relevance in
let anon = Context.make_annot Anonymous r in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca4fea45c5..c6035f78ff 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -143,9 +143,16 @@ let remember_subst u subst =
Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
with Not_found -> subst
+type param_univs = (unit -> Universe.t) list
+
+let make_param_univs env argtys =
+ Array.map_to_list (fun arg () ->
+ Sorts.univ_of_sort (snd (Reduction.dest_arity env arg)))
+ argtys
+
(* Bind expected levels of parameters to actual levels *)
(* Propagate the new levels in the signature *)
-let make_subst env =
+let make_subst =
let rec make subst = function
| LocalDef _ :: sign, exp, args ->
make subst (sign, exp, args)
@@ -158,8 +165,8 @@ let make_subst env =
(* arity is a global level which, at typing time, will be enforce *)
(* to be greater than the level of the argument; this is probably *)
(* a useless extra constraint *)
- let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in
- make (cons_subst u s subst) (sign, exp, args)
+ let s = a () in
+ make (cons_subst u s subst) (sign, exp, args)
| LocalAssum (_na,_t) :: sign, Some u::exp, [] ->
(* No more argument here: we add the remaining universes to the *)
(* substitution (when [u] is distinct from all other universes in the *)
@@ -178,9 +185,8 @@ let make_subst env =
exception SingletonInductiveBecomesProp of Id.t
-let instantiate_universes env ctx ar argsorts =
- let args = Array.to_list argsorts in
- let subst = make_subst env (ctx,ar.template_param_levels,args) in
+let instantiate_universes ctx ar args =
+ let subst = make_subst (ctx,ar.template_param_levels,args) in
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
@@ -198,12 +204,19 @@ let relevance_of_inductive env ind =
let _, mip = lookup_mind_specif env ind in
mip.mind_relevance
-let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps =
+let check_instance mib u =
+ if not (match mib.mind_universes with
+ | Monomorphic _ -> Instance.is_empty u
+ | Polymorphic uctx -> Instance.length u = AUContext.size uctx)
+ then CErrors.anomaly Pp.(str "bad instance length on mutind.")
+
+let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps =
+ check_instance mib u;
match mip.mind_arity with
| RegularArity a -> subst_instance_constr u a.mind_user_arity
| TemplateArity ar ->
let ctx = List.rev mip.mind_arity_ctxt in
- let ctx,s = instantiate_universes env ctx ar paramtyps in
+ let ctx,s = instantiate_universes ctx ar paramtyps in
(* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
the situation where a non-Prop singleton inductive becomes Prop
when applied to Prop params *)
@@ -211,21 +224,21 @@ let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps =
then raise (SingletonInductiveBecomesProp mip.mind_typename);
Term.mkArity (List.rev ctx,s)
-let type_of_inductive env pind =
- type_of_inductive_gen env pind [||]
+let type_of_inductive pind =
+ type_of_inductive_gen pind []
-let constrained_type_of_inductive env ((mib,_mip),u as pind) =
- let ty = type_of_inductive env pind in
+let constrained_type_of_inductive ((mib,_mip),u as pind) =
+ let ty = type_of_inductive pind in
let cst = instantiate_inductive_constraints mib u in
(ty, cst)
-let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args =
- let ty = type_of_inductive_gen env pind args in
+let constrained_type_of_inductive_knowing_parameters ((mib,_mip),u as pind) args =
+ let ty = type_of_inductive_gen pind args in
let cst = instantiate_inductive_constraints mib u in
(ty, cst)
-let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
- type_of_inductive_gen ~polyprop env mip args
+let type_of_inductive_knowing_parameters ?(polyprop=true) mip args =
+ type_of_inductive_gen ~polyprop mip args
(* The max of an array of universes *)
@@ -244,6 +257,7 @@ let max_inductive_sort =
(* Type of a constructor *)
let type_of_constructor (cstr, u) (mib,mip) =
+ check_instance mib u;
let ind = inductive_of_constructor cstr in
let specif = mip.mind_user_lc in
let i = index_of_constructor cstr in
@@ -581,7 +595,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
let push_ind specif env =
let r = specif.mind_relevance in
let anon = Context.make_annot Anonymous r in
- let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+ let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive ((mib,specif),u)) lpar) in
push_rel decl env
in
let env = Array.fold_right push_ind mib.mind_packets env in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 8c40c318c5..b690fe1157 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -41,16 +41,22 @@ val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_contex
val instantiate_inductive_constraints :
mutual_inductive_body -> Instance.t -> Constraint.t
-val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
+type param_univs = (unit -> Universe.t) list
+
+val make_param_univs : Environ.env -> constr array -> param_univs
+(** The constr array is the types of the arguments to a template
+ polymorphic inductive. *)
+
+val constrained_type_of_inductive : mind_specif puniverses -> types constrained
val constrained_type_of_inductive_knowing_parameters :
- env -> mind_specif puniverses -> types Lazy.t array -> types constrained
+ mind_specif puniverses -> param_univs -> types constrained
val relevance_of_inductive : env -> inductive -> Sorts.relevance
-val type_of_inductive : env -> mind_specif puniverses -> types
+val type_of_inductive : mind_specif puniverses -> types
val type_of_inductive_knowing_parameters :
- env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
+ ?polyprop:bool -> mind_specif puniverses -> param_univs -> types
val elim_sort : mind_specif -> Sorts.family
@@ -117,8 +123,8 @@ exception SingletonInductiveBecomesProp of Id.t
val max_inductive_sort : Sorts.t array -> Universe.t
-val instantiate_universes : env -> Constr.rel_context ->
- template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t
+val instantiate_universes : Constr.rel_context ->
+ template_arity -> param_univs -> Constr.rel_context * Sorts.t
(** {6 Debug} *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f6f2058c13..8db8a044a8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -321,6 +321,8 @@ let universes_of_private eff =
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
+let structure_body_of_safe_env env = env.revstruct
+
let sections_of_safe_env senv = senv.sections
let get_section = function
@@ -757,7 +759,7 @@ let translate_direct_opaque env kn ce =
let () = assert (is_empty_private u) in
{ cb with const_body = OpaqueDef c }
-let export_side_effects mb env (b_ctx, eff) =
+let export_side_effects mb env eff =
let not_exists e = not (Environ.mem_constant e.seff_constant env) in
let aux (acc,sl) e =
if not (not_exists e) then acc, sl
@@ -774,7 +776,7 @@ let export_side_effects mb env (b_ctx, eff) =
in
let rec translate_seff sl seff acc env =
match seff with
- | [] -> List.rev acc, b_ctx
+ | [] -> List.rev acc
| eff :: rest ->
if Int.equal sl 0 then
let env, cb =
@@ -803,8 +805,8 @@ let push_opaque_proof pf senv =
let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
senv, o
-let export_private_constants ce senv =
- let exported, ce = export_side_effects senv.revstruct senv.env ce in
+let export_private_constants eff senv =
+ let exported = export_side_effects senv.revstruct senv.env eff in
let map senv (kn, c) = match c.const_body with
| OpaqueDef p ->
let local = empty_private c.const_universes in
@@ -817,7 +819,7 @@ let export_private_constants ce senv =
let exported = List.map (fun (kn, _) -> kn) exported in
(* No delayed constants to declare *)
let senv = List.fold_left add_constant_aux senv bodies in
- (ce, exported), senv
+ exported, senv
let add_constant l decl senv =
let kn = Constant.make2 senv.modpath l in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 92bbd264fa..e472dfd5e5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -37,6 +37,8 @@ val env_of_safe_env : safe_environment -> Environ.env
val sections_of_safe_env : safe_environment -> section_data Section.t option
+val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
+
(** The safe_environment state monad *)
type safe_transformer0 = safe_environment -> safe_environment
@@ -84,8 +86,8 @@ type side_effect_declaration =
type exported_private_constant = Constant.t
val export_private_constants :
- private_constants Entries.proof_output ->
- (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
+ private_constants ->
+ exported_private_constant list safe_transformer
(** returns the main constant *)
val add_constant :
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 0a654adf7f..11c455de73 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -150,8 +150,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
(* nparams done *)
(* params_ctxt done because part of the inductive types *)
(* Don't check the sort of the type if polymorphic *)
- let ty1 = type_of_inductive env ((mib1, p1), inst) in
- let ty2 = type_of_inductive env ((mib2, p2), inst) in
+ let ty1 = type_of_inductive ((mib1, p1), inst) in
+ let ty2 = type_of_inductive ((mib2, p2), inst) in
let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in
cst
in
diff --git a/kernel/term.ml b/kernel/term.ml
index 87678b911e..a2586e74f7 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -363,24 +363,3 @@ let rec isArity c =
| Cast (c,_,_) -> isArity c
| Sort _ -> true
| _ -> false
-
-(** Kind of type *)
-
-(* Experimental, used in Presburger contrib *)
-type ('constr, 'types) kind_of_type =
- | SortType of Sorts.t
- | CastType of 'types * 'types
- | ProdType of Name.t Context.binder_annot * 'types * 'types
- | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types
- | AtomicType of 'constr * 'constr array
-
-let kind_of_type t = match kind t with
- | Sort s -> SortType s
- | Cast (c,_,t) -> CastType (c, t)
- | Prod (na,t,c) -> ProdType (na, t, c)
- | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
- | App (c,l) -> AtomicType (c, l)
- | (Rel _ | Meta _ | Var _ | Evar _ | Const _
- | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
- -> AtomicType (t,[||])
- | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
diff --git a/kernel/term.mli b/kernel/term.mli
index d2de4177ce..1fef54257a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -181,17 +181,6 @@ val destArity : types -> arity
(** Tell if a term has the form of an arity *)
val isArity : types -> bool
-(** {5 Kind of type} *)
-
-type ('constr, 'types) kind_of_type =
- | SortType of Sorts.t
- | CastType of 'types * 'types
- | ProdType of Name.t Context.binder_annot * 'types * 'types
- | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types
- | AtomicType of 'constr * 'constr array
-
-val kind_of_type : types -> (constr, types) kind_of_type
-
(* Deprecated *)
type sorts_family = Sorts.family = InSProp | InProp | InSet | InType
[@@ocaml.deprecated "Alias for Sorts.family"]
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f221ac7a4f..6c06c1e0f1 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -12,6 +12,7 @@ open Names
open Constr
open Environ
open Reduction
+open Univ
(* Type errors. *)
@@ -47,7 +48,7 @@ type ('constr, 'types) ptype_error =
| UnboundVar of variable
| NotAType of ('constr, 'types) punsafe_judgment
| BadAssumption of ('constr, 'types) punsafe_judgment
- | ReferenceVariables of Id.t * 'constr
+ | ReferenceVariables of Id.t * GlobRef.t
| ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
* (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -63,8 +64,8 @@ type ('constr, 'types) ptype_error =
| IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
- | UnsatisfiedConstraints of Univ.Constraint.t
- | UndeclaredUniverse of Univ.Level.t
+ | UnsatisfiedConstraints of Constraint.t
+ | UndeclaredUniverse of Level.t
| DisallowedSProp
| BadRelevance
@@ -83,7 +84,7 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
- | BadUnivs
+ | MissingConstraints of (Universe.Set.t * Universe.t)
exception InductiveError of inductive_error
@@ -181,7 +182,7 @@ let map_ptype_error f = function
| UnboundVar id -> UnboundVar id
| NotAType j -> NotAType (on_judgment f j)
| BadAssumption j -> BadAssumption (on_judgment f j)
-| ReferenceVariables (id, c) -> ReferenceVariables (id, f c)
+| ReferenceVariables (id, c) -> ReferenceVariables (id, c)
| ElimArity (pi, c, j, ar) -> ElimArity (pi, f c, on_judgment f j, ar)
| CaseNotInductive j -> CaseNotInductive (on_judgment f j)
| WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index ae6fd31762..d9842ecefa 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -11,6 +11,7 @@
open Names
open Constr
open Environ
+open Univ
(** Type errors. {% \label{typeerrors} %} *)
@@ -48,7 +49,7 @@ type ('constr, 'types) ptype_error =
| UnboundVar of variable
| NotAType of ('constr, 'types) punsafe_judgment
| BadAssumption of ('constr, 'types) punsafe_judgment
- | ReferenceVariables of Id.t * 'constr
+ | ReferenceVariables of Id.t * GlobRef.t
| ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
* (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -64,8 +65,8 @@ type ('constr, 'types) ptype_error =
| IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
- | UnsatisfiedConstraints of Univ.Constraint.t
- | UndeclaredUniverse of Univ.Level.t
+ | UnsatisfiedConstraints of Constraint.t
+ | UndeclaredUniverse of Level.t
| DisallowedSProp
| BadRelevance
@@ -86,7 +87,8 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
- | BadUnivs
+ | MissingConstraints of (Universe.Set.t * Universe.t)
+ (* each universe in the set should have been <= the other one *)
exception InductiveError of inductive_error
@@ -100,7 +102,7 @@ val error_not_type : env -> unsafe_judgment -> 'a
val error_assumption : env -> unsafe_judgment -> 'a
-val error_reference_variables : env -> Id.t -> constr -> 'a
+val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a
val error_elim_arity :
env -> pinductive -> constr -> unsafe_judgment ->
@@ -133,9 +135,9 @@ val error_ill_typed_rec_body :
val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
-val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
+val error_unsatisfied_constraints : env -> Constraint.t -> 'a
-val error_undeclared_universe : env -> Univ.Level.t -> 'a
+val error_undeclared_universe : env -> Level.t -> 'a
val error_disallowed_sprop : env -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c74bfd0688..80accc1ced 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -116,7 +116,7 @@ let type_of_variable env id =
(* Checks if a context of variables can be instantiated by the
variables of the current env.
Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env ?evars f c sign =
+let check_hyps_inclusion env ?evars c sign =
let conv env a b = conv env ?evars a b in
Context.Named.fold_outside
(fun d1 () ->
@@ -133,7 +133,7 @@ let check_hyps_inclusion env ?evars f c sign =
| LocalDef _, LocalAssum _ -> raise NotConvertible
| LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1);
with Not_found | NotConvertible | Option.Heterogeneous ->
- error_reference_variables env id (f c))
+ error_reference_variables env id c)
sign
~init:()
@@ -146,14 +146,14 @@ let check_hyps_inclusion env ?evars f c sign =
let type_of_constant env (kn,_u as cst) =
let cb = lookup_constant kn env in
- let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
+ let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in
let ty, cu = constant_type env cst in
let () = check_constraints cu env in
ty
let type_of_constant_in env (kn,_u as cst) =
let cb = lookup_constant kn env in
- let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
+ let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in
constant_type_in env cst
(* Type of a lambda-abstraction. *)
@@ -368,19 +368,19 @@ let check_cast env c ct k expected_type =
the App case of execute; from this constraints, the expected
dynamic constraints of the form u<=v are enforced *)
-let type_of_inductive_knowing_parameters env (ind,u as indu) args =
+let type_of_inductive_knowing_parameters env (ind,u) args =
let (mib,_mip) as spec = lookup_mind_specif env ind in
- check_hyps_inclusion env mkIndU indu mib.mind_hyps;
+ check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters
- env (spec,u) args
+ (spec,u) (Inductive.make_param_univs env args)
in
check_constraints cst env;
t
-let type_of_inductive env (ind,u as indu) =
+let type_of_inductive env (ind,u) =
let (mib,mip) = lookup_mind_specif env ind in
- check_hyps_inclusion env mkIndU indu mib.mind_hyps;
- let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in
+ check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
+ let t,cst = Inductive.constrained_type_of_inductive ((mib,mip),u) in
check_constraints cst env;
t
@@ -390,7 +390,7 @@ let type_of_constructor env (c,_u as cu) =
let () =
let ((kn,_),_) = c in
let mib = lookup_mind kn env in
- check_hyps_inclusion env mkConstructU cu mib.mind_hyps
+ check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps
in
let specif = lookup_mind_specif env (inductive_of_constructor c) in
let t,cst = constrained_type_of_constructor cu specif in
@@ -461,8 +461,7 @@ let type_of_global_in_context env r =
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
let univs = Declareops.inductive_polymorphic_context mib in
let inst = Univ.make_abstract_instance univs in
- let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
- Inductive.type_of_inductive env (specif, inst), univs
+ Inductive.type_of_inductive (specif, inst), univs
| ConstructRef cstr ->
let (mib,_ as specif) =
Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
@@ -515,8 +514,7 @@ let rec execute env cstr =
let f', ft =
match kind f with
| Ind ind when Environ.template_polymorphic_pind ind env ->
- let args = Array.map (fun t -> lazy t) argst in
- f, type_of_inductive_knowing_parameters env ind args
+ f, type_of_inductive_knowing_parameters env ind argst
| _ ->
(* No template polymorphism *)
execute env f
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index ae816fe26e..f88bc653de 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
(** Check that hyps are included in env and fails with error otherwise *)
val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
- ('a -> constr) -> 'a -> Constr.named_context -> unit
+ GlobRef.t -> Constr.named_context -> unit
val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 33336079bb..4d15ce741c 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -128,7 +128,7 @@ let enforce_leq_alg u v g =
| exception (UniverseInconsistency _ as e) -> Inr e)
in
(* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *)
- let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in
+ let c = List.map (fun u -> List.map (fun v -> (u,v)) (Universe.repr v)) (Universe.repr u) in
let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in
(* We pick a best constraint: smallest number of constraints, not an error if possible. *)
let order x y = match x, y with
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0712774576..94f7076c02 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -42,6 +42,8 @@ struct
let make dp i = (DirPath.hcons dp,i)
+ let repr x : t = x
+
let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
@@ -320,8 +322,9 @@ struct
if u == v then 0
else
let (x, n) = u and (x', n') = v in
- if Int.equal n n' then Level.compare x x'
- else n - n'
+ let c = Int.compare n n' in
+ if Int.equal 0 c then Level.compare x x'
+ else c
let sprop = hcons (Level.sprop, 0)
let prop = hcons (Level.prop, 0)
@@ -427,6 +430,10 @@ struct
let hcons = Hashcons.recursive_hcons Huniv.generate Huniv.hcons Expr.hcons
+ module Self = struct type nonrec t = t let compare = compare end
+ module Map = CMap.Make(Self)
+ module Set = CSet.Make(Self)
+
let make l = tip (Expr.make l)
let tip x = tip x
@@ -524,15 +531,10 @@ struct
Used to type the products. *)
let sup x y = merge_univs x y
- let empty = []
-
let exists = List.exists
let for_all = List.for_all
-
- let smart_map = List.Smart.map
-
- let map = List.map
+ let repr x : t = x
end
type universe = Universe.t
@@ -550,8 +552,6 @@ let pr_uni = Universe.pr
let sup = Universe.sup
let super = Universe.super
-open Universe
-
let universe_level = Universe.level
@@ -576,7 +576,7 @@ type univ_inconsistency = constraint_type * universe * universe * explanation La
exception UniverseInconsistency of univ_inconsistency
let error_inconsistency o u v p =
- raise (UniverseInconsistency (o,make u,make v,p))
+ raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
(* Constraints and sets of constraints. *)
@@ -677,7 +677,7 @@ let enforce_eq u v c =
let constraint_add_leq v u c =
(* We just discard trivial constraints like u<=u *)
- if Expr.equal v u then c
+ if Universe.Expr.equal v u then c
else
match v, u with
| (x,n), (y,m) ->
@@ -695,13 +695,13 @@ let constraint_add_leq v u c =
else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *)
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
+let check_univ_leq_one u v = Universe.exists (Universe.Expr.leq u) v
let check_univ_leq u v =
Universe.for_all (fun u -> check_univ_leq_one u v) u
let enforce_leq u v c =
- match is_sprop u, is_sprop v with
+ match Universe.is_sprop u, Universe.is_sprop v with
| true, true -> c
| true, false | false, true ->
raise (UniverseInconsistency (Le, u, v, None))
@@ -925,7 +925,7 @@ let subst_instance_instance s i =
let subst_instance_universe s u =
let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
- let u' = Universe.smart_map f u in
+ let u' = List.Smart.map f u in
if u == u' then u
else Universe.sort u'
@@ -1108,7 +1108,7 @@ let subst_univs_level_level subst l =
let subst_univs_level_universe subst u =
let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
- let u' = Universe.smart_map f u in
+ let u' = List.Smart.map f u in
if u == u' then u
else Universe.sort u'
@@ -1150,7 +1150,7 @@ let subst_univs_universe fn ul =
if CList.is_empty subst then ul
else
let substs =
- List.fold_left Universe.merge_univs Universe.empty subst
+ List.fold_left Universe.merge_univs [] subst
in
List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
substs nosubst
diff --git a/kernel/univ.mli b/kernel/univ.mli
index f7c984870f..94e57b9efc 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -16,6 +16,7 @@ sig
type t
val make : Names.DirPath.t -> int -> t
+ val repr : t -> Names.DirPath.t * int
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
@@ -138,8 +139,10 @@ sig
val exists : (Level.t * int -> bool) -> t -> bool
val for_all : (Level.t * int -> bool) -> t -> bool
+ val repr : t -> (Level.t * int) list
- val map : (Level.t * int -> 'a) -> t -> 'a list
+ module Set : CSet.S with type elt = t
+ module Map : CMap.ExtS with type key = t and module Set := Set
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:40:11 +0000