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)