Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Enforce Prop < Set directly in the universe graph (fixes #50).

  • Loading branch information...
commit 1bd42a6dcc1cf959df7dfbb1e80530cb4c8dccb2 1 parent 21cacbb
@mattam82 mattam82 authored
Showing with 16 additions and 13 deletions.
  1. +12 −12 kernel/univ.ml
  2. +3 −0  kernel/univ.mli
  3. +1 −1  library/universes.ml
View
24 kernel/univ.ml
@@ -842,9 +842,6 @@ let is_type0_univ = Universe.is_type0
let is_univ_variable l = Universe.level l <> None
-let initial_universes = LMap.empty
-let is_initial_universes = LMap.is_empty
-
(* Every Level.t has a unique canonical arc representative *)
(* repr : universes -> Level.t -> canonical_arc *)
@@ -1240,6 +1237,10 @@ let enforce_univ_lt u v g =
| EQ -> anomaly (Pp.str "Univ.compare")
| (LE p|LT p) -> error_inconsistency Lt u v (List.rev p))
+let empty_universes = LMap.empty
+let initial_universes = enforce_univ_lt Level.prop Level.set LMap.empty
+let is_initial_universes = LMap.equal (==) initial_universes
+
(* Constraints and sets of constraints. *)
type univ_constraint = Level.t * constraint_type * Level.t
@@ -1741,15 +1742,14 @@ let check_consistent_constraints (ctx,cstrs) cstrs' =
let to_constraints g s =
let rec tr (x,d,y) acc =
- let add l d l' acc = Constraint.add (l,UniverseConstraints.tr_dir d,l') acc in
- match Universe.level x, d, Universe.level y with
- | _, ULe, Some l' -> enforce_leq x y acc
- | Some l, UEq, Some l' -> enforce_eq x y acc
- | _, ULub, _ -> acc
- | _, d, _ ->
- let f = if d = ULe then check_leq else check_eq in
- if f g x y then acc else
- raise (Invalid_argument
+ match Universe.level x, d, Universe.level y with
+ | _, ULe, Some l' -> enforce_leq x y acc
+ | Some l, UEq, Some l' -> enforce_eq x y acc
+ | _, ULub, _ -> acc
+ | _, d, _ ->
+ let f = if d = ULe then check_leq else check_eq in
+ if f g x y then acc else
+ raise (Invalid_argument
"to_constraints: non-trivial algebraic constraint between universes")
in UniverseConstraints.fold tr s Constraint.empty
View
3  kernel/univ.mli
@@ -168,6 +168,9 @@ val check_eq : check_function
val lax_check_eq : check_function (* same, without anomaly *)
(** The empty graph of universes *)
+val empty_universes : universes
+
+(** The initial graph of universes: Prop < Set *)
val initial_universes : universes
val is_initial_universes : universes -> bool
View
2  library/universes.ml
@@ -514,7 +514,7 @@ let normalize_context_set ctx us algs =
let csts =
(* We first put constraints in a normal-form: all self-loops are collapsed
to equalities. *)
- let g = Univ.merge_constraints csts Univ.initial_universes in
+ let g = Univ.merge_constraints csts Univ.empty_universes in
Univ.constraints_of_universes (Univ.normalize_universes g)
in
let noneqs =
Please sign in to comment.
Something went wrong with that request. Please try again.