-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathnorm.mli
148 lines (96 loc) · 3.28 KB
/
norm.mli
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
type __ = Obj.t
type 'a option =
| Some of 'a
| None
type ('a, 'b) prod =
| Pair of 'a * 'b
type 'a list =
| Nil
| Cons of 'a * 'a list
val beq_nat : int -> int -> bool
type id =
int
(* singleton inductive, whose constructor was Id *)
val beq_id : id -> id -> bool
type 'a partial_map = id -> 'a option
val empty : 'a1 partial_map
val extend : 'a1 partial_map -> id -> 'a1 -> id -> 'a1 option
type ty =
| TBool
| TArrow of ty * ty
type tm =
| Tvar of id
| Tapp of tm * tm
| Tabs of id * ty * tm
| Ttrue
| Tfalse
| Tif of tm * tm * tm
val subst : id -> tm -> tm -> tm
type value =
| V_abs of id * ty * tm
| V_true
| V_false
type step =
| ST_AppAbs of id * ty * tm * tm * value
| ST_App1 of tm * tm * tm * step
| ST_App2 of tm * tm * tm * value * step
| ST_IfTrue of tm * tm
| ST_IfFalse of tm * tm
| ST_If of tm * tm * tm * tm * step
type ('x, 'r) multi =
| Multi_refl of 'x
| Multi_step of 'x * 'x * 'x * 'r * ('x, 'r) multi
type ('x, 'p) ex =
| Ex_intro of 'x * 'p
type context = ty partial_map
type has_type =
| T_Var of (id -> ty option) * id * ty
| T_Abs of ty partial_map * id * ty * ty * tm * has_type
| T_App of ty * ty * context * tm * tm * has_type * has_type
| T_True of context
| T_False of context
| T_If of context * tm * tm * tm * ty * has_type * has_type * has_type
val context_invariance :
context -> (id -> ty option) -> tm -> ty -> has_type -> has_type
val substitution_preserves_typing :
ty partial_map -> id -> ty -> tm -> tm -> ty -> has_type -> has_type ->
has_type
val preservation : tm -> tm -> ty -> has_type -> step -> has_type
type halts = (tm, ((tm, step) multi, value) prod) ex
val value_halts : tm -> value -> halts
type r = __
val r_halts : ty -> tm -> r -> halts
val r_typable_empty : ty -> tm -> r -> has_type
type ('p, 'q) iff = ('p -> 'q, 'q -> 'p) prod
val ex_falso_quodlibet : __ -> 'a1
val step_preserves_halting : tm -> tm -> step -> (halts, halts) iff
val step_preserves_R : ty -> tm -> tm -> step -> r -> r
val multistep_preserves_R : ty -> tm -> tm -> (tm, step) multi -> r -> r
val step_preserves_R' : ty -> tm -> tm -> has_type -> step -> r -> r
val multistep_preserves_R' :
ty -> tm -> tm -> has_type -> (tm, step) multi -> r -> r
type env = (id, tm) prod list
val msubst : env -> tm -> tm
type tass = (id, ty) prod list
val mextend : context -> tass -> context
val drop : id -> (id, 'a1) prod list -> (id, 'a1) prod list
type instantiation =
| V_nil
| V_cons of id * ty * tm * tass * env * value * r * instantiation
val instantiation_R : tass -> env -> instantiation -> id -> tm -> ty -> r
val instantiation_drop : tass -> env -> instantiation -> id -> instantiation
val multistep_App2 :
tm -> tm -> tm -> value -> (tm, step) multi -> (tm, step) multi
val multistep_If :
tm -> tm -> tm -> tm -> (tm, step) multi -> (tm, step) multi
val msubst_preserves_typing :
tass -> env -> instantiation -> context -> tm -> ty -> has_type -> has_type
val multi_trans :
'a1 -> 'a1 -> 'a1 -> ('a1, 'a2) multi -> ('a1, 'a2) multi -> ('a1, 'a2)
multi
val multi_R : 'a1 -> 'a1 -> 'a2 -> ('a1, 'a2) multi
val msubst_R : tass -> env -> tm -> ty -> has_type -> instantiation -> r
val normalization : tm -> ty -> has_type -> halts
val beq_ty : ty -> ty -> bool
val type_check : context -> tm -> ty option
val type_checking_sound : context -> tm -> ty -> has_type