forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
pan_to_crepScript.sml
330 lines (305 loc) · 10.5 KB
/
pan_to_crepScript.sml
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
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
(*
Compilation from panLang to crepLang.
*)
open preamble pan_commonTheory panLangTheory crepLangTheory
val _ = new_theory "pan_to_crep"
val _ = set_grammar_ancestry ["pan_common", "panLang","crepLang", "backend_common"];
Datatype:
context =
<| vars : panLang$varname |-> shape # num list;
funcs : panLang$funname |-> (panLang$varname # shape) list;
eids : panLang$eid |-> 'a word;
vmax : num|>
End
(* using this style to avoid using HD for code extraction later *)
Definition cexp_heads_def:
(cexp_heads [] = SOME []) /\
(cexp_heads (e::es) =
case (e,cexp_heads es) of
| [], _ => NONE
| _ , NONE => NONE
| x::xs, SOME ys => SOME (x::ys))
End
Definition comp_field_def:
(comp_field i [] es = ([Const 0w], One)) ∧
(comp_field i (sh::shs) es =
if i = (0:num) then (TAKE (size_of_shape sh) es, sh)
else comp_field (i-1) shs (DROP (size_of_shape sh) es))
End
Definition compile_panop_def:
compile_panop panLang$Mul = crepLang$Mul
End
Definition compile_exp_def:
(compile_exp ctxt ((Const c):'a panLang$exp) =
([(Const c): 'a crepLang$exp], One)) /\
(compile_exp ctxt (Var vname) =
case FLOOKUP ctxt.vars vname of
| SOME (shape, ns) => (MAP Var ns, shape)
| NONE => ([Const 0w], One)) /\
(compile_exp ctxt (Label fname) = ([Label fname], One)) /\
(compile_exp ctxt (Struct es) =
let cexps = MAP (compile_exp ctxt) es in
(FLAT (MAP FST cexps), Comb (MAP SND cexps))) /\
(compile_exp ctxt (Field index e) =
let (cexp, shape) = compile_exp ctxt e in
case shape of
| One => ([Const 0w], One)
| Comb shapes => comp_field index shapes cexp) /\
(compile_exp ctxt (Load sh e) =
let (cexp, shape) = compile_exp ctxt e in
case cexp of
| e::es => (load_shape (0w) (size_of_shape sh) e, sh)
| _ => ([Const 0w], One)) /\
(compile_exp ctxt (LoadByte e) =
let (cexp, shape) = compile_exp ctxt e in
case (cexp, shape) of
| (e::es, One) => ([LoadByte e], One)
| (_, _) => ([Const 0w], One)) /\
(* have a check here for the shape *)
(compile_exp ctxt (Op bop es) =
let cexps = MAP FST (MAP (compile_exp ctxt) es) in
case cexp_heads cexps of
| SOME es => ([Op bop es], One)
| _ => ([Const 0w], One)) /\
(compile_exp ctxt (Panop pop es) =
let cexps = MAP FST (MAP (compile_exp ctxt) es) in
case cexp_heads cexps of
| SOME es => ([Crepop (compile_panop pop) es], One)
| _ => ([Const 0w], One)) /\
(compile_exp ctxt (Cmp cmp e e') =
let ce = FST (compile_exp ctxt e);
ce' = FST (compile_exp ctxt e') in
case (ce, ce') of
| (e::es, e'::es') => ([Cmp cmp e e'], One)
| (_, _) => ([Const 0w], One)) /\
(compile_exp ctxt (Shift sh e n) =
case FST (compile_exp ctxt e) of
| [] => ([Const 0w], One)
| e::es => ([Shift sh e n], One)) /\
(compile_exp ctxt BaseAddr = ([BaseAddr], One))
Termination
wf_rel_tac `measure (\e. panLang$exp_size ARB (SND e))` >>
rpt strip_tac >>
imp_res_tac panLangTheory.MEM_IMP_exp_size >>
TRY (first_x_assum (assume_tac o Q.SPEC `ARB`)) >>
decide_tac
End
Definition exp_hdl_def:
exp_hdl fm v =
case FLOOKUP fm v of
| NONE => Skip
| SOME (vshp, ns) => nested_seq
(MAP2 Assign ns (load_globals 0w (LENGTH ns)))
End
Definition ret_var_def:
(ret_var One ns = oHD ns) /\
(ret_var (Comb sh) ns =
if size_of_shape (Comb sh) = 1 then oHD ns
else NONE)
End
Definition ret_hdl_def:
(ret_hdl One ns = Skip) /\
(ret_hdl (Comb sh) ns =
if 1 < size_of_shape (Comb sh) then (assign_ret ns)
else Skip)
End
(* defining it with inner case to enable rewriting later *)
Definition wrap_rt_def:
wrap_rt n =
case n of
| NONE => NONE
| SOME (One, []) => NONE
| m => m
End
Definition compile_def:
(compile _ (Skip:'a panLang$prog) = (Skip:'a crepLang$prog)) /\
(compile ctxt (Dec v e p) =
let (es, sh) = compile_exp ctxt e;
vmax = ctxt.vmax;
nvars = GENLIST (λx. vmax + SUC x) (size_of_shape sh);
nctxt = ctxt with <|vars := ctxt.vars |+ (v, (sh, nvars));
vmax := ctxt.vmax + size_of_shape sh|> in
if size_of_shape sh = LENGTH es
then nested_decs nvars es (compile nctxt p)
else Skip) /\
(compile ctxt (Assign v e) =
let (es, sh) = compile_exp ctxt e in
case FLOOKUP ctxt.vars v of
| SOME (vshp, ns) =>
if LENGTH ns = LENGTH es
then if distinct_lists ns (FLAT (MAP var_cexp es))
then nested_seq (MAP2 Assign ns es)
else let vmax = ctxt.vmax;
temps = GENLIST (λx. vmax + SUC x) (LENGTH ns) in
nested_decs temps es
(nested_seq (MAP2 Assign ns (MAP Var temps)))
else Skip:'a crepLang$prog
| NONE => Skip) /\
(compile ctxt (Store ad v) =
case compile_exp ctxt ad of
| (e::es',sh') =>
let (es,sh) = compile_exp ctxt v;
adv = ctxt.vmax + 1;
temps = GENLIST (λx. adv + SUC x) (size_of_shape sh) in
if size_of_shape sh = LENGTH es
then nested_decs (adv::temps) (e::es)
(nested_seq (stores (Var adv) (MAP Var temps) 0w))
else Skip
| (_,_) => Skip) /\
(compile ctxt (StoreByte dest src) =
case (compile_exp ctxt dest, compile_exp ctxt src) of
| (ad::ads, _), (e::es, _) => StoreByte ad e
| _ => Skip) /\
(compile ctxt (Return rt) =
let (ces,sh) = compile_exp ctxt rt in
if size_of_shape sh = 0 then Return (Const 0w)
else case ces of
| [] => Skip
| e::es => if size_of_shape sh = 1 then (Return e) else
let temps = GENLIST (λx. ctxt.vmax + SUC x) (size_of_shape sh) in
if size_of_shape sh = LENGTH (e::es)
then Seq (nested_decs temps (e::es)
(nested_seq (store_globals 0w (MAP Var temps)))) (Return (Const 0w))
else Skip) /\
(compile ctxt (Raise eid excp) =
case FLOOKUP ctxt.eids eid of
| SOME n =>
let (ces,sh) = compile_exp ctxt excp;
temps = GENLIST (λx. ctxt.vmax + SUC x) (size_of_shape sh) in
if size_of_shape sh = LENGTH ces
then Seq (nested_decs temps ces (nested_seq (store_globals 0w (MAP Var temps))))
(Raise n)
else Skip
| NONE => Skip) /\
(compile ctxt (Seq p p') =
Seq (compile ctxt p) (compile ctxt p')) /\
(compile ctxt (If e p p') =
case compile_exp ctxt e of
| (ce::ces, _) =>
If ce (compile ctxt p) (compile ctxt p')
| _ => Skip) /\
(compile ctxt (While e p) =
case compile_exp ctxt e of
| (ce::ces, _) =>
While ce (compile ctxt p)
| _ => Skip) /\
(compile ctxt Break = Break) /\
(compile ctxt Continue = Continue) /\
(compile ctxt (Call rtyp e es) =
let (cs, sh) = compile_exp ctxt e;
cexps = MAP (compile_exp ctxt) es;
args = FLAT (MAP FST cexps) in
case cs of
| ce::ces =>
(case rtyp of
| NONE => Call NONE ce args
| SOME (rt, hdl) =>
(case wrap_rt (FLOOKUP ctxt.vars rt) of
| NONE =>
(case hdl of
| NONE => Call NONE ce args
| SOME (eid, evar, p) =>
(case FLOOKUP ctxt.eids eid of
| NONE => Call NONE ce args
| SOME neid =>
let comp_hdl = compile ctxt p;
hndlr = Seq (exp_hdl ctxt.vars evar) comp_hdl in
Call (SOME (NONE, Skip, (SOME (neid, hndlr)))) ce args))
| SOME (sh, ns) =>
(case hdl of
| NONE => Call (SOME ((ret_var sh ns), (ret_hdl sh ns), NONE)) ce args
| SOME (eid, evar, p) =>
(case FLOOKUP ctxt.eids eid of
| NONE => Call (SOME ((ret_var sh ns), (ret_hdl sh ns), NONE)) ce args
| SOME neid =>
let comp_hdl = compile ctxt p;
hndlr = Seq (exp_hdl ctxt.vars evar) comp_hdl in
Call (SOME ((ret_var sh ns), (ret_hdl sh ns),
(SOME (neid, hndlr)))) ce args))))
| [] => Skip) /\
(compile ctxt (ExtCall f ptr1 len1 ptr2 len2) =
let
(ptr1',sh1) = compile_exp ctxt ptr1;
(len1',sh2) = compile_exp ctxt len1;
(ptr2',sh3) = compile_exp ctxt ptr2;
(len2',sh4) = compile_exp ctxt len2;
n = FOLDR MAX 0 (FLAT(MAP var_cexp (FLAT [ptr1';len1';ptr2';len2'])))
in
case ((sh1,ptr1'),(sh2,len1'),(sh3,ptr2'),(sh4,len2')) of
| ((One, pc::pcs), (One, lc::lcs),
(One, pc'::pcs'), (One, lc'::lcs')) =>
Dec (n+1) pc
$ Dec (n+2) lc
$ Dec (n+3) pc'
$ Dec (n+4) lc'
$ crepLang$ExtCall f (n+1) (n+2) (n+3) (n+4)
| _ => Skip) /\
(compile ctxt (ShMem op r ad) =
(case compile_exp ctxt ad of
(a::_, _) =>
(case FLOOKUP ctxt.vars r of
SOME (_, r'::_) => ShMem op r' a
| _ => Skip)
| _ => Skip)) ∧
(compile ctxt Tick = Tick)
End
Definition mk_ctxt_def:
mk_ctxt vmap fs m (es:panLang$eid |-> 'a word) =
<|vars := vmap;
funcs := fs;
eids := es;
vmax := m|>
End
(*
Definition shape_vars_def:
(shape_vars [] ns = []) ∧
(shape_vars (sh::shs) ns = (sh, TAKE (size_of_shape sh) ns) ::
shape_vars shs (DROP (size_of_shape sh) ns))
End
*)
(* params : (varname # shape) list *)
Definition make_vmap_def:
make_vmap params =
let pvars = MAP FST params;
shs = MAP SND params;
ns = GENLIST I (size_of_shape (Comb shs));
(* defining in this way to make proof in sync with "with_shape" *)
cvars = ZIP (shs, with_shape shs ns) in
FEMPTY |++ ZIP (pvars, cvars)
End
Definition comp_func_def:
comp_func fs eids params body =
let vmap = make_vmap params;
shapes = MAP SND params;
vmax = size_of_shape (Comb shapes) - 1 in
compile (mk_ctxt vmap fs vmax eids) body
End
Definition get_eids_def:
get_eids prog =
let eids = remove_dup (FLAT (MAP (exp_ids o SND o SND) prog));
ns = GENLIST (λx. n2w x) (LENGTH eids);
es = MAP2 (λx y. (x,y)) eids ns in
alist_to_fmap es
End
Definition make_funcs_def:
make_funcs prog =
let fnames = MAP FST prog;
params = MAP (FST o SND) prog;
fs = MAP2 (λx y. (x,y)) fnames params in
alist_to_fmap fs
End
Definition crep_vars_def:
crep_vars params =
let shapes = MAP SND params;
len = size_of_shape (Comb shapes) in
GENLIST I len
End
Definition compile_prog_def:
compile_prog prog =
let comp = comp_func (make_funcs prog) (get_eids prog) in
MAP (λ(name, params, body).
(name,
crep_vars params,
comp params body)) prog
End
val _ = export_theory();