diff -r 28d85e8ff391 -r 002b07ea0a57 thys2/Translation2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Translation2.thy	Thu Jun 06 17:27:45 2013 +0100
@@ -0,0 +1,71 @@
+theory Translation2
+imports Abacus Recs
+begin
+
+fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
+
+fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "mv_box m n = [Dec m 3, Inc n, Goto 0]"
+
+text {* The compilation of @{text "z"}-operator. *}
+
+definition rec_ci_z :: "abc_inst list"
+  where
+  "rec_ci_z = [Goto 1]"
+
+text {* The compilation of @{text "s"}-operator. *}
+
+definition rec_ci_s :: "abc_inst list"
+  where
+  "rec_ci_s = addition 0 1 2 ; [Inc 1]"
+
+fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
+  where
+  "mv_boxes ab bb 0 = []" |
+  "mv_boxes ab bb (Suc n) = mv_boxes ab bb n ; mv_box (ab + n) (bb + n)"
+
+fun empty_boxes :: "nat \<Rightarrow> abc_inst list"
+  where
+  "empty_boxes 0 = []" |
+  "empty_boxes (Suc n) = empty_boxes n ; [Dec n 2, Goto 0]"
+
+fun cn_merge_gs :: "(abc_inst list \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
+  where
+  "cn_merge_gs [] n p = []" |
+  "cn_merge_gs (g # gs) n p = 
+      (let (ga, gp) = g in ga ; mv_box n p ; cn_merge_gs gs n (Suc p))"
+
+
+text {* Returns the abacus program and a number for how much memory 
+  is used.
+*}
+ 
+fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat"
+  where
+  "rec_ci Z = ([Goto 1], 2)" |
+  "rec_ci S = ((addition 0 1 2) ; [Inc 1], 3)" |
+  "rec_ci (Id m n) = (addition n m (m + 1), m + 2)" |
+  "rec_ci (Cn n f gs) = (let cied_gs = map (\<lambda> g. rec_ci g) gs in
+                       let cied_f = rec_ci f in 
+                       let qstr = Max (set (map snd (cied_f # cied_gs))) in 
+                       (cn_merge_gs cied_gs n qstr; mv_boxes 0 (qstr + length gs) n; 
+                         mv_boxes qstr 0 (length gs) ; fst cied_f; mv_box (arity f) (Suc (qstr + length gs)); 
+                         empty_boxes (length gs); mv_boxes (qstr + length gs) 0 (Suc n),  Suc (qstr + length gs + n)))" |
+  "rec_ci (Pr n f g) = (let (fa, fp) = rec_ci f in 
+                         let (ga, gp) = rec_ci g in 
+                         let qstr = max fp gp in 
+                         let e = length ga + 7 in 
+                         (mv_box 0 qstr; mv_boxes 1 0 n; fa; mv_box n (Suc qstr); mv_boxes 0 2 n;
+                          mv_box (Suc qstr) 1; (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @ 
+                          [Dec (Suc (Suc n)) 0, Inc 1, Goto (length ga + 4)]), Suc qstr))" |
+  "rec_ci (Mn n f) = (let (fa, fp) = rec_ci f in
+                      let len = length fa in  
+                      (mv_boxes 0 (Suc 0) n; (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
+                       Goto (len + 1), Inc 0, Goto 0]), fp))"
+
+
+
+end