------------------------------------------------------------------------
-- A derivation of a compiler for a simple language
------------------------------------------------------------------------

module CompositionBased where

open import Data.Nat
open import Data.Product
open import Data.Vec using (Vec; []; _∷_)
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Relation.Binary.HeterogeneousEquality as H

import Derivation
open import ReverseComposition as RC
  hiding (_↑_⇨_; module Derivation; module Stack)

------------------------------------------------------------------------
-- Language

-- A simple expression language.

data Expr : Set where
  val : (n : ℕ) → Expr
  _⊖_ : (e₁ e₂ : Expr) → Expr

-- The semantics of the language.

⟦_⟧ : Expr → ℕ
⟦ val n   ⟧ = n
⟦ e₁ ⊖ e₂ ⟧ = ⟦ e₁ ⟧ ∸ ⟦ e₂ ⟧

------------------------------------------------------------------------
-- Rewrite the evaluator in "compositional" style

-- An abbreviation.

infixl 5 _↑_

_↑_ : Set → ℕ → Set
A ↑ n = RC._↑_⇨_ A n A

module Compositional where

  open RC.Derivation
  open MonoidLaws

  ⟦_⟧↑ : Expr → ℕ ↑ 0
  ⟦ e ⟧↑ = return ⟦ e ⟧

  sub : ℕ ↑ 2
  sub = Λ λ m → Λ λ n → return (m ∸ n)

  mutual

    ⟦_⟧C : Expr → ℕ ↑ 0
    ⟦ e ⟧C = witness (eval e)

    eval : (e : Expr) → EqualTo ⟦ e ⟧↑
    eval (val n)   = ▷ return n ∎
    eval (e₁ ⊖ e₂) = ▷
      return (⟦ e₁ ⟧ ∸ ⟦ e₂ ⟧)  ≡⟨ P.refl ⟩
      ⟦ e₂ ⟧↑ ⊙ ⟦ e₁ ⟧↑ ⊙ sub   ≈⟨ proof (eval e₂) ⊙-cong
                                   proof (eval e₁) ⊙-cong refl sub ⟩
      ⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub   ∎

------------------------------------------------------------------------
-- Rewrite the evaluator in accumulator style

module Accumulator where

  open RC.Derivation
  open MonoidLaws
  open Compositional using (⟦_⟧↑; sub; ⟦_⟧C)

  mutual

    ⟦_⟧A : Expr → ∀ {i} → ℕ ↑ suc i → ℕ ↑ i
    ⟦ e ⟧A f = witness (eval e f)

    eval : ∀ (e : Expr) {i} (f : ℕ ↑ suc i) →
           EqualTo (⟦ e ⟧C ⊙ f)
    eval (val n)   f = ▷ return n ⊙ f ∎
    eval (e₁ ⊖ e₂) f = ▷
      (⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub) ⊙ f  ≈⟨ assoc ⟦ e₂ ⟧C (⟦ e₁ ⟧C ⊙ sub) f ⟩
      ⟦ e₂ ⟧C ⊙ (⟦ e₁ ⟧C ⊙ sub) ⊙ f  ≈⟨ refl ⟦ e₂ ⟧C ⊙-cong
                                        assoc ⟦ e₁ ⟧C sub f ⟩
      ⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub ⊙ f    ≈⟨ refl ⟦ e₂ ⟧C ⊙-cong
                                        proof (eval e₁ (sub ⊙ f)) ⟩
      ⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧A (sub ⊙ f)    ≈⟨ proof (eval e₂ (⟦ e₁ ⟧A (sub ⊙ f))) ⟩
      ⟦ e₂ ⟧A (⟦ e₁ ⟧A (sub ⊙ f))    ∎

  halt : ℕ ↑ 1
  halt = identity

  correct : ∀ e → ∃ λ f → ⟦ e ⟧↑ ≈ ⟦ e ⟧A f
  correct e = halt , (
    ⟦ e ⟧↑         ≈⟨ proof $ Compositional.eval e ⟩
    ⟦ e ⟧C         ≈⟨ sym $ right-identity ⟦ e ⟧C ⟩
    ⟦ e ⟧C ⊙ halt  ≈⟨ proof $ eval e halt ⟩
    ⟦ e ⟧A halt    ∎)

  -- ⟦_⟧A preserves equality of the accumulators.

  ⟦_⟧A-cong : (e : Expr) → ∀ {i} {f g : ℕ ↑ suc i} →
              f ≈ g → ⟦ e ⟧A f ≈ ⟦ e ⟧A g
  ⟦_⟧A-cong (val n)   f≈g = f≈g ·-cong H.refl
  ⟦_⟧A-cong (e₁ ⊖ e₂) f≈g =
    ⟦ e₂ ⟧A-cong (⟦ e₁ ⟧A-cong (refl sub ⊙-cong f≈g))

------------------------------------------------------------------------
-- Defunctionalise

module Defunctionalised where

  open RC.Derivation
  open Compositional using (⟦_⟧↑; sub)
  open Accumulator using (⟦_⟧A; ⟦_⟧A-cong)

  data Term : ℕ → Set where
    return⊙ : ∀ {i} (n : ℕ) (t : Term (1 + i)) → Term i
    sub⊙    : ∀ {i} (t : Term (1 + i)) → Term (2 + i)
    halt    : Term 1

  -- The semantics of Term.

  apply : ∀ {i} → Term i → ℕ ↑ i
  apply (return⊙ n t) = return n ⊙ apply t
  apply (sub⊙ t)      = sub ⊙ apply t
  apply halt          = Accumulator.halt

  -- The right-hand sides evaluate, so the code above is equivalent to
  -- the following one.

  exec : ∀ {i} → Term i → ℕ ↑ i
  exec (return⊙ n t) = exec t · n
  exec (sub⊙ t)      = Λ λ m → Λ λ n → exec t · (m ∸ n)
  exec halt          = Λ λ n → return n

  -- Compiler.

  mutual

    comp : ∀ {i} → Expr → Term (suc i) → Term i
    comp e t = proj₁ (comp′ e t)

    comp′ : ∀ (e : Expr) {i} (t : Term (suc i)) →
            ∃ λ (t′ : Term i) → ⟦ e ⟧A (exec t) ≈ exec t′
    comp′ (val n) t = return⊙ n t , (
      exec t · n          ≡⟨ P.refl ⟩
      exec (return⊙ n t)  ∎)
    comp′ (e₁ ⊖ e₂) t = comp e₂ (comp e₁ (sub⊙ t)) , (
      ⟦ e₂ ⟧A (⟦ e₁ ⟧A (sub ⊙ exec t))   ≡⟨ P.refl ⟩
      ⟦ e₂ ⟧A (⟦ e₁ ⟧A (exec (sub⊙ t)))  ≈⟨ ⟦ e₂ ⟧A-cong (proj₂ $ comp′ e₁ (sub⊙ t)) ⟩
      ⟦ e₂ ⟧A (exec (comp e₁ (sub⊙ t)))  ≈⟨ proj₂ $ comp′ e₂ (comp e₁ (sub⊙ t)) ⟩
      exec (comp e₂ (comp e₁ (sub⊙ t)))  ∎)

  correct : ∀ e → ⟦ e ⟧↑ ≈ exec (comp e halt)
  correct e =
    ⟦ e ⟧↑                   ≈⟨ proj₂ (Accumulator.correct e) ⟩
    ⟦ e ⟧A Accumulator.halt  ≡⟨ P.refl ⟩
    ⟦ e ⟧A (exec halt)       ≈⟨ proj₂ (comp′ e halt) ⟩
    exec (comp e halt)       ∎

------------------------------------------------------------------------
-- Switch to an explicit stack

module Stack where

  open Derivation
  open Compositional using (⟦_⟧↑)
  open Defunctionalised using (Term; return⊙; sub⊙; halt; comp)
  open P.≡-Reasoning

  _^_ : Set → ℕ → Set
  A ^ n = Vec A n → A

  mutual

    exec : ∀ {i} → Term i → ℕ ^ i
    exec t = witness ∘ exec′ t

    exec′ : ∀ {i} (t : Term i) (xs : Vec ℕ i) →
            EqualTo (app (Defunctionalised.exec t) xs)
    exec′ (return⊙ n t) s = ▷ begin
      app (Defunctionalised.exec t) (n ∷ s)  ≡⟨ proof (exec′ t (n ∷ s)) ⟩
      exec t (n ∷ s)                         ∎
    exec′ (sub⊙ t) (m ∷ n ∷ s) = ▷ begin
      app (Defunctionalised.exec t) (m ∸ n ∷ s)  ≡⟨ proof (exec′ t (m ∸ n ∷ s)) ⟩
      exec t (m ∸ n ∷ s)                         ∎
    exec′ halt (n ∷ []) = ▷ begin n ∎

  correct : ∀ e → ⟦ e ⟧ ≡ exec (comp e halt) []
  correct e = begin
    ⟦ e ⟧                                                 ≡⟨ P.refl ⟩
    run ⟦ e ⟧↑                                            ≡⟨ run-cong (Defunctionalised.correct e) ⟩
    run (Defunctionalised.exec (comp e halt))             ≡⟨ P.refl ⟩
    app {A = ℕ} (Defunctionalised.exec (comp e halt)) []  ≡⟨ proj₂ $ exec′ (comp e halt) [] ⟩
    exec (comp e halt) []                                 ∎

------------------------------------------------------------------------
-- Wrapping up

module Finally where

  Code : Set
  Code = Defunctionalised.Term 0

  comp : Expr → Code
  comp e = Defunctionalised.comp e Defunctionalised.halt

  exec : Code → ℕ
  exec = flip Stack.exec []

  correct : ∀ e → ⟦ e ⟧ ≡ exec (comp e)
  correct = Stack.correct