Fishy!

Fishy1

module Fish where

open import Function hiding (const)
open import Data.Bool
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality

data Exp : Set where
  Const : ℕ -> Exp
  Plus  : Exp -> Exp -> Exp
  Exit  : Exp -> Exp

----------------------------------------------------------------------
-- Direct style

R = ℕ ⊎ ℕ

const : ℕ -> R
const i = inj₁ i

add : R -> R -> R
add (inj₁ x) (inj₁ x') = inj₁ (x + x')
add (inj₁ x) (inj₂ y) = inj₂ y
add (inj₂ y) y' = inj₂ y

exit : R -> R
exit (inj₁ x) = inj₂ x
exit (inj₂ y) = inj₂ y

eval : Exp -> R
eval (Const y) = const y
eval (Plus y y') = add (eval y) (eval y')
eval (Exit e) = exit (eval e)

-- Funny, how this stuff is immediate :)
thm-determ : ∀ {e : Exp}{v1 v2 : R} -> eval e ≡ v1 -> eval e ≡ v2 -> v1 ≡ v2
thm-determ refl refl = refl

-- This is immediate by normalisation of Agda terms as well :)
thm-terminates : ∀ (e : Exp) -> ∃ (\v -> eval e ≡ v)
thm-terminates e = eval e, refl

----------------------------------------------------------------------
-- Continuations, take 1, naive translation.

module Naive where
  constK : ℕ -> (R -> R) -> R
  constK i k = k (const i)

  exitK : R -> (R -> R) -> R
  exitK v k = k (exit v)

  addK : R -> R -> (R -> R) -> R
  addK v1 v2 k = k (add v1 v2)

  evalK : Exp -> (R -> R) -> R
  evalK (Const y) k = constK y k
  evalK (Plus y y') k = evalK y (\v1 ->
                           evalK y' (\v2 -> addK v1 v2 k))
  evalK (Exit y) k = evalK y (\v1 -> exitK v1 k)

run1 : Exp -> R
run1 e = Naive.evalK e id

-- I so much love me dependent type checker :)
thm-determ-naive : ∀ {e : Exp}{v1 v2 : R} -> run1 e ≡ v1 -> run1 e ≡ v2 ->
                  v1 ≡ v2
thm-determ-naive refl refl = refl

-- This so much feels like cheating. The ∃ is a Σ-type with two components:
--  * The value in question: By definition the evalK on the identity
--  * A proof that the output of the Σ-proj₁ is ≡ to run1 e.
-- The proof is immediate by normalisation in Agda :)
thm-run1-terminates : ∀ (e : Exp) -> ∃ (\v -> run1 e ≡ v)
thm-run1-terminates e = Naive.evalK e id , refl

----------------------------------------------------------------------
-- Continuations, take 2, exploit continuations

module NotNaive where
  -- As before
  constK : ℕ -> (ℕ -> ℕ) -> ℕ
  constK i k = k i

  -- Exit circumventing the 'rest-of-the-program' by not invoking the
  -- continuation
  exitK : ℕ -> (ℕ -> ℕ) -> ℕ
  exitK i k = i

  addK : ℕ -> ℕ -> (ℕ -> ℕ) -> ℕ
  addK v1 v2 k = k (v1 + v2)

  evalK : Exp -> (ℕ -> ℕ) -> ℕ
  evalK (Const y) k = constK y k
  evalK (Plus y y') k = evalK y (\v1 -> evalK y' (\v2 -> addK v1 v2 k))
  evalK (Exit y) k = evalK y (\v1 -> exitK v1 k)

run2 : Exp -> ℕ
run2 e = NotNaive.evalK e id

thm-determ-2 : ∀ {e : Exp}{v1 v2 : ℕ} -> run2 e ≡ v1 -> run2 e ≡ v2 ->
               v1 ≡ v2
thm-determ-2 refl refl = refl

thm-run2-terminates : ∀ (e : Exp) -> ∃ (\v -> run2 e ≡ v)
thm-run2-terminates e = NotNaive.evalK e id , refl

t1 = Plus (Const 20) (Const 22)
t2 = Plus (Exit (Const 88)) (Const 22)

----------------------------------------------------------------------
-- Dependent analysis :)

module DepAnalysis where

  data E : Bool -> Set where
    Const : ℕ -> E true
    Plus  : ∀ {c1 c2} -> E c1 -> E c2 -> E (c1 ∧ c2)
    Exit  : ∀ {c} -> E c -> E false

  pure : {b : Bool} -> E b -> Bool
  pure {x} e = x