diff options
| -rw-r--r-- | kernel/inductive.ml | 9 | ||||
| -rw-r--r-- | kernel/inductive.mli | 11 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 12 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 9 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 1 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 15 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 14 | ||||
| -rw-r--r-- | proofs/logic.ml | 3 |
8 files changed, 60 insertions, 14 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 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 diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 62cd844d8..502e238b3 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -42,7 +42,7 @@ let type_of_var env id = with Not_found -> anomaly ("type_of: variable "^(string_of_id id)^" unbound") -let retype sigma = +let retype ?(polyprop=true) sigma = let rec type_of env cstr= match kind_of_term cstr with | Meta n -> @@ -127,7 +127,8 @@ let retype sigma = match kind_of_term c with | Ind ind -> let (_,mip) = lookup_mind_specif env ind in - (try Inductive.type_of_inductive_knowing_parameters env mip argtyps + (try Inductive.type_of_inductive_knowing_parameters + ~polyprop env mip argtyps with Reduction.NotArity -> anomaly "type_of: Not an arity") | Const cst -> let t = constant_type env cst in @@ -140,8 +141,10 @@ let retype sigma = in type_of, sort_of, sort_family_of, type_of_global_reference_knowing_parameters -let get_sort_of env sigma t = let _,f,_,_ = retype sigma in f env t -let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma in f env c +let get_sort_of ?(polyprop=true) env sigma t = + let _,f,_,_ = retype ~polyprop sigma in f env t +let get_sort_family_of ?(polyprop=true) env sigma c = + let _,_,f,_ = retype ~polyprop sigma in f env c let type_of_global_reference_knowing_parameters env sigma c args = let _,_,_,f = retype sigma in f env c args @@ -161,8 +164,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* We are outside the kernel: we take fresh universes *) (* to avoid tactics and co to refresh universes themselves *) -let get_type_of ?(refresh=true) env sigma c = - let f,_,_,_ = retype sigma in +let get_type_of ?(polyprop=true) ?(refresh=true) env sigma c = + let f,_,_,_ = retype ~polyprop sigma in let t = f env c in if refresh then refresh_universes t else t 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 diff --git a/proofs/logic.ml b/proofs/logic.ml index b482628b9..e72580e69 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -321,7 +321,8 @@ let check_conv_leq_goal env sigma arg ty conclty = raise (RefinerError (BadType (arg,ty,conclty))) let goal_type_of env sigma c = - (if !check then type_of else Retyping.get_type_of ~refresh:true) env sigma c + if !check then type_of env sigma c + else Retyping.get_type_of ~refresh:true env sigma c let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in |