```{-# OPTIONS --no-termination-check #-}

-- Formalisation of "Calculating an Exceptional Machine" by Graham
-- Hutton and Joel Wright.

-- Note that the development below does not quite correspond to what
-- Graham and Joel did. I tried following the ideas from
-- HuttonsRazor.agda without looking at the paper, and ended up with a
-- slightly different end product. The difference seems to be that I
-- treated the computations in the Maybe monad as opaque (analogously
-- to the additions), but it seems reasonable to incorporate those
-- directly into the abstract machine, which I believe that Graham and
-- Joel did.

-- This module formalises Hutton's razor plus exceptions.

open import Relation.Binary.PropositionalEquality

module Exceptions
-- Assume extensionality; it appears to be necessary for a
-- proof below.
(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
import Level
open ≡-Reasoning
open import Derivation

------------------------------------------------------------------------
-- Expressions

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₂ ⟧

------------------------------------------------------------------------
-- Calculation of an abstract machine

module Calculational where

module Step₁ where

Cont : Set
Cont = Maybe ℕ -> Maybe ℕ

mutual

-- Let us derive a function eval which satisfies
--   eval e c ≡ c ⟦ e ⟧.
-- The derivation is done in evalP, whose type guarantees
-- correctness.

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)))
∎

-- The code above contains some continuations. Let us name them.
-- The identity continuation, used to connect eval to ⟦_⟧, is also
-- named.

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)

-- The top-level evaluation function can be recovered by using the
-- identity continuation.

⟦_⟧' : Expr -> Maybe ℕ
⟦ e ⟧' = eval e c₁

correct : forall e -> ⟦ e ⟧ ≡ ⟦ e ⟧'
correct e = proof (evalP e c₁)

-- ⑵ Defunctionalise, i.e. get rid of the higher-order
--   continuations.

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

-- Define the semantics of the continuations in terms of the
-- higher-order ones.

⟦_⟧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

-- Define a variant of Step₁.eval which uses first-order
-- continuations.

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

-- Also make sure that the semantics of continuations does not
-- refer to Step₁.eval.

-- Note that eval above uses ⟦_⟧c, so it has to be updated.

-- Note that the code in this block does not please the
-- termination checker.

⟦_⟧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)
∎

-- The top-level evaluation function can be recovered.

⟦_⟧' : 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 ⟧'
∎

-- ⑶ Refactor. TODO.
```