diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-04 18:04:58 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-04 18:04:58 +0000 |
commit | 7382948497f1ae935bd2b16596e468605a3d8033 (patch) | |
tree | bfcc2f4ec453b7989f0d47b15a1ff1667b99d385 /pretyping/retyping.mli | |
parent | b639dd55cc3bc6ef4cf77a549786209e094830a2 (diff) |
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
Diffstat (limited to 'pretyping/retyping.mli')
-rw-r--r-- | pretyping/retyping.mli | 14 |
1 files changed, 11 insertions, 3 deletions
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 |