module memory where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Maybe as Maybe using (Maybe; just; nothing)

open import Word.Base using (Word; ∅; push-low; _○; _●; _◍)

-- An n-bit address space, addressing values of a given type.
memory : ℕ → Set → Set
memory zero A = A
memory (suc n) A = memory n (A × A)

read : {n : ℕ} {A : Set} → memory n A → (Word n → Maybe A)
read ram ∅ = just ram
read ram (w ○) = Maybe.map proj₁ (read ram w)
read ram (w ●) = Maybe.map proj₂ (read ram w)
read ram (w ◍) = nothing

modify : {n : ℕ} {A : Set} → Word n → (A → A) → memory n A → Maybe (memory n A)
modify ∅ f x = just (f x)
modify (w ○) f = modify w (Data.Product.map₁ f)
modify (w ●) f = modify w (Data.Product.map₂ f)
modify (w ◍) f _ = nothing

write : {n : ℕ} {A : Set} → Word n → A → memory n A → Maybe (memory n A)
write w a = modify w (λ _ → a)