1 CodeGenIf = List + |
|
2 types 'v binop = 'v => 'v => 'v |
|
3 'v test = 'v => bool |
|
4 datatype ('a,'v) expr = Vex 'a |
|
5 | Cex 'v |
|
6 | Bex ('v binop) (('a,'v) expr) (('a,'v) expr) |
|
7 | Ifex ('v test) (('a,'v)expr) (('a,'v)expr) (('a,'v)expr) |
|
8 consts value :: ('a => 'v) => ('a,'v)expr => 'v |
|
9 primrec value expr |
|
10 "value env (Vex a) = env a" |
|
11 "value env (Cex v) = v" |
|
12 "value env (Bex f e1 e2) = f (value env e1) (value env e2)" |
|
13 "value env (Ifex t b e1 e2) = |
|
14 (if t(value env b) then value env e1 else value env e2)" |
|
15 datatype ('a,'v) instr = Load 'a |
|
16 | Const 'v |
|
17 | Apply ('v binop) |
|
18 | Jump nat |
|
19 | Test ('v test) nat |
|
20 consts exec :: "('a => 'v) * 'v list * (('a,'v) instr) list => 'v list" |
|
21 recdef exec "measure(%(s,vs,is).length is)" |
|
22 simpset "simpset() addsimps [diff_less_Suc]" |
|
23 "exec(s, vs, []) = vs" |
|
24 "exec(s, vs, i#is) = (case i of |
|
25 Load a => exec(s,(s a)#vs,is) |
|
26 | Const v => exec(s,v#vs,is) |
|
27 | Apply f => exec(s, (f (hd vs) (hd(tl vs)))#(tl(tl vs)), is) |
|
28 | Jump n => exec(s, vs, drop n is) |
|
29 | Test t n => (if t(hd vs) then exec(s,tl vs, drop n is) |
|
30 else exec(s,tl vs, is)))" |
|
31 consts comp :: ('a,'v) expr => (('a,'v) instr) list |
|
32 primrec comp expr |
|
33 "comp (Vex a) = [Load a]" |
|
34 "comp (Cex v) = [Const v]" |
|
35 "comp (Bex f e1 e2) = (comp e2)@(comp e1)@[Apply f]" |
|
36 "comp (Ifex t b e1 e2) = (let is1 = comp e1; is2 = comp e2 |
|
37 in comp b @ [Test t (Suc(length is2))] @ |
|
38 is2 @ [Jump (length is1)] @ is1)" |
|
39 |
|
40 consts wf :: ('a,'v)instr list => bool |
|
41 primrec wf list |
|
42 "wf [] = True" |
|
43 "wf (i#is) = (wf is & (case i of Load a => True | Const v => True |
|
44 | Apply f => True | Jump n => n <= length is | Test t n => n <= length is))" |
|
45 |
|
46 end |
|