From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- kernel/univ.ml | 596 ++++++++++++++++++++++++++------------------------------- 1 file changed, 273 insertions(+), 323 deletions(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index 09f884ec..3158db52 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* int - val eq : t -> t -> bool - val hcons : t -> t -end - -module HashedList (M : Hashconsed) : -sig - type t = private Nil | Cons of M.t * int * t - val nil : t - val cons : M.t -> t -> t -end = -struct - type t = Nil | Cons of M.t * int * t - module Self = - struct - type _t = t - type t = _t - type u = (M.t -> M.t) - let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 - | _ -> false - let hashcons hc = function - | Nil -> Nil - | Cons (x, h, l) -> Cons (hc x, h, l) - end - module Hcons = Hashcons.Make(Self) - let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons - (** No recursive call: the interface guarantees that all HLists from this - program are already hashconsed. If we get some external HList, we can - still reconstruct it by traversing it entirely. *) - let nil = Nil - let cons x l = - let h = M.hash x in - let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in - let h = Hashset.Combine.combine h hl in - hcons (Cons (x, h, l)) -end - -module HList = struct - - module type S = sig - type elt - type t = private Nil | Cons of elt * int * t - val hash : t -> int - val nil : t - val cons : elt -> t -> t - val tip : elt -> t - val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a - val map : (elt -> elt) -> t -> t - val smartmap : (elt -> elt) -> t -> t - val exists : (elt -> bool) -> t -> bool - val for_all : (elt -> bool) -> t -> bool - val for_all2 : (elt -> elt -> bool) -> t -> t -> bool - val mem : elt -> t -> bool - val remove : elt -> t -> t - val to_list : t -> elt list - val compare : (elt -> elt -> int) -> t -> t -> int - end - - module Make (H : Hashconsed) : S with type elt = H.t = - struct - type elt = H.t - include HashedList(H) - - let hash = function Nil -> 0 | Cons (_, h, _) -> h - - let tip e = cons e nil - - let rec fold f l accu = match l with - | Nil -> accu - | Cons (x, _, l) -> fold f l (f x accu) - - let rec map f = function - | Nil -> nil - | Cons (x, _, l) -> cons (f x) (map f l) - - let smartmap = map - (** Apriori hashconsing ensures that the map is equal to its argument *) - - let rec exists f = function - | Nil -> false - | Cons (x, _, l) -> f x || exists f l - - let rec for_all f = function - | Nil -> true - | Cons (x, _, l) -> f x && for_all f l - - let rec for_all2 f l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2 - | _ -> false - - let rec to_list = function - | Nil -> [] - | Cons (x, _, l) -> x :: to_list l - - let rec remove x = function - | Nil -> nil - | Cons (y, _, l) -> - if H.eq x y then l - else cons y (remove x l) - - let rec mem x = function - | Nil -> false - | Cons (y, _, l) -> H.eq x y || mem x l - - let rec compare cmp l1 l2 = match l1, l2 with - | Nil, Nil -> 0 - | Cons (x1, h1, l1), Cons (x2, h2, l2) -> - let c = Int.compare h1 h2 in - if c == 0 then - let c = cmp x1 x2 in - if c == 0 then - compare cmp l1 l2 - else c - else c - | Cons _, Nil -> 1 - | Nil, Cons _ -> -1 - - end -end - module RawLevel = struct open Names @@ -248,8 +123,7 @@ module Level = struct (** Hashcons on levels + their hash *) module Self = struct - type _t = t - type t = _t + type nonrec t = t type u = unit let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash @@ -320,6 +194,10 @@ module Level = struct let make m n = make (Level (n, Names.DirPath.hcons m)) + let name u = + match data u with + | Level (n, d) -> Some (d, n) + | _ -> None end (** Level maps *) @@ -390,12 +268,11 @@ struct module Expr = struct type t = Level.t * int - type _t = t - + (* Hashing of expressions *) module ExprHash = struct - type t = _t + type t = Level.t * int type u = Level.t -> Level.t let hashcons hdir (b,n as x) = let b' = hdir b in @@ -409,25 +286,12 @@ struct end - module HExpr = - struct - - module H = Hashcons.Make(ExprHash) - - type t = ExprHash.t - - let hcons = - Hashcons.simple_hcons H.generate H.hcons Level.hcons - let hash = ExprHash.hash - let eq x y = x == y || - (let (u,n) = x and (v,n') = y in - Int.equal n n' && Level.equal u v) - - end + module H = Hashcons.Make(ExprHash) - let hcons = HExpr.hcons + let hcons = + Hashcons.simple_hcons H.generate H.hcons Level.hcons - let make l = hcons (l, 0) + let make l = (l, 0) let compare u v = if u == v then 0 @@ -436,14 +300,10 @@ struct if Int.equal n n' then Level.compare x x' else n - n' - let prop = make Level.prop - let set = make Level.set + let prop = hcons (Level.prop, 0) + let set = hcons (Level.set, 0) let type1 = hcons (Level.set, 1) - let is_prop = function - | (l,0) -> Level.is_prop l - | _ -> false - let is_small = function | (l,0) -> Level.is_small l | _ -> false @@ -452,6 +312,8 @@ struct (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) + let hash = ExprHash.hash + let leq (u,n) (v,n') = let cmp = Level.compare u v in if Int.equal cmp 0 then n <= n' @@ -461,13 +323,13 @@ struct let successor (u,n) = if Level.is_prop u then type1 - else hcons (u, n + 1) + else (u, n + 1) let addn k (u,n as x) = if k = 0 then x else if Level.is_prop u then - hcons (Level.set,n+k) - else hcons (u,n+k) + (Level.set,n+k) + else (u,n+k) type super_result = SuperSame of bool @@ -481,19 +343,16 @@ struct returning [SuperSame] if they refer to the same level at potentially different increments or [SuperDiff] if they are different. The booleans indicate if the left expression is "smaller" than the right one in both cases. *) - let super (u,n as x) (v,n' as y) = + let super (u,n) (v,n') = let cmp = Level.compare u v in if Int.equal cmp 0 then SuperSame (n < n') else - match x, y with - | (l,0), (l',0) -> - let open RawLevel in - (match Level.data l, Level.data l' with - | Prop, Prop -> SuperSame false - | Prop, _ -> SuperSame true - | _, Prop -> SuperSame false - | _, _ -> SuperDiff cmp) - | _, _ -> SuperDiff cmp + let open RawLevel in + match Level.data u, n, Level.data v, n' with + | Prop, _, Prop, _ -> SuperSame (n < n') + | Prop, 0, _, _ -> SuperSame true + | _, _, Prop, 0 -> SuperSame false + | _, _, _, _ -> SuperDiff cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v @@ -519,71 +378,63 @@ struct let v' = f v in if v' == v then x else if Level.is_prop v' && n != 0 then - hcons (Level.set, n) - else hcons (v', n) + (Level.set, n) + else (v', n) end - - let compare_expr = Expr.compare - module Huniv = HList.Make(Expr.HExpr) - type t = Huniv.t - open Huniv - - let equal x y = x == y || - (Huniv.hash x == Huniv.hash y && - Huniv.for_all2 Expr.equal x y) + type t = Expr.t list - let hash = Huniv.hash + let tip l = [l] + let cons x l = x :: l - let compare x y = - if x == y then 0 - else - let hx = Huniv.hash x and hy = Huniv.hash y in - let c = Int.compare hx hy in - if c == 0 then - Huniv.compare (fun e1 e2 -> compare_expr e1 e2) x y - else c + let rec hash = function + | [] -> 0 + | e :: l -> Hashset.Combine.combinesmall (Expr.ExprHash.hash e) (hash l) - let rec hcons = function - | Nil -> Huniv.nil - | Cons (x, _, l) -> Huniv.cons x (hcons l) + let equal x y = x == y || List.equal Expr.equal x y - let make l = Huniv.tip (Expr.make l) - let tip x = Huniv.tip x + let compare x y = if x == y then 0 else List.compare Expr.compare x y + + module Huniv = Hashcons.Hlist(Expr) + + let hcons = Hashcons.recursive_hcons Huniv.generate Huniv.hcons Expr.hcons + + let make l = tip (Expr.make l) + let tip x = tip x let pr l = match l with - | Cons (u, _, Nil) -> Expr.pr u + | [u] -> Expr.pr u | _ -> str "max(" ++ hov 0 - (prlist_with_sep pr_comma Expr.pr (to_list l)) ++ + (prlist_with_sep pr_comma Expr.pr l) ++ str ")" let pr_with f l = match l with - | Cons (u, _, Nil) -> Expr.pr_with f u + | [u] -> Expr.pr_with f u | _ -> str "max(" ++ hov 0 - (prlist_with_sep pr_comma (Expr.pr_with f) (to_list l)) ++ + (prlist_with_sep pr_comma (Expr.pr_with f) l) ++ str ")" let is_level l = match l with - | Cons (l, _, Nil) -> Expr.is_level l + | [l] -> Expr.is_level l | _ -> false let rec is_levels l = match l with - | Cons (l, _, r) -> Expr.is_level l && is_levels r - | Nil -> true + | l :: r -> Expr.is_level l && is_levels r + | [] -> true let level l = match l with - | Cons (l, _, Nil) -> Expr.level l + | [l] -> Expr.level l | _ -> None let levels l = - fold (fun x acc -> LSet.add (Expr.get_level x) acc) l LSet.empty + List.fold_left (fun acc x -> LSet.add (Expr.get_level x) acc) LSet.empty l let is_small u = match u with - | Cons (l, _, Nil) -> Expr.is_small l + | [l] -> Expr.is_small l | _ -> false (* The lower predicative level of the hierarchy that contains (impredicative) @@ -605,16 +456,16 @@ struct let super l = if is_small l then type1 else - Huniv.map (fun x -> Expr.successor x) l + List.smartmap (fun x -> Expr.successor x) l let addn n l = - Huniv.map (fun x -> Expr.addn n x) l + List.smartmap (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with - | Nil, _ -> l2 - | _, Nil -> l1 - | Cons (h1, _, t1), Cons (h2, _, t2) -> + | [], _ -> l2 + | _, [] -> l1 + | h1 :: t1, h2 :: t2 -> let open Expr in (match super h1 h2 with | SuperSame true (* h1 < h2 *) -> merge_univs t1 l2 @@ -627,7 +478,7 @@ struct let sort u = let rec aux a l = match l with - | Cons (b, _, l') -> + | b :: l' -> let open Expr in (match super a b with | SuperSame false -> aux a l' @@ -635,22 +486,23 @@ struct | SuperDiff c -> if c <= 0 then cons a l else cons b (aux a l')) - | Nil -> cons a l + | [] -> cons a l in - fold (fun a acc -> aux a acc) u nil - + List.fold_right (fun a acc -> aux a acc) u [] + (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y - let empty = nil + let empty = [] - let exists = Huniv.exists + let exists = List.exists - let for_all = Huniv.for_all + let for_all = List.for_all - let smartmap = Huniv.smartmap + let smartmap = List.smartmap + let map = List.map end type universe = Universe.t @@ -729,8 +581,11 @@ struct pp_std ++ prl u1 ++ pr_constraint_type op ++ prl u2 ++ fnl () ) c (str "") + let universes_of c = + fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty end +let universes_of_constraints = Constraint.universes_of let empty_constraint = Constraint.empty let union_constraint = Constraint.union let eq_constraint = Constraint.equal @@ -785,7 +640,7 @@ let enforce_eq_level u v c = let enforce_eq u v c = match Universe.level u, Universe.level v with | Some u, Some v -> enforce_eq_level u v c - | _ -> anomaly (Pp.str "A universe comparison can only happen between variables") + | _ -> anomaly (Pp.str "A universe comparison can only happen between variables.") let check_univ_eq u v = Universe.equal u v @@ -805,13 +660,13 @@ let constraint_add_leq v u 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 anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints") + else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.") else if j = 0 then Constraint.add (x,Le,y) c else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints") + else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *) let check_univ_leq_one u v = Universe.exists (Expr.leq u) v @@ -819,13 +674,7 @@ let check_univ_leq u v = Universe.for_all (fun u -> check_univ_leq_one u v) u let enforce_leq u v c = - let open Universe.Huniv in - let rec aux acc v = - match v with - | Cons (v, _, l) -> - aux (fold (fun u -> constraint_add_leq u v) u c) l - | Nil -> acc - in aux c v + List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v let enforce_leq u v c = if check_univ_leq u v then c @@ -834,21 +683,16 @@ let enforce_leq u v c = let enforce_leq_level u v c = if Level.equal u v then c else Constraint.add (u,Le,v) c -let enforce_univ_constraint (u,d,v) = - match d with - | Eq -> enforce_eq u v - | Le -> enforce_leq u v - | Lt -> enforce_leq (super u) v - (* Miscellaneous functions to remove or test local univ assumed to occur in a universe *) -let univ_level_mem u v = Huniv.mem (Expr.make u) v +let univ_level_mem u v = + List.exists (fun (l, n) -> Int.equal n 0 && Level.equal u l) v let univ_level_rem u v min = match Universe.level v with | Some u' -> if Level.equal u u' then min else v - | None -> Huniv.remove (Universe.Expr.make u) v + | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v (* Is u mentionned in v (or equals to v) ? *) @@ -865,15 +709,55 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - -module Instance : sig +module Variance = +struct + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + + let sup x y = + match x, y with + | Irrelevant, s | s, Irrelevant -> s + | Invariant, _ | _, Invariant -> Invariant + | Covariant, Covariant -> Covariant + + let check_subtype x y = match x, y with + | (Irrelevant | Covariant | Invariant), Irrelevant -> true + | Irrelevant, Covariant -> false + | (Covariant | Invariant), Covariant -> true + | (Irrelevant | Covariant), Invariant -> false + | Invariant, Invariant -> true + + let pr = function + | Irrelevant -> str "*" + | Covariant -> str "+" + | Invariant -> str "=" + + let leq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant -> enforce_leq_level u u' csts + | Invariant -> enforce_eq_level u u' csts + + let eq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant | Invariant -> enforce_eq_level u u' csts + + let leq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 leq_constraint csts variance u u' + + let eq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 eq_constraint csts variance u u' +end + +module Instance : sig type t = Level.t array val empty : t @@ -893,7 +777,7 @@ module Instance : sig val subst_fn : universe_level_subst_fn -> t -> t - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t val levels : t -> LSet.t end = struct @@ -903,8 +787,7 @@ struct module HInstancestruct = struct - type _t = t - type t = _t + type nonrec t = t type u = Level.t -> Level.t let hashcons huniv a = @@ -970,8 +853,12 @@ struct let levels x = LSet.of_array x - let pr = - prvect_with_sep spc + let pr prl ?variance = + let ppu i u = + let v = Option.map (fun v -> v.(i)) variance in + pr_opt_no_spc Variance.pr v ++ prl u + in + prvecti_with_sep spc ppu let equal t u = t == u || @@ -986,9 +873,37 @@ let enforce_eq_instances x y = let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with") - (Pp.str " instances of different lengths")); + (Pp.str " instances of different lengths.")); CArray.fold_right2 enforce_eq_level ax ay +let enforce_eq_variance_instances = Variance.eq_constraints +let enforce_leq_variance_instances = Variance.leq_constraints + +let subst_instance_level s l = + match l.Level.data with + | Level.Var n -> s.(n) + | _ -> l + +let subst_instance_instance s i = + Array.smartmap (fun l -> subst_instance_level s l) i + +let subst_instance_universe s u = + let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in + let u' = Universe.smartmap f u in + if u == u' then u + else Universe.sort u' + +let subst_instance_constraint s (u,d,v as c) = + let u' = subst_instance_level s u in + let v' = subst_instance_level s v in + if u' == u && v' == v then c + else (u',d,v') + +let subst_instance_constraints s csts = + Constraint.fold + (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) + csts Constraint.empty + type universe_instance = Instance.t type 'a puniverses = 'a * Instance.t @@ -1010,9 +925,9 @@ struct let empty = (Instance.empty, Constraint.empty) let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst - let pr prl (univs, cst as ctx) = + let pr prl ?variance (univs, cst as ctx) = if is_empty ctx then mt() else - h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) + h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -1032,6 +947,69 @@ end type universe_context = UContext.t let hcons_universe_context = UContext.hcons +module AUContext = +struct + include UContext + + let repr (inst, cst) = + (Array.mapi (fun i l -> Level.var i) inst, cst) + + let instantiate inst (u, cst) = + assert (Array.length u = Array.length inst); + subst_instance_constraints inst cst + +end + +type abstract_universe_context = AUContext.t +let hcons_abstract_universe_context = AUContext.hcons + +(** Universe info for cumulative inductive types: A context of + universe levels with universe constraints, representing local + universe variables and constraints, together with an array of + Variance.t. + + This data structure maintains the invariant that the variance + array has the same length as the universe instance. *) +module CumulativityInfo = +struct + type t = universe_context * Variance.t array + + let make x = + if (Instance.length (UContext.instance (fst x))) = + (Array.length (snd x)) then x + else anomaly (Pp.str "Invalid subtyping information encountered!") + + let empty = (UContext.empty, [||]) + let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance + + let pr prl (univs, variance) = + UContext.pr prl ~variance univs + + let hcons (univs, variance) = (* should variance be hconsed? *) + (UContext.hcons univs, variance) + + let univ_context (univs, subtypcst) = univs + let variance (univs, variance) = variance + + (** This function takes a universe context representing constraints + of an inductive and produces a CumulativityInfo.t with the + trivial subtyping relation. *) + let from_universe_context univs = + (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant)) + + let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts + let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts + +end + +type cumulativity_info = CumulativityInfo.t +let hcons_cumulativity_info = CumulativityInfo.hcons + +module ACumulativityInfo = CumulativityInfo + +type abstract_cumulativity_info = ACumulativityInfo.t +let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons + (** A set of universes with universe constraints. We linearize the set to a list after typechecking. Beware, representation could change. @@ -1091,6 +1069,7 @@ struct let constraints (univs, cst) = cst let levels (univs, cst) = univs + let size (univs,_) = LSet.cardinal univs end type universe_context_set = ContextSet.t @@ -1136,6 +1115,9 @@ let subst_univs_level_constraints subst csts = (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) csts Constraint.empty +let subst_univs_level_abstract_universe_context subst (inst, csts) = + inst, subst_univs_level_constraints subst csts + (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe @@ -1146,7 +1128,7 @@ let subst_univs_expr_opt fn (l,n) = let subst_univs_universe fn ul = let subst, nosubst = - Universe.Huniv.fold (fun u (subst,nosubst) -> + List.fold_right (fun u (subst,nosubst) -> try let a' = subst_univs_expr_opt fn u in (a' :: subst, nosubst) with Not_found -> (subst, u :: nosubst)) @@ -1157,59 +1139,9 @@ let subst_univs_universe fn ul = let substs = List.fold_left Universe.merge_univs Universe.empty subst in - List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) + List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u)) substs nosubst -let subst_univs_level fn l = - try Some (fn l) - with Not_found -> None - -let subst_univs_constraint fn (u,d,v as c) cstrs = - let u' = subst_univs_level fn u in - let v' = subst_univs_level fn v in - match u', v' with - | None, None -> Constraint.add c cstrs - | Some u, None -> enforce_univ_constraint (u,d,make v) cstrs - | None, Some v -> enforce_univ_constraint (make u,d,v) cstrs - | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs - -let subst_univs_constraints subst csts = - Constraint.fold - (fun c cstrs -> subst_univs_constraint subst c cstrs) - csts Constraint.empty - -let subst_instance_level s l = - match l.Level.data with - | Level.Var n -> s.(n) - | _ -> l - -let subst_instance_instance s i = - Array.smartmap (fun l -> subst_instance_level s l) i - -let subst_instance_universe s u = - let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in - if u == u' then u - else Universe.sort u' - -let subst_instance_constraint s (u,d,v as c) = - let u' = subst_instance_level s u in - let v' = subst_instance_level s v in - if u' == u && v' == v then c - else (u',d,v') - -let subst_instance_constraints s csts = - Constraint.fold - (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) - csts Constraint.empty - -(** Substitute instance inst for ctx in csts *) -let instantiate_univ_context (ctx, csts) = - (ctx, subst_instance_constraints ctx csts) - -let instantiate_univ_constraints u (_, csts) = - subst_instance_constraints u csts - let make_instance_subst i = let arr = Instance.to_array i in Array.fold_left_i (fun i acc l -> @@ -1222,16 +1154,35 @@ let make_inverse_instance_subst i = LMap.add (Level.var i) l acc) LMap.empty arr -let abstract_universes poly ctx = +let make_abstract_instance (ctx, _) = + Array.mapi (fun i l -> Level.var i) ctx + +let abstract_universes ctx = let instance = UContext.instance ctx in - if poly then - let subst = make_instance_subst instance in - let cstrs = subst_univs_level_constraints subst - (UContext.constraints ctx) - in - let ctx = UContext.make (instance, cstrs) in - subst, ctx - else empty_level_subst, ctx + let subst = make_instance_subst instance in + let cstrs = subst_univs_level_constraints subst + (UContext.constraints ctx) + in + let ctx = UContext.make (instance, cstrs) in + instance, ctx + +let abstract_cumulativity_info (univs, variance) = + let subst, univs = abstract_universes univs in + subst, (univs, variance) + +let rec compact_univ s vars i u = + match u with + | [] -> (s, List.rev vars) + | (lvl, _) :: u -> + match Level.var_index lvl with + | Some k when not (LMap.mem lvl s) -> + let lvl' = Level.var i in + compact_univ (LMap.add lvl lvl' s) (k :: vars) (i+1) u + | _ -> compact_univ s vars i u + +let compact_univ u = + let (s, s') = compact_univ LMap.empty [] 0 u in + (subst_univs_level_universe s u, s') (** Pretty-printing *) @@ -1239,6 +1190,12 @@ let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr +let pr_cumulativity_info = CumulativityInfo.pr + +let pr_abstract_universe_context = AUContext.pr + +let pr_abstract_cumulativity_info = ACumulativityInfo.pr + let pr_universe_context_set = ContextSet.pr let pr_universe_subst = @@ -1287,10 +1244,3 @@ let explain_universe_inconsistency prl (o,u,v,p) = let compare_levels = Level.compare let eq_levels = Level.equal let equal_universes = Universe.equal - - -let subst_instance_constraints = - if Flags.profile then - let key = Profile.declare_profile "subst_instance_constraints" in - Profile.profile2 key subst_instance_constraints - else subst_instance_constraints -- cgit v1.2.3