From 35fba70509d9fb219b2a88f8e7bd246b2671b39b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 9 Nov 2017 17:27:58 +0100 Subject: Simplification: cumulativity information is variance information. Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *) --- kernel/reduction.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 059f259ae..d064b3687 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -47,6 +47,9 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t +val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t -> + Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t + val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare -- cgit v1.2.3