```------------------------------------------------------------------------
-- 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 ^ (1 + 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 (1 + 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 : ℕ → ℕ ^ 0
return n = n

sub : ℕ ^ 2
sub m n = m ∸ n

private
mutual

⟦_⟧' : Expr → ℕ ^ 0
⟦ 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₁ ⟧' <\$ 0 \$> (⟦ e₂ ⟧' <\$ 1 \$> 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 0 (Step₁.return n)
sub    : Cmd 2 Step₁.sub

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

comp : (e : Expr) → Tree 0 ⟦ 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)

-- 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 (1 + 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 (1 + n) 1 sem →
Code (m + n) 1 (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 0 1)

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