diff options
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | kernel/cooking.ml | 4 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 5 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 | ||||
| -rw-r--r-- | kernel/typeops.mli | 3 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/termops.ml | 5 | ||||
| -rw-r--r-- | pretyping/termops.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 6 |
9 files changed, 26 insertions, 14 deletions
@@ -18,6 +18,7 @@ Language (e.g. "Record stream := { hd : nat; tl : stream }.") - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent statements. +- Support for sort-polymorphism on constants denoting inductive types. Vernacular commands @@ -100,8 +101,8 @@ Notations, coercions and implicit arguments (DOC TODO?) - New options Global and Local to "Implicit Arguments" for section surviving or non export outside module. -- Level "constr" moved from 9 to 8 and notation "[ _ ]" now at level 0 - (easy to fix in case of incompatibilites). (DOC TODO?) +- Level "constr" moved from 9 to 8 and notation "[ _ ]" now reserved at level 0 + (may need to move post-fixed uses of [ ] at level 8). (DOC TODO?) - Structure/Record now printed as Record (unless option Printing All is set). - Support for parametric notations defining constants. - Insertion of coercions below product types refrains to unfold @@ -317,7 +318,7 @@ Syntax Language and commands -- Added sort-polymorphism for definitions in Type. +- Added sort-polymorphism for definitions in Type (but finally abandonned). - Support for implicit arguments in the types of parameters in (co-)fixpoints and (co-)inductive declarations. - Improved type inference: use as much of possible general information. diff --git a/kernel/cooking.ml b/kernel/cooking.ml index cc5beb974..a5cda5d13 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -129,6 +129,8 @@ let cook_constant env r = | PolymorphicArity (ctx,s) -> let t = mkArity (ctx,Type s.poly_level) in let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in - Typeops.make_polymorphic_if_arity env typ in + let j = make_judge (force (Option.get body)) typ in + Typeops.make_polymorphic_if_constant_for_ind env j + in let boxed = Cemitcodes.is_boxed cb.const_body_code in (body, typ, cb.const_constraints, cb.const_opaque, boxed,false) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index aedc44ac8..2b28a7147 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,10 +24,7 @@ open Typeops let constrain_type env j cst1 = function | None -> -(* To have definitions in Type polymorphic - make_polymorphic_if_arity env j.uj_type, cst1 -*) - NonPolymorphicType j.uj_type, cst1 + make_polymorphic_if_constant_for_ind env j, cst1 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 616349ba0..53f230baa 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -135,10 +135,10 @@ let extract_context_levels env = List.fold_left (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] -let make_polymorphic_if_arity env t = +let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with - | Sort (Type u) -> + | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> let param_ccls = extract_context_levels env params in let s = { poly_param_levels = param_ccls; poly_level = u} in PolymorphicArity (params,s) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index fe428230a..5bb0dee1d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -105,5 +105,6 @@ val type_of_constant_knowing_parameters : env -> constant_type -> constr array -> types (* Make a type polymorphic if an arity *) -val make_polymorphic_if_arity : env -> types -> constant_type +val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> + constant_type diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 19df941b2..0c03d1b6a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -411,7 +411,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct | App (f,args) -> let f = whd_evar (Evd.evars_of !evdref) f in begin match kind_of_term f with - | Ind _ (* | Const _ *) -> + | Ind _ | Const _ + when isInd f or has_polymorphic_type (destConst f) + -> let sigma = evars_of !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in let t = Retyping.get_type_of env sigma c in diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 124637e13..6d8946f44 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -877,6 +877,11 @@ let isGlobalRef c = | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false +let has_polymorphic_type c = + match (Global.lookup_constant c).Declarations.const_type with + | Declarations.PolymorphicArity _ -> true + | _ -> false + (* nouvelle version de renommage des variables (DEC 98) *) (* This is the algorithm to display distinct bound variables diff --git a/pretyping/termops.mli b/pretyping/termops.mli index ded85464e..608a7d9db 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -237,6 +237,8 @@ val is_section_variable : identifier -> bool val isGlobalRef : constr -> bool +val has_polymorphic_type : constant -> bool + (* Combinators on judgments *) val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment diff --git a/proofs/logic.ml b/proofs/logic.ml index 67bb3a3c2..654bc504a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -278,8 +278,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty) = match kind_of_term f with - | (Ind _ (* needed if defs in Type are polymorphic: | Const _*)) - when not (array_exists occur_meta l) (* we could be finer *) -> + | Ind _ | Const _ + when not (array_exists occur_meta l) (* we could be finer *) + & (isInd f or has_polymorphic_type (destConst f)) + -> (* Sort-polymorphism of definition and inductive types *) goalacc, type_of_global_reference_knowing_parameters env sigma f l |