author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Wed, 26 Jun 2013 14:42:42 +0100 | |
changeset 270 | ccec33db31d4 |
parent 268 | 002b07ea0a57 |
child 271 | 4457185b22ef |
permissions | -rw-r--r-- |
268
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
theory Translation2 |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
imports Abacus Recs |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
begin |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
where |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
"addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
where |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
"mv_box m n = [Dec m 3, Inc n, Goto 0]" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
text {* The compilation of @{text "z"}-operator. *} |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
definition rec_ci_z :: "abc_inst list" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
where |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
"rec_ci_z = [Goto 1]" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
text {* The compilation of @{text "s"}-operator. *} |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
definition rec_ci_s :: "abc_inst list" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
where |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
"rec_ci_s = addition 0 1 2 ; [Inc 1]" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
where |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
"mv_boxes ab bb 0 = []" | |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
"mv_boxes ab bb (Suc n) = mv_boxes ab bb n ; mv_box (ab + n) (bb + n)" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
fun empty_boxes :: "nat \<Rightarrow> abc_inst list" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
where |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
"empty_boxes 0 = []" | |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
"empty_boxes (Suc n) = empty_boxes n ; [Dec n 2, Goto 0]" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
fun cn_merge_gs :: "(abc_inst list \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
where |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
"cn_merge_gs [] n p = []" | |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
"cn_merge_gs (g # gs) n p = |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
(let (ga, gp) = g in ga ; mv_box n p ; cn_merge_gs gs n (Suc p))" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
text {* Returns the abacus program and a number for how much memory |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
is used. |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
*} |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
where |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
"rec_ci Z = ([Goto 1], 2)" | |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
"rec_ci S = ((addition 0 1 2) ; [Inc 1], 3)" | |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
"rec_ci (Id m n) = (addition n m (m + 1), m + 2)" | |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
"rec_ci (Cn n f gs) = (let cied_gs = map (\<lambda> g. rec_ci g) gs in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
let cied_f = rec_ci f in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
let qstr = Max (set (map snd (cied_f # cied_gs))) in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
(cn_merge_gs cied_gs n qstr; mv_boxes 0 (qstr + length gs) n; |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
mv_boxes qstr 0 (length gs) ; fst cied_f; mv_box (arity f) (Suc (qstr + length gs)); |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
empty_boxes (length gs); mv_boxes (qstr + length gs) 0 (Suc n), Suc (qstr + length gs + n)))" | |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
"rec_ci (Pr n f g) = (let (fa, fp) = rec_ci f in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
let (ga, gp) = rec_ci g in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
let qstr = max fp gp in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
let e = length ga + 7 in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
(mv_box 0 qstr; mv_boxes 1 0 n; fa; mv_box n (Suc qstr); mv_boxes 0 2 n; |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
mv_box (Suc qstr) 1; (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @ |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
[Dec (Suc (Suc n)) 0, Inc 1, Goto (length ga + 4)]), Suc qstr))" | |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
"rec_ci (Mn n f) = (let (fa, fp) = rec_ci f in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
let len = length fa in |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
66 |
(mv_boxes 0 (Suc 0) n; (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3), |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
Goto (len + 1), Inc 0, Goto 0]), fp))" |
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
|
002b07ea0a57
added theorey by Jian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
end |