{-# OPTIONS --no-termination-check #-}
open import Relation.Binary.PropositionalEquality
module Exceptions
(ext : forall {a b : Set} {f g : a -> b} ->
(forall x -> f x ≡ g x) -> f ≡ g)
where
open import Data.Nat
open import Data.Maybe as Maybe
open import Category.Monad
import Level
open ≡-Reasoning
open import Derivation
open RawMonadPlus (Maybe.monadPlus {f = Level.zero})
data Expr : Set where
val : ℕ -> Expr
_⊕_ : Expr -> Expr -> Expr
throw : Expr
catch : Expr -> Expr -> Expr
⟦_⟧ : Expr -> Maybe ℕ
⟦ val n ⟧ = return n
⟦ e₁ ⊕ e₂ ⟧ = pure _+_ ⊛ ⟦ e₁ ⟧ ⊛ ⟦ e₂ ⟧
⟦ throw ⟧ = ∅
⟦ catch e₁ e₂ ⟧ = ⟦ e₁ ⟧ ∣ ⟦ e₂ ⟧
module Calculational where
module Step₁ where
Cont : Set
Cont = Maybe ℕ -> Maybe ℕ
mutual
eval : Expr -> Cont -> Maybe ℕ
eval e c = witness (evalP e c)
evalP : (e : Expr) (c : Cont) -> EqualTo (c ⟦ e ⟧)
evalP (val n) c = ▷ begin c (return n) ∎
evalP (e₁ ⊕ e₂) c = ▷ begin
c (pure _+_ ⊛ ⟦ e₁ ⟧ ⊛ ⟦ e₂ ⟧)
≡⟨ refl ⟩
(\(m : _) -> c (pure _+_ ⊛ m ⊛ ⟦ e₂ ⟧)) ⟦ e₁ ⟧
≡⟨ proof (evalP e₁ (\m -> c (pure _+_ ⊛ m ⊛ ⟦ e₂ ⟧))) ⟩
eval e₁ (\m -> c (pure _+_ ⊛ m ⊛ ⟦ e₂ ⟧))
≡⟨ refl ⟩
eval e₁ (\m -> (\(n : _) -> c (pure _+_ ⊛ m ⊛ n)) ⟦ e₂ ⟧)
≡⟨ cong (eval e₁)
(ext (\m -> proof (evalP e₂
(\n -> c (pure _+_ ⊛ m ⊛ n))))) ⟩
eval e₁ (\m -> eval e₂ (\n -> c (pure _+_ ⊛ m ⊛ n)))
∎
evalP throw c = ▷ begin c ∅ ∎
evalP (catch e₁ e₂) c = ▷ begin
c (⟦ e₁ ⟧ ∣ ⟦ e₂ ⟧)
≡⟨ refl ⟩
(\(m : _) -> c (m ∣ ⟦ e₂ ⟧)) ⟦ e₁ ⟧
≡⟨ proof (evalP e₁ (\m -> c (m ∣ ⟦ e₂ ⟧))) ⟩
eval e₁ (\m -> c (m ∣ ⟦ e₂ ⟧))
≡⟨ refl ⟩
eval e₁ (\m -> (\(n : _) -> c (m ∣ n)) ⟦ e₂ ⟧)
≡⟨ cong (eval e₁)
(ext (\m -> proof (evalP e₂ (\n -> c (m ∣ n))))) ⟩
eval e₁ (\m -> eval e₂ (\n -> c (m ∣ n)))
∎
c₁ : Cont
c₁ = \n -> n
c₂ : Cont -> Maybe ℕ -> Cont
c₂ c m = \n -> c (pure _+_ ⊛ m ⊛ n)
c₃ : Expr -> Cont -> Cont
c₃ e c = \m -> eval e (c₂ c m)
c₄ : Cont -> Maybe ℕ -> Cont
c₄ c m = \n -> c (m ∣ n)
c₅ : Expr -> Cont -> Cont
c₅ e c = \m -> eval e (c₄ c m)
⟦_⟧' : Expr -> Maybe ℕ
⟦ e ⟧' = eval e c₁
correct : forall e -> ⟦ e ⟧ ≡ ⟦ e ⟧'
correct e = proof (evalP e c₁)
module Step₂ where
data Cont : Set where
c₁ : Cont
c₂ : Cont -> Maybe ℕ -> Cont
c₃ : Expr -> Cont -> Cont
c₄ : Cont -> Maybe ℕ -> Cont
c₅ : Expr -> Cont -> Cont
⟦_⟧c : Cont -> Step₁.Cont
⟦ c₁ ⟧c = Step₁.c₁
⟦ c₂ c n ⟧c = Step₁.c₂ ⟦ c ⟧c n
⟦ c₃ e c ⟧c = Step₁.c₃ e ⟦ c ⟧c
⟦ c₄ c n ⟧c = Step₁.c₄ ⟦ c ⟧c n
⟦ c₅ e c ⟧c = Step₁.c₅ e ⟦ c ⟧c
mutual
eval : Expr -> Cont -> Maybe ℕ
eval e c = witness (evalP e c)
evalP : (e : Expr) (c : Cont) ->
EqualTo (Step₁.eval e ⟦ c ⟧c)
evalP (val n) c = ▷ begin ⟦ c ⟧c (return n) ∎
evalP (e₁ ⊕ e₂) c = ▷ begin
Step₁.eval e₁ (\m -> Step₁.eval e₂
(\n -> ⟦ c ⟧c (pure _+_ ⊛ m ⊛ n)))
≡⟨ refl ⟩
Step₁.eval e₁ ⟦ c₃ e₂ c ⟧c
≡⟨ proof (evalP e₁ (c₃ e₂ c)) ⟩
eval e₁ (c₃ e₂ c)
∎
evalP throw c = ▷ begin ⟦ c ⟧c ∅ ∎
evalP (catch e₁ e₂) c = ▷ begin
Step₁.eval e₁ (\m -> Step₁.eval e₂ (\n -> ⟦ c ⟧c (m ∣ n)))
≡⟨ refl ⟩
Step₁.eval e₁ ⟦ c₅ e₂ c ⟧c
≡⟨ proof (evalP e₁ (c₅ e₂ c)) ⟩
eval e₁ (c₅ e₂ c)
∎
mutual
⟦_⟧c' : Cont -> Step₁.Cont
⟦ c ⟧c' n = witness (cSem c n)
eval' : Expr -> Cont -> Maybe ℕ
eval' e c = witness (evalP' e c)
cSem : (c : Cont) (n : Maybe ℕ) -> EqualTo (⟦ c ⟧c n)
cSem c₁ n = ▷ begin n ∎
cSem (c₂ c m) n = ▷ begin
⟦ c ⟧c (pure _+_ ⊛ m ⊛ n)
≡⟨ proof (cSem c (pure _+_ ⊛ m ⊛ n)) ⟩
⟦ c ⟧c' (pure _+_ ⊛ m ⊛ n)
∎
cSem (c₃ e c) n = ▷ begin
Step₁.eval e ⟦ c₂ c n ⟧c
≡⟨ proof (evalP e (c₂ c n)) ⟩
eval e (c₂ c n)
≡⟨ proof (evalP' e (c₂ c n)) ⟩
eval' e (c₂ c n)
∎
cSem (c₄ c m) n = ▷ begin
⟦ c ⟧c (m ∣ n)
≡⟨ proof (cSem c (m ∣ n)) ⟩
⟦ c ⟧c' (m ∣ n)
∎
cSem (c₅ e c) n = ▷ begin
Step₁.eval e ⟦ c₄ c n ⟧c
≡⟨ proof (evalP e (c₄ c n)) ⟩
eval e (c₄ c n)
≡⟨ proof (evalP' e (c₄ c n)) ⟩
eval' e (c₄ c n)
∎
evalP' : (e : Expr) (c : Cont) ->
EqualTo (eval e c)
evalP' (val n) c = ▷ begin
⟦ c ⟧c (return n)
≡⟨ proof (cSem c (return n)) ⟩
⟦ c ⟧c' (return n)
∎
evalP' (e₁ ⊕ e₂) c = ▷ begin
eval e₁ (c₃ e₂ c)
≡⟨ proof (evalP' e₁ (c₃ e₂ c)) ⟩
eval' e₁ (c₃ e₂ c)
∎
evalP' throw c = ▷ begin
⟦ c ⟧c ∅
≡⟨ proof (cSem c ∅) ⟩
⟦ c ⟧c' ∅
∎
evalP' (catch e₁ e₂) c = ▷ begin
eval e₁ (c₅ e₂ c)
≡⟨ proof (evalP' e₁ (c₅ e₂ c)) ⟩
eval' e₁ (c₅ e₂ c)
∎
⟦_⟧' : Expr -> Maybe ℕ
⟦ e ⟧' = eval' e c₁
correct : forall e -> ⟦ e ⟧ ≡ ⟦ e ⟧'
correct e = begin
⟦ e ⟧
≡⟨ Step₁.correct e ⟩
Step₁.⟦_⟧' e
≡⟨ proof (evalP e c₁) ⟩
eval e c₁
≡⟨ proof (evalP' e c₁) ⟩
⟦ e ⟧'
∎