diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-28 19:45:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-28 19:48:55 +0100 |
| commit | 4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e (patch) | |
| tree | 9cfec2542b673e85dc04e340db656e8a3a98dc68 /pretyping | |
| parent | 9348b4e69738c36a49e61a23a75a55c0e51f8fb7 (diff) | |
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.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/retyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 5 |
2 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 9653b0eef..f8f086fad 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 af86df499..6fdde9046 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 |