summaryrefslogtreecommitdiff
path: root/pretyping/typing.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /pretyping/typing.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'pretyping/typing.ml')
-rw-r--r--pretyping/typing.ml194
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
+