diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.ml | 6 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 27 | ||||
| -rw-r--r-- | kernel/univ.mli | 22 |
5 files changed, 18 insertions, 43 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8efda16d64..68d44f8782 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -218,7 +218,9 @@ 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) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in + let new_levels = Array.init (UContext.size uctx) + (fun i -> Level.make (Level.UGlobal.make DirPath.empty 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 30d96a22e0..05c5c0e821 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -593,10 +593,10 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = ienv_decompose_prod ienv' (n-1) b | _ -> assert false +let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0)) +let dummy_implicit_sort = mkType (Universe.make dummy_univ) let lambda_implicit_lift n a = - 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 + let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in iterate lambda_implicit n (lift n a) (* This removes global parameters of the inductive types in lc (for diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 064fffe98e..5fc8d0297f 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.make2 mp (Level.Id.make (n-2))) + | n -> Level.make (Level.UGlobal.make mp (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 57a5dce8a4..7b5ed05bda 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -37,19 +37,10 @@ module RawLevel = struct open Names - module Id = struct - type t = int + module UGlobal = struct + type t = DirPath.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 make dp i = (DirPath.hcons dp,i) let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' @@ -64,7 +55,7 @@ struct type t = | Prop | Set - | Level of Qualid.t + | Level of UGlobal.t | Var of int (* Hash-consing *) @@ -74,8 +65,7 @@ struct match x, y with | Prop, Prop -> true | Set, Set -> true - | Level (d,n), Level (d',n') -> - Int.equal n n' && DirPath.equal d d' + | Level l, Level l' -> UGlobal.equal l l' | Var n, Var n' -> Int.equal n n' | _ -> false @@ -125,14 +115,12 @@ end module Level = struct - module Id = RawLevel.Id - - module Qualid = RawLevel.Qualid + module UGlobal = RawLevel.UGlobal type raw_level = RawLevel.t = | Prop | Set - | Level of Qualid.t + | Level of UGlobal.t | Var of int (** Embed levels with their hash value *) @@ -212,7 +200,6 @@ module Level = struct match data u with | Var n -> Some n | _ -> None - let make2 m n = make (Level (Names.DirPath.hcons m, n)) let make qid = make (Level qid) let name u = diff --git a/kernel/univ.mli b/kernel/univ.mli index 69aecac4f3..512f38cedd 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -12,20 +12,10 @@ module Level : sig - module Id : sig + module UGlobal : 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 make : Names.DirPath.t -> int -> t val equal : t -> t -> bool val hash : t -> int val compare : t -> t -> int @@ -57,11 +47,7 @@ sig val hash : t -> int - 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. *) + val make : UGlobal.t -> t val pr : t -> Pp.t (** Pretty-printing *) @@ -73,7 +59,7 @@ sig val var_index : t -> int option - val name : t -> Qualid.t option + val name : t -> UGlobal.t option end (** Sets of universe levels *) |