\begin{code}

module Scheme.Auxiliary-Functions where

open import Scheme.Domain-Notation
open import Scheme.Domain-Equations
open import Scheme.Abstract-Syntax using (Ide)

open import Data.Nat.Base
  using (NonZero; pred) public

-- 7.2.4. Auxiliary functions

postulate _==α΄΅_ : Ide β†’ Ide β†’ Bool

_[_/_] : 𝐔 β†’ 𝐋 β†’ Ide β†’ 𝐔
ρ [ Ξ± / I ] = β—… Ξ» Iβ€² β†’ if I ==α΄΅ Iβ€² then Ξ± else β–» ρ Iβ€²

lookup : 𝐔 β†’ Ide β†’ 𝐋
lookup = Ξ» ρ I β†’ β–» ρ I

extends : 𝐔 β†’ Ide ⋆′ β†’ 𝐋 ⋆ β†’ 𝐔
extends = fix Ξ» extendsβ€² β†’
  Ξ» ρ I⋆′ α⋆ β†’
    Ξ· (#β€² I⋆′ == 0) ⟢ ρ ,
      ( ( ( (Ξ» I β†’ Ξ» I⋆′′ β†’
              extendsβ€² (ρ [ (α⋆ ↓ 1) / I ]) I⋆′′ (α⋆ † 1)) β™―)
          (I⋆′ ↓′ 1)) β™―) (I⋆′ †′ 1)

postulate
  wrong : String β†’ 𝐂
  -- wrong : 𝐗 β†’ 𝐂 -- implementation-dependent

send : 𝐄 β†’ 𝐊 β†’ 𝐂
send = Ξ» Ο΅ ΞΊ β†’ β–» ΞΊ ⟨ Ο΅ ⟩

single : (𝐄 β†’ 𝐂) β†’ 𝐊
single =
  Ξ» ψ β†’ β—… Ξ» ϡ⋆ β†’ 
    (# ϡ⋆ ==βŠ₯ 1) ⟢ ψ (ϡ⋆ ↓ 1) ,
      wrong "wrong number of return values"

postulate
  new : 𝐒 β†’ 𝕃 (𝐋 + 𝐗)
-- new : 𝐒 β†’ (𝐋 + {error}) -- implementation-dependent

hold : 𝐋 β†’ 𝐊 β†’ 𝐂
hold = Ξ» Ξ± ΞΊ β†’ β—… Ξ» Οƒ β†’ β–» (send (β–» Οƒ Ξ± ↓1) ΞΊ) Οƒ

-- assign : 𝐋 β†’ 𝐄 β†’ 𝐂 β†’ 𝐂
-- assign = Ξ» Ξ± Ο΅ ΞΈ Οƒ β†’ ΞΈ (update Ξ± Ο΅ Οƒ)
-- forward reference to update

postulate
  _==α΄Έ_ : 𝐋 β†’ 𝐋 β†’ 𝐓

-- R5RS and [Stoy] explain _[_/_] only in connection with environments
_[_/_]β€² : 𝐒 β†’ (𝐄 Γ— 𝐓) β†’ 𝐋 β†’ 𝐒
Οƒ [ z / Ξ± ]β€² = β—… Ξ» Ξ±β€² β†’ (Ξ± ==α΄Έ Ξ±β€²) ⟢ z , β–» Οƒ Ξ±β€²

update : 𝐋 β†’ 𝐄 β†’ 𝐒 β†’ 𝐒
update = Ξ» Ξ± Ο΅ Οƒ β†’ Οƒ [ (Ο΅ , Ξ· true) / Ξ± ]β€²

assign : 𝐋 β†’ 𝐄 β†’ 𝐂 β†’ 𝐂
assign = Ξ» Ξ± Ο΅ ΞΈ β†’ β—… Ξ» Οƒ β†’ β–» ΞΈ (update Ξ± Ο΅ Οƒ)

tievals : (𝐋 ⋆ β†’ 𝐂) β†’ 𝐄 ⋆ β†’ 𝐂
tievals = fix Ξ» tievalsβ€² β†’
  Ξ» ψ ϡ⋆ β†’ β—… Ξ» Οƒ β†’
    (# ϡ⋆ ==βŠ₯ 0) ⟢ β–» (ψ ⟨⟩) Οƒ ,
      ((new Οƒ βˆˆπ‹) ⟢
          β–»  (tievalsβ€² (Ξ» α⋆ β†’ ψ (⟨ new Οƒ |𝐋 ⟩ Β§ α⋆)) (ϡ⋆ † 1))
             (update (new Οƒ |𝐋) (ϡ⋆ ↓ 1) Οƒ) ,
        β–» (wrong "out of memory") Οƒ )

list : 𝐄 ⋆ β†’ 𝐊 β†’ 𝐂
-- Add declarations:
dropfirst : 𝐄 ⋆ β†’ 𝐍 β†’ 𝐄 ⋆
takefirst : 𝐄 ⋆ β†’ 𝐍 β†’ 𝐄 ⋆

tievalsrest : (𝐋 ⋆ β†’ 𝐂) β†’ 𝐄 ⋆ β†’ 𝐍 β†’ 𝐂
tievalsrest =
  Ξ» ψ ϡ⋆ Ξ½ β†’ list  (dropfirst ϡ⋆ Ξ½)
                   (single (Ξ» Ο΅ β†’ tievals ψ ((takefirst ϡ⋆ Ξ½) Β§ ⟨ Ο΅ ⟩)))

dropfirst = fix Ξ» dropfirstβ€² β†’
  Ξ» ϡ⋆ Ξ½ β†’
    (Ξ½ ==βŠ₯ 0) ⟢ ϡ⋆ ,
      dropfirstβ€² (ϡ⋆ † 1) (((Ξ· ∘ pred) β™―) Ξ½)

takefirst = fix Ξ» takefirstβ€² β†’
  Ξ» ϡ⋆ Ξ½ β†’
    (Ξ½ ==βŠ₯ 0) ⟢ ⟨⟩ ,
      ( ⟨ ϡ⋆ ↓ 1 ⟩ Β§ (takefirstβ€² (ϡ⋆ † 1) (((Ξ· ∘ pred) β™―) Ξ½)) )

truish : 𝐄 β†’ 𝐓
-- truish = Ξ» Ο΅ β†’ Ο΅ = false ⟢ false , true
truish = Ξ» Ο΅ β†’ (misc-false β™―) (β–» Ο΅) ⟢ (Ξ· false) , (Ξ· true) where
  misc-false : (𝐐 + 𝐇 + 𝐑 + 𝐄𝐩 + 𝐄𝐯 + 𝐄𝐬 + 𝐌 + 𝐅) β†’ 𝕃 Bool
  misc-false (inj-𝐌 ΞΌ)  = ((Ξ» { false β†’ Ξ· true ; _ β†’ Ξ· false }) β™―) (ΞΌ)
  misc-false (inj₁ _)   = Ξ· false
  misc-false (injβ‚‚ _)   = Ξ· false

-- Added:
misc-undefined : (𝐐 + 𝐇 + 𝐑 + 𝐄𝐩 + 𝐄𝐯 + 𝐄𝐬 + 𝐌 + 𝐅) β†’ 𝕃 Bool
misc-undefined (inj-𝐌 ΞΌ)  = ((Ξ» { undefined β†’ Ξ· true ; _ β†’ Ξ· false }) β™―) (ΞΌ)
misc-undefined (inj₁ _)    = Ξ· false
misc-undefined (injβ‚‚ _)    = Ξ· false

-- permute    : Exp ⋆′ β†’ Exp ⋆′  -- implementation-dependent
-- unpermute  : 𝐄 ⋆ β†’ 𝐄 ⋆      -- inverse of permute

applicate : 𝐄 β†’ 𝐄 ⋆ β†’ 𝐊 β†’ 𝐂
applicate =
  Ξ» Ο΅ ϡ⋆ ΞΊ β†’
    (Ο΅ βˆˆπ…) ⟢ (β–» (Ο΅ |𝐅) ↓2) ϡ⋆ ΞΊ ,
      wrong "bad procedure"

onearg : (𝐄 β†’ 𝐊 β†’ 𝐂) β†’ (𝐄 ⋆ β†’ 𝐊 β†’ 𝐂)
onearg =
  Ξ» ΞΆ ϡ⋆ ΞΊ β†’
    (# ϡ⋆ ==βŠ₯ 1) ⟢ ΞΆ (ϡ⋆ ↓ 1) ΞΊ ,
      wrong "wrong number of arguments"

twoarg : (𝐄 β†’ 𝐄 β†’ 𝐊 β†’ 𝐂) β†’ (𝐄 ⋆ β†’ 𝐊 β†’ 𝐂)
twoarg =
  Ξ» ΞΆ ϡ⋆ ΞΊ β†’
    (# ϡ⋆ ==βŠ₯ 2) ⟢ ΞΆ (ϡ⋆ ↓ 1) (ϡ⋆ ↓ 2) ΞΊ ,
      wrong "wrong number of arguments"

cons : 𝐄 ⋆ β†’ 𝐊 β†’ 𝐂

-- list : 𝐄 ⋆ β†’ 𝐊 β†’ 𝐂
list = fix Ξ» listβ€² β†’
  Ξ» ϡ⋆ ΞΊ β†’
    (# ϡ⋆ ==βŠ₯ 0) ⟢ send (β—… (Ξ· (inj-𝐌 (Ξ· null)))) ΞΊ ,
      listβ€² (ϡ⋆ † 1) (single (Ξ» Ο΅ β†’ cons ⟨ (ϡ⋆ ↓ 1) , Ο΅ ⟩ ΞΊ))

-- cons : 𝐄 ⋆ β†’ 𝐊 β†’ 𝐂
cons = twoarg
  Ξ» ϡ₁ Ο΅β‚‚ ΞΊ β†’ β—… Ξ» Οƒ β†’
    (new Οƒ βˆˆπ‹) ⟢
        (Ξ» Οƒβ€² β†’ (new Οƒβ€² βˆˆπ‹) ⟢
                    β–» (send ((new Οƒ |𝐋 , new Οƒβ€² |𝐋 , (Ξ· true)) 𝐄𝐩-in-𝐄) ΞΊ)
                      (update (new Οƒβ€² |𝐋) Ο΅β‚‚ Οƒβ€²) ,
                  β–» (wrong "out of memory") Οƒβ€²)
        (update (new Οƒ |𝐋) ϡ₁ Οƒ) ,
      β–» (wrong "out of memory") Οƒ
\end{code}