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 |= *) --- engine/universes.ml | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'engine/universes.ml') diff --git a/engine/universes.ml b/engine/universes.ml index eaddf98a8..3a00f0fd1 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -1103,14 +1103,3 @@ let solve_constraints_system levels level_bounds level_min = done; done; v - - -(** Operations for universe_info_ind *) - -(** Given a universe context representing constraints of an inductive - this function produces a UInfoInd.t that with the trivial subtyping relation. *) -let univ_inf_ind_from_universe_context univcst = - let freshunivs = Instance.of_array - (Array.map (fun _ -> new_univ_level ()) - (Instance.to_array (UContext.instance univcst))) - in CumulativityInfo.from_universe_context univcst freshunivs -- cgit v1.2.3