Scheme.Semantic Functions

{-# OPTIONS --allow-unsolved-metas #-}

module Scheme.Semantic-Functions where

open import Scheme.Domain-Notation
open import Scheme.Abstract-Syntax
open import Scheme.Domain-Equations
open import Scheme.Auxiliary-Functions

-- 7.2.3. Semantic functions

postulate π’¦βŸ¦_⟧ : Con β†’ 𝐄
β„°βŸ¦_⟧   : Exp β†’ 𝐔 β†’ 𝐊 β†’ 𝐂
β„°β‹†βŸ¦_⟧  : Exp ⋆′ β†’ 𝐔 β†’ 𝐊 β†’ 𝐂
π’žβ‹†βŸ¦_⟧  : Com ⋆′ β†’ 𝐔 β†’ 𝐂 β†’ 𝐂

-- Definition of 𝒦 deliberately omitted.

β„°βŸ¦ con K ⟧ = Ξ» ρ ΞΊ β†’ send (π’¦βŸ¦ K ⟧) ΞΊ

β„°βŸ¦ ide I ⟧ = Ξ» ρ ΞΊ β†’
  hold (lookup ρ I) (single (Ξ» Ο΅ β†’
    (misc-undefined β™―) (β–» Ο΅) ⟢ wrong "undefined variable" ,
      send Ο΅ ΞΊ))

-- Non-compositional:
-- β„°βŸ¦ β¦… Eβ‚€ ␣ E⋆ ⦆ ⟧ =
--   Ξ» ρ ΞΊ β†’ β„°β‹†βŸ¦ permute (⟨ Eβ‚€ ⟩ Β§ E⋆ ) ⟧
--           ρ
--           (Ξ» ϡ⋆ β†’ ((Ξ» ϡ⋆ β†’ applicate (ϡ⋆ ↓ 1) (ϡ⋆ † 1) ΞΊ)
--                    (unpermute ϡ⋆)))

β„°βŸ¦ β¦… Eβ‚€ ␣ E⋆ ⦆ ⟧ = Ξ» ρ ΞΊ β†’
  β„°βŸ¦ Eβ‚€ ⟧ ρ (single (Ξ» Ο΅β‚€ β†’
    β„°β‹†βŸ¦ E⋆ ⟧ ρ (β—… Ξ» ϡ⋆ β†’
      applicate Ο΅β‚€ ϡ⋆ ΞΊ)))

β„°βŸ¦ β¦…lambda␣⦅ I⋆ ⦆ Γ⋆ ␣ Eβ‚€ ⦆ ⟧ = Ξ» ρ ΞΊ β†’ β—… Ξ» Οƒ β†’ 
    (new Οƒ βˆˆπ‹) ⟢
        β–» (send (β—… ( (new Οƒ |𝐋) ,
                     (Ξ» ϡ⋆ ΞΊβ€² β†’
                        (# ϡ⋆ ==βŠ₯ #β€² I⋆) ⟢
                            tievals
                              (Ξ» α⋆ β†’ (Ξ» ρ′ β†’ π’žβ‹†βŸ¦ Γ⋆ ⟧ ρ′ (β„°βŸ¦ Eβ‚€ ⟧ ρ′ ΞΊβ€²))
                                      (extends ρ I⋆ α⋆))
                              ϡ⋆ ,
                          wrong "wrong number of arguments"
                     )
                   ) 𝐅-in-𝐄)
                ΞΊ)
          (update (new Οƒ |𝐋) unspecified-in-𝐄 Οƒ) ,
      β–» (wrong "out of memory") Οƒ

\clearpage

β„°βŸ¦ β¦…lambda␣⦅ I⋆ Β· I ⦆ Γ⋆ ␣ Eβ‚€ ⦆ ⟧ = Ξ» ρ ΞΊ β†’ β—… Ξ» Οƒ β†’ 
    (new Οƒ βˆˆπ‹) ⟢
        β–» (send (β—… ( (new Οƒ |𝐋) ,
                     (Ξ» ϡ⋆ ΞΊβ€² β†’
                        (# ϡ⋆ >=βŠ₯ #β€² I⋆) ⟢
                           tievalsrest
                              (Ξ» α⋆ β†’ (Ξ» ρ′ β†’ π’žβ‹†βŸ¦ Γ⋆ ⟧ ρ′ (β„°βŸ¦ Eβ‚€ ⟧ ρ′ ΞΊβ€²))
                              (extends ρ (I⋆ Β§β€² ( 1 , I )) α⋆))
                              ϡ⋆
                              (Ξ· (#β€² I⋆)) ,
                          wrong "too few arguments"
                     )
                   ) 𝐅-in-𝐄)
                ΞΊ)
          (update (new Οƒ |𝐋) unspecified-in-𝐄 Οƒ) ,
      β–» (wrong "out of memory") Οƒ

-- Non-compositional:
-- β„°βŸ¦ β¦…lambda I ␣ Γ⋆ ␣ Eβ‚€ ⦆ ⟧ = β„°βŸ¦ β¦…lambda β¦… Β· I ⦆ Γ⋆ ␣ Eβ‚€ ⦆ ⟧

β„°βŸ¦ β¦…lambda I ␣ Γ⋆ ␣ Eβ‚€ ⦆ ⟧ = Ξ» ρ ΞΊ β†’ β—… Ξ» Οƒ β†’ 
    (new Οƒ βˆˆπ‹) ⟢
        β–» (send (β—… ( (new Οƒ |𝐋) ,
                     (Ξ» ϡ⋆ ΞΊβ€² β†’
                        tievalsrest
                          (Ξ» α⋆ β†’ (Ξ» ρ′ β†’ π’žβ‹†βŸ¦ Γ⋆ ⟧ ρ′ (β„°βŸ¦ Eβ‚€ ⟧ ρ′ ΞΊβ€²))
                                  (extends ρ (1 , I) α⋆))
                          ϡ⋆
                          (Ξ· 0))
                   ) 𝐅-in-𝐄)
                ΞΊ)
          (update (new Οƒ |𝐋) unspecified-in-𝐄 Οƒ) ,
      β–» (wrong "out of memory") Οƒ


β„°βŸ¦ β¦…if Eβ‚€ ␣ E₁ ␣ Eβ‚‚ ⦆ ⟧ = Ξ» ρ ΞΊ β†’ 
  β„°βŸ¦ Eβ‚€ ⟧ ρ (single (Ξ» Ο΅ β†’
    truish Ο΅ ⟢ β„°βŸ¦ E₁ ⟧ ρ ΞΊ ,
      β„°βŸ¦ Eβ‚‚ ⟧ ρ ΞΊ))

β„°βŸ¦ β¦…if Eβ‚€ ␣ E₁ ⦆ ⟧ = Ξ» ρ ΞΊ β†’ 
  β„°βŸ¦ Eβ‚€ ⟧ ρ (single (Ξ» Ο΅ β†’
    truish Ο΅ ⟢ β„°βŸ¦ E₁ ⟧ ρ ΞΊ ,
      send unspecified-in-𝐄 ΞΊ))

-- Here and elsewhere, any expressed value other than `undefined`
-- may be used in place of `unspecified`.

\clearpage

β„°βŸ¦ β¦…set! I ␣ E ⦆ ⟧ = Ξ» ρ ΞΊ β†’
  β„°βŸ¦ E ⟧ ρ (single (Ξ» Ο΅ β†’
    assign (lookup ρ I) Ο΅ (send unspecified-in-𝐄 ΞΊ)))

-- β„°β‹†βŸ¦_⟧  : Exp ⋆′ β†’ 𝐔 β†’ 𝐊 β†’ 𝐂

β„°β‹†βŸ¦ 0 , _ ⟧  = Ξ» ρ ΞΊ β†’ β–» ΞΊ ⟨⟩

-- Cannot split on argument of non-datatype Exp ^ suc n:
-- β„°β‹†βŸ¦ suc n , E , Es ⟧ = Ξ» ρ ΞΊ β†’
--   β„°βŸ¦ E ⟧ ρ (single (Ξ» Ο΅β‚€ β†’
--     β„°β‹†βŸ¦ n , Es ⟧ ρ (β—… Ξ» ϡ⋆ β†’
--       β–» ΞΊ (⟨ Ο΅β‚€ ⟩ Β§ ϡ⋆))))

β„°β‹†βŸ¦ 1 , E ⟧  = Ξ» ρ ΞΊ β†’
  β„°βŸ¦ E ⟧ ρ (single (Ξ» Ο΅ β†’ β–» ΞΊ ⟨ Ο΅ ⟩ ))

β„°β‹†βŸ¦ suc (suc n) , E , Es ⟧ = Ξ» ρ ΞΊ β†’
  β„°βŸ¦ E ⟧ ρ (single (Ξ» Ο΅β‚€ β†’
    β„°β‹†βŸ¦ suc n , Es ⟧ ρ (β—… Ξ» ϡ⋆ β†’
      β–» ΞΊ (⟨ Ο΅β‚€ ⟩ Β§ ϡ⋆))))

-- π’žβ‹†βŸ¦_⟧  : Com ⋆′ β†’ 𝐔 β†’ 𝐂 β†’ 𝐂

π’žβ‹†βŸ¦ 0 , _ ⟧ =  Ξ» ρ ΞΈ β†’ ΞΈ

π’žβ‹†βŸ¦ 1 , Ξ“ ⟧ = Ξ» ρ ΞΈ β†’ β„°βŸ¦ Ξ“ ⟧ ρ (β—… Ξ» ϡ⋆ β†’ ΞΈ)

π’žβ‹†βŸ¦ suc (suc n) , Ξ“ , Ξ“s ⟧ = Ξ» ρ ΞΈ β†’
  β„°βŸ¦ Ξ“ ⟧ ρ (β—… Ξ» ϡ⋆ β†’
    π’žβ‹†βŸ¦ suc n , Ξ“s ⟧ ρ ΞΈ)