diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 50 | ||||
| -rw-r--r-- | kernel/univ.mli | 31 |
5 files changed, 70 insertions, 17 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a4a02791b4..8efda16d64 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -218,7 +218,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in let uctx = CumulativityInfo.univ_context cumi in - let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in + let new_levels = Array.init (UContext.size uctx) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bbcf07f7e..30d96a22e0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -594,7 +594,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = | _ -> assert false let lambda_implicit_lift n a = - let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in + let level = Level.make2 (DirPath.make [Id.of_string "implicit"]) (Level.Id.make 0) in let implicit_sort = mkType (Universe.make level) in let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in iterate lambda_implicit n (lift n a) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index afdc8f1511..064fffe98e 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -921,7 +921,7 @@ let sort_universes g = let types = Array.init (max_lvl + 1) (function | 0 -> Level.prop | 1 -> Level.set - | n -> Level.make mp (n-2)) + | n -> Level.make2 mp (Level.Id.make (n-2))) in let g = Array.fold_left (fun g u -> let g, u = safe_repr g u in diff --git a/kernel/univ.ml b/kernel/univ.ml index 2b3b4f9486..57a5dce8a4 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -36,10 +36,35 @@ open Util module RawLevel = struct open Names + + module Id = struct + type t = int + + let make i = i + let to_string i = string_of_int i + + end + + module Qualid = struct + type t = DirPath.t * Id.t + + let make dp i = (dp,i) + let repr x = 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) + + let compare (d, i) (d', i') = + let c = Int.compare i i' in + if Int.equal c 0 then DirPath.compare d d' + else c + end + type t = | Prop | Set - | Level of int * DirPath.t + | Level of Qualid.t | Var of int (* Hash-consing *) @@ -49,7 +74,7 @@ struct match x, y with | Prop, Prop -> true | Set, Set -> true - | Level (n,d), Level (n',d') -> + | Level (d,n), Level (d',n') -> Int.equal n n' && DirPath.equal d d' | Var n, Var n' -> Int.equal n n' | _ -> false @@ -62,7 +87,7 @@ struct | Set, Set -> 0 | Set, _ -> -1 | _, Set -> 1 - | Level (i1, dp1), Level (i2, dp2) -> + | Level (dp1, i1), Level (dp2, i2) -> if i1 < i2 then -1 else if i1 > i2 then 1 else DirPath.compare dp1 dp2 @@ -83,9 +108,9 @@ struct let hcons = function | Prop as x -> x | Set as x -> x - | Level (n,d) as x -> + | Level (d,n) as x -> let d' = Names.DirPath.hcons d in - if d' == d then x else Level (n,d') + if d' == d then x else Level (d',n) | Var _n as x -> x open Hashset.Combine @@ -94,18 +119,20 @@ struct | Prop -> combinesmall 1 0 | Set -> combinesmall 1 1 | Var n -> combinesmall 2 n - | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d)) + | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d)) end module Level = struct - open Names + module Id = RawLevel.Id + + module Qualid = RawLevel.Qualid type raw_level = RawLevel.t = | Prop | Set - | Level of int * DirPath.t + | Level of Qualid.t | Var of int (** Embed levels with their hash value *) @@ -166,7 +193,7 @@ module Level = struct match data x with | Prop -> "Prop" | Set -> "Set" - | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n + | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n | Var n -> "Var(" ^ string_of_int n ^ ")" let pr u = str (to_string u) @@ -185,11 +212,12 @@ module Level = struct match data u with | Var n -> Some n | _ -> None - let make m n = make (Level (n, Names.DirPath.hcons m)) + let make2 m n = make (Level (Names.DirPath.hcons m, n)) + let make qid = make (Level qid) let name u = match data u with - | Level (n, d) -> Some (d, n) + | Level (d, n) -> Some (d, n) | _ -> None end diff --git a/kernel/univ.mli b/kernel/univ.mli index de7b334ae4..69aecac4f3 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -11,9 +11,32 @@ (** Universes. *) module Level : sig + + module Id : sig + type t + + val make : int -> t + val to_string : t -> string + + end + (** Non-qualified global universe level *) + + module Qualid : sig + type t + + val make : Names.DirPath.t -> Id.t -> t + val repr : t -> Names.DirPath.t * Id.t + val equal : t -> t -> bool + val hash : t -> int + val compare : t -> t -> int + + end + (** Qualified global universe level *) + type t (** Type of universe levels. A universe level is essentially a unique name - that will be associated to constraints later on. *) + that will be associated to constraints later on. A level can be local to a + definition or global. *) val set : t val prop : t @@ -34,7 +57,9 @@ sig val hash : t -> int - val make : Names.DirPath.t -> int -> t + val make : Qualid.t -> t + + val make2 : Names.DirPath.t -> Id.t -> t (** Create a new universe level from a unique identifier and an associated module path. *) @@ -48,7 +73,7 @@ sig val var_index : t -> int option - val name : t -> (Names.DirPath.t * int) option + val name : t -> Qualid.t option end (** Sets of universe levels *) |