cek-call-cc/src/Project/Definitions.agda

module Project.Definitions where

open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product renaming (_,_ to _ʻ_)
open import Project.Util using (_$_)

infix 4 _∋_
infix 4 _·_
infixl 6 _,_
infixr 7 _⇒_

data Type : Set where
  ⊥ : Type
  `ℕ : Type
  _⇒_ : Type → Type → Type

data Context : Set where
  ∅ : Context
  _,_ : Context → Type → Context

data Value : Type → Set

data Env : Context → Set where
  ∅ : Env ∅
  _[_∶_] : ∀ {Γ} → Env Γ → (A : Type) → Value A → Env (Γ , A)

data _∋_ : Context → Type → Set where
  zero : ∀ {Γ A} → Γ , A ∋ A
  suc : ∀ {Γ A B} → Γ ∋ A → Γ , B ∋ A

lookup : ∀ {Γ A} → Env Γ → Γ ∋ A → Value A
lookup ∅ ()
lookup (env [ A ∶ x ]) zero = x
lookup (env [ A ∶ x ]) (suc id) = lookup env id

data Aexp Context : Type → Set
data Exp Context : Type → Set

data Aexp Γ where
  value : ∀ {A} → Value A → Aexp Γ A

  -- Natural numbers
  zero : Aexp Γ `ℕ
  suc : Aexp Γ `ℕ → Aexp Γ `ℕ

  -- Functions
  `_ : ∀ {A} → Γ ∋ A → Aexp Γ A
  ƛ : ∀ {B} {A : Type} → Exp (Γ , A) B → Aexp Γ (A ⇒ B)

data Exp Γ where
  abort : ∀ {A} → Aexp Γ ⊥ → Exp Γ A

  -- Atomic expressions
  atomic : ∀ {A} → Aexp Γ A → Exp Γ A

  -- Natural numbers
  case : ∀ {A} → Aexp Γ `ℕ → Exp Γ A → Aexp Γ (`ℕ ⇒ A) → Exp Γ A

  -- Functions
  _·_ : ∀ {A B} → Aexp Γ (A ⇒ B) → Aexp Γ A → Exp Γ B

  -- Call/cc
  call/cc : ∀ {A Tω} → Aexp (Γ) ((A ⇒ ⊥) ⇒ Tω) → Exp Γ Tω

  -- Let
  `let : ∀ {A B : Type} → Exp Γ A → Exp (Γ , A) B → Exp Γ B


-- exp = let (call/cc ƛ . let (abort `0) (`0 · 2)) ((\ . suc `0) · `0)
-- exp = let (s = call/cc ƛk . let (k' = abort k) (k' · 2)) (suc s)
-- exp = 3
exp : Exp ∅ `ℕ
exp =
  `let (call/cc (
    -- `let (` zero · suc (suc zero)) (abort (` zero))
    ƛ (` zero · suc (suc zero))
  )) (`let (abort (` zero)) ((ƛ (atomic (suc (` suc zero)))) · ` zero))

data Kont (Tω : Type) : Type → Set
record Letk (Tv Tω : Type) : Set

data Value where
  -- Natural numbers
  zero : Value `ℕ
  suc : Value `ℕ → Value `ℕ

  -- Functions
  clo : ∀ {Γ} {A B : Type} → Exp (Γ , A) B → Env Γ → Value (A ⇒ B)

  -- Call/CC
  -- cont : ∀ {Tω A} → Kont Tω A → Value (A ⇒ ⊥)
  cont : ∀ {Tω A B} → Kont Tω A → Value (B ⇒ ⊥)

record Letk Tω Tv where
  inductive
  constructor letk
  field
    {Tc} : Type
    Γ : Context
    C : Exp (Γ , Tv) Tc
    E : Env Γ
    K : Kont Tω Tc

data Kont Tω where
  halt : Kont Tω Tω
  kont : ∀ {Tc} → Letk Tω Tc → Kont Tω Tc

-- A is the type of C
-- B is the eventual type
record State (Tω : Type) : Set where
  constructor mkState
  field
    Tc : Type
    Γ : Context
    C : Exp Γ Tc
    E : Env Γ
    K : Kont Tω Tc