-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathAlgorithm.v
254 lines (213 loc) · 8.68 KB
/
Algorithm.v
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
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
Require Import Infrastructure.
Require Import List.
Import ListNotations.
(* ********************************************************************** *)
(** * Algorithmic queue *)
Inductive qs : Set :=
| qs_arr (A:sty)
| qs_all (X:typvar) (A:sty)
| qs_rcd (l:nat).
Definition size_elem (s : qs) : nat :=
match s with
| qs_arr A => size_sty A
| qs_all _ A => size_sty A
| qs_rcd _ => 0
end.
(* ********************************************************************** *)
(** * Q => A *)
Definition seqs : Set := list qs.
Definition applyfs (Q : seqs) (A : sty) :=
fold_right (fun el acc =>
match el with
| qs_arr A => sty_arrow A acc
| qs_rcd l => sty_rcd l acc
| qs_all X A => sty_all A (close_sty_wrt_sty X acc)
end) A Q.
(**
Well-formedness of Q
Q grows at the tail, which requires that variales appearing later should be
fresh with respect to previous items.
The following is not correct.
Inductive wf_fs : seqs -> Prop :=
| fs_empty : wf_fs []
| fs_arr : forall Q A, lc_sty A -> wf_fs Q -> wf_fs ((qs_arr A) :: Q )
| fs_rcd : forall Q l, wf_fs Q -> wf_fs ((qs_rcd l) :: Q)
| fs_all : forall Q X A,
lc_sty A ->
X `notin` fv_sty_in_sty A ->
not_occur X Q ->
wf_fs Q -> wf_fs ((qs_all X A) :: Q).
*)
(** [qvars_notin s Q] means all type binders of [Q] do not occur in [s] *)
Inductive qvars_notin (s : vars) : seqs -> Prop :=
| qvars_empty : qvars_notin s []
| qvars_arr : forall Q A, qvars_notin s Q -> qvars_notin s ((qs_arr A) :: Q)
| qvars_rcd : forall Q l, qvars_notin s Q -> qvars_notin s ((qs_rcd l) :: Q)
| qvars_all : forall Q X A,
qvars_notin s Q ->
X `notin` s ->
qvars_notin s ((qs_all X A) :: Q).
(** [wf_fs Q]: well-formedness of [Q], ensuring that type bidners appearing later are fresh with respect to previous items *)
Inductive wf_fs : seqs -> Prop :=
| fs_empty : wf_fs []
| fs_arr : forall Q A,
lc_sty A ->
wf_fs Q ->
qvars_notin (fv_sty_in_sty A) Q ->
wf_fs ((qs_arr A) :: Q )
| fs_rcd : forall Q l, wf_fs Q -> wf_fs ((qs_rcd l) :: Q)
| fs_all : forall Q X A,
lc_sty A ->
X `notin` fv_sty_in_sty A ->
qvars_notin (fv_sty_in_sty (sty_var_f X) \u fv_sty_in_sty A) Q ->
wf_fs Q -> wf_fs ((qs_all X A) :: Q).
Hint Constructors qvars_notin wf_fs.
(* ********************************************************************** *)
(** * Freshness *)
Definition fv_qs (B : qs) : vars :=
match B with
| qs_arr A => fv_sty_in_sty A
| qs_rcd l => {}
| qs_all X A => singleton X `union` fv_sty_in_sty A
end.
Definition seqs_vars (fs : seqs) : vars :=
fold_right (fun qs acc => fv_qs qs \u acc) empty fs.
Ltac gather_atoms ::=
let A := gather_atoms_with (fun x : vars => x) in
let B := gather_atoms_with (fun x : var => {{ x }}) in
let C1 := gather_atoms_with (fun x : ctx => dom x) in
let C2 := gather_atoms_with (fun x : tctx => dom x) in
let C3 := gather_atoms_with (fun x : stctx => dom x) in
let C4 := gather_atoms_with (fun x : sctx => dom x) in
let D1 := gather_atoms_with (fun x => fv_ty_in_ty x) in
let D2 := gather_atoms_with (fun x => fv_ty_in_exp x) in
let D3 := gather_atoms_with (fun x => fv_exp_in_exp x) in
let D4 := gather_atoms_with (fun x => fv_sty_in_sty x) in
let D5 := gather_atoms_with (fun x => fv_sty_in_sexp x) in
let D6 := gather_atoms_with (fun x => fv_sexp_in_sexp x) in
let D7 := gather_atoms_with (fun x => seqs_vars x) in
constr:(A \u B \u C1 \u C2 \u C3 \u C4 \u D1 \u D2 \u D3 \u D4 \u D5 \u D6 \u D7).
(* ********************************************************************** *)
(** * Two meta-functions of coercions *)
Fixpoint calTop (Q : seqs) : co :=
match Q with
| nil => co_top
| cons l fs' =>
match l with
| qs_arr _ => co_trans (co_arr co_top (calTop fs')) co_topArr
| qs_rcd l => co_trans (calTop fs') co_id
| qs_all _ _ => co_trans (co_forall (calTop fs')) co_topAll
end
end.
Fixpoint calAnd (Q : seqs) : co :=
match Q with
| nil => co_id
| cons l fs' =>
match l with
| qs_arr _ => co_trans (co_arr co_id (calAnd fs')) co_distArr
| qs_rcd l => co_trans (calAnd fs') (co_id)
| qs_all _ _ => co_trans (co_forall (calAnd fs')) co_distPoly
end
end.
(* ********************************************************************** *)
(** * Algorithmic subtyping *)
Inductive asub : sty -> seqs -> sty -> co -> Prop :=
| A_nat :
asub sty_nat nil sty_nat co_id
| A_var : forall (X:typvar),
asub (sty_var_f X) nil (sty_var_f X) co_id
| A_top : forall (A:sty) (Q:seqs),
lc_sty A ->
wf_fs Q ->
asub A Q sty_top (co_trans (calTop Q ) co_top)
| A_bot : forall (A:sty) (Q:seqs),
lc_sty A ->
wf_fs Q ->
asub sty_bot Q A co_bot
| A_and : forall (A:sty) (Q:seqs) (B1 B2:sty) (c1 c2:co),
asub A Q B1 c1 ->
asub A Q B2 c2 ->
asub A Q (sty_and B1 B2) (co_trans (calAnd Q ) (co_pair c1 c2))
| A_rcdNat : forall (l:nat) (A:sty) (Q:seqs) (c:co),
asub A Q sty_nat c ->
asub (sty_rcd l A) (cons (qs_rcd l) Q ) sty_nat c
| A_rcdBot : forall (l:nat) (A:sty) (Q:seqs) (c:co),
asub A Q sty_bot c ->
asub (sty_rcd l A) (cons (qs_rcd l) Q ) sty_bot c
| A_rcdVar : forall (l:nat) (A:sty) (Q:seqs) (X:typvar) (c:co),
asub A Q (sty_var_f X) c ->
asub (sty_rcd l A) (cons (qs_rcd l) Q ) (sty_var_f X) c
| A_rcd : forall (A:sty) (Q:seqs) (l:nat) (B:sty) (c:co),
asub A ( Q ++ [(qs_rcd l)]) B c ->
asub A Q (sty_rcd l B) c
| A_arr : forall (A:sty) (Q:seqs) (B1 B2:sty) (c:co),
asub A (Q ++ [(qs_arr B1)]) B2 c ->
asub A Q (sty_arrow B1 B2) c
| A_forall : forall (L:vars) (A:sty) (Q:seqs) (B1 B2:sty) (c:co),
(forall X, X \notin L ->
asub A (Q ++ [(qs_all X B1)]) (open_sty_wrt_sty B2 (sty_var_f X)) c) ->
asub A Q (sty_all B1 B2) c
| A_andNat1 : forall (A1 A2:sty) (Q:seqs) (c:co),
lc_sty A2 ->
asub A1 Q sty_nat c ->
asub (sty_and A1 A2) Q sty_nat (co_trans c co_proj1)
| A_andNat2 : forall (A1 A2:sty) (Q:seqs) (c:co),
lc_sty A1 ->
asub A2 Q sty_nat c ->
asub (sty_and A1 A2) Q sty_nat (co_trans c co_proj2)
| A_andBot1 : forall (A1 A2:sty) (Q:seqs) (c:co),
lc_sty A2 ->
asub A1 Q sty_bot c ->
asub (sty_and A1 A2) Q sty_bot (co_trans c co_proj1)
| A_andBot2 : forall (A1 A2:sty) (Q:seqs) (c:co),
lc_sty A1 ->
asub A2 Q sty_bot c ->
asub (sty_and A1 A2) Q sty_bot (co_trans c co_proj2)
| A_andVar1 : forall (A1 A2:sty) (Q:seqs) (X:typvar) (c:co),
lc_sty A2 ->
asub A1 Q (sty_var_f X) c ->
asub (sty_and A1 A2) Q (sty_var_f X) (co_trans c co_proj1)
| A_andVar2 : forall (A1 A2:sty) (Q:seqs) (X:typvar) (c:co),
lc_sty A1 ->
asub A2 Q (sty_var_f X) c ->
asub (sty_and A1 A2) Q (sty_var_f X) (co_trans c co_proj2)
| A_arrNat : forall (A1 A2 A:sty) (Q:seqs) (c1 c2:co),
qvars_notin (fv_sty_in_sty A) Q ->
asub A nil A1 c1 ->
asub A2 Q sty_nat c2 ->
asub (sty_arrow A1 A2) (cons (qs_arr A) Q) sty_nat (co_arr c1 c2)
| A_arrBot : forall (A1 A2 A:sty) (Q:seqs) (c1 c2:co),
qvars_notin (fv_sty_in_sty A) Q ->
asub A nil A1 c1 ->
asub A2 Q sty_bot c2 ->
asub (sty_arrow A1 A2) (cons (qs_arr A) Q) sty_bot (co_arr c1 c2)
| A_arrVar : forall (A1 A2 A:sty) (Q:seqs) (X:typvar) (c1 c2:co),
qvars_notin (fv_sty_in_sty A) Q ->
asub A nil A1 c1 ->
asub A2 Q (sty_var_f X) c2 ->
asub (sty_arrow A1 A2) (cons (qs_arr A) Q) (sty_var_f X) (co_arr c1 c2)
| A_allNat : forall (L:vars) (A1 A2 A:sty) (Q:seqs) (c c':co) (X : typvar),
X `notin` fv_sty_in_sty A ->
X `notin` fv_sty_in_sty A1 ->
X `notin` fv_sty_in_sty A2 ->
qvars_notin (fv_sty_in_sty A \u fv_sty_in_sty (sty_var_f X)) Q ->
asub A nil A1 c' ->
asub (open_sty_wrt_sty A2 (sty_var_f X) ) Q sty_nat c ->
asub (sty_all A1 A2) (cons (qs_all X A) Q) sty_nat (co_forall c)
| A_allBot : forall (L:vars) (A1 A2 A:sty) (Q:seqs) (c c':co) (X : typvar),
X `notin` fv_sty_in_sty A ->
X `notin` fv_sty_in_sty A1 ->
X `notin` fv_sty_in_sty A2 ->
qvars_notin (fv_sty_in_sty A \u fv_sty_in_sty (sty_var_f X)) Q ->
asub A nil A1 c' ->
asub (open_sty_wrt_sty A2 (sty_var_f X) ) Q sty_bot c ->
asub (sty_all A1 A2) (cons (qs_all X A) Q) sty_bot (co_forall c)
| A_allVar : forall (L:vars) (A1 A2 A:sty) (Q:seqs) (Y:typvar) (c c':co) (X : typvar),
X `notin` fv_sty_in_sty A ->
X `notin` fv_sty_in_sty A1 ->
X `notin` fv_sty_in_sty A2 ->
qvars_notin (fv_sty_in_sty A \u fv_sty_in_sty (sty_var_f X)) Q ->
asub A nil A1 c' ->
asub (open_sty_wrt_sty A2 (sty_var_f X) ) Q (sty_var_f Y) c ->
asub (sty_all A1 A2) (cons (qs_all X A) Q) (sty_var_f Y) (co_forall c).
Hint Constructors asub.