diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 186 |
1 files changed, 102 insertions, 84 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index a84cd612..be922c7d 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: typing.ml,v 1.32.6.2 2004/07/16 19:30:46 herbelin Exp $ *) +(* $Id: typing.ml 8673 2006-03-29 21:21:52Z herbelin $ *) open Util open Names @@ -16,68 +16,67 @@ open Reductionops open Type_errors open Pretype_errors open Inductive +open Inductiveops open Typeops +open Evd + +let meta_type env mv = + let ty = + try Evd.meta_ftype env mv + with Not_found -> error ("unknown meta ?"^string_of_int mv) in + meta_instance env ty let vect_lift = Array.mapi lift let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) -type 'a mach_flags = { - fix : bool; - nocheck : bool } - (* The typing machine without information, without universes but with existential variables. *) -let assumption_of_judgment env sigma j = - assumption_of_judgment env (j_nf_evar sigma j) - -let type_judgment env sigma j = - type_judgment env (j_nf_evar sigma j) - - -let rec execute mf env sigma cstr = +(* cstr must be in n.f. w.r.t. evars and execute returns a judgement + where both the term and type are in n.f. *) +let rec execute env evd cstr = match kind_of_term cstr with | Meta n -> - error "execute: found a non-instanciated goal" + { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) } | Evar ev -> - let ty = Instantiate.existential_type sigma ev in - let jty = execute mf env sigma ty in - let jty = assumption_of_judgment env sigma jty in + let sigma = Evd.evars_of evd in + let ty = Evd.existential_type sigma ev in + let jty = execute env evd (nf_evar (evars_of evd) ty) in + let jty = assumption_of_judgment env jty in { uj_val = cstr; uj_type = jty } | Rel n -> - judge_of_relative env n + j_nf_evar (evars_of evd) (judge_of_relative env n) | Var id -> - judge_of_variable env id + j_nf_evar (evars_of evd) (judge_of_variable env id) | Const c -> - make_judge cstr (constant_type env c) + make_judge cstr (nf_evar (evars_of evd) (constant_type env c)) | Ind ind -> - make_judge cstr (type_of_inductive env ind) + make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind)) | Construct cstruct -> - make_judge cstr (type_of_constructor env cstruct) - + make_judge cstr + (nf_evar (evars_of evd) (type_of_constructor env cstruct)) + | Case (ci,p,c,lf) -> - let cj = execute mf env sigma c in - let pj = execute mf env sigma p in - let lfj = execute_array mf env sigma lf in + let cj = execute env evd c in + let pj = execute env evd p in + let lfj = execute_array env evd lf in let (j,_) = judge_of_case env ci pj cj lfj in j | Fix ((vn,i as vni),recdef) -> - if (not mf.fix) && array_exists (fun n -> n < 0) vn then - error "General Fixpoints not allowed"; - let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in + let (_,tys,_ as recdef') = execute_recdef env evd recdef in let fix = (vni,recdef') in check_fix env fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in + let (_,tys,_ as recdef') = execute_recdef env evd recdef in let cofix = (i,recdef') in check_cofix env cofix; make_judge (mkCoFix cofix) tys.(i) @@ -89,86 +88,105 @@ let rec execute mf env sigma cstr = judge_of_type u | App (f,args) -> - let j = execute mf env sigma f in - let jl = execute_array mf env sigma args in + let j = execute env evd f in + let jl = execute_array env evd args in let (j,_) = judge_of_apply env j jl in - j + if isInd f then + (* Sort-polymorphism of inductive types *) + adjust_inductive_level env evd (destInd f) args j + else + j | Lambda (name,c1,c2) -> - let j = execute mf env sigma c1 in - let var = type_judgment env sigma j in + let j = execute env evd c1 in + let var = type_judgment env j in let env1 = push_rel (name,None,var.utj_val) env in - let j' = execute mf env1 sigma c2 in + let j' = execute env1 evd c2 in judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> - let j = execute mf env sigma c1 in - let varj = type_judgment env sigma j in + let j = execute env evd c1 in + let varj = type_judgment env j in let env1 = push_rel (name,None,varj.utj_val) env in - let j' = execute mf env1 sigma c2 in - let varj' = type_judgment env1 sigma j' in + let j' = execute env1 evd c2 in + let varj' = type_judgment env1 j' in judge_of_product env name varj varj' | LetIn (name,c1,c2,c3) -> - let j1 = execute mf env sigma c1 in - let j2 = execute mf env sigma c2 in - let j2 = type_judgment env sigma j2 in - let _ = judge_of_cast env j1 j2 in + let j1 = execute env evd c1 in + let j2 = execute env evd c2 in + let j2 = type_judgment env j2 in + let _ = judge_of_cast env j1 DEFAULTcast j2 in let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in - let j3 = execute mf env1 sigma c3 in + let j3 = execute env1 evd c3 in judge_of_letin env name j1 j2 j3 - | Cast (c,t) -> - let cj = execute mf env sigma c in - let tj = execute mf env sigma t in - let tj = type_judgment env sigma tj in - let j, _ = judge_of_cast env cj tj in + | Cast (c,k,t) -> + let cj = execute env evd c in + let tj = execute env evd t in + let tj = type_judgment env tj in + let j, _ = judge_of_cast env cj k tj in j -and execute_recdef mf env sigma (names,lar,vdef) = - let larj = execute_array mf env sigma lar in - let lara = Array.map (assumption_of_judgment env sigma) larj in +and execute_recdef env evd (names,lar,vdef) = + let larj = execute_array env evd lar in + let lara = Array.map (assumption_of_judgment env) larj in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array mf env1 sigma vdef in + let vdefj = execute_array env1 evd vdef in let vdefv = Array.map j_val vdefj in let _ = type_fixpoint env1 names lara vdefj in (names,lara,vdefv) -and execute_array mf env sigma v = - let jl = execute_list mf env sigma (Array.to_list v) in - Array.of_list jl - -and execute_list mf env sigma = function - | [] -> - [] - | c::r -> - let j = execute mf env sigma c in - let jr = execute_list mf env sigma r in - j::jr - - -let safe_machine env sigma constr = - let mf = { fix = false; nocheck = false } in - execute mf env sigma constr - -let unsafe_machine env sigma constr = - let mf = { fix = false; nocheck = true } in - execute mf env sigma constr +and execute_array env evd = Array.map (execute env evd) + +and execute_list env evd = List.map (execute env evd) + +and adjust_inductive_level env evd ind args j = + let specif = lookup_mind_specif env ind in + if is_small_inductive specif then + (* No polymorphism *) + j + else + (* Retyping constructor with the actual arguments *) + let env',llc,ls0 = constructor_instances env specif ind args in + let llj = Array.map (execute_array env' evd) llc in + let ls = + Array.map (fun lj -> + let ls = + Array.map (fun c -> decomp_sort env (evars_of evd) c.uj_type) lj + in + max_inductive_sort ls) llj + in + let s = find_inductive_level env specif ind ls0 ls in + on_judgment_type (set_inductive_level env s) j + +let mcheck env evd c t = + let sigma = Evd.evars_of evd in + let j = execute env evd (nf_evar sigma c) in + if not (is_conv_leq env sigma j.uj_type t) then + error_actual_type env j (nf_evar sigma t) (* Type of a constr *) - -let type_of env sigma c = - let j = safe_machine env sigma c in + +let mtype_of env evd c = + let j = execute env evd (nf_evar (evars_of evd) c) in (* No normalization: it breaks Pattern! *) (*nf_betaiota*) (body_of_type j.uj_type) -(* The typed type of a judgment. *) +let msort_of env evd c = + let j = execute env evd (nf_evar (evars_of evd) c) in + let a = type_judgment env j in + a.utj_type -let execute_type env sigma constr = - let j = execute { fix=false; nocheck=true } env sigma constr in - assumption_of_judgment env sigma j +let type_of env sigma c = + mtype_of env (Evd.create_evar_defs sigma) c +let sort_of env sigma c = + msort_of env (Evd.create_evar_defs sigma) c +let check env sigma c = + mcheck env (Evd.create_evar_defs sigma) c -let execute_rec_type env sigma constr = - let j = execute { fix=false; nocheck=false } env sigma constr in - assumption_of_judgment env sigma j +(* The typed type of a judgment. *) +let mtype_of_type env evd constr = + let j = execute env evd (nf_evar (evars_of evd) constr) in + assumption_of_judgment env j |