[Started on the derivation. Did (parts of) the defunctionalisation.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080315011706] hunk ./Wand2.agda 22
+open import Logic
+
+------------------------------------------------------------------------
+-- Type system
hunk ./Wand2.agda 110
--- These two functions are also terminating. Due to the use of
--- "reverse" this is not apparent to the termination checker, though.
+-- The interpreter's result type.
+
+Dom : Ctxt -> Ty -> Set
+Dom Γ σ = Env ⟦_⟧⋆ Γ -> Cont ⟦ σ ⟧⋆
+
+-- These two functions are also terminating. Due to the use of reverse
+-- this is not apparent to the termination checker, though.
hunk ./Wand2.agda 120
-  ⟦_⟧ : forall {Γ σ} -> Γ ⊢ σ -> Env ⟦_⟧⋆ Γ -> Cont ⟦ σ ⟧⋆
+  ⟦_⟧ : forall {Γ σ} -> Γ ⊢ σ -> Dom Γ σ
hunk ./Wand2.agda 133
-            Env ⟦_⟧⋆ Γ -> Cont ⟦ τ ⟧⋆
+            Dom Γ τ
hunk ./Wand2.agda 147
+------------------------------------------------------------------------
+-- First step of the derivation: name subexpressions
+
+module Naming where
+
+  *fetch : forall {Γ τ} -> Γ ∋ τ -> Dom Γ τ
+  *fetch x = \ρ k -> k (Env-lookup x ρ)
+
+  *close : forall {Γ Γ⁺ τ} -> Dom (Γ ▻▻ Γ⁺) τ -> Dom Γ (Γ⁺ → τ)
+  *close v = \ρ k -> k (\vs k' -> v (ρ ▻▻▻ vs) k')
+
+  Dom' : Ctxt -> Ctxt -> Ty -> Set
+  Dom' Δ⁺ Γ τ = Env ⟦_⟧⋆ Δ⁺ -> Dom Γ τ
+
+  *clear-ev : forall {Γ τ} -> Dom' ε Γ τ -> Dom Γ τ
+  *clear-ev f = \ρ k -> f ε ρ k
+
+  *jsr : forall {Γ Δ⁺ σ τ} ->
+         Dom Γ σ -> Dom' (Δ⁺ ▻ σ) Γ τ -> Dom' Δ⁺ Γ τ
+  *jsr a as ρ' = \ρ k -> a ρ (\v -> as (ρ' ▻ ↦ v) ρ k)
+
+  *ev-fn : forall {Γ Γ⁺ τ} -> Dom Γ (Γ⁺ → τ) -> Dom' Γ⁺ Γ τ
+  *ev-fn f ρ' = \ρ k -> f ρ (\v -> v ρ' k)
+
+  -- Note that *jsr and *ev-fn have similar structure. Try to merge
+  -- them.
+
+  *ap : forall {Γ Γ⁺ τ} -> Dom' (Γ⁺ ▻ Γ⁺ → τ) Γ τ
+  *ap (↦ v ◅ ρ') ρ k = v ρ' k
+
+  -- Note that *ev-fn f = *jsr f *ap:
+
+  prop : forall {Γ Γ⁺ τ} (f : Dom Γ (Γ⁺ → τ)) (ρ' : Env ⟦_⟧⋆ Γ⁺) ->
+         *ev-fn {τ = τ} f ρ' ≡ *jsr {τ = τ} f (*ap {τ = τ}) ρ'
+  prop f ρ' = ≡-refl
+
+------------------------------------------------------------------------
+-- Second step: defunctionalise
+
+module Compiler where
+
+  mutual
+
+    data Code : Ctxt -> Ty -> Set where
+      *fetch    : forall {Γ τ} -> Γ ∋ τ -> Code Γ τ
+      *close    : forall {Γ Γ⁺ τ} ->
+                  Code (Γ ▻▻ Γ⁺) τ -> Code Γ (Γ⁺ → τ)
+      *clear-ev : forall {Γ τ} -> Code' ε Γ τ -> Code Γ τ
+
+    data Code' : Ctxt -> Ctxt -> Ty -> Set where
+      *jsr : forall {Γ Δ⁺ σ τ} ->
+             Code Γ σ -> Code' (Δ⁺ ▻ σ) Γ τ -> Code' Δ⁺ Γ τ
+      *ap  : forall {Γ Γ⁺ τ} -> Code' (Γ⁺ ▻ Γ⁺ → τ) Γ τ
+
+  -- Compiler. It is terminating, but the use of reverse means that
+  -- the termination checker cannot see this.
+
+  mutual
+
+    comp : forall {Γ σ} -> Γ ⊢ σ -> Code Γ σ
+    comp (var x)   = *fetch x
+    comp (λ t)     = *close (comp t)
+    comp (t₁ · t₂) = *clear-ev (comp' t₁ (reverse id t₂))
+
+    comp' : forall {Γ Γ⁺ Δ⁺ τ} ->
+            Γ ⊢ Γ⁺ → τ ->
+            Star (flip₁ (DecoratedWith (\σ -> Γ ⊢ σ)))
+                 (nonEmpty Δ⁺) (nonEmpty Γ⁺) ->
+            Code' Δ⁺ Γ τ
+    comp' t₁ ε          = *jsr (comp t₁) *ap
+    comp' t₁ (↦ a ◅ as) = *jsr (comp a) (comp' t₁ as)
+
+------------------------------------------------------------------------
+-- Back to the example again
+
+module Example₃ (x : ε ⊢ base 0#) (y : ε ⊢ base 1#) where
+
+  open Example x y
+  open Compiler
+
+  code : Code ε (base 0#)
+  code = comp application
+