From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 Mar 2017 23:20:25 +0200 Subject: Actually exporting delayed universes in the EConstr implementation. For now we only normalize sorts, and we leave instances for the next commit. --- engine/eConstr.ml | 54 +++++++++++++++++++++++++++++++++++--------- engine/eConstr.mli | 26 ++++++++++++++++++--- engine/namegen.ml | 2 +- engine/termops.ml | 9 ++++++-- plugins/ltac/rewrite.ml | 2 +- plugins/ltac/taccoerce.ml | 2 +- plugins/omega/coq_omega.ml | 2 +- pretyping/coercion.ml | 6 ++--- pretyping/constr_matching.ml | 13 +++++++---- pretyping/detyping.ml | 2 +- pretyping/evarconv.ml | 3 +++ pretyping/evardefine.ml | 6 ++--- pretyping/evarsolve.ml | 9 ++++++-- pretyping/inductiveops.ml | 1 + pretyping/pretyping.ml | 8 +++++-- pretyping/reductionops.mli | 6 ++--- pretyping/retyping.ml | 16 ++++++++----- pretyping/typing.ml | 15 +++++++----- pretyping/unification.ml | 2 ++ tactics/class_tactics.ml | 6 ++++- vernac/command.ml | 4 ++-- 21 files changed, 140 insertions(+), 54 deletions(-) diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 094841d69..166340b41 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -16,12 +16,19 @@ open Evd module API : sig +module ESorts : +sig +type t +val make : Sorts.t -> t +val kind : Evd.evar_map -> t -> Sorts.t +val unsafe_to_sorts : t -> Sorts.t +end type t -val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type val whd_evar : Evd.evar_map -> t -> t -val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t +val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t val of_constr : Constr.t -> t val to_constr : evar_map -> t -> Constr.t val unsafe_to_constr : t -> Constr.t @@ -33,6 +40,16 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) end = struct +module ESorts = +struct + type t = Sorts.t + let make s = s + let kind sigma = function + | Type u -> sort_of_univ (Evd.normalize_universe sigma u) + | s -> s + let unsafe_to_sorts s = s +end + type t = Constr.t let safe_evar_value sigma ev = @@ -46,9 +63,6 @@ let rec whd_evar sigma c = | Some c -> whd_evar sigma c | None -> c end - | Sort (Type u) -> - let u' = Evd.normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') | Const (c', u) when not (Univ.Instance.is_empty u) -> let u' = Evd.normalize_universe_instance sigma u in if u' == u then c else mkConstU (c', u') @@ -82,8 +96,25 @@ let of_constr c = c let unsafe_to_constr c = c let unsafe_eq = Refl -let rec to_constr sigma t = - Constr.map (fun t -> to_constr sigma t) (whd_evar sigma t) +let rec to_constr sigma c = match Constr.kind c with +| Evar ev -> + begin match safe_evar_value sigma ev with + | Some c -> to_constr sigma c + | None -> Constr.map (fun c -> to_constr sigma c) c + end +| Sort (Type u) -> + let u' = Evd.normalize_universe sigma u in + if u' == u then c else mkSort (Sorts.sort_of_univ u') +| Const (c', u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkConstU (c', u') +| Ind (i, u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkIndU (i, u') +| Construct (co, u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkConstructU (co, u') +| _ -> Constr.map (fun c -> to_constr sigma c) c let of_named_decl d = d let unsafe_to_named_decl d = d @@ -108,14 +139,14 @@ type rel_context = (constr, types) Context.Rel.pt let in_punivs a = (a, Univ.Instance.empty) -let mkProp = of_kind (Sort Sorts.prop) -let mkSet = of_kind (Sort Sorts.set) -let mkType u = of_kind (Sort (Sorts.Type u)) +let mkProp = of_kind (Sort (ESorts.make Sorts.prop)) +let mkSet = of_kind (Sort (ESorts.make Sorts.set)) +let mkType u = of_kind (Sort (ESorts.make (Sorts.Type u))) let mkRel n = of_kind (Rel n) let mkVar id = of_kind (Var id) let mkMeta n = of_kind (Meta n) let mkEvar e = of_kind (Evar e) -let mkSort s = of_kind (Sort s) +let mkSort s = of_kind (Sort (ESorts.make s)) let mkCast (b, k, t) = of_kind (Cast (b, k, t)) let mkProd (na, t, u) = of_kind (Prod (na, t, u)) let mkLambda (na, t, c) = of_kind (Lambda (na, t, c)) @@ -730,6 +761,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference = module Unsafe = struct +let to_sorts = ESorts.unsafe_to_sorts let to_constr = unsafe_to_constr let to_rel_decl = unsafe_to_rel_decl let to_named_decl = unsafe_to_named_decl diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e7287fc06..db10fbf42 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -28,9 +28,26 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt type named_context = (constr, types) Context.Named.pt type rel_context = (constr, types) Context.Rel.pt +(** {5 Universe variables} *) + +module ESorts : +sig + type t + (** Type of sorts up-to universe unification. Essentially a wrapper around + Sorts.t so that normalization is ensured statically. *) + + val make : Sorts.t -> t + (** Turn a sort into an up-to sort. *) + + val kind : Evd.evar_map -> t -> Sorts.t + (** Returns the view into the current sort. Note that the kind of a variable + may change if the unification state of the evar map changes. *) + +end + (** {5 Destructors} *) -val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term (** Same as {!Constr.kind} except that it expands evars and normalizes universes on the fly. *) @@ -43,7 +60,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) -val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t +val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t (** Construct a term from a view. *) val of_constr : Constr.t -> t @@ -123,7 +140,7 @@ val isRelN : Evd.evar_map -> int -> t -> bool val destRel : Evd.evar_map -> t -> int val destMeta : Evd.evar_map -> t -> metavariable val destVar : Evd.evar_map -> t -> Id.t -val destSort : Evd.evar_map -> t -> Sorts.t +val destSort : Evd.evar_map -> t -> ESorts.t val destCast : Evd.evar_map -> t -> t * cast_kind * t val destProd : Evd.evar_map -> t -> Name.t * types * types val destLambda : Evd.evar_map -> t -> Name.t * types * t @@ -242,6 +259,9 @@ sig val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *) + val to_sorts : ESorts.t -> Sorts.t + (** Physical identity. Does not care for normalization. *) + val eq : (t, Constr.t) eq (** Use for transparent cast between types. *) end diff --git a/engine/namegen.ml b/engine/namegen.ml index 7b7302957..3b979f206 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -123,7 +123,7 @@ let hdchar env sigma c = | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x)) | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x)) | Var id -> lowercase_first_char id - | Sort s -> sort_hdchar s + | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else diff --git a/engine/termops.ml b/engine/termops.ml index 410fb75c5..a67916345 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1181,14 +1181,19 @@ let base_sort_cmp pb s0 s1 = | _ -> false let rec is_Prop sigma c = match EConstr.kind sigma c with - | Sort (Prop Null) -> true + | Sort u -> + begin match EConstr.ESorts.kind sigma u with + | Prop Null -> true + | _ -> false + end | Cast (c,_,_) -> is_Prop sigma c | _ -> false (* eq_constr extended with universe erasure *) let compare_constr_univ sigma f cv_pb t1 t2 = + let open EConstr in match EConstr.kind sigma t1, EConstr.kind sigma t2 with - Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 + Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2) | Prod (_,t1,c1), Prod (_,t2,c2) -> f Reduction.CONV t1 t2 && f cv_pb c1 c2 | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2 diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 55172cba6..b84be4600 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -434,7 +434,7 @@ module TypeGlobal = struct end let sort_of_rel env evm rel = - Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel) + ESorts.kind evm (Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel)) let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 114b8dda0..95620b374 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -164,7 +164,7 @@ let id_of_name = function basename | Sort s -> begin - match s with + match ESorts.kind sigma s with | Prop _ -> Label.to_id (Label.make "Prop") | Type _ -> Label.to_id (Label.make "Type") end diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index adf926958..a2016cb03 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1714,7 +1714,7 @@ let onClearedName2 id tac = end }) let rec is_Prop sigma c = match EConstr.kind sigma c with - | Sort (Prop Null) -> true + | Sort s -> Sorts.is_prop (ESorts.kind sigma s) | Cast (c,_,_) -> is_Prop sigma c | _ -> false diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 8794f238b..542db7fdf 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -199,7 +199,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) in match (EConstr.kind !evdref x, EConstr.kind !evdref y) with | Sort s, Sort s' -> - (match s, s' with + (match ESorts.kind !evdref s, ESorts.kind !evdref s' with | Prop x, Prop y when x == y -> None | Prop _, Type _ -> None | Type x, Type y when Univ.Universe.equal x y -> None (* false *) @@ -406,7 +406,7 @@ let inh_app_fun resolve_tc env evd j = let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = s } + | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind sigma s } | _ -> error_not_a_type env sigma j let inh_tosort_force loc env evd j = @@ -421,7 +421,7 @@ let inh_tosort_force loc env evd j = let inh_coerce_to_sort loc env evd j = let typ = whd_all env evd j.uj_type in match EConstr.kind evd typ with - | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) + | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = ESorts.kind evd s }) | Evar ev -> let (evd',s) = Evardefine.define_evar_as_sort env evd ev in (evd',{ utj_val = j.uj_val; utj_type = s }) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index cad21543b..30b83cf88 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -205,11 +205,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PRel n1, Rel n2 when Int.equal n1 n2 -> subst - | PSort GProp, Sort (Prop Null) -> subst - - | PSort GSet, Sort (Prop Pos) -> subst - - | PSort (GType _), Sort (Type _) -> subst + | PSort ps, Sort s -> + + begin match ps, ESorts.kind sigma s with + | GProp, Prop Null -> subst + | GSet, Prop Pos -> subst + | GType _, Type _ -> subst + | _ -> raise PatternMatchingFailure + end | PApp (p, [||]), _ -> sorec ctx env subst p t diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1adda14ab..84022f57f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -457,7 +457,7 @@ let rec detype flags avoid env sigma t = | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id, None) with Not_found -> GVar (dl, id)) - | Sort s -> GSort (dl,detype_sort sigma s) + | Sort s -> GSort (dl,detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> detype flags avoid env sigma c1 | Cast (c1,k,c2) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 85cc8762e..b6fa25769 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -150,6 +150,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> + let s = ESorts.kind sigma s in lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] | _ -> @@ -775,6 +776,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Sort s1, Sort s2 when app_empty -> (try + let s1 = ESorts.kind evd s1 in + let s2 = ESorts.kind evd s2 in let evd' = if pbty == CONV then Evd.set_eq_sort env evd s1 s2 diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 20d86f81b..c5ae684e3 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -91,7 +91,7 @@ let define_pure_evar_as_product evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in - if is_prop_sort s then + if is_prop_sort (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) new_evar_unsafe newenv evd1 concl ~src ~filter else @@ -102,7 +102,7 @@ let define_pure_evar_as_product evd evk = (Sigma.to_evar_map evd3, e) in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in - let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in + let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in evd3, rng in let prod = mkProd (Name id, dom, subst_var id rng) in @@ -174,7 +174,7 @@ let define_evar_as_sort env evd (ev,args) = let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in let sort = destSort evd concl in let evd' = Evd.define ev (Constr.mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s + Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4d78d2eb0..77086d046 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -50,6 +50,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) let modified = ref false in (* direction: true for fresh universes lower than the existing ones *) let refresh_sort status ~direction s = + let s = ESorts.kind !evdref s in let s' = evd_comb0 (new_sort_variable status) evdref in let evd = if direction then set_leq_sort env !evdref s' s @@ -59,7 +60,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) in let rec refresh ~onlyalg status ~direction t = match EConstr.kind !evdref t with - | Sort (Type u as s) -> + | Sort s -> + begin match ESorts.kind !evdref s with + | Type u -> (match Univ.universe_level u with | None -> refresh_sort status ~direction s | Some l -> @@ -71,10 +74,12 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if onlyalg && alg then (evdref := Evd.make_flexible_variable !evdref false l; t) else t)) - | Sort (Prop Pos as s) when refreshset && not direction -> + | Prop Pos when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) refresh_sort status ~direction s + | _ -> t + end | Prod (na,u,v) -> mkProd (na, u, refresh ~onlyalg status ~direction v) | _ -> t diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d5967c4bf..88c492f03 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -617,6 +617,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity) | TemplateArity ar -> let _,scl = splay_arity env sigma conclty in + let scl = EConstr.ESorts.kind sigma scl in let ctx = List.rev mip.mind_arity_ctxt in let evdref = ref sigma in let ctx = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 846d8055a..c673851c8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1071,7 +1071,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> let rec is_Type c = match EConstr.kind !evdref c with - | Sort (Type _) -> true + | Sort s -> + begin match ESorts.kind !evdref s with + | Type _ -> true + | Prop _ -> false + end | Cast (c, _, _) -> is_Type c | _ -> false in @@ -1081,7 +1085,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with - | Sort s -> s + | Sort s -> ESorts.kind sigma s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 18416b142..01707b47a 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -215,8 +215,8 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts -val sort_of_arity : env -> evar_map -> constr -> sorts +val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * ESorts.t +val sort_of_arity : env -> evar_map -> constr -> ESorts.t val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_prod_assum : @@ -232,7 +232,7 @@ type 'a miota_args = { val reducible_mind_case : evar_map -> constr -> bool val reduce_mind_case : evar_map -> constr miota_args -> constr -val find_conclusion : env -> evar_map -> constr -> (constr, constr, Sorts.t, Univ.Instance.t) kind_of_term +val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, Univ.Instance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index bb1b2901e..9c9751af8 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -77,7 +77,7 @@ let sort_of_atomic_type env sigma ft args = let rec concl_of_arity env n ar args = match EConstr.kind sigma (whd_all env sigma ar), args with | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l - | Sort s, [] -> s + | Sort s, [] -> ESorts.kind sigma s | _ -> retype_error NotASort in concl_of_arity env 0 ft (Array.to_list args) @@ -87,9 +87,11 @@ let type_of_var env id = let decomp_sort env sigma t = match EConstr.kind sigma (whd_all env sigma t) with - | Sort s -> s + | Sort s -> ESorts.kind sigma s | _ -> retype_error NotASort +let destSort sigma s = ESorts.kind sigma (destSort sigma s) + let retype ?(polyprop=true) sigma = let rec type_of env cstr = match EConstr.kind sigma cstr with @@ -142,8 +144,11 @@ let retype ?(polyprop=true) sigma = and sort_of env t = match EConstr.kind sigma t with | Cast (c,_, s) when isSort sigma s -> destSort sigma s - | Sort (Prop c) -> type1_sort - | Sort (Type u) -> Type (Univ.super u) + | Sort s -> + begin match ESorts.kind sigma s with + | Prop _ -> type1_sort + | Type u -> Type (Univ.super u) + end | Prod (name,t,c2) -> (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with | _, (Prop Null as s) -> s @@ -163,8 +168,7 @@ let retype ?(polyprop=true) sigma = and sort_family_of env t = match EConstr.kind sigma t with | Cast (c,_, s) when isSort sigma s -> family_of_sort (destSort sigma s) - | Sort (Prop c) -> InType - | Sort (Type u) -> InType + | Sort _ -> InType | Prod (name,t,c2) -> let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in if not (is_impredicative_set env) && diff --git a/pretyping/typing.ml b/pretyping/typing.ml index dec22ecd0..d9d64e7eb 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -46,7 +46,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl = let e_type_judgment env evdref j = match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = s } + | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind !evdref s } | Evar ev -> let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in evdref := evd; { utj_val = j.uj_val; utj_type = s } @@ -102,6 +102,7 @@ let e_is_correct_arity env evdref c pj ind specif params = if not (Evarconv.e_cumul env evdref a1 a1') then error (); srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Sort s, [] -> + let s = ESorts.kind !evdref s in if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () | Evar (ev,_), [] -> @@ -161,7 +162,7 @@ let check_type_fixpoint loc env evdref lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in - let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in + let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in if not (List.exists ((==) ksort) sorts) then @@ -288,11 +289,13 @@ let rec execute env evdref cstr = check_cofix env !evdref cofix; make_judge (mkCoFix cofix) tys.(i) - | Sort (Prop c) -> - judge_of_prop_contents c - - | Sort (Type u) -> + | Sort s -> + begin match ESorts.kind !evdref s with + | Prop c -> + judge_of_prop_contents c + | Type u -> judge_of_type u + end | Proj (p, c) -> let cj = execute env evdref c in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 611d165fe..035b0c223 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -780,6 +780,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else error_cannot_unify_local curenv sigma (m,n,cN) | Sort s1, Sort s2 -> (try + let s1 = ESorts.kind sigma s1 in + let s2 = ESorts.kind sigma s2 in let sigma' = if pb == CUMUL then Evd.set_leq_sort curenv sigma s1 s2 diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index c53e47d92..7eadde78d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -512,7 +512,11 @@ let pr_depth l = prlist_with_sep (next_sep debug_seps) int (List.rev l) let is_Prop env sigma concl = let ty = Retyping.get_type_of env sigma concl in match EConstr.kind sigma ty with - | Sort (Prop Null) -> true + | Sort s -> + begin match ESorts.kind sigma s with + | Prop Null -> true + | _ -> false + end | _ -> false let is_unique env sigma concl = diff --git a/vernac/command.ml b/vernac/command.ml index 32b0abb8a..db203b425 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -987,8 +987,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = try let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in match ctx, EConstr.kind !evdref ar with - | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null) - when Reductionops.is_conv env !evdref t u -> t + | [LocalAssum (_,t); LocalAssum (_,u)], Sort s + when Sorts.is_prop (ESorts.kind !evdref s) && Reductionops.is_conv env !evdref t u -> t | _, _ -> error () with e when CErrors.noncritical e -> error () in -- cgit v1.2.3