Memory.idr

data SignedNat : Bool -> Nat -> Type where
  Neg : (n:Nat) -> SignedNat True n
  Pos : (n:Nat) -> SignedNat False n

data Memory : sna -> mem -> Type where
  MWord : sna -> mem -> Memory sna mem
  MEnd : sna -> Memory sna Void

data MemoryAddress : Nat -> Type where
  MAddr : (n:Nat) -> MemoryAddress n

createSignedNat : (b:Bool) -> (m:Nat) -> SignedNat b m
createSignedNat False v = Pos v
createSignedNat True v = Neg v

interface TypeOfReadSign maddr mem where
  typeOfReadSign : maddr -> mem -> Bool

implementation TypeOfReadSign maddr Void where
  typeOfReadSign _ _ = False

implementation TypeOfReadSign (MemoryAddress Z) (Memory (SignedNat s v) rest) where
  typeOfReadSign _ (MEnd (Pos _)) = False
  typeOfReadSign _ (MEnd (Neg _)) = True
  typeOfReadSign _ (MWord (Pos _) _) = False
  typeOfReadSign _ (MWord (Neg _) _) = True

implementation TypeOfReadSign (MemoryAddress (S n)) (Memory sn Void) where
  typeOfReadSign _ _ = False

implementation (TypeOfReadSign (MemoryAddress n) rest) => TypeOfReadSign (MemoryAddress (S n)) (Memory sn rest) where
  typeOfReadSign (MAddr (S n)) (MEnd _) = False
  typeOfReadSign (MAddr (S n)) (MWord _ rest) = typeOfReadSign (MAddr n) rest

interface TypeOfReadMag maddr mem where
  typeOfReadMag : maddr -> mem -> Nat

implementation TypeOfReadMag maddr Void where
  typeOfReadMag _ _ = 0

implementation TypeOfReadMag (MemoryAddress Z) (Memory (SignedNat s v) rest) where
  typeOfReadMag _ (MEnd (Pos mag)) = mag
  typeOfReadMag _ (MEnd (Neg mag)) = mag
  typeOfReadMag _ (MWord (Pos mag) _) = mag
  typeOfReadMag _ (MWord (Neg mag) _) = mag

implementation (TypeOfReadMag (MemoryAddress n) rest) => TypeOfReadMag (MemoryAddress (S n)) (Memory (SignedNat s v) rest) where
  typeOfReadMag (MAddr (S n)) (MEnd _) = 0
  typeOfReadMag (MAddr (S n)) (MWord _ rest) = typeOfReadMag (MAddr n) rest

readRam : (TypeOfReadSign maddr mem, TypeOfReadMag maddr mem) => (a : maddr) -> (m : mem) -> (SignedNat (typeOfReadSign a m) (typeOfReadMag a m))
readRam maddr mem = createSignedNat (typeOfReadSign maddr mem) (typeOfReadMag maddr mem)

ram : Memory (SignedNat False 3) (Memory (SignedNat False 4) (Memory (SignedNat False 5) Void))
ram = MWord (Pos 3) (MWord (Pos 4) (MEnd (Pos 5)))

proofWord1IsPos4 : readRam (MAddr 1) (MWord (Pos 3) (MWord (Pos 4) (MEnd (Pos 5)))) = Pos 4
proofWord1IsPos4 = Refl