Create a gist now

Instantly share code, notes, and snippets.

@jlouis /Fishy1 Secret
Created Jan 20, 2011

Fishy!
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment