diff options
author | 2011-07-04 18:04:58 +0000 | |
---|---|---|
committer | 2011-07-04 18:04:58 +0000 | |
commit | 7382948497f1ae935bd2b16596e468605a3d8033 (patch) | |
tree | bfcc2f4ec453b7989f0d47b15a1ff1667b99d385 /plugins/extraction | |
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 'plugins/extraction')
-rw-r--r-- | plugins/extraction/extraction.ml | 12 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 9 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 1 |
3 files changed, 20 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 979240663..455965af4 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -34,9 +34,17 @@ let current_fixpoints = ref ([] : constant list) let none = Evd.empty -let type_of env c = Retyping.get_type_of env none (strip_outer_cast c) +let type_of env c = + try + let polyprop = (lang() = Haskell) in + Retyping.get_type_of ~polyprop env none (strip_outer_cast c) + with SingletonInductiveBecomesProp id -> error_singleton_become_prop id -let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c) +let sort_of env c = + try + let polyprop = (lang() = Haskell) in + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) + with SingletonInductiveBecomesProp id -> error_singleton_become_prop id (*S Generation of flags and signatures. *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ad5424deb..aa312321b 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -334,6 +334,15 @@ let error_no_module_expr mp = ++ str "some Declare Module outside any Module Type.\n" ++ str "This situation is currently unsupported by the extraction.") +let error_singleton_become_prop id = + err (str "The informative inductive type " ++ pr_id id ++ + str " has a Prop instance.\n" ++ + str "This happens when a sort-polymorphic singleton inductive type\n" ++ + str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++ + str "The Ocaml extraction cannot handle this situation yet.\n" ++ + str "Instead, use a sort-monomorphic type such as (True /\\ True)\n" ++ + str "or extract to Haskell.") + let error_unknown_module m = err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index ce57a7840..d656edfb7 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -29,6 +29,7 @@ val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a val error_no_module_expr : module_path -> 'a +val error_singleton_become_prop : identifier -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a |