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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id$ *)
open Util
open Names
open Term
open Environ
open Reductionops
open Type_errors
open Pretype_errors
open Inductive
open Typeops
let vect_lift = Array.mapi lift
let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
(* 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 check_type env (sigma,_) j ty =
if not (is_conv_leq env sigma j.uj_type ty) then
error_actual_type env (j_nf_evar sigma j) (nf_evar sigma ty)
let rec execute env evd cstr =
match kind_of_term cstr with
| Meta n ->
{ uj_val = cstr; uj_type = Evarutil.meta_type (snd evd) n }
| Evar ev ->
let sigma = fst evd in
let ty = Evd.existential_type sigma ev in
let jty = execute env evd ty in
let jty = assumption_of_judgment env evd 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 (constant_type 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 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) ->
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 env evd 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 j = execute env evd f in
let jl = execute_array env evd args in
let (j,_) = judge_of_apply env j jl in
j
| Lambda (name,c1,c2) ->
let j = execute env evd c1 in
let var = type_judgment env evd j in
let env1 = push_rel (name,None,var.utj_val) env in
let j' = execute env1 evd c2 in
judge_of_abstraction env1 name var j'
| Prod (name,c1,c2) ->
let j = execute env evd c1 in
let varj = type_judgment env evd j in
let env1 = push_rel (name,None,varj.utj_val) env in
let j' = execute env1 evd c2 in
let varj' = type_judgment env1 evd 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 j2 = type_judgment env evd j2 in
let _ = judge_of_cast env j1 j2 in
let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
let j3 = execute env1 evd c3 in
judge_of_letin env name j1 j2 j3
| Cast (c,t) ->
let cj = execute env evd c in
let tj = execute env evd t in
let tj = type_judgment env evd tj in
let j, _ = judge_of_cast env cj tj in
j
and execute_recdef env evd (names,lar,vdef) =
let larj = execute_array env evd lar in
let lara = Array.map (assumption_of_judgment env evd) larj in
let env1 = push_rec_types (names,lara,vdef) env 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 env evd v =
let jl = execute_list env evd (Array.to_list v) in
Array.of_list jl
and execute_list env evd = function
| [] ->
[]
| c::r ->
let j = execute env evd c in
let jr = execute_list env evd r in
j::jr
let mcheck env evd c t =
let j = execute env evd c in
check_type env evd j t
(* Type of a constr *)
let mtype_of env evd c =
let j = execute env evd c in
(* No normalization: it breaks Pattern! *)
(*nf_betaiota*) (body_of_type j.uj_type)
let msort_of env evd c =
let j = execute env evd c in
let a = type_judgment env evd j in
a.utj_type
let type_of env sigma c =
mtype_of env (sigma, Evd.Metamap.empty) c
let sort_of env sigma c =
msort_of env (sigma, Evd.Metamap.empty) c
let check env sigma c =
mcheck env (sigma, Evd.Metamap.empty) c
(* The typed type of a judgment. *)
let mtype_of_type env evd constr =
let j = execute env evd constr in
assumption_of_judgment env evd j
|
