\begin{code}
module Scm.Auxiliary-Functions where

open import Scm.Notation
open import Scm.Abstract-Syntax
open import Scm.Domain-Equations

-- Environments ρ : 𝐔 = Ide β†’ 𝐋

postulate _==_ : Ide β†’ Ide β†’ Bool

_[_/_] : 𝐔 β†’ 𝐋 β†’ Ide β†’ 𝐔
ρ [ Ξ± / I ] = Ξ» Iβ€² β†’ Ξ· (I == Iβ€²) ⟢ Ξ± , ρ Iβ€²

postulate unknown : 𝐋
-- ρ I = unknown represents the lack of a binding for I in ρ

postulate initial-env : 𝐔
-- initial-env shoud include various procedures and values

-- Stores Οƒ : 𝐒 = 𝐋 β†’ 𝐄

_[_/_]β€² : 𝐒 β†’ 𝐄 β†’ 𝐋 β†’ 𝐒
Οƒ [ Ο΅ / Ξ± ]β€² = Ξ» Ξ±β€² β†’ (Ξ± ==α΄Έ Ξ±β€²) ⟢ Ο΅ , Οƒ Ξ±β€²

assign : 𝐋 β†’ 𝐄 β†’ 𝐂 β†’ 𝐂
assign = Ξ» Ξ± Ο΅ ΞΈ Οƒ β†’ ΞΈ (Οƒ [ Ο΅ / Ξ± ]β€²)

hold : 𝐋 β†’ (𝐄 β†’ 𝐂) β†’ 𝐂
hold = Ξ» Ξ± ΞΊ Οƒ β†’ ΞΊ (Οƒ Ξ±) Οƒ

postulate new : (𝐋 β†’ 𝐂) β†’ 𝐂
-- new ΞΊ Οƒ = ΞΊ Ξ± Οƒβ€² where Οƒ Ξ± = unallocated, Οƒβ€² Ξ± β‰  unallocated

alloc : 𝐄 β†’ (𝐋 β†’ 𝐂) β†’ 𝐂
alloc = Ξ» Ο΅ ΞΊ β†’ new (Ξ» Ξ± β†’ assign Ξ± Ο΅ (ΞΊ Ξ±))
-- should be βŠ₯ when Ο΅ |-𝐌 == unallocated

initial-store : 𝐒
initial-store = Ξ» Ξ± β†’ Ξ· unallocated 𝐌-in-𝐄

postulate finished : 𝐂
-- normal termination with answer depending on final store

truish : 𝐄 β†’ 𝐓
truish =
  Ξ» Ο΅ β†’ (Ο΅ ∈-𝐓) ⟢
      (((Ο΅ |-𝐓) ==α΅€ Ξ· false) ⟢ Ξ· false , Ξ· true) ,
    Ξ· true
\end{code}
\clearpage
\begin{code}
-- Lists

cons : 𝐅
cons =
  Ξ» ϡ⋆ ΞΊ β†’
      (# ϡ⋆ ==βŠ₯ 2) ⟢ alloc (ϡ⋆ ↓ 1) (Ξ» α₁ β†’
                        alloc (ϡ⋆ ↓ 2) (Ξ» Ξ±β‚‚ β†’
                          ΞΊ ((α₁ , Ξ±β‚‚) 𝐏-in-𝐄))) , 
    βŠ₯

list : 𝐅
list = fix Ξ» listβ€² β†’
  Ξ» ϡ⋆ ΞΊ β†’
    (# ϡ⋆ ==βŠ₯ 0) ⟢ ΞΊ (Ξ· null 𝐌-in-𝐄) ,
      listβ€² (ϡ⋆ † 1) (Ξ» Ο΅ β†’ cons ⟨ (ϡ⋆ ↓ 1) , Ο΅ ⟩ ΞΊ)

car : 𝐅
car =
  Ξ» ϡ⋆ ΞΊ β†’ (# ϡ⋆ ==βŠ₯ 1) ⟢ hold ((ϡ⋆ ↓ 1) |-𝐏 ↓²1) ΞΊ , βŠ₯

cdr : 𝐅
cdr =
  Ξ» ϡ⋆ ΞΊ β†’ (# ϡ⋆ ==βŠ₯ 1) ⟢ hold ((ϡ⋆ ↓ 1) |-𝐏 ↓²2) ΞΊ , βŠ₯

setcar : 𝐅
setcar =
  Ξ» ϡ⋆ ΞΊ β†’
      (# ϡ⋆ ==βŠ₯ 2) ⟢ assign  ((ϡ⋆ ↓ 1) |-𝐏 ↓²1)
                             (ϡ⋆ ↓ 2)
                             (ΞΊ (Ξ· unspecified 𝐌-in-𝐄)) , 
    βŠ₯

setcdr : 𝐅
setcdr =
  Ξ» ϡ⋆ ΞΊ β†’
      (# ϡ⋆ ==βŠ₯ 2) ⟢ assign  ((ϡ⋆ ↓ 1) |-𝐏 ↓²2)
                             (ϡ⋆ ↓ 2)
                             (ΞΊ (Ξ· unspecified 𝐌-in-𝐄)) , 
    βŠ₯
\end{code}