From 090fffa57b2235f70d4355f5dc85d73fa2634655 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 17 Nov 2014 18:09:48 +0100 Subject: Option -type-in-type continued (deactivate test for inferred sort of inductive types + deactivate test for equality of sort + deactivate the check that the constraints Prop/Set <= Type are declared). --- kernel/indtypes.ml | 6 +++--- kernel/reduction.ml | 5 +++-- pretyping/evarconv.ml | 2 +- pretyping/evd.ml | 10 +++++++--- pretyping/evd.mli | 2 +- pretyping/indrec.ml | 2 +- pretyping/reductionops.ml | 2 +- pretyping/unification.ml | 2 +- 8 files changed, 18 insertions(+), 13 deletions(-) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 45e0261d3c..afd7cde979 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -299,8 +299,8 @@ let typecheck_inductive env ctx mie = let full_polymorphic () = let defu = Term.univ_of_sort def_level in let is_natural = - check_leq (universes env') infu defu && - not (is_type0m_univ defu && not is_unit) + type_in_type env || (check_leq (universes env') infu defu && + not (is_type0m_univ defu && not is_unit)) in let _ = (** Impredicative sort, always allow *) @@ -326,7 +326,7 @@ let typecheck_inductive env ctx mie = (* conclusions of the parameters *) (* We enforce [u >= lev] in case [lev] has a strict upper *) (* constraints over [u] *) - let b = check_leq (universes env') infu u in + let b = type_in_type env || check_leq (universes env') infu u in if not b then anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 64964f85e8..704b345bdd 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -573,13 +573,14 @@ let check_sort_cmp_universes env pb s0 s1 univs = end | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible | (Prop c1, Type u) -> - let u0 = univ_of_sort s0 in + if not (type_in_type env) then + let u0 = univ_of_sort s0 in (match pb with | CUMUL -> check_leq univs u0 u | CONV -> check_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then + if not (type_in_type env) then (match pb with | CUMUL -> check_leq univs u1 u2 | CONV -> check_eq univs u1 u2) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 799ca25233..0dc7961103 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -711,7 +711,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (try let evd' = if pbty == CONV - then Evd.set_eq_sort evd s1 s2 + then Evd.set_eq_sort env evd s1 s2 else Evd.set_leq_sort env evd s1 s2 in Success evd' with Univ.UniverseInconsistency p -> diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d36a6a20fb..d5e3c6715c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1114,12 +1114,16 @@ let normalize_sort evars s = if u' == u then s else Type u' (* FIXME inefficient *) -let set_eq_sort d s1 s2 = +let set_eq_sort env d s1 s2 = let s1 = normalize_sort d s1 and s2 = normalize_sort d s2 in match is_eq_sort s1 s2 with | None -> d - | Some (u1, u2) -> add_universe_constraints d - (Universes.Constraints.singleton (u1,Universes.UEq,u2)) + | Some (u1, u2) -> + if not (type_in_type env) then + add_universe_constraints d + (Universes.Constraints.singleton (u1,Universes.UEq,u2)) + else + d let has_lub evd u1 u2 = (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 6c7ef2168c..df5269d345 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -504,7 +504,7 @@ val normalize_universe : evar_map -> Univ.universe -> Univ.universe val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map -val set_eq_sort : evar_map -> sorts -> sorts -> evar_map +val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index d566dd9b23..c1ac0d995b 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -520,7 +520,7 @@ let weaken_sort_scheme env evd set sort npars term ty = | Prod (n,t,c) -> if Int.equal np 0 then let osort, t' = change_sort_arity sort t in - evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort env) !evdref sort osort; + evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort; mkProd (n, t', c), mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) else diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3837ef0c8f..3e549fa846 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1267,7 +1267,7 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y let sigma_compare_sorts env pb s0 s1 sigma = match pb with - | Reduction.CONV -> Evd.set_eq_sort sigma s0 s1 + | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1 | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1 let sigma_compare_instances flex i0 i1 sigma = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f52f0f89b4..a59aceb8cf 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -654,7 +654,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let sigma' = if pb == CUMUL then Evd.set_leq_sort curenv sigma s1 s2 - else Evd.set_eq_sort sigma s1 s2 + else Evd.set_eq_sort curenv sigma s1 s2 in (sigma', metasubst, evarsubst) with e when Errors.noncritical e -> error_cannot_unify curenv sigma (m,n)) -- cgit v1.2.3