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