49 "rec_ci S = ((addition 0 1 2) ; [Inc 1], 3)" | |
49 "rec_ci S = ((addition 0 1 2) ; [Inc 1], 3)" | |
50 "rec_ci (Id m n) = (addition n m (m + 1), m + 2)" | |
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 |
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 |
52 let cied_f = rec_ci f in |
53 let qstr = Max (set (map snd (cied_f # cied_gs))) 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; |
54 (cn_merge_gs cied_gs n qstr; |
55 mv_boxes qstr 0 (length gs) ; fst cied_f; mv_box (arity f) (Suc (qstr + length gs)); |
55 mv_boxes 0 (qstr + length gs) n; |
56 empty_boxes (length gs); mv_boxes (qstr + length gs) 0 (Suc n), Suc (qstr + length gs + n)))" | |
56 mv_boxes qstr 0 (length gs) ; |
|
57 fst cied_f; |
|
58 mv_box (arity f) (Suc (qstr + length gs)); |
|
59 empty_boxes (length gs); |
|
60 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 |
61 "rec_ci (Pr n f g) = (let (fa, fp) = rec_ci f in |
58 let (ga, gp) = rec_ci g in |
62 let (ga, gp) = rec_ci g in |
59 let qstr = max fp gp in |
63 let qstr = max fp gp in |
60 let e = length ga + 7 in |
64 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; |
65 (mv_box 0 qstr; |
62 mv_box (Suc qstr) 1; (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @ |
66 mv_boxes 1 0 n; |
63 [Dec (Suc (Suc n)) 0, Inc 1, Goto (length ga + 4)]), Suc qstr))" | |
67 fa; |
|
68 mv_box n (Suc qstr); |
|
69 mv_boxes 0 2 n; |
|
70 mv_box (Suc qstr) 1; |
|
71 (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @ |
|
72 [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 |
73 "rec_ci (Mn n f) = (let (fa, fp) = rec_ci f in |
65 let len = length fa in |
74 let len = length fa in |
66 (mv_boxes 0 (Suc 0) n; (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3), |
75 (mv_boxes 0 (Suc 0) n; |
67 Goto (len + 1), Inc 0, Goto 0]), fp))" |
76 (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3), |
|
77 Goto (len + 1), Inc 0, Goto 0]), fp))" |
68 |
78 |
69 |
79 |
70 |
80 |
71 end |
81 end |