1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: typing.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Names
open Term
open Environ
open Reductionops
open Type_errors
open Pretype_errors
open Inductive
open Inductiveops
open Typeops
open Evd
let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in
meta_instance evd ty
let constant_type_knowing_parameters env cst jl =
let paramstyp = Array.map (fun j -> j.uj_type) jl in
type_of_constant_knowing_parameters env (constant_type env cst) paramstyp
let inductive_type_knowing_parameters env ind jl =
let (mib,mip) = lookup_mind_specif env ind in
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 evdref cstr =
match kind_of_term cstr with
| Meta n ->
{ uj_val = cstr; uj_type = meta_type !evdref n }
| Evar ev ->
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 ->
judge_of_relative env n
| Var id ->
judge_of_variable env id
| Const c ->
make_judge cstr (type_of_constant env c)
| Ind ind ->
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 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 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 evdref recdef in
let cofix = (i,recdef') in
check_cofix env cofix;
make_judge (mkCoFix cofix) tys.(i)
| Sort (Prop c) ->
judge_of_prop_contents c
| Sort (Type u) ->
judge_of_type u
| App (f,args) ->
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 !evdref jl))
| Const cst ->
(* Sort-polymorphism of inductive types *)
make_judge f
(constant_type_knowing_parameters env cst
(jv_nf_evar !evdref jl))
| _ ->
execute env evdref f
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 evdref c2 in
judge_of_abstraction env1 name var j'
| Prod (name,c1,c2) ->
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 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 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 evdref c3 in
judge_of_letin env name j1 j2 j3
| Cast (c,k,t) ->
let cj = execute env evdref c in
let tj = execute env evdref t in
let tj = type_judgment env tj in
e_judge_of_cast env evdref cj k tj
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 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 evdref = Array.map (execute env evdref)
and execute_list env evdref = List.map (execute env evdref)
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 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
(* 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
(* Try to solve the existential variables by typing *)
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
|
