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