Skip to content

Scm.Auxiliary-Functions

{-# OPTIONS --rewriting --confluence-check --lossy-unification #-}

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

-- Lists

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

list : βŸͺ 𝐅 ⟫
list = fix {D = 𝐅} Ξ» 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-𝐄)) , 
    βŠ₯