1 theory Abacus

     2 imports Main

     3 begin 

     4 

     5 datatype abc_inst =

     6      Inc nat

     7    | Dec nat nat

     8    | Goto nat

     9   

    10 type_synonym abc_prog = "abc_inst list"

    11 

    12 type_synonym abc_state = nat

    13 

    14 text {*

    15   The memory of Abacus machine is defined as a list of contents, with 

    16   every units addressed by index into the list.

    17   *}

    18 type_synonym abc_lm = "nat list"

    19 

    20 text {*

    21   Fetching contents out of memory. Units not represented by list elements are considered

    22   as having content @{text "0"}.

    23 *}

    24 fun abc_lm_v :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat"

    25   where 

    26     "abc_lm_v lm n = (if n < length lm then lm ! n else 0)"         

    27 

    28 

    29 text {*

    30   Set the content of memory unit @{text "n"} to value @{text "v"}.

    31   @{text "am"} is the Abacus memory before setting.

    32   If address @{text "n"} is outside to scope of @{text "am"}, @{text "am"} 

    33   is extended so that @{text "n"} becomes in scope.

    34 *}

    35 

    36 fun abc_lm_s :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_lm"

    37   where

    38     "abc_lm_s am n v = (if n < length am then am[n := v] else 

    39                            am @ (replicate (n - length am) 0) @ [v])"

    40 

    41 

    42 text {*

    43   The configuration of Abaucs machines consists of its current state and its

    44   current memory:

    45 *}

    46 

    47 type_synonym abc_conf = "abc_state \<times> abc_lm"

    48 

    49 text {*

    50   Fetch instruction out of Abacus program:

    51 *}

    52 

    53 fun abc_fetch :: "nat \<Rightarrow> abc_prog \<Rightarrow> abc_inst option" 

    54   where

    55   "abc_fetch s p = (if s < length p then Some (p ! s) else None)"

    56 

    57 text {*

    58   Single step execution of Abacus machine. If no instruction is feteched, 

    59   configuration does not change.

    60 *}

    61 

    62 fun abc_step_l :: "abc_conf \<Rightarrow> abc_inst option \<Rightarrow> abc_conf"

    63   where

    64   "abc_step_l (s, lm) a = (case a of 

    65                None \<Rightarrow> (s, lm) |

    66                Some (Inc n)  \<Rightarrow> (let nv = abc_lm_v lm n in

    67                        (s + 1, abc_lm_s lm n (nv + 1))) |

    68                Some (Dec n e) \<Rightarrow> (let nv = abc_lm_v lm n in

    69                        if (nv = 0) then (e, abc_lm_s lm n 0) 

    70                        else (s + 1,  abc_lm_s lm n (nv - 1))) |

    71                Some (Goto n) \<Rightarrow> (n, lm) 

    72                )"

    73 

    74 text {*

    75   Multi-step execution of Abacus machine.

    76 *}

    77 fun abc_steps_l :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> nat \<Rightarrow> abc_conf"

    78   where

    79   "abc_steps_l (s, lm) p 0 = (s, lm)" |

    80   "abc_steps_l (s, lm) p (Suc n) = 

    81       abc_steps_l (abc_step_l (s, lm) (abc_fetch s p)) p n"

    82 

    83 fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"

    84   where

    85   "abc_inst_shift (Inc m) n = Inc m" |

    86   "abc_inst_shift (Dec m e) n = Dec m (e + n)" |

    87   "abc_inst_shift (Goto m) n = Goto (m + n)"

    88 

    89 fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" 

    90   where

    91   "abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs" 

    92 

    93 fun abc_comp :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> abc_inst list" (infixl ";" 99)

    94   where

    95   "al; bl = (let al_len = length al in al @ abc_shift bl al_len)"

    96 

    97 

    98 end