[Simplified the proof again.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080514102418] hunk ./ApplicationBased.agda 14
-open import Data.Star hiding (return; reverse)
hunk ./ApplicationBased.agda 15
+open import Data.Function
hunk ./ApplicationBased.agda 103
+  Stack : ℕ -> Set
+  Stack = Vec ℕ
+
hunk ./ApplicationBased.agda 107
-  -- stack depth.
+  -- stack depth, plus their semantics.
hunk ./ApplicationBased.agda 109
-  data Cmd : ℕ -> ℕ -> Set where
-    push : forall {n} -> ℕ -> Cmd n (1 + n)
-    sub  : forall {n} -> Cmd (2 + n) (1 + n)
+  Sem : ℕ -> ℕ -> Set
+  Sem i f = Stack i -> Stack f
hunk ./ApplicationBased.agda 112
-  Code : ℕ -> ℕ -> Set
-  Code = Star Cmd
+  app : forall m {n} -> ℕ ^ m -> Sem (m + n) (1 + n)
+  app zero    f xs       = f ∷ xs
+  app (suc m) f (x ∷ xs) = app m (x <$ m $> f) xs
hunk ./ApplicationBased.agda 116
-  Stack : ℕ -> Set
-  Stack = Vec ℕ
+  data Cmd : (i f : ℕ) -> Sem i f -> Set where
+    push : forall {n} (x : ℕ) -> Cmd n (1 + n) (app 0 x)
+    sub  : forall {n} -> Cmd (2 + n) (1 + n) (app 2 _∸_)
+
+  data Code : (i f : ℕ) -> Sem i f -> Set where
+    ε   : forall {i} -> Code i i id
+    _◅_ : forall {i m f s₁ s₂} ->
+          Cmd i m s₁ -> Code m f s₂ -> Code i f (s₂ ∘ s₁)
hunk ./ApplicationBased.agda 127
-  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)
+  exec : forall {m n sem} -> Code m n sem -> Stack m -> Stack n
+  exec {sem = sem} _ = sem
hunk ./ApplicationBased.agda 130
-  -- Correct compiler.
+  module Details where
hunk ./ApplicationBased.agda 132
-  app : forall {a} m {n} -> a ^ m -> Vec a (m + n) -> Vec a (1 + n)
-  app zero    f xs       = f ∷ xs
-  app (suc m) f (x ∷ xs) = app m (x <$ m $> f) xs
+    -- The virtual machine is actually a virtual machine.
hunk ./ApplicationBased.agda 134
-  mutual
+    exec' : forall {m n sem} -> Code m n sem -> Stack m -> Stack n
+    exec' ε             s           = s
+    exec' (push x ◅ cs) s           = exec' cs (x ∷ s)
+    exec' (sub    ◅ cs) (n ∷ m ∷ s) = exec' cs (m ∸ n ∷ s)
hunk ./ApplicationBased.agda 139
-    comp : forall {m n f} ->
-           Tree m f -> Code (1 + n) 1 -> Code (m + n) 1
-    comp t cs = proj₁ (compP t cs)
+    -- The structure of this proof shows that exec and exec' are
+    -- _identical_ (modulo normalisation).
+
+    execOK : forall {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.
hunk ./ApplicationBased.agda 150
-    compP : forall {m n f} (t : Tree m f) (cs : Code (1 + n) 1) ->
-            Σ (Code (m + n) 1) \cs' ->
-              forall s -> exec cs (app m f s) ≡ exec cs' s
-    compP (cmd (return n)) cs = (push n ◅ cs , \s -> begin
-                                                 exec cs (n ∷ s)
-                                                   ≡⟨ ≡-refl ⟩
-                                                 exec (push n ◅ cs) s
-                                                   ∎)
-    compP (cmd sub) cs = (sub ◅ cs , prf)
-      where
-      prf : (s : Stack (2 + _)) ->
-            exec cs (app 2 Step₁.sub s) ≡ exec (sub ◅ cs) s
-      prf (n ∷ m ∷ s) = begin
-        exec cs (m ∸ n ∷ s)
-          ≡⟨ ≡-refl ⟩
-        exec (sub ◅ cs) (n ∷ m ∷ s)
-          ∎
-    compP (_$$_ {n} {x} {f} t₁ t₂) cs =
-      (comp t₁ (comp t₂ cs) , \s -> begin
-                                exec cs (app n (x <$ n $> f) s)
-                                  ≡⟨ ≡-refl ⟩
-                                exec cs (app (suc n) f (x ∷ s))
-                                  ≡⟨ proj₂ (compP t₂ cs) (x ∷ s) ⟩
-                                exec (comp t₂ cs) (x ∷ s)
-                                  ≡⟨ proj₂ (compP t₁ (comp t₂ cs)) s ⟩
-                                exec (comp t₁ (comp t₂ cs)) s
-                                  ∎)
+  comp : forall {m n f sem} ->
+         Tree m f -> Code (1 + n) 1 sem ->
+         Code (m + n) 1 (sem ∘ app m f)
+  comp (cmd (return n)) cs = push n ◅ cs
+  comp (cmd sub)        cs = sub ◅ cs
+  comp (t₁ $$ t₂)       cs = comp t₁ (comp t₂ cs)
hunk ./ApplicationBased.agda 163
-  Code = Step₃.Code 0 1
+  Code = Σ₀ (Step₃.Code 0 1)
hunk ./ApplicationBased.agda 166
-  comp e = Step₃.comp (Step₂.comp e) ε
+  comp e = (_ , Step₃.comp (Step₂.comp e) Step₃.ε)
hunk ./ApplicationBased.agda 169
-  exec cs = head (Step₃.exec cs [])
+  exec cs = head (Step₃.exec (proj₂ cs) [])
hunk ./ApplicationBased.agda 172
-  correct e = ≡-cong head (proj₂ (Step₃.compP (Step₂.comp e) ε) [])
+  correct e = ≡-refl