From e6bffa602c0d744a24d7ea7418020ebd8b7dfbbf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 7 Oct 2017 11:35:34 +0200 Subject: Fix typo in Univ.CumulativityInfo --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b117f8714b..c2e4d59082 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -234,7 +234,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in - let sbsubst = CumulativityInfo.subtyping_susbst cumi in + let sbsubst = CumulativityInfo.subtyping_subst cumi in let dosubst = subst_univs_level_constr sbsubst in let uctx = CumulativityInfo.univ_context cumi in let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in -- cgit v1.2.3 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/indtypes.ml | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index c2e4d59082..f2677acd64 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -234,22 +234,32 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in - let sbsubst = CumulativityInfo.subtyping_subst cumi in - let dosubst = subst_univs_level_constr sbsubst in let uctx = CumulativityInfo.univ_context cumi in - let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) 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 + let dosubst = subst_univs_level_constr lmap in + let instance_other = Instance.of_array new_levels in + let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in let env = Environ.push_context uctx env_ar in let env = Environ.push_context uctx_other env in - let env = push_context (CumulativityInfo.subtyp_context cumi) env in + let subtyp_constraints = + Variance.leq_constraints (CumulativityInfo.variance cumi) + (UContext.instance uctx) instance_other + Constraint.empty + in + let env = Environ.add_constraints subtyp_constraints env in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor env dosubst full_arity numparams true; Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc - | TemplateArity _ -> () + | TemplateArity _ -> + anomaly ~label:"check_subtyping" + Pp.(str "template polymorphism and cumulative polymorphism are not compatible") ) inds (* Type-check an inductive definition. Does not check positivity -- cgit v1.2.3 From d81ea7705cd60b6bcb1de07282860228a23b68ac Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 11 Nov 2017 21:57:25 +0100 Subject: Universe instance printer: add optional variance argument. --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f2677acd64..cfca335d32 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -246,7 +246,7 @@ let check_subtyping cumi paramsctxt env_ar inds = let env = Environ.push_context uctx env_ar in let env = Environ.push_context uctx_other env in let subtyp_constraints = - Variance.leq_constraints (CumulativityInfo.variance cumi) + CumulativityInfo.leq_constraints cumi (UContext.instance uctx) instance_other Constraint.empty in -- cgit v1.2.3