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
|
(* $Id$ *)
open Util
open Names
open Generic
open Term
open Environ
open Reduction
open Type_errors
open Typeops
let vect_lift = Array.mapi lift
let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
type 'a mach_flags = {
fix : bool;
nocheck : bool }
(* The typing machine without information, without universes but with
existential variables. *)
let rec execute mf env sigma cstr =
match kind_of_term cstr with
| IsMeta n ->
error "execute: found a non-instanciated goal"
| IsEvar _ ->
let ty = type_of_existential env sigma cstr in
let jty = execute mf env sigma ty in
{ uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type }
| IsRel n ->
relative env n
| IsVar id ->
make_judge cstr (snd (lookup_var id env))
| IsAbst _ ->
if evaluable_abst env cstr then
execute mf env sigma (abst_value env cstr)
else
error "Cannot typecheck an unevaluable abstraction"
| IsConst c ->
make_judge cstr (type_of_constant env sigma c)
| IsMutInd ind ->
make_judge cstr (type_of_inductive env sigma ind)
| IsMutConstruct cstruct ->
let (typ,kind) = destCast (type_of_constructor env sigma cstruct) in
{ uj_val = cstr; uj_type = typ; uj_kind = kind }
| IsMutCase (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
type_of_case env sigma ci pj cj lfj
| IsFix ((vn,i as vni),(lar,lfi,vdef)) ->
if (not mf.fix) && array_exists (fun n -> n < 0) vn then
error "General Fixpoints not allowed";
let larjv,vdefv = execute_fix mf env sigma lar lfi vdef in
let larv = Array.map body_of_type larjv in
let fix = vni,(larv,lfi,vdefv) in
check_fix env sigma fix;
make_judge (mkFix fix) larjv.(i)
| IsCoFix (i,(lar,lfi,vdef)) ->
let (larjv,vdefv) = execute_fix mf env sigma lar lfi vdef in
let larv = Array.map body_of_type larjv in
let cofix = i,(larv,lfi,vdefv) in
check_cofix env sigma cofix;
make_judge (mkCoFix cofix) larjv.(i)
| IsSort (Prop c) ->
judge_of_prop_contents c
| IsSort (Type u) ->
let (j,_) = judge_of_type u in j
| IsAppL (f,args) ->
let j = execute mf env sigma f in
let jl = execute_list mf env sigma args in
let (j,_) = apply_rel_list env sigma mf.nocheck jl j in
j
| IsLambda (name,c1,c2) ->
let j = execute mf env sigma c1 in
let var = assumption_of_judgment env sigma j in
let env1 = push_rel (name,var) env in
let j' = execute mf env1 sigma c2 in
let (j,_) = abs_rel env1 sigma name var j' in
j
| IsProd (name,c1,c2) ->
let j = execute mf env sigma c1 in
let var = assumption_of_judgment env sigma j in
let env1 = push_rel (name,var) env in
let j' = execute mf env1 sigma c2 in
let (j,_) = gen_rel env1 sigma name var j' in
j
| IsCast (c,t) ->
let cj = execute mf env sigma c in
let tj = execute mf env sigma t in
cast_rel env sigma cj tj
| _ -> error_cant_execute CCI env cstr
and execute_fix mf env sigma lar lfi vdef =
let larj = execute_array mf env sigma lar in
let lara = Array.map (assumption_of_judgment env sigma) larj in
let nlara =
List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
let env1 =
List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
let vdefj = execute_array mf env1 sigma vdef in
let vdefv = Array.map j_val_only vdefj in
let cst3 = type_fixpoint env1 sigma lfi lara vdefj in
(lara,vdefv)
and execute_array mf env sigma v =
let jl = execute_list mf env sigma (Array.to_list v) in
Array.of_list jl
and execute_list mf env sigma = function
| [] ->
[]
| c::r ->
let j = execute mf env sigma c in
let jr = execute_list mf env sigma r in
j::jr
let safe_machine env sigma constr =
let mf = { fix = false; nocheck = false } in
execute mf env sigma constr
let unsafe_machine env sigma constr =
let mf = { fix = false; nocheck = true } in
execute mf env sigma constr
(* Type of a constr *)
let type_of env sigma c =
let j = safe_machine env sigma c in
nf_betaiota env sigma j.uj_type
(* The typed type of a judgment. *)
let execute_type env sigma constr =
let j = execute { fix=false; nocheck=true } env sigma constr in
assumption_of_judgment env sigma j
let execute_rec_type env sigma constr =
let j = execute { fix=false; nocheck=false } env sigma constr in
assumption_of_judgment env sigma j
|
