{-# OPTIONS --safe --cubical #-}

module Spartan6.Foundation.Memory where

open import Spartan6.Prelude

Memory : ℕ → ℕ → Type₀
Memory depth width = Vec (Word width) depth

read : ∀ {depth width} → Fin depth → Memory depth width → Word width
read = lookup

write : ∀ {depth width}
      → Fin depth → Word width → Memory depth width → Memory depth width
write fzero value (current ∷ memory) = value ∷ memory
write (fsuc address) value (current ∷ memory) =
  current ∷ write address value memory

writeIf : ∀ {depth width}
        → Bit → Fin depth → Word width → Memory depth width
        → Memory depth width
writeIf false address value memory = memory
writeIf true address value memory = write address value memory

read-after-write-same : ∀ {depth width}
  (address : Fin depth) (value : Word width) (memory : Memory depth width)
  → read address (write address value memory) ≡ value
read-after-write-same fzero value (current ∷ memory) = refl
read-after-write-same (fsuc address) value (current ∷ memory) =
  read-after-write-same address value memory

writeIf-low : ∀ {depth width}
  (address : Fin depth) (value : Word width) (memory : Memory depth width)
  → writeIf low address value memory ≡ memory
writeIf-low address value memory = refl

writeIf-high : ∀ {depth width}
  (address : Fin depth) (value : Word width) (memory : Memory depth width)
  → writeIf high address value memory ≡ write address value memory
writeIf-high address value memory = refl