(* Title: thys/Abacus.thy

   Author: Jian Xu, Xingyuan Zhang, and Christian Urban

*)

theory Abacus_Defs

imports Abacus

begin

abbreviation

  "layout \<equiv> layout_of"

fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat"

  where

abbreviation

  "TMGoto \<equiv> [(Nop, 1), (Nop, 1)]"

abbreviation 

  "TMInc \<equiv> [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4), 

            (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),

            (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]"

abbreviation

  "TMDec \<equiv> [(W1, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),

             (R, 5), (W0, 4), (R, 6), (W0, 5), (L, 7), (L, 8),

             (L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),

             (R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),

             (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),

             (R, 0), (W0, 16)]"

abbreviation

  "TMFindnth \<equiv> findnth"

fun compile_goto :: "nat \<Rightarrow> instr list" 

  where

  "compile_goto s = shift TMGoto (s - 1)"

fun compile_inc :: "nat \<Rightarrow> nat \<Rightarrow> instr list"

  where

  "compile_inc s n = (shift (TMFindnth n) (s - 1)) @ (shift (shift TMInc (2 * n)) (s - 1))"

fun compile_dec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"

  where

  "compile_dec s n e = (shift (TMFindnth n) (s - 1)) @ (adjust (shift (shift TMDec (2 * n)) (s - 1)) e)"

fun compile :: "abc_prog \<Rightarrow> nat \<Rightarrow> abc_inst \<Rightarrow> instr list"

  where

  "compile ap s (Inc n) = compile_inc s n"

| "compile ap s (Dec n e) = compile_dec s n (address ap e)"

| "compile ap s (Goto e) = compile_goto (address ap e)"

lemma

  "compile ap s i = ci (layout ap) s i"

apply(cases i)

apply(simp add: ci.simps shift.simps start_of.simps tinc_b_def)

apply(simp add: ci.simps shift.simps start_of.simps tdec_b_def)

apply(simp add: ci.simps shift.simps start_of.simps)

done

end