------------------------------------------------------------------------
-- Another approach to compiling Hutton's razor
------------------------------------------------------------------------

-- Uses generalised application instead of generalised composition.
-- Based on an idea due to Graham and Diana.

module ApplicationBased where

open import Derivation

open import Data.Nat
open import Data.Vec
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

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

-- A simple expression language. I prefer subtraction to addition
-- because subtraction is not commutative, so the arguments cannot be
-- swapped freely.

data Expr : Set where
  val : ℕ → Expr
  _⊖_ : Expr → Expr → Expr

-- The semantics of the language.

⟦_⟧ : Expr → ℕ
⟦ val n ⟧ = n
⟦ m ⊖ n ⟧ = ⟦ m ⟧ ∸ ⟦ n ⟧

------------------------------------------------------------------------
-- Stacks

-- Stack A n represents stacks of size n, containing elements of
-- type A.

Stack : Set → ℕ → Set
Stack = Vec

-- The type A ^ n represents functions from stacks with n elements
-- to a single result. The first function argument is the top of the
-- stack.

_^_ : Set → ℕ → Set
A ^ zero  = A
A ^ suc n = A → A ^ n

-- x <$ n $> f puts x at the bottom of the stack given to f:
--
--   x <$ n $> f = λ y₁ … y_n → f y₁ … y_n x

_<$_$>_ : ∀ {A} → A → (n : ℕ) → A ^ ( + n) → A ^ n
x <$ zero  $> f = f x
x <$ suc n $> f = λ y → x <$ n $> f y

-- app interprets functions of type A ^ m:
--
--   app m f (x₁ ∷ … ∷ x_m ∷ ys) = f x_m … x₁ ∷ ys

app : ∀ {A} m {n} → A ^ m → Stack A (m + n) → Stack A ( + n)
app zero    f xs       = f ∷ xs
app (suc m) f (x ∷ xs) = app m (x <$ m $> f) xs

------------------------------------------------------------------------
-- First step: Rewrite the evaluator

module Step₁ where

  return : ℕ → ℕ ^ 
  return n = n

  sub : ℕ ^ 
  sub m n = m ∸ n

  private
   mutual

    ⟦_⟧' : Expr → ℕ ^ 
    ⟦ e ⟧' = witness (eval e)

    -- Note: This correctness proof is not used anywhere.

    eval : (e : Expr) → EqualTo ⟦ e ⟧
    eval (val n)   = ▷ begin return n ∎
    eval (e₁ ⊖ e₂) = ▷ begin
      ⟦ e₁ ⟧ ∸ ⟦ e₂ ⟧
        ≡⟨ cong₂ _∸_ (proof (eval e₁)) (proof (eval e₂)) ⟩
      ⟦ e₁ ⟧' ∸ ⟦ e₂ ⟧'
        ≡⟨ refl ⟩
      ⟦ e₁ ⟧' <$  $> (⟦ e₂ ⟧' <$  $> sub)
        ∎

------------------------------------------------------------------------
-- Second step: Defunctionalise

module Step₂ where

  -- The commands and command trees are indexed on their semantics.

  data Cmd : (n : ℕ) → ℕ ^ n → Set where
    return : (n : ℕ) → Cmd  (Step₁.return n)
    sub    : Cmd  Step₁.sub

  data Tree : (n : ℕ) → ℕ ^ n → Set where
    cmd  : ∀ {n f} → Cmd n f → Tree n f
    _$$_ : ∀ {n x f} →
           Tree  x → Tree ( + n) f → Tree n (x <$ n $> f)

  comp : (e : Expr) → Tree  ⟦ e ⟧
  comp (val n)   = cmd (return n)
  comp (e₁ ⊖ e₂) = comp e₁ $$ (comp e₂ $$ cmd sub)

------------------------------------------------------------------------
-- Third step: Linearise the command trees

module Step₃ where

  open Step₂ hiding (comp)
  open Step₂ hiding (comp) renaming (return to push)

  -- The code type is indexed on initial and final stack depth, plus
  -- its semantics.

  Sem : ℕ → ℕ → Set
  Sem i f = Stack ℕ i → Stack ℕ f

  data Code : (i f : ℕ) → Sem i f → Set where
    ε   : ∀ {i} → Code i i id
    _◅_ : ∀ {n g i f s} →
          Step₂.Cmd n g → Code ( + i) f s →
          Code (n + i) f (s ∘ app n g)

  -- Virtual machine.

  exec : ∀ {m n sem} → Code m n sem → Sem m n
  exec {sem = sem} _ = sem

  module Details where

    -- The virtual machine is actually a virtual machine.

    exec' : ∀ {m n sem} → Code m n sem → Sem m n
    exec' ε             s           = s
    exec' (push x ◅ cs) s           = exec' cs (x ∷ s)
    exec' (sub    ◅ cs) (n ∷ m ∷ s) = exec' cs (m ∸ n ∷ s)

    -- The structure of this proof shows that exec and exec' are
    -- _identical_ (modulo normalisation).

    execOK : ∀ {m n sem} (cs : Code m n sem) (s : Stack ℕ m) →
             exec cs s ≡ exec' cs s
    execOK ε             s           = refl
    execOK (push x ◅ cs) s           = execOK cs (x ∷ s)
    execOK (sub    ◅ cs) (n ∷ m ∷ s) = execOK cs (m ∸ n ∷ s)

  -- Correct compiler.

  comp : ∀ {m n f sem} →
         Tree m f → Code ( + n)  sem →
         Code (m + n)  (sem ∘ app m f)
  comp (cmd c)    cs = c ◅ cs
  comp (t₁ $$ t₂) cs = comp t₁ (comp t₂ cs)

------------------------------------------------------------------------
-- Step four: Assemble the pieces

module Step₄ where

  Code : Set
  Code = ∃ (Step₃.Code  )

  comp : Expr → Code
  comp e = (_ , Step₃.comp (Step₂.comp e) Step₃.ε)

  exec : Code → ℕ
  exec cs = head (Step₃.exec (proj₂ cs) [])

  correct : (e : Expr) → ⟦ e ⟧ ≡ exec (comp e)
  correct e = refl