aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-28 19:45:31 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-28 19:48:55 +0100
commit4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e (patch)
tree9cfec2542b673e85dc04e340db656e8a3a98dc68 /pretyping
parent9348b4e69738c36a49e61a23a75a55c0e51f8fb7 (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.ml4
-rw-r--r--pretyping/retyping.mli5
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