diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 113 |
1 files changed, 56 insertions, 57 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index f9110c62a..7dd552e38 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -12,8 +12,10 @@ open Util open Names open Term open Environ -open Reduction +open Reductionops open Type_errors +open Pretype_errors +open Inductive open Typeops let vect_lift = Array.mapi lift @@ -26,111 +28,108 @@ type 'a mach_flags = { (* 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 = match kind_of_term cstr with - | IsMeta n -> + | Meta n -> error "execute: found a non-instanciated goal" - | IsEvar ev -> - let ty = type_of_existential env sigma ev in + | 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 { uj_val = cstr; uj_type = jty } - | IsRel n -> - relative env n - - | IsVar id -> - (try - make_judge cstr (snd (lookup_named id env)) - with Not_found -> - error ("execute: variable " ^ (string_of_id id) ^ " not defined")) + | Rel n -> + judge_of_relative env n + + | Var id -> + judge_of_variable env id - | IsConst c -> - make_judge cstr (type_of_constant env sigma c) + | Const c -> + make_judge cstr (constant_type env c) - | IsMutInd ind -> - make_judge cstr (type_of_inductive env sigma ind) + | Ind ind -> + make_judge cstr (type_of_inductive env ind) - | IsMutConstruct cstruct -> - make_judge cstr (type_of_constructor env sigma cstruct) + | Construct cstruct -> + make_judge cstr (type_of_constructor env cstruct) - | IsMutCase (ci,p,c,lf) -> + | 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 (j,_) = judge_of_case env sigma ci pj cj lfj in + let (j,_) = judge_of_case env ci pj cj lfj in j - | IsFix ((vn,i as vni),recdef) -> + | 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_fix mf env sigma recdef in + let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in let fix = (vni,recdef') in - check_fix env sigma fix; + check_fix env fix; make_judge (mkFix fix) tys.(i) - | IsCoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_fix mf env sigma recdef in + | CoFix (i,recdef) -> + let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in let cofix = (i,recdef') in - check_cofix env sigma cofix; + check_cofix env cofix; make_judge (mkCoFix cofix) tys.(i) - | IsSort (Prop c) -> + | Sort (Prop c) -> judge_of_prop_contents c - | IsSort (Type u) -> + | Sort (Type u) -> let (j,_) = judge_of_type u in j - | IsApp (f,args) -> + | App (f,args) -> let j = execute mf env sigma f in - let jl = execute_list mf env sigma (Array.to_list args) in - let (j,_) = apply_rel_list env sigma mf.nocheck jl j in + let jl = execute_array mf env sigma args in + let (j,_) = judge_of_apply env j jl in j - | IsLambda (name,c1,c2) -> + | Lambda (name,c1,c2) -> let j = execute mf env sigma c1 in - let var = assumption_of_judgment env sigma j in - let env1 = push_rel_assum (name,var) env in + let var = type_judgment env sigma j in + let env1 = push_rel (name,None,var.utj_val) env in let j' = execute mf env1 sigma c2 in - let (j,_) = abs_rel env1 sigma name var j' in - j + judge_of_abstraction env1 name var j' - | IsProd (name,c1,c2) -> + | Prod (name,c1,c2) -> let j = execute mf env sigma c1 in let varj = type_judgment env sigma j in - let env1 = push_rel_assum (name,varj.utj_val) env in + let env1 = push_rel (name,None,varj.utj_val) env in let j' = execute mf env1 sigma c2 in let varj' = type_judgment env sigma j' in - let (j,_) = gen_rel env1 sigma name varj varj' in + let (j,_) = judge_of_product env1 name varj varj' in j - | IsLetIn (name,c1,c2,c3) -> - let j1 = execute mf env sigma c1 in - let j2 = execute mf env sigma c2 in - let tj2 = assumption_of_judgment env sigma j2 in - let { uj_val = b; uj_type = t },_ = cast_rel env sigma j1 tj2 in - let j3 = execute mf (push_rel_def (name,b,t) env) sigma c3 in - { uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ; - uj_type = type_app (subst1 j1.uj_val) j3.uj_type } + | LetIn (name,c1,c2,c3) -> + let j1 = execute mf env sigma (mkCast (c1, c2)) in + let env1 = push_rel (name,Some j1.uj_val,j1.uj_type) env in + let j3 = execute mf env1 sigma c3 in + judge_of_letin env name j1 j3 - | IsCast (c,t) -> + | Cast (c,t) -> let cj = execute mf env sigma c in let tj = execute mf env sigma t in - let tj = assumption_of_judgment env sigma tj in - let j, _ = cast_rel env sigma cj tj in + let tj = type_judgment env sigma tj in + let j, _ = judge_of_cast env cj tj in j - -and execute_fix mf env sigma (names,lar,vdef) = + +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 - let ctxt = - array_map2_i (fun i na ty -> (na, type_app (lift i) ty)) names lara in - let env1 = - Array.fold_left (fun env nvar -> push_rel_assum nvar env) env ctxt in + let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array mf env1 sigma vdef in let vdefv = Array.map j_val vdefj in - let cst3 = type_fixpoint env1 sigma names lara vdefj in + let _ = type_fixpoint env1 names lara vdefj in (names,lara,vdefv) and execute_array mf env sigma v = |