From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- kernel/typeops.ml | 65 +++++++++++++++++++++++++++---------------------------- 1 file changed, 32 insertions(+), 33 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 779a427a..8299a3c9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: typeops.ml 8673 2006-03-29 21:21:52Z herbelin $ *) +(* $Id: typeops.ml 8871 2006-05-28 16:46:48Z herbelin $ *) open Util open Names @@ -245,14 +245,28 @@ let judge_of_cast env cj k tj = (* Inductive types. *) -let judge_of_inductive env i = - let constr = mkInd i in - let _ = - let (kn,_) = i in - let mib = lookup_mind kn env in - check_args env constr mib.mind_hyps in - let specif = lookup_mind_specif env i in - make_judge constr (type_of_inductive specif) +(* 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_inductive_knowing_parameters env mip paramstyp in + make_judge c t + +let judge_of_inductive env ind = + judge_of_inductive_knowing_parameters env ind [||] (* Constructors. *) @@ -334,14 +348,15 @@ let rec execute env cstr cu = (* Lambda calculus operators *) | App (f,args) -> - let (j,cu1) = execute env f cu in - let (jl,cu2) = execute_array env args cu1 in - let (j',cu) = univ_combinator cu2 (judge_of_apply env j jl) in - if isInd f then - (* Sort-polymorphism of inductive types *) - adjust_inductive_level env (destInd f) args (j',cu) - else - (j',cu) + let (jl,cu1) = execute_array env args cu in + let (j,cu2) = + if isInd f then + (* Sort-polymorphism of inductive types *) + judge_of_inductive_knowing_parameters env (destInd f) jl, cu1 + else + execute env f cu1 + in + univ_combinator cu2 (judge_of_apply env j jl) | Lambda (name,c1,c2) -> let (varj,cu1) = execute_type env c1 cu in @@ -421,22 +436,6 @@ and execute_array env = array_fold_map' (execute env) and execute_list env = list_fold_map' (execute env) -and adjust_inductive_level env ind args (j,cu) = - let specif = lookup_mind_specif env ind in - if is_small_inductive specif then - (* No polymorphism *) - (j,cu) - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let (llj,cu1) = array_fold_map' (execute_array env') llc cu in - let ls = - Array.map (fun lj -> - max_inductive_sort (Array.map (sort_judgment env) lj)) llj - in - let s = find_inductive_level env specif ind ls0 ls in - (on_judgment_type (set_inductive_level env s) j, cu1) - (* Derived functions *) let infer env constr = let (j,(cst,_)) = -- cgit v1.2.3