Levy language (Call by push value)

gistfile1.hs

open import Data.Bool
open import Data.Empty
open import Data.Maybe
open import Data.Nat
open import Relation.Nullary 
open import Relation.Binary.PropositionalEquality
open import Data.Fin
open import Data.List
open import Data.Unit
open import Data.Sum hiding (map)
open import Data.Product hiding (map)

{- 
Andrew Miller  March 19 2013.
Brief encoding of CBPV (Call By Push Value) aka the Levy language

P. B. Levy - Call by Push Value Tutorial
http://www.cs.bham.ac.uk/~pbl/papers/cbpvefftt.pdf

P. B. Levy - Adjunction models for CBPV Using Stacks
http://www.cs.bham.ac.uk/~pbl/papers/ctcs02journal.pdf

Based on STLC agda encoding from G. Allais
http://perso.ens-lyon.fr/guillaume.allais/pdf/gallais_m1-1.pdf

-}

module Levy where

mutual
  -- A ∷= UB 
  data VType : Set where
    U : CType -> VType
    VUnit : VType
    _⊕_ : VType -> VType -> VType
    _⊗_ : VType -> VType -> VType

  -- B ∷= FA | A -> B
  data CType : Set where
    F : VType -> CType
    _⇒_ : VType -> CType -> CType
--    _⊕c_ : CType → CType → CType

data Con : Set where
  ε' : Con
  _∘_ : Con -> VType -> Con

data Var : (Γ : Con) (σ : VType) → Set where
  zero : ∀ {Γ σ} → Var (Γ ∘ σ) σ
  suc : ∀ {Γ σ τ} → Var Γ τ → Var (Γ ∘ σ) τ

  -- M ∷= λx.M:B | V′M | inj₁ M | inj₂ M | x

mutual
  data VTerm : Con → VType → Set where
    weakv : ∀ {Γ σ τ} → VTerm Γ τ → VTerm (Γ ∘ σ) τ
    var : ∀ {Γ σ} → Var Γ σ → VTerm Γ σ
    thunk : ∀ {Γ σ} → CTerm Γ σ → VTerm Γ (U σ)
    unit : ∀ {Γ} → VTerm Γ VUnit
    inj1 : ∀ {Γ σ₁ σ₂} → VTerm Γ σ₁ → VTerm Γ (σ₁ ⊕ σ₂)
    inj2 : ∀ {Γ σ₁ σ₂} → VTerm Γ σ₂ → VTerm Γ (σ₁ ⊕ σ₂)
  
  data CTerm : Con → CType → Set where
    weakc : ∀ {Γ σ τ} → CTerm Γ τ → CTerm (Γ ∘ σ) τ
    lam : ∀ {Γ σ τ} → CTerm (Γ ∘ σ) τ → CTerm Γ (σ ⇒ τ)
    _′_ : ∀ {Γ σ τ} → VTerm Γ σ → CTerm Γ (σ ⇒ τ) → CTerm Γ τ
    return : ∀ {Γ σ} → VTerm Γ σ → CTerm Γ (F σ)
    pmSum : ∀ {Γ σ₁ σ₂ τ} → VTerm Γ (σ₁ ⊕ σ₂)
              → CTerm (Γ ∘ σ₁) τ
              → CTerm (Γ ∘ σ₂) τ
                → CTerm Γ τ

-- Mapping from type to denotation

mutual
  Comp : CType → Set
  Comp (F x) = Val x
  Comp (x ⇒ x₁) = Val x → Comp x₁

  Val : VType → Set
  Val (U f) = Comp f
  Val VUnit = ⊤
  Val (τ₁ ⊕ τ₂) = Val τ₁ ⊎ Val τ₂
  Val (τ₁ ⊗ τ₂) = Val τ₁ × Val τ₂

data Env : Con → Set where
  ε : Env ε'
  _::_ : ∀ {Γ σ} → Val σ → Env Γ → Env (Γ ∘ σ)

_!!_ : ∀ {Γ σ} → Env Γ → Var Γ σ → Val σ
(x :: ρ) !! zero = x
(_ :: ρ) !! suc p = ρ !! p

mutual
  ⟦_⟧c : ∀ {Γ σ} → CTerm Γ σ → Env Γ → Comp σ
  ⟦_⟧c (weakc t) (_ :: ρ) = ⟦ t ⟧c ρ
  ⟦_⟧c (lam t) ρ = λ z → ⟦ t ⟧c (z :: ρ)
  ⟦_⟧c (x ′ t) ρ = ⟦ t ⟧c ρ (⟦ x ⟧ ρ)
  ⟦_⟧c (return t) ρ = ⟦ t ⟧ ρ
  ⟦_⟧c (pmSum x t₁ t₂) ρ with ⟦ x ⟧ ρ
  ... | inj₁ y = ⟦ t₁ ⟧c (y :: ρ)
  ... | inj₂ y = ⟦ t₂ ⟧c (y :: ρ)

  ⟦_⟧ : ∀ {Γ σ} → VTerm Γ σ → Env Γ → Val σ
  ⟦_⟧ (weakv t) (_ :: ρ) = ⟦ t ⟧ ρ
  ⟦_⟧ unit ρ = tt
  ⟦_⟧ (inj1 x) ρ = inj₁ (⟦ x ⟧ ρ)
  ⟦_⟧ (inj2 x) ρ = inj₂ (⟦ x ⟧ ρ)
  ⟦_⟧ (var x) ρ = ρ !! x
  ⟦_⟧ (thunk x) ρ = ⟦ x ⟧c ρ

bool : VType
bool = VUnit ⊕ VUnit


v0 : ∀ {Γ σ} → VTerm (Γ ∘ σ) σ
v0 = var zero

v1 : ∀ {Γ σ σ₁} → VTerm ((Γ ∘ σ) ∘ σ₁) σ
v1 = var (suc zero)

v2 : ∀ {Γ σ σ₁ σ₂} → VTerm (((Γ ∘ σ) ∘ σ₁) ∘ σ₂) σ
v2 = var (suc (suc zero))

vtrue : ∀ {Γ} → VTerm Γ bool
vtrue = inj1 unit

vfalse : ∀ {Γ} → VTerm Γ bool
vfalse = inj2 unit

vnot : ∀ {Γ} → CTerm Γ (bool ⇒ F bool)
vnot = lam (pmSum v0 (return vfalse) (return vtrue))

vand : ∀ {Γ} → CTerm Γ (bool ⇒ (bool ⇒ F bool))
vand = lam (lam (pmSum v0 (return v2) (return vfalse)))

vxor : ∀ {Γ} → CTerm Γ (bool ⇒ (bool ⇒ F bool))
vxor = lam (lam (pmSum v0 (v2 ′ vnot) (return v2)))