1 theory Translation2

     2 imports Abacus Recs

     3 begin

     4 

     5 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

     6   where

     7   "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"

     8 

     9 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    10   where

    11   "mv_box m n = [Dec m 3, Inc n, Goto 0]"

    12 

    13 text {* The compilation of @{text "z"}-operator. *}

    14 

    15 definition rec_ci_z :: "abc_inst list"

    16   where

    17   "rec_ci_z = [Goto 1]"

    18 

    19 text {* The compilation of @{text "s"}-operator. *}

    20 

    21 definition rec_ci_s :: "abc_inst list"

    22   where

    23   "rec_ci_s = addition 0 1 2 ; [Inc 1]"

    24 

    25 fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"

    26   where

    27   "mv_boxes ab bb 0 = []" |

    28   "mv_boxes ab bb (Suc n) = mv_boxes ab bb n ; mv_box (ab + n) (bb + n)"

    29 

    30 fun empty_boxes :: "nat \<Rightarrow> abc_inst list"

    31   where

    32   "empty_boxes 0 = []" |

    33   "empty_boxes (Suc n) = empty_boxes n ; [Dec n 2, Goto 0]"

    34 

    35 fun cn_merge_gs :: "(abc_inst list \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"

    36   where

    37   "cn_merge_gs [] n p = []" |

    38   "cn_merge_gs (g # gs) n p = 

    39       (let (ga, gp) = g in ga ; mv_box n p ; cn_merge_gs gs n (Suc p))"

    40 

    41 

    42 text {* Returns the abacus program and a number for how much memory 

    43   is used.

    44 *}

    45  

    46 fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat"

    47   where

    48   "rec_ci Z = ([Goto 1], 2)" |

    49   "rec_ci S = ((addition 0 1 2) ; [Inc 1], 3)" |

    50   "rec_ci (Id m n) = (addition n m (m + 1), m + 2)" |

    51   "rec_ci (Cn n f gs) = (let cied_gs = map (\<lambda> g. rec_ci g) gs in

    52                        let cied_f = rec_ci f in 

    53                        let qstr = Max (set (map snd (cied_f # cied_gs))) in 

    54                        (cn_merge_gs cied_gs n qstr; mv_boxes 0 (qstr + length gs) n; 

    55                          mv_boxes qstr 0 (length gs) ; fst cied_f; mv_box (arity f) (Suc (qstr + length gs)); 

    56                          empty_boxes (length gs); mv_boxes (qstr + length gs) 0 (Suc n),  Suc (qstr + length gs + n)))" |

    57   "rec_ci (Pr n f g) = (let (fa, fp) = rec_ci f in 

    58                          let (ga, gp) = rec_ci g in 

    59                          let qstr = max fp gp in 

    60                          let e = length ga + 7 in 

    61                          (mv_box 0 qstr; mv_boxes 1 0 n; fa; mv_box n (Suc qstr); mv_boxes 0 2 n;

    62                           mv_box (Suc qstr) 1; (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @ 

    63                           [Dec (Suc (Suc n)) 0, Inc 1, Goto (length ga + 4)]), Suc qstr))" |

    64   "rec_ci (Mn n f) = (let (fa, fp) = rec_ci f in

    65                       let len = length fa in  

    66                       (mv_boxes 0 (Suc 0) n; (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),

    67                        Goto (len + 1), Inc 0, Goto 0]), fp))"

    68 

    69 

    70 

    71 end