EvalContML1.agda

module EvalContML1 where

open import Data.Nat as N using (ℕ)
open import Data.Bool as B using (Bool; false; true)
open import Relation.Binary.PropositionalEquality

data Value : Set where
  int : ℕ → Value
  bool : Bool → Value

infix 5 _+_
infix 6 _*_
infix 4 _<_
infix 3 if_then_else_

data Exp : Set where
  value : Value → Exp
  _+_ : Exp → Exp → Exp
  _*_ : Exp → Exp → Exp
  _<_ : Exp → Exp → Exp
  if_then_else_ : Exp → Exp → Exp → Exp

data Cont : Set where
  empty : Cont
  ⟦·+_⟧≫_ : Exp → Cont → Cont
  ⟦_+·⟧≫_ : Value → Cont → Cont
  ⟦·*_⟧≫_ : Exp → Cont → Cont
  ⟦_*·⟧≫_ : Value → Cont → Cont
  ⟦·<_⟧≫_ : Exp → Cont → Cont
  ⟦_<·⟧≫_ : Value → Cont → Cont
  ⟦if·then_else_⟧≫_ : Exp → Exp → Cont → Cont
  branch : Exp → Exp → Cont → Cont

_<b_ : ℕ → ℕ → Bool
N.zero  <b N.zero  = false
N.zero  <b N.suc _ = true
N.suc n <b N.zero  = false
N.suc n <b N.suc m = n <b m

infix 2 _≫_⇓_
infix 2 _⇒_⇓_

data _≫_⇓_ : Exp → Cont → Value → Set
data _⇒_⇓_ : Value → Cont → Value → Set

data _≫_⇓_ where
  e-int   : ∀ {i : ℕ} {k v}
            → int i ⇒ k ⇓ v
            → value (int i) ≫ k ⇓ v
  e-bool  : ∀ {b : Bool} {k v}
            → bool b ⇒ k ⇓ v
            → value (bool b) ≫ k ⇓ v
  e-binop-plus : ∀ {e₁ e₂ k v} → e₁ ≫ ⟦·+ e₂ ⟧≫ k ⇓ v → (e₁ + e₂) ≫ k ⇓ v
  e-binop-mult : ∀ {e₁ e₂ k v} → e₁ ≫ ⟦·* e₂ ⟧≫ k ⇓ v → (e₁ * e₂) ≫ k ⇓ v
  e-binop-lt   : ∀ {e₁ e₂ k v} → e₁ ≫ ⟦·< e₂ ⟧≫ k ⇓ v → (e₁ < e₂) ≫ k ⇓ v
  e-if         : ∀ {e₁ e₂ e₃ k v}
                 → e₁ ≫ (⟦if·then e₂ else e₃ ⟧≫ k) ⇓ v
                 → if e₁ then e₂ else e₃ ≫ k ⇓ v

data _⇒_⇓_ where
  c-ret   : ∀ {v} → v ⇒ empty ⇓ v
  c-evalr-plus : ∀ {e v₁ v₂ k}
                 → e ≫ (⟦ v₁ +·⟧≫ k) ⇓ v₂
                 → v₁ ⇒ ⟦·+ e ⟧≫ k ⇓ v₂
  c-evalr-mult : ∀ {e v₁ v₂ k}
                 → e ≫ (⟦ v₁ *·⟧≫ k) ⇓ v₂
                 → v₁ ⇒ ⟦·* e ⟧≫ k ⇓ v₂
  c-evalr-lt   : ∀ {e v₁ v₂ k}
                 → e ≫ (⟦ v₁ <·⟧≫ k) ⇓ v₂
                 → v₁ ⇒ ⟦·< e ⟧≫ k ⇓ v₂
  c-plus : ∀ {i₁ i₂ i₃ k v}
           → i₁ N.+ i₂ ≡ i₃
           → int i₃ ⇒ k ⇓ v
           → int i₂ ⇒ ⟦ int i₁ +·⟧≫ k ⇓ v
  c-mult : ∀ {i₁ i₂ i₃ k v}
           → i₁ N.* i₂ ≡ i₃
           → int i₃ ⇒ k ⇓ v
           → int i₂ ⇒ ⟦ int i₁ *·⟧≫ k ⇓ v
  c-lt   : ∀ {i₁ i₂ b k v}
           → i₁ <b i₂ ≡ b
           → bool b ⇒ k ⇓ v
           → int i₂ ⇒ ⟦ int i₁ <·⟧≫ k ⇓ v
  c-ift  : ∀ {e₁ e₂ k v}
           → e₁ ≫ k ⇓ v
           → bool true ⇒ ⟦if·then e₁ else e₂ ⟧≫ k ⇓ v
  c-iff  : ∀ {e₁ e₂ k v}
           → e₂ ≫ k ⇓ v
           → bool false ⇒ ⟦if·then e₁ else e₂ ⟧≫ k ⇓ v

ex₁ : (value (int 3) + value (int 5)) ≫ empty ⇓ int 8
ex₁ = e-binop-plus (e-int (c-evalr-plus (e-int (c-plus refl c-ret))))

ex₂ : (value (int 4) + value (int 5)) * (value (int 1) + value (int 10)) ≫ empty ⇓ int 99
ex₂ = e-binop-mult
        (e-binop-plus
          (e-int
            (c-evalr-plus
              (e-int
                (c-plus {i₃ = 9}
                  refl
                  (c-evalr-mult
                    (e-binop-plus
                      (e-int
                        (c-evalr-plus
                          (e-int
                            (c-plus {i₃ = 11}
                              refl
                              (c-mult {i₃ = 99} refl c-ret))))))))))))

ex₃ : if value (int 4) < value (int 5)
      then value (int 2) + value (int 3)
      else value (int 8) * value (int 8) ≫ empty ⇓ int 5
ex₃ = e-if
        (e-binop-lt
         (e-int
          (c-evalr-lt
           (e-int
            (c-lt refl
             (c-ift
              (e-binop-plus
               (e-int (c-evalr-plus (e-int (c-plus refl c-ret)))))))))))