aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/environ.ml15
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/indTyping.ml2
-rw-r--r--kernel/uGraph.ml32
-rw-r--r--kernel/uGraph.mli12
-rw-r--r--kernel/univ.ml42
-rw-r--r--kernel/vmbytecodes.ml6
7 files changed, 74 insertions, 37 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 03c9cb4be6..dec9e1deb8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -274,6 +274,11 @@ let is_impredicative_sort env = function
let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u)
+let is_impredicative_family env = function
+ | Sorts.InSProp | Sorts.InProp -> true
+ | Sorts.InSet -> is_impredicative_set env
+ | Sorts.InType -> false
+
let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
@@ -467,14 +472,22 @@ let same_flags {
[@warning "+9"]
let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
+let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
let set_typing_flags c env =
if same_flags env.env_typing_flags c then env
- else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c }
+ else
+ let env = { env with env_typing_flags = c } in
+ let env = set_cumulative_sprop c.cumulative_sprop env in
+ let env = set_type_in_type (not c.check_universes) env in
+ env
let set_cumulative_sprop b env =
set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
+let set_type_in_type b env =
+ set_typing_flags {env.env_typing_flags with check_universes=not b} env
+
let set_allow_sprop b env =
{ env with env_stratification =
{ env.env_stratification with env_sprop_allowed = b } }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 974e794c6b..f443ba38e1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -122,6 +122,7 @@ val indices_matter : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_univ : env -> Univ.Universe.t -> bool
+val is_impredicative_family : env -> Sorts.family -> bool
(** is the local context empty *)
val empty_context : env -> bool
@@ -320,6 +321,7 @@ val push_subgraph : Univ.ContextSet.t -> env -> env
val set_engagement : engagement -> env -> env
val set_typing_flags : typing_flags -> env -> env
val set_cumulative_sprop : bool -> env -> env
+val set_type_in_type : bool -> env -> env
val set_allow_sprop : bool -> env -> env
val sprop_allowed : env -> bool
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 179353d3f0..b2520b780f 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -77,7 +77,7 @@ let check_univ_leq ?(is_real_arg=false) env u info =
else info
in
(* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *)
- if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
+ if 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
&& Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 52e93a9e22..096e458ec4 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -29,7 +29,12 @@ module G = AcyclicGraph.Make(struct
code (eg add_universe with a constraint vs G.add with no
constraint) *)
-type t = { graph: G.t; sprop_cumulative : bool }
+type t = {
+ graph: G.t;
+ sprop_cumulative : bool;
+ type_in_type : bool;
+}
+
type 'a check_function = t -> 'a -> 'a -> bool
let g_map f g =
@@ -39,6 +44,10 @@ let g_map f g =
let set_cumulative_sprop b g = {g with sprop_cumulative=b}
+let set_type_in_type b g = {g with type_in_type=b}
+
+let type_in_type g = g.type_in_type
+
let check_smaller_expr g (u,n) (v,m) =
let diff = n - m in
match diff with
@@ -55,28 +64,33 @@ let real_check_leq g u v =
Universe.for_all (fun ul -> exists_bigger g ul v) u
let check_leq g u v =
+ type_in_type g ||
Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) ||
(not (Universe.is_sprop u) && not (Universe.is_sprop v) &&
(is_type0m_univ u ||
real_check_leq g u v))
let check_eq g u v =
+ type_in_type g ||
Universe.equal u v ||
(not (Universe.is_sprop u || Universe.is_sprop v) &&
(real_check_leq g u v && real_check_leq g v u))
let check_eq_level g u v =
u == v ||
+ type_in_type g ||
(not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v)
-let empty_universes = {graph=G.empty; sprop_cumulative=false}
+let empty_universes = {graph=G.empty; sprop_cumulative=false; type_in_type=false}
let initial_universes =
let big_rank = 1000000 in
let g = G.empty in
let g = G.add ~rank:big_rank Level.prop g in
let g = G.add ~rank:big_rank Level.set g in
- {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false}
+ {empty_universes with graph=G.enforce_lt Level.prop Level.set g}
+
+let initial_universes_with g = {g with graph=initial_universes.graph}
let enforce_constraint (u,d,v) g =
match d with
@@ -91,6 +105,10 @@ let enforce_constraint (u,d,v as cst) g =
| true, Le, false when g.sprop_cumulative -> g
| _ -> raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None))
+let enforce_constraint cst g =
+ if not (type_in_type g) then enforce_constraint cst g
+ else try enforce_constraint cst g with UniverseInconsistency _ -> g
+
let merge_constraints csts g = Constraint.fold enforce_constraint csts g
let check_constraint g (u,d,v) =
@@ -103,8 +121,8 @@ let check_constraint g (u,d,v as cst) =
match Level.is_sprop u, d, Level.is_sprop v with
| false, _, false -> check_constraint g.graph cst
| true, (Eq|Le), true -> true
- | true, Le, false -> g.sprop_cumulative
- | _ -> false
+ | true, Le, false -> g.sprop_cumulative || type_in_type g
+ | _ -> type_in_type g
let check_constraints csts g = Constraint.for_all (check_constraint g) csts
@@ -145,8 +163,10 @@ let enforce_leq_alg u v g =
let enforce_leq_alg u v g =
match Universe.is_sprop u, Universe.is_sprop v with
| true, true -> Constraint.empty, g
- | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None))
| false, false -> enforce_leq_alg u v g
+ | left, _ ->
+ if left && g.sprop_cumulative then Constraint.empty, g
+ else raise (UniverseInconsistency (Le, u, v, None))
(* sanity check wrapper *)
let enforce_leq_alg u v g =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index c9fbd7f694..87b3634e28 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -16,6 +16,15 @@ type t
val set_cumulative_sprop : bool -> t -> t
(** Makes the system incomplete. *)
+val set_type_in_type : bool -> t -> t
+
+(** When [type_in_type], functions adding constraints do not fail and
+ may instead ignore inconsistent constraints.
+
+ Checking functions such as [check_leq] always return [true].
+*)
+val type_in_type : t -> bool
+
type 'a check_function = t -> 'a -> 'a -> bool
val check_leq : Universe.t check_function
@@ -25,6 +34,9 @@ val check_eq_level : Level.t check_function
(** The initial graph of universes: Prop < Set *)
val initial_universes : t
+(** Initial universes, but keeping options such as type in type from the argument. *)
+val initial_universes_with : t -> t
+
(** Check equality of instances w.r.t. a universe graph *)
val check_eq_instances : Instance.t check_function
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6d8aa02dff..a2fd14025e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -205,12 +205,6 @@ module Level = struct
let pr u = str (to_string u)
- let apart u v =
- match data u, data v with
- | SProp, _ | _, SProp
- | Prop, Set | Set, Prop -> true
- | _ -> false
-
let vars = Array.init 20 (fun i -> make (Var i))
let var n =
@@ -250,7 +244,7 @@ module LMap = struct
ext empty
let pr f m =
- h 0 (prlist_with_sep fnl (fun (u, v) ->
+ h (prlist_with_sep fnl (fun (u, v) ->
Level.pr u ++ f v) (bindings m))
end
@@ -568,16 +562,6 @@ let constraint_type_ord c1 c2 = match c1, c2 with
| Eq, Eq -> 0
| Eq, _ -> 1
-(* Universe inconsistency: error raised when trying to enforce a relation
- that would create a cycle in the graph of universes. *)
-
-type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
-
-exception UniverseInconsistency of univ_inconsistency
-
-let error_inconsistency o u v p =
- raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
-
(* Constraints and sets of constraints. *)
type univ_constraint = Level.t * constraint_type * Level.t
@@ -660,8 +644,6 @@ type 'a constraint_function = 'a -> 'a -> constraints -> constraints
let enforce_eq_level u v c =
(* We discard trivial constraints like u=u *)
if Level.equal u v then c
- else if Level.apart u v then
- error_inconsistency Eq u v None
else Constraint.add (u,Eq,v) c
let enforce_eq u v c =
@@ -684,9 +666,9 @@ let constraint_add_leq v u c =
let j = m - n in
if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
Constraint.add (x,Lt,y) c
- else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
- if Level.equal x y then (* u+(k+1) <= u *)
- raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None))
+ else if j <= -1 (* n = m+k, v+k <= u and k>0 *) then
+ if Level.equal x y then (* u+k <= u with k>0 *)
+ Constraint.add (x,Lt,x) c
else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
else if j = 0 then
Constraint.add (x,Le,y) c
@@ -703,8 +685,8 @@ let check_univ_leq u v =
let enforce_leq u v c =
match Universe.is_sprop u, Universe.is_sprop v with
| true, true -> c
- | true, false | false, true ->
- raise (UniverseInconsistency (Le, u, v, None))
+ | true, false -> Constraint.add (Level.sprop,Le,Level.prop) c
+ | false, true -> Constraint.add (Level.prop,Le,Level.sprop) c
| false, false ->
List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
@@ -961,7 +943,7 @@ struct
let pr prl ?variance (univs, cst as ctx) =
if is_empty ctx then mt() else
- h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+ h (Instance.pr prl ?variance univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst))
let hcons (univs, cst) =
(Instance.hcons univs, hcons_constraints cst)
@@ -1076,7 +1058,7 @@ struct
let pr prl (univs, cst as ctx) =
if is_empty ctx then mt() else
- h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+ h (LSet.pr prl univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst))
let constraints (_univs, cst) = cst
let levels (univs, _cst) = univs
@@ -1232,6 +1214,14 @@ let hcons_universe_context_set (v, c) =
let hcons_univ x = Universe.hcons x
+(* Universe inconsistency: error raised when trying to enforce a relation
+ that would create a cycle in the graph of universes. *)
+
+type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
+
+(* Do not use in this file as we may be type-in-type *)
+exception UniverseInconsistency of univ_inconsistency
+
let explain_universe_inconsistency prl (o,u,v,p : univ_inconsistency) =
let pr_uni = Universe.pr_with prl in
let pr_rel = function
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index 74405a0105..c156a21c86 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -106,14 +106,14 @@ let rec pp_instr i =
| Kclosure(lbl, n) ->
str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
| Kclosurerec(fv,init,lblt,lblb) ->
- h 1 (str "closurerec " ++
+ hv 1 (str "closurerec " ++
int fv ++ str ", " ++ int init ++
str " types = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
str " bodies = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblb))
| Kclosurecofix (fv,init,lblt,lblb) ->
- h 1 (str "closurecofix " ++
+ hv 1 (str "closurecofix " ++
int fv ++ str ", " ++ int init ++
str " types = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
@@ -129,7 +129,7 @@ let rec pp_instr i =
str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
pp_lbl lbls ++ str ", " ++ int sz
| Kswitch(lblc,lblb) ->
- h 1 (str "switch " ++
+ hv 1 (str "switch " ++
prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
str " | " ++
prlist_with_sep spc pp_lbl (Array.to_list lblb))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 07:40:51 +0000