From 9348b4e69738c36a49e61a23a75a55c0e51f8fb7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 28 Nov 2017 19:34:13 +0100 Subject: Moving non-recursive function sort_family_of out of the retype block of recursive functions. --- pretyping/retyping.ml | 48 ++++++++++++++++++++++++------------------------ 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5dd6879d39..9653b0eef8 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -166,23 +166,6 @@ let retype ?(polyprop=true) sigma = | Lambda _ | Fix _ | Construct _ -> retype_error NotAType | _ -> decomp_sort env sigma (type_of env t) - and sort_family_of env t = - match EConstr.kind sigma t with - | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) - | 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) && - s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env sigma f -> - let t = type_of_global_reference_knowing_parameters env f args in - Sorts.family (sort_of_atomic_type env sigma t args) - | App(f,args) -> - Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) - | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | _ -> - Sorts.family (decomp_sort env sigma (type_of env t)) - and type_of_global_reference_knowing_parameters env c args = let argtyps = Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in @@ -198,15 +181,32 @@ let retype ?(polyprop=true) sigma = EConstr.of_constr (type_of_constructor env (cstr, u)) | _ -> assert false - in type_of, sort_of, sort_family_of, - type_of_global_reference_knowing_parameters + in type_of, sort_of, type_of_global_reference_knowing_parameters + +let get_sort_family_of ~polyprop env sigma t = + let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in + let rec sort_family_of env t = + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) + | 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) && + s2 == InSet && sort_family_of env t == InType then InType else s2 + | App(f,args) when is_template_polymorphic env sigma f -> + let t = type_of_global_reference_knowing_parameters env f args in + Sorts.family (sort_of_atomic_type env sigma t args) + | App(f,args) -> + Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) + | Lambda _ | Fix _ | Construct _ -> retype_error NotAType + | _ -> + Sorts.family (decomp_sort env sigma (type_of env t)) + in sort_family_of env t let get_sort_of ?(polyprop=true) env sigma t = - let _,f,_,_ = retype ~polyprop sigma in anomaly_on_error (f env) t -let get_sort_family_of ?(polyprop=true) env sigma c = - let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c + let _,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) t let type_of_global_reference_knowing_parameters env sigma c args = - let _,_,_,f = retype sigma in anomaly_on_error (f env c) args + let _,_,f = retype sigma in anomaly_on_error (f env c) args let type_of_global_reference_knowing_conclusion env sigma c conclty = match EConstr.kind sigma c with @@ -232,7 +232,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* get_type_of polyprop lax env sigma c *) let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = - let f,_,_,_ = retype ~polyprop sigma in + let f,_,_ = retype ~polyprop sigma in if lax then f env c else anomaly_on_error (f env) c (* Makes an unsafe judgment from a constr *) -- cgit v1.2.3 From 4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 28 Nov 2017 19:45:31 +0100 Subject: Adding a variant get_truncation_family_of of get_sort_family_of. This function returns InProp or InSet for inductive types only when the inductive type has been explicitly truncated to Prop or (impredicative) Set. For instance, singleton inductive types and small (predicative) inductive types are not truncated and hence in Type. --- API/API.mli | 2 +- pretyping/retyping.ml | 4 +++- pretyping/retyping.mli | 5 ++++- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/API/API.mli b/API/API.mli index 7ec3cbee3b..2e1d077c74 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3696,7 +3696,7 @@ end module Retyping : (* reconstruct the type of a term knowing that it was already typechecked *) sig val get_type_of : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types - val get_sort_family_of : ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family + val get_sort_family_of : ?truncation_style:bool -> ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family val expand_projection : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.constr -> EConstr.constr list -> EConstr.constr val get_sort_of : ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.t diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 9653b0eef8..f8f086fad3 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -183,7 +183,7 @@ let retype ?(polyprop=true) sigma = in type_of, sort_of, type_of_global_reference_knowing_parameters -let get_sort_family_of ~polyprop env sigma t = +let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in let rec sort_family_of env t = match EConstr.kind sigma t with @@ -194,11 +194,13 @@ let get_sort_family_of ~polyprop env sigma t = if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 | App(f,args) when is_template_polymorphic env sigma f -> + if truncation_style then InType else let t = type_of_global_reference_knowing_parameters env f args in Sorts.family (sort_of_atomic_type env sigma t args) | App(f,args) -> Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType + | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType | _ -> Sorts.family (decomp_sort env sigma (type_of env t)) in sort_family_of env t diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index af86df499c..6fdde90463 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -31,8 +31,11 @@ val get_type_of : val get_sort_of : ?polyprop:bool -> env -> evar_map -> types -> Sorts.t +(* When [truncation_style] is [true], tells if the type has been explicitly + truncated to Prop or (impredicative) Set; in particular, singleton type and + small inductive types, which have all eliminations to Type, are in Type *) val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> Sorts.family + ?truncation_style:bool -> ?polyprop:bool -> env -> evar_map -> types -> Sorts.family (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment -- cgit v1.2.3 From 08da05299d32886bb516124fa497347b40249006 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 28 Nov 2017 19:49:02 +0100 Subject: In injection/inversion, consider all template-polymorphic types as injectable. In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273). --- tactics/equality.ml | 2 +- test-suite/bugs/closed/3125.v | 27 +++++++++++++++++++++++++++ 2 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/3125.v diff --git a/tactics/equality.ml b/tactics/equality.ml index c36ad980ef..0d6263246e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -739,7 +739,7 @@ let keep_proof_equalities = function let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let project env sorts posn t1 t2 = let ty1 = get_type_of env sigma t1 in - let s = get_sort_family_of env sigma ty1 in + let s = get_sort_family_of ~truncation_style:true env sigma ty1 in if Sorts.List.mem s sorts then [(List.rev posn,t1,t2)] else [] in diff --git a/test-suite/bugs/closed/3125.v b/test-suite/bugs/closed/3125.v new file mode 100644 index 0000000000..797146174d --- /dev/null +++ b/test-suite/bugs/closed/3125.v @@ -0,0 +1,27 @@ +(* Not considering singleton template-polymorphic inductive types as + propositions for injection/inversion *) + +(* This is also #4560 and #6273 *) + +Inductive foo := foo_1. + +Goal forall (a b : foo), Some a = Some b -> a = b. +Proof. + intros a b H. + inversion H. + reflexivity. +Qed. + +(* Check that Prop is not concerned *) + +Inductive bar : Prop := bar_1. + +Goal + forall (a b : bar), + Some a = Some b -> + a = b. +Proof. + intros a b H. + inversion H. + Fail reflexivity. +Abort. -- cgit v1.2.3