{-# 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
open import Category.Monad
import Level
open ≡-Reasoning
open import Derivation
open RawMonadPlus (Maybe.monadPlus {f = Level.zero})

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

  -- ⑴ Add continuations.

  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.