open import Data.Nat

module RegisterMachine (n : ℕ) where

----------------------------------------------------------------------
-- Representation of a register machine
--
open import Data.Fin hiding (_+_; _≤_)
open import Relation.Nullary

-- Values
Val : Set
Val = Fin 256

0V : Val
0V = zero

255V : Val
255V = fromℕ 255

+1 : Val → Val
+1 x with toℕ x ≤? 254
... | yes x≤254 = let x<255 = s≤s x≤254 in suc (fromℕ≤ x<255)
... | no _ = 0V

-1 : Val → Val
-1 zero = 255V
-1 (suc x) = inject₁ x

-- Register addresses
Reg : Set
Reg = Fin n

-- Memory
Mem : Set
Mem = Reg → Val

----------------------------------------------------------------------
-- A RM program is a list of instructions
--
open import Data.List

mutual
  data Inst : Set where
    inc : (x : Reg) → Inst
    dec : (x : Reg) → Inst
    loop : (x : Reg) → (is : Prog) → Inst

  Prog : Set
  Prog = List (Inst)

-- Number of instructions
mutual
  size : Inst → ℕ
  size (inc x) = 1
  size (dec x) = 1
  size (loop x p) = suc (size∗ p)

  size∗ : Prog → ℕ
  size∗ [] = 0
  size∗ (i ∷ is) = size i + size∗ is

-- Loop depth
mutual
  depth : Inst → ℕ
  depth (inc x) = 0
  depth (dec x) = 0
  depth (loop x p) = suc (depth∗ p)

  depth∗ : Prog → ℕ
  depth∗ [] = 1
  depth∗ (i ∷ is) = (depth i) ⊔ (depth∗ is)