diff options
author | 2011-07-04 18:04:58 +0000 | |
---|---|---|
committer | 2011-07-04 18:04:58 +0000 | |
commit | 7382948497f1ae935bd2b16596e468605a3d8033 (patch) | |
tree | bfcc2f4ec453b7989f0d47b15a1ff1667b99d385 /kernel | |
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 'kernel')
-rw-r--r-- | kernel/inductive.ml | 9 | ||||
-rw-r--r-- | kernel/inductive.mli | 11 |
2 files changed, 18 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 07195c493..aeeefbfa4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -178,13 +178,20 @@ let instantiate_universes env ctx ar argsorts = (* This is a Type with constraints *) else Type level -let type_of_inductive_knowing_parameters env mip paramtyps = +exception SingletonInductiveBecomesProp of identifier + +let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps = match mip.mind_arity with | Monomorphic s -> s.mind_user_arity | Polymorphic ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (is_type0m_univ ar.poly_level) && s = prop_sort + then raise (SingletonInductiveBecomesProp mip.mind_typename); mkArity (List.rev ctx,s) (* Type of a (non applied) inductive type *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c14f69343..a124647c6 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -82,7 +82,16 @@ val check_cofix : env -> cofixpoint -> unit (** {6 Support for sort-polymorphic inductive types } *) -val type_of_inductive_knowing_parameters : +(** The "polyprop" optional argument below allows to control + the "Prop-polymorphism". By default, it is allowed. + But when "polyprop=false", the following exception is raised + when a polymorphic singleton inductive type becomes Prop due to + parameter instantiation. This is used by the Ocaml extraction, + which cannot handle (yet?) Prop-polymorphism. *) + +exception SingletonInductiveBecomesProp of identifier + +val type_of_inductive_knowing_parameters : ?polyprop:bool -> env -> one_inductive_body -> types array -> types val max_inductive_sort : sorts array -> universe |