aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml29
-rw-r--r--kernel/declarations.mli2
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/indtypes.ml15
-rw-r--r--kernel/inductive.ml42
-rw-r--r--kernel/typeops.ml2
6 files changed, 61 insertions, 33 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index f72eb2acbe..c6eacc289c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -556,7 +556,7 @@ let eq_constr_univs univs m n =
if m == n then true
else
let eq_universes _ = Univ.Instance.check_eq univs in
- let eq_sorts s1 s2 = Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
+ let eq_sorts s1 s2 = s1 == s2 || Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
let rec eq_constr' m n =
m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
in compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -565,8 +565,10 @@ let leq_constr_univs univs m n =
if m == n then true
else
let eq_universes _ = Univ.Instance.check_eq univs in
- let eq_sorts s1 s2 = Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
- let leq_sorts s1 s2 = Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
+ let eq_sorts s1 s2 = s1 == s2 ||
+ Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
+ let leq_sorts s1 s2 = s1 == s2 ||
+ Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
let rec eq_constr' m n =
m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
in
@@ -582,9 +584,11 @@ let eq_constr_universes m n =
let eq_universes strict l l' =
cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in
let eq_sorts s1 s2 =
- cstrs := Univ.UniverseConstraints.add
- (Sorts.univ_of_sort s1, Univ.UEq, Sorts.univ_of_sort s2) !cstrs;
- true
+ if Sorts.equal s1 s2 then true
+ else
+ (cstrs := Univ.UniverseConstraints.add
+ (Sorts.univ_of_sort s1, Univ.UEq, Sorts.univ_of_sort s2) !cstrs;
+ true)
in
let rec eq_constr' m n =
m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -599,12 +603,17 @@ let leq_constr_universes m n =
let eq_universes strict l l' =
cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in
let eq_sorts s1 s2 =
- cstrs := Univ.UniverseConstraints.add
- (Sorts.univ_of_sort s1,Univ.UEq,Sorts.univ_of_sort s2) !cstrs; true
+ if Sorts.equal s1 s2 then true
+ else (cstrs := Univ.UniverseConstraints.add
+ (Sorts.univ_of_sort s1,Univ.UEq,Sorts.univ_of_sort s2) !cstrs;
+ true)
in
let leq_sorts s1 s2 =
- cstrs := Univ.UniverseConstraints.add
- (Sorts.univ_of_sort s1,Univ.ULe,Sorts.univ_of_sort s2) !cstrs; true
+ if Sorts.equal s1 s2 then true
+ else
+ (cstrs := Univ.UniverseConstraints.add
+ (Sorts.univ_of_sort s1,Univ.ULe,Sorts.univ_of_sort s2) !cstrs;
+ true)
in
let rec eq_constr' m n =
m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index b8dfe63d3a..85dac4bfcc 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -27,7 +27,7 @@ type engagement = ImpredicativeSet
*)
type template_arity = {
- template_param_levels : Univ.universe option list;
+ template_param_levels : Univ.universe_level option list;
template_level : Univ.universe;
}
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 55868097fe..dd906bab24 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -31,8 +31,8 @@ let map_decl_arity f g = function
| TemplateArity a -> TemplateArity (g a)
let hcons_template_arity ar =
- { template_param_levels =
- List.smartmap (Option.smartmap Univ.hcons_univ) ar.template_param_levels;
+ { template_param_levels = ar.template_param_levels;
+ (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *)
template_level = Univ.hcons_univ ar.template_level }
(** {6 Constants } *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0f9c7421f3..85d04e5e24 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -195,11 +195,11 @@ let is_impredicative env u =
let param_ccls params =
let has_some_univ u = function
- | Some v when Universe.equal u v -> true
+ | Some v when Univ.Level.equal u v -> true
| _ -> false
in
let remove_some_univ u = function
- | Some v when Universe.equal u v -> None
+ | Some v when Univ.Level.equal u v -> None
| x -> x
in
let fold l (_, b, p) = match b with
@@ -210,10 +210,13 @@ let param_ccls params =
(* polymorphism unless there is aliasing (i.e. non distinct levels) *)
begin match kind_of_term c with
| Sort (Type u) ->
- if List.exists (has_some_univ u) l then
- None :: List.map (remove_some_univ u) l
- else
- Some u :: l
+ (match Univ.Universe.level u with
+ | Some u ->
+ if List.exists (has_some_univ u) l then
+ None :: List.map (remove_some_univ u) l
+ else
+ Some u :: l
+ | None -> None :: l)
| _ ->
None :: l
end
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 7cf5dd62dc..3f1c4e75fd 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -155,10 +155,7 @@ let sort_as_univ = function
(* Template polymorphism *)
let cons_subst u su subst =
- try
- (u, sup su (List.assoc_f Universe.equal u subst)) ::
- List.remove_assoc_f Universe.equal u subst
- with Not_found -> (u, su) :: subst
+ Univ.LMap.add u su subst
let actualize_decl_level env lev t =
let sign,s = dest_arity env t in
@@ -192,7 +189,7 @@ let rec make_subst env = function
d::ctx, subst
| sign, [], _ ->
(* Uniform parameters are exhausted *)
- sign,[]
+ sign, Univ.LMap.empty
| [], _, _ ->
assert false
@@ -201,7 +198,7 @@ exception SingletonInductiveBecomesProp of Id.t
let instantiate_universes env ctx ar argsorts =
let args = Array.to_list argsorts in
let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
- let level = subst_large_constraints subst ar.template_level 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 *)
if is_type0m_univ level then prop_sort
@@ -214,11 +211,13 @@ let instantiate_universes env ctx ar argsorts =
(* Type of an inductive type *)
-let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps =
match mip.mind_arity with
| RegularArity a ->
- let subst = make_inductive_subst mib u in
- (subst_univs_constr subst a.mind_user_arity, subst)
+ if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty)
+ else
+ let subst = make_inductive_subst mib u in
+ (subst_univs_constr subst a.mind_user_arity, subst)
| TemplateArity ar ->
let ctx = List.rev mip.mind_arity_ctxt in
let ctx,s = instantiate_universes env ctx ar paramtyps in
@@ -229,21 +228,38 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
then raise (SingletonInductiveBecomesProp mip.mind_typename);
mkArity (List.rev ctx,s), Univ.LMap.empty
+let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+ match mip.mind_arity with
+ | RegularArity a ->
+ if not mib.mind_polymorphic then a.mind_user_arity
+ else
+ let subst = make_inductive_subst mib u in
+ (subst_univs_constr subst 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
+ (* 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 *)
+ if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+ then raise (SingletonInductiveBecomesProp mip.mind_typename);
+ mkArity (List.rev ctx,s)
+
let type_of_inductive env pind =
- fst (type_of_inductive_gen env pind [||])
+ type_of_inductive_gen env pind [||]
let constrained_type_of_inductive env ((mib,mip),u as pind) =
- let ty, subst = type_of_inductive_gen env pind [||] in
+ let ty, subst = type_of_inductive_subst env pind [||] in
let cst = instantiate_inductive_constraints mib subst in
(ty, cst)
let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
- let ty, subst = type_of_inductive_gen env pind args in
+ let ty, subst = type_of_inductive_subst env pind args in
let cst = instantiate_inductive_constraints mib subst in
(ty, cst)
let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args =
- fst (type_of_inductive_gen env mip args)
+ type_of_inductive_gen env mip args
(* The max of an array of universes *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c6355b3eab..49f883628d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -115,7 +115,7 @@ let check_hyps_inclusion env c sign =
let extract_level env p =
let _,c = dest_prod_assum env p in
- match kind_of_term c with Sort (Type u) -> Some u | _ -> None
+ match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
let extract_context_levels env l =
let fold l (_, b, p) = match b with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:26:49 +0000