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 |= *) --- printing/printmod.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'printing/printmod.ml') diff --git a/printing/printmod.ml b/printing/printmod.ml index fb9d45a79..35487e09c 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -113,13 +113,12 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let instantiate_cumulativity_info cumi = let open Univ in let univs = ACumulativityInfo.univ_context cumi in - let subtyp = ACumulativityInfo.subtyp_context cumi in let expose ctx = let inst = AUContext.instance ctx in let cst = AUContext.instantiate inst ctx in UContext.make (inst, cst) in - CumulativityInfo.make (expose univs, expose subtyp) + CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi) let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) -- cgit v1.2.3