module Heap where
open import GeneralLemmas hiding (lookup)
infix 8 _▸_
infix 7 _⊆_
infix 10 _!_
abstract
Heap : Set → Set
Ptr : Set
∅ : {A : Set} → Heap A
Heap = List
Ptr = ℕ
∅ = []
_!_ : {A : Set} → Heap A → Ptr → Maybe A
_▸_ : {A : Set} → Heap A → A → Heap A × Ptr
[] ! n = nothing
(x ∷ h) ! zero = just x
(x ∷ h) ! suc ptr = h ! ptr
h ▸ a = (h ++ a ∷ [] , length h)
!-▸ : {A : Set}(h : Heap A)(x : A) →
let (h' , ptr) = h ▸ x in h' ! ptr ≡ just x
!-▸ [] x = refl
!-▸ (_ ∷ h) x = !-▸ h x
_⊆_ : {A : Set} → Heap A → Heap A → Set
h₁ ⊆ h₂ = ∀ ptr {x} → h₁ ! ptr ≡ just x → h₂ ! ptr ≡ just x
⊆-refl : {A : Set}(h : Heap A) → h ⊆ h
⊆-refl h ptr eq = eq
⊆-trans : {A : Set}{h₁ h₂ h₃ : Heap A}
→ h₁ ⊆ h₂ → h₂ ⊆ h₃ → h₁ ⊆ h₃
⊆-trans h₁⊆h₂ h₂⊆h₃ ptr eq = h₂⊆h₃ ptr (h₁⊆h₂ ptr eq)
abstract
h⊆h▸x : {A : Set}(h : Heap A){x : A} → h ⊆ proj₁ (h ▸ x)
h⊆h▸x [] ptr ()
h⊆h▸x (x ∷ h) zero eq = eq
h⊆h▸x (x ∷ h) (suc ptr) eq = h⊆h▸x h ptr eq