theory Translation2imports Abacus Recsbeginfun 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