diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-28 16:46:48 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-28 16:46:48 +0000 |
commit | b49f1fc6d92189a5b9e985042e8d0d07ee0d5220 (patch) | |
tree | 597c65e3b53fb9fe04ee3fd926ce4d3b5330b445 /kernel | |
parent | 598512fa6c6902dda926e3daa1a6def7d5651acb (diff) |
- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites
(i.e. cachées sous un nom de constante) sont considérées comme
monomorphes.
- Divers: renommage type_of_applied_inductive, un peu de documentation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8871 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/indtypes.ml | 35 | ||||
-rw-r--r-- | kernel/inductive.ml | 2 | ||||
-rw-r--r-- | kernel/inductive.mli | 2 | ||||
-rw-r--r-- | kernel/typeops.ml | 20 | ||||
-rw-r--r-- | kernel/typeops.mli | 2 |
5 files changed, 40 insertions, 21 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b5de04221..41ca4e661 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -164,8 +164,8 @@ let small_unit constrsinfos = *) let inductive_levels arities inds = - let levels = Array.map (function _,_,Type u -> Some u | _ -> None) arities in - let cstrs_levels = Array.map (fun (_,_,_,_,_,lev) -> lev) inds in + let levels = Array.map pi3 arities in + let cstrs_levels = Array.map (fun (_,_,_,_,lev) -> lev) inds in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) solve_constraints_system levels cstrs_levels @@ -217,7 +217,12 @@ let typecheck_inductive env mie = let cst = Constraint.union cst cst2 in let id = ind.mind_entry_typename in let env_ar' = push_rel (Name id, None, full_arity) env_ar in - let lev = snd (dest_arity env_params arity.utj_val) in + let lev = + (* Decide that if the conclusion is not explicitly Type *) + (* then the inductive type is not polymorphic *) + match kind_of_term (snd (decompose_prod_assum arity.utj_val)) with + | Sort (Type u) -> Some u + | _ -> None in (cst,env_ar',(id,full_arity,lev)::l)) (cst1,env,[]) mie.mind_entry_inds in @@ -227,11 +232,11 @@ let typecheck_inductive env mie = (* Now, we type the constructors (without params) *) let inds,cst = List.fold_right2 - (fun ind (id,full_arity,_) (inds,cst) -> + (fun ind arity_data (inds,cst) -> let (info,lc',cstrs_univ,cst') = infer_constructor_packet env_arities params ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in - let ind' = (id,full_arity,consnames,info,lc',cstrs_univ) in + let ind' = (arity_data,consnames,info,lc',cstrs_univ) in (ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds arity_list @@ -249,23 +254,25 @@ let typecheck_inductive env mie = (* Compute/check the sorts of the inductive types *) let ind_min_levels = inductive_levels arities inds in - let inds = - array_map2 (fun (id,full_arity,cn,info,lc,_) lev -> + let inds, cst = + array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> let sign, s = dest_arity env full_arity in - let status = match s with - | Type _ -> + let status,cst = match s with + | Type _ when ar_level <> None (* Explicitly polymorphic *) -> (* The polymorphic level is a function of the level of the *) (* conclusions of the parameters *) - Inr (param_ccls, lev) + Inr (param_ccls, lev), cst + | Type u (* Not an explicit occurrence of Type *) -> + Inl (info,full_arity,s), enforce_geq u lev cst | Prop Pos when engagement env <> Some ImpredicativeSet -> (* Predicative set: check that the content is indeed predicative *) if not (is_empty_univ lev) & not (is_base_univ lev) then error "Large non-propositional inductive types must be in Type"; - Inl (info,full_arity,s) + Inl (info,full_arity,s), cst | Prop _ -> - Inl (info,full_arity,s) in - (id,cn,lc,(sign,status))) - inds ind_min_levels in + Inl (info,full_arity,s), cst in + (id,cn,lc,(sign,status)),cst) + inds ind_min_levels cst in (env_arities, params, inds, cst) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index efae466f8..52f2ea3db 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -164,7 +164,7 @@ let instantiate_inductive_with_param_levels env ar mip paramtyps = let subst = make_subst env ar.mind_param_levels args in sort_of_instantiated_universe mip subst ar.mind_level -let type_of_applied_inductive env mip paramtyps = +let type_of_inductive_knowing_parameters env mip paramtyps = match mip.mind_arity with | Monomorphic s -> s.mind_user_arity diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c0a138bde..0f05ffc6b 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -75,7 +75,7 @@ val check_cofix : env -> cofixpoint -> unit (*s Support for sort-polymorphic inductive types *) -val type_of_applied_inductive : +val type_of_inductive_knowing_parameters : env -> one_inductive_body -> types array -> types val set_inductive_level : env -> sorts -> types -> types diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 435b3e31c..4b5a6e01a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -245,16 +245,28 @@ let judge_of_cast env cj k tj = (* Inductive types. *) -let judge_of_applied_inductive env ind jl = +(* The type is parametric over the uniform parameters whose conclusion + is in Type; to enforce the internal constraints between the + parameters and the instances of Type occurring in the type of the + constructors, we use the level variables _statically_ assigned to + the conclusions of the parameters as mediators: e.g. if a parameter + has conclusion Type(alpha), static constraints of the form alpha<=v + exist between alpha and the Type's occurring in the constructor + types; when the parameters is finally instantiated by a term of + conclusion Type(u), then the constraints u<=alpha is computed in + the App case of execute; from this constraints, the expected + dynamic constraints of the form u<=v are enforced *) + +let judge_of_inductive_knowing_parameters env ind jl = let c = mkInd ind in let (mib,mip) = lookup_mind_specif env ind in check_args env c mib.mind_hyps; let paramstyp = Array.map (fun j -> j.uj_type) jl in - let t = Inductive.type_of_applied_inductive env mip paramstyp in + let t = Inductive.type_of_inductive_knowing_parameters env mip paramstyp in make_judge c t let judge_of_inductive env ind = - judge_of_applied_inductive env ind [||] + judge_of_inductive_knowing_parameters env ind [||] (* Constructors. *) @@ -340,7 +352,7 @@ let rec execute env cstr cu = let (j,cu2) = if isInd f then (* Sort-polymorphism of inductive types *) - judge_of_applied_inductive env (destInd f) jl, cu1 + judge_of_inductive_knowing_parameters env (destInd f) jl, cu1 else execute env f cu1 in diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 25f7d15db..6e20cd42d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -78,7 +78,7 @@ val judge_of_cast : val judge_of_inductive : env -> inductive -> unsafe_judgment -val judge_of_applied_inductive : +val judge_of_inductive_knowing_parameters : env -> inductive -> unsafe_judgment array -> unsafe_judgment val judge_of_constructor : env -> constructor -> unsafe_judgment |