--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Abacus.thy Thu Jun 06 17:27:45 2013 +0100
@@ -0,0 +1,98 @@
+theory Abacus
+imports Main
+begin
+
+datatype abc_inst =
+ Inc nat
+ | Dec nat nat
+ | Goto nat
+
+type_synonym abc_prog = "abc_inst list"
+
+type_synonym abc_state = nat
+
+text {*
+ The memory of Abacus machine is defined as a list of contents, with
+ every units addressed by index into the list.
+ *}
+type_synonym abc_lm = "nat list"
+
+text {*
+ Fetching contents out of memory. Units not represented by list elements are considered
+ as having content @{text "0"}.
+*}
+fun abc_lm_v :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat"
+ where
+ "abc_lm_v lm n = (if n < length lm then lm ! n else 0)"
+
+
+text {*
+ Set the content of memory unit @{text "n"} to value @{text "v"}.
+ @{text "am"} is the Abacus memory before setting.
+ If address @{text "n"} is outside to scope of @{text "am"}, @{text "am"}
+ is extended so that @{text "n"} becomes in scope.
+*}
+
+fun abc_lm_s :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_lm"
+ where
+ "abc_lm_s am n v = (if n < length am then am[n := v] else
+ am @ (replicate (n - length am) 0) @ [v])"
+
+
+text {*
+ The configuration of Abaucs machines consists of its current state and its
+ current memory:
+*}
+
+type_synonym abc_conf = "abc_state \<times> abc_lm"
+
+text {*
+ Fetch instruction out of Abacus program:
+*}
+
+fun abc_fetch :: "nat \<Rightarrow> abc_prog \<Rightarrow> abc_inst option"
+ where
+ "abc_fetch s p = (if s < length p then Some (p ! s) else None)"
+
+text {*
+ Single step execution of Abacus machine. If no instruction is feteched,
+ configuration does not change.
+*}
+
+fun abc_step_l :: "abc_conf \<Rightarrow> abc_inst option \<Rightarrow> abc_conf"
+ where
+ "abc_step_l (s, lm) a = (case a of
+ None \<Rightarrow> (s, lm) |
+ Some (Inc n) \<Rightarrow> (let nv = abc_lm_v lm n in
+ (s + 1, abc_lm_s lm n (nv + 1))) |
+ Some (Dec n e) \<Rightarrow> (let nv = abc_lm_v lm n in
+ if (nv = 0) then (e, abc_lm_s lm n 0)
+ else (s + 1, abc_lm_s lm n (nv - 1))) |
+ Some (Goto n) \<Rightarrow> (n, lm)
+ )"
+
+text {*
+ Multi-step execution of Abacus machine.
+*}
+fun abc_steps_l :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> nat \<Rightarrow> abc_conf"
+ where
+ "abc_steps_l (s, lm) p 0 = (s, lm)" |
+ "abc_steps_l (s, lm) p (Suc n) =
+ abc_steps_l (abc_step_l (s, lm) (abc_fetch s p)) p n"
+
+fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"
+ where
+ "abc_inst_shift (Inc m) n = Inc m" |
+ "abc_inst_shift (Dec m e) n = Dec m (e + n)" |
+ "abc_inst_shift (Goto m) n = Goto (m + n)"
+
+fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list"
+ where
+ "abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs"
+
+fun abc_comp :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> abc_inst list" (infixl ";" 99)
+ where
+ "al; bl = (let al_len = length al in al @ abc_shift bl al_len)"
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Translation2.thy Thu Jun 06 17:27:45 2013 +0100
@@ -0,0 +1,71 @@
+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