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/typeops.ml | |
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/typeops.ml')
-rw-r--r-- | kernel/typeops.ml | 20 |
1 files changed, 16 insertions, 4 deletions
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 |