[Another approach to compiling Hutton's razor.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080513181929] addfile ./ApplicationBased.agda
hunk ./ApplicationBased.agda 1
+------------------------------------------------------------------------
+-- 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 Data.Star hiding (return)
+open import Data.Star.Nat
+open import Data.Star.Vec
+open import Data.Star.Decoration
+
+------------------------------------------------------------------------
+-- Language
+
+-- A simple expression language. I prefer subtraction to addition
+-- since subtraction is not commutative, so the arguments cannot be
+-- swapped freely.
+
+data Expr : Set where
+  val : ℕ -> Expr
+  _⊖_ : Expr -> Expr -> Expr
+
+-- Its semantics.
+
+⟦_⟧ : Expr -> ℕ
+⟦ val n ⟧ = n
+⟦ m ⊖ n ⟧ = ⟦ m ⟧ ∸ ⟦ n ⟧
+
+------------------------------------------------------------------------
+-- First step: Rewrite the evaluator
+
+module Step₁ where
+
+  _^_ : Set -> ℕ -> Set
+  a ^ ε       = a
+  a ^ (_ ◅ n) = a -> a ^ n
+
+  return : ℕ -> ℕ ^ 0#
+  return n = n
+
+  sub : ℕ ^ 2#
+  sub m n = m ∸ n
+
+  _<$_$>_ : forall {a} -> a -> (n : ℕ) -> a ^ (1# + n) -> a ^ n
+  x <$ ε     $> f = f x
+  x <$ _ ◅ n $> f = \y -> x <$ n $> f y
+
+  ⟦_⟧' : Expr -> ℕ ^ 0#
+  ⟦ val n ⟧' = return n
+  ⟦ m ⊖ n ⟧' = ⟦ m ⟧' <$ 0# $> (⟦ n ⟧' <$ 1# $> sub)
+
+------------------------------------------------------------------------
+-- Second step: Defunctionalise
+
+module Step₂ where
+
+  data Cmd : ℕ -> Set where
+    return : ℕ -> Cmd 0#
+    sub    : Cmd 2#
+
+  data Tree : ℕ -> Set where
+    cmd  : forall {n} -> Cmd n -> Tree (1# + n)
+    _$$_ : forall {n} -> Tree 1# -> Tree (1# + n) -> Tree n
+
+  comp : Expr -> Tree 1#
+  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 (Cmd; comp)
+
+  -- The commands and the code type are indexed on initial and final
+  -- stack depth.
+
+  data Cmd : ℕ -> ℕ -> Set where
+    push : forall {n} -> ℕ -> Cmd n (1# + n)
+    sub  : forall {n} -> Cmd (2# + n) (1# + n)
+
+  Code : ℕ -> ℕ -> Set
+  Code = Star Cmd
+
+  Stack : ℕ -> Set
+  Stack = Vec ℕ
+
+  comp : forall {m n} -> Tree (1# + m) -> Code (m + n) (1# + n)
+  comp (cmd (return n)) = push n ◅ ε
+  comp (cmd sub)        = sub ◅ ε
+  comp (t₁ $$ t₂)       = comp t₁ ◅◅ comp t₂
+
+  exec : forall {m n} -> Code m n -> Stack m -> Stack n
+  exec ε             s               = s
+  exec (push n ◅ cs) s               = exec cs (n ∷ s)
+  exec (sub    ◅ cs) (↦ n ◅ ↦ m ◅ s) = exec cs (m ∸ n ∷ s)
+
+------------------------------------------------------------------------
+-- 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)
+
+  exec : Code -> ℕ
+  exec cs = head (Step₃.exec cs ε)