diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 194 |
1 files changed, 115 insertions, 79 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 43e19ca7..831787a0 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: typing.ml 10785 2008-04-13 21:41:54Z herbelin $ *) +(* $Id$ *) open Util open Names @@ -35,155 +35,191 @@ let inductive_type_knowing_parameters env ind jl = let paramstyp = Array.map (fun j -> j.uj_type) jl in Inductive.type_of_inductive_knowing_parameters env mip paramstyp +let e_judge_of_apply env evdref funj argjv = + let rec apply_rec n typ = function + | [] -> + { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = typ } + | hj::restjl -> + match kind_of_term (whd_betadeltaiota env !evdref typ) with + | Prod (_,c1,c2) -> + if Evarconv.e_cumul env evdref hj.uj_type c1 then + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + else + error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv + | _ -> + error_cant_apply_not_functional env funj argjv + in + apply_rec 1 funj.uj_type (Array.to_list argjv) + +let check_branch_types env evdref cj (lfj,explft) = + if Array.length lfj <> Array.length explft then + error_number_branches env cj (Array.length explft); + for i = 0 to Array.length explft - 1 do + if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then + error_ill_formed_branch env cj.uj_val i lfj.(i).uj_type explft.(i) + done + +let e_judge_of_case env evdref ci pj cj lfj = + let indspec = + try find_mrectype env !evdref cj.uj_type + with Not_found -> error_case_not_inductive env cj in + let _ = check_case_info env (fst indspec) ci in + let (bty,rslty,univ) = type_case_branches env indspec pj cj.uj_val in + check_branch_types env evdref cj (lfj,bty); + { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); + uj_type = rslty } + +let e_judge_of_cast env evdref cj k tj = + let expected_type = tj.utj_val in + if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then + error_actual_type env cj expected_type; + { uj_val = mkCast (cj.uj_val, k, expected_type); + uj_type = expected_type } + (* The typing machine without information, without universes but with existential variables. *) (* 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 = +let rec execute env evdref cstr = match kind_of_term cstr with | Meta n -> - { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) } + { uj_val = cstr; uj_type = meta_type !evdref n } | Evar ev -> - 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 ty = Evd.existential_type !evdref ev in + let jty = execute env evdref (whd_evar !evdref ty) in let jty = assumption_of_judgment env jty in { uj_val = cstr; uj_type = jty } - - | Rel n -> - j_nf_evar (evars_of evd) (judge_of_relative env n) - | Var id -> - j_nf_evar (evars_of evd) (judge_of_variable env id) - + | Rel n -> + judge_of_relative env n + + | Var id -> + judge_of_variable env id + | Const c -> - make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c)) - + make_judge cstr (type_of_constant env c) + | Ind ind -> - make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind)) - - | Construct cstruct -> - make_judge cstr - (nf_evar (evars_of evd) (type_of_constructor env cstruct)) + make_judge cstr (type_of_inductive env ind) + + | Construct cstruct -> + make_judge cstr (type_of_constructor env cstruct) | Case (ci,p,c,lf) -> - 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 - + let cj = execute env evdref c in + let pj = execute env evdref p in + let lfj = execute_array env evdref lf in + e_judge_of_case env evdref ci pj cj lfj + | Fix ((vn,i as vni),recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evd recdef in + let (_,tys,_ as recdef') = execute_recdef env evdref 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 env evd recdef in + let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in check_cofix env cofix; make_judge (mkCoFix cofix) tys.(i) - - | Sort (Prop c) -> + + | Sort (Prop c) -> judge_of_prop_contents c | Sort (Type u) -> judge_of_type u - + | App (f,args) -> - let jl = execute_array env evd args in + let jl = execute_array env evdref args in let j = match kind_of_term f with | Ind ind -> (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env ind - (jv_nf_evar (evars_of evd) jl)) - | Const cst -> + (jv_nf_evar !evdref jl)) + | Const cst -> (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env cst - (jv_nf_evar (evars_of evd) jl)) - | _ -> - execute env evd f + (jv_nf_evar !evdref jl)) + | _ -> + execute env evdref f in - fst (judge_of_apply env j jl) - - | Lambda (name,c1,c2) -> - let j = execute env evd c1 in + e_judge_of_apply env evdref j jl + + | Lambda (name,c1,c2) -> + let j = execute env evdref c1 in let var = type_judgment env j in let env1 = push_rel (name,None,var.utj_val) env in - let j' = execute env1 evd c2 in + let j' = execute env1 evdref c2 in judge_of_abstraction env1 name var j' - + | Prod (name,c1,c2) -> - let j = execute env evd c1 in + let j = execute env evdref c1 in let varj = type_judgment env j in let env1 = push_rel (name,None,varj.utj_val) env in - let j' = execute env1 evd c2 in + let j' = execute env1 evdref c2 in let varj' = type_judgment env1 j' in judge_of_product env name varj varj' | LetIn (name,c1,c2,c3) -> - let j1 = execute env evd c1 in - let j2 = execute env evd c2 in + let j1 = execute env evdref c1 in + let j2 = execute env evdref 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 env1 evd c3 in + let j3 = execute env1 evdref c3 in judge_of_letin env name j1 j2 j3 - + | Cast (c,k,t) -> - let cj = execute env evd c in - let tj = execute env evd t in + let cj = execute env evdref c in + let tj = execute env evdref t in let tj = type_judgment env tj in - let j, _ = judge_of_cast env cj k tj in - j + e_judge_of_cast env evdref cj k tj -and execute_recdef env evd (names,lar,vdef) = - let larj = execute_array env evd lar in +and execute_recdef env evdref (names,lar,vdef) = + let larj = execute_array env evdref 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 env1 evd vdef in + let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in let _ = type_fixpoint env1 names lara vdefj in (names,lara,vdefv) -and execute_array env evd = Array.map (execute env evd) +and execute_array env evdref = Array.map (execute env evdref) -and execute_list env evd = List.map (execute env evd) +and execute_list env evdref = List.map (execute env evdref) -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) +let check env evd c t = + let evdref = ref evd in + let j = execute env evdref c in + if not (Evarconv.e_cumul env evdref j.uj_type t) then + error_actual_type env j (nf_evar evd t) (* Type of a constr *) - -let mtype_of env evd c = - let j = execute env evd (nf_evar (evars_of evd) c) in + +let type_of env evd c = + let j = execute env (ref evd) c in (* We are outside the kernel: we take fresh universes *) (* to avoid tactics and co to refresh universes themselves *) Termops.refresh_universes j.uj_type -let msort_of env evd c = - let j = execute env evd (nf_evar (evars_of evd) c) in +(* Sort of a type *) + +let sort_of env evd c = + let j = execute env (ref evd) c in let a = type_judgment env j in a.utj_type -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 +(* Try to solve the existential variables by typing *) -(* 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 +let solve_evars env evd c = + let evdref = ref evd in + let c = (execute env evdref c).uj_val in + (* side-effect on evdref *) + nf_evar !evdref c + |