From 7382948497f1ae935bd2b16596e468605a3d8033 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 4 Jul 2011 18:04:58 +0000 Subject: Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml A particular case in sort-polymorphism of inductive types allows an informative type (such as prod) to have instances in Prop: (I,I) : True * True : Prop This is due to the fact that prod is a singleton type: indeed (I,I) has no informative content. But this invalidates an important invariant for the correctness of the extraction: inductive constructors stop having always the same sort as their inductive type. Consider for instance: Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x). Definition test := f _ (I,I) (fun _ => 0). Then the inductive element (I,I) is extracted as a logical part __, but during a strict evaluation (i.e. in Ocaml, not Haskell), this __ will be given to fst, and hence to a match, leading to a nasty result (potentially segfault). Haskell is not affected, since fst is never evaluated. This patch adds a check for this situation during any Ocaml extraction, leading for the moment to a fatal error. Some functions in inductive.ml and retyping.ml now have an extra optional argument ?(polyprop=true) that should stay untouched in regular Coq usage, while type-checking done during extraction will disable this prop-polymorphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/retyping.mli | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) (limited to 'pretyping/retyping.mli') diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index c0d6336cc..445f623a4 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -17,9 +17,17 @@ open Environ either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too. *) -val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types -val get_sort_of : env -> evar_map -> types -> sorts -val get_sort_family_of : env -> evar_map -> types -> sorts_family +(** The "polyprop" optional argument is used by the extraction to + disable "Prop-polymorphism", cf comment in [inductive.ml] *) + +val get_type_of : + ?polyprop:bool -> ?refresh:bool -> env -> evar_map -> constr -> types + +val get_sort_of : + ?polyprop:bool -> env -> evar_map -> types -> sorts + +val get_sort_family_of : + ?polyprop:bool -> env -> evar_map -> types -> sorts_family (** Makes an assumption from a constr *) val get_assumption_of : env -> evar_map -> constr -> types -- cgit v1.2.3