module Heap where

open import GeneralLemmas hiding (lookup)

infix 8 _▸_
infix 7 _⊆_
infix 10 _!_

abstract
  -- | Definition
  Heap : Set  Set
  Ptr  : Set
      : {A : Set}  Heap A

  -- | Internally, this uses lists (but it is not visible from the outside)
  Heap = List
  Ptr = 
   = []

  -- | Dereferencing and allocation
  _!_ : {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

-- | Subheap preorder
_⊆_      : {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