deepDeref.agda

{-# OPTIONS --overlapping-instances #-}

module Pointer where

open import Prelude

-- Allowes retrieving data by valid pointer
data Heap : Set
private variable h : Heap

-- A value on a heap ≡ a valid pointer
data Value : Set
private variable
  v : Value
  w : Value
  u : Value

-- Proof that value v exists in heap h
data InHeap (v : Value) : (h : Heap) → Set

-- References v h ≡ proof that value v references only values in h
data References : Value → Heap → Set

data Heap where
  HNil : Heap
  HCons : (h : Heap) (v : Value) → ⦃ References v h ⦄ → Heap

data Value where
  -- Plain number
  VNat : Nat → Value
  -- A pair of values
  VCons : Value → Value
        → Value

data InHeap v where
  instance
    HHere : ⦃ xᵣ : References v h ⦄ → InHeap v (HCons h v)
    HThere : ⦃ xₕ : InHeap v h ⦄ → ⦃ yᵣ : References w h ⦄ → InHeap v (HCons h w)

data References where
  instance
    RNat : ∀ {n} → References (VNat n) h
    RCons : {yᵥ : Value} → ⦃ yₕ : InHeap yᵥ h ⦄
          → {zᵥ : Value} → ⦃ zₕ : InHeap zᵥ h ⦄
          → References (VCons yᵥ zᵥ) h

weaken-ref : References v h → ⦃ yᵣ : References w h ⦄ → References v (HCons h w)
weaken-ref RNat = RNat
weaken-ref RCons = RCons

inHeap⇒ref : InHeap v h → References v h
inHeap⇒ref (HHere ⦃ xᵣ ⦄) = weaken-ref xᵣ
inHeap⇒ref (HThere ⦃ xₕ ⦄ ⦃ yᵣ ⦄) = weaken-ref (inHeap⇒ref xₕ)

-- 𝕧 : FlatValue v is "unfolded" heap value v
data FlatValue : Value → Set where
  FNat : (n : Nat) → FlatValue (VNat n)
  FCons : {w : Value} → (𝕨 : FlatValue w)
        → {u : Value} → (𝕦 : FlatValue u)
        → FlatValue (VCons w u)

deepDeref : (h : Heap) (v : Value) → ⦃ r : References v h ⦄ → FlatValue v
deepDeref h (VNat n) = FNat n
deepDeref h (VCons yᵥ zᵥ) ⦃ r = RCons ⦃ yₕ = yₕ ⦄ ⦃ zₕ = zₕ ⦄ ⦄ = FCons (deepDeref h yᵥ ⦃ inHeap⇒ref yₕ ⦄) (deepDeref h zᵥ ⦃ inHeap⇒ref zₕ ⦄)

-- Erased version of FlatValue
data FlatValue' : Set where
  FNat' : (n : Nat) → FlatValue'
  FCons' : (𝕨 : FlatValue')
        → (𝕦 : FlatValue')
        → FlatValue'

erase : FlatValue v → FlatValue'
erase (FNat n) = FNat' n
erase (FCons 𝕨 𝕦) = FCons' (erase 𝕨) (erase 𝕦)

put : (h : Heap) (v : Value) → ⦃ r : References v h ⦄ → Σ Heap (InHeap v)
put h v ⦃ r ⦄ = HCons h v , HHere

ex : FlatValue'
ex = let h = HNil
         a = VNat 1
         h , _ = put h a
         b = VNat 2
         h , _ = put h b
         c = VCons a b
         h , _ = put h c
      in erase (deepDeref h c)