[Broke out the stack code to a separate section.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091105001251
 Ignore-this: f13672eea1fe4cc2212c6782546bd03
] hunk ./ApplicationBased.agda 37
--- First step: Rewrite the evaluator
+-- Stacks
hunk ./ApplicationBased.agda 39
-module Step₁ where
+-- 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
hunk ./ApplicationBased.agda 53
-  -- 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.
+-- 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
hunk ./ApplicationBased.agda 57
-  _^_ : Set → ℕ → Set
-  A ^ zero  = A
-  A ^ suc n = A → A ^ n
+_<$_$>_ : ∀ {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
hunk ./ApplicationBased.agda 80
-  -- 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
-
hunk ./ApplicationBased.agda 103
-  open Step₁ using (_^_; _<$_$>_)
-
hunk ./ApplicationBased.agda 123
-  open Step₁ using (_^_; _<$_$>_)
-  open Step₂ hiding (Cmd; comp)
+  open Step₂ hiding (comp)
+  open Step₂ hiding (comp) renaming (return to push)
hunk ./ApplicationBased.agda 126
-  Stack : ℕ → Set
-  Stack = Vec ℕ
-
-  -- The commands and the code type are indexed on initial and final
-  -- stack depth, plus their semantics.
+  -- The code type is indexed on initial and final stack depth, plus
+  -- its semantics.
hunk ./ApplicationBased.agda 130
-  Sem i f = Stack i → Stack f
-
-  -- app interprets functions of type ℕ ^ m:
-  --
-  --   app m f (x₁ ∷ … ∷ x_m ∷ ys) = f x_m … x₁ ∷ ys
-
-  app : ∀ 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
-
-  data Cmd : (i f : ℕ) → Sem i f → Set where
-    push : ∀ {n} (x : ℕ) → Cmd n (1 + n) (app 0 x)
-    sub  : ∀ {n} → Cmd (2 + n) (1 + n) (app 2 _∸_)
+  Sem i f = Stack ℕ i → Stack ℕ f
hunk ./ApplicationBased.agda 134
-    _◅_ : ∀ {i m f s₁ s₂} →
-          Cmd i m s₁ → Code m f s₂ → Code i f (s₂ ∘ s₁)
+    _◅_ : ∀ {n g i f s} →
+          Step₂.Cmd n g → Code (1 + i) f s →
+          Code (n + i) f (s ∘ app n g)
hunk ./ApplicationBased.agda 140
-  exec : ∀ {m n sem} → Code m n sem → Stack m → Stack n
+  exec : ∀ {m n sem} → Code m n sem → Sem m n
hunk ./ApplicationBased.agda 147
-    exec' : ∀ {m n sem} → Code m n sem → Stack m → Stack n
+    exec' : ∀ {m n sem} → Code m n sem → Sem m n
hunk ./ApplicationBased.agda 155
-    execOK : ∀ {m n sem} (cs : Code m n sem) (s : Stack m) →
+    execOK : ∀ {m n sem} (cs : Code m n sem) (s : Stack ℕ m) →