[Removed the universe, which turned out to be unnecessary.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080305234646
 + When I specialised the types the type indices turned into integers,
   so I did not need to pattern match on any elements of Set.
] hunk ./Wand.agda 303
-module Universe where
+module Stack where
hunk ./Wand.agda 307
-  -- To simplify the development, let's define a type ("universe")
-  -- capturing the types used. Having a representation for types means
-  -- that we can pattern match on them.
-
-  -- TODO: Is this actually used in the final version of the code?
-
-  infixr 5 _→_
-
-  data Ty : Set where
-    v   : Ty
-    c   : Ty
-    _→_ : Ty -> Ty -> Ty
-
-  ⟦_⟧⋆ : Ty -> Set
-  ⟦ v ⟧⋆     = V
-  ⟦ c ⟧⋆     = C
-  ⟦ σ → τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆
-
-  fun : [ Ty ] -> Ty -> Ty
-  fun []       τ = τ
-  fun (σ ∷ σs) τ = σ → fun σs τ
-
-  k : Ty
-  k = v → c
-
-  -- The following type constructor is used a lot below.
-
hunk ./Wand.agda 309
-  _^_→_ : Ty -> ℕ -> Ty -> Ty
-  a ^ n → b = fun (replicate n a) b
+  -- This type constructor is used by Wand to represent a stack:
hunk ./Wand.agda 311
-  -- A bunch of lemmas about it.
+  _^_→_ : Set -> ℕ -> Set -> Set
+  A ^ n → B = Fun (replicate₁ n A) B
hunk ./Wand.agda 314
-  fun-Fun-lemma : forall σs {τ} ->
-                  ⟦ fun σs τ ⟧⋆ ≡₁ Fun (map₀₁ ⟦_⟧⋆ σs) ⟦ τ ⟧⋆
-  fun-Fun-lemma []       = ≡₁-refl
-  fun-Fun-lemma (σ ∷ σs) =
-    ≡₁-cong (\t -> ⟦ σ ⟧⋆ -> t) (fun-Fun-lemma σs)
+  -- A bunch of lemmas about it.
hunk ./Wand.agda 316
-  shift-lemma : forall {a b} n ->
-                ⟦ a ^ suc n → b ⟧⋆ ≡₁ ⟦ a ^ n → (a → b) ⟧⋆
+  shift-lemma : forall {A B} n ->
+                A ^ suc n → B ≡₁ A ^ n → (A -> B)
hunk ./Wand.agda 319
-  shift-lemma {a} (suc n) = ≡₁-cong (\t -> ⟦ a ⟧⋆ -> t) (shift-lemma n)
+  shift-lemma {A} (suc n) = ≡₁-cong (\t -> A -> t) (shift-lemma n)
hunk ./Wand.agda 321
-  merge-lemma : forall {a b} m n ->
-                ⟦ a ^ m → a ^ n → b ⟧⋆ ≡₁ ⟦ a ^ m + n → b ⟧⋆
+  merge-lemma : forall {A B} m n ->
+                A ^ m → A ^ n → B ≡₁ A ^ m + n → B
hunk ./Wand.agda 324
-  merge-lemma {a} (suc m) n =
-    ≡₁-cong (\t -> ⟦ a ⟧⋆ -> t) (merge-lemma m n)
+  merge-lemma {A} (suc m) n = ≡₁-cong (\t -> A -> t) (merge-lemma m n)
hunk ./Wand.agda 326
-  swap-lemma : forall {a b} m n ->
-               ⟦ a ^ m + n → b ⟧⋆ ≡₁ ⟦ a ^ n + m → b ⟧⋆
+  swap-lemma : forall {A B} m n ->
+               A ^ m + n → B ≡₁ A ^ n + m → B
hunk ./Wand.agda 334
-  B⋆ : forall {a b} ts₁ ts₂ ->
-       ⟦ a → fun ts₁ b ⟧⋆ -> ⟦ fun ts₂ a ⟧⋆ -> ⟦ fun ts₂ (fun ts₁ b) ⟧⋆
-  B⋆ ts₁ ts₂ f g = cast₁ (f ⟪ map₀₁ ⟦_⟧⋆ ts₂ ⟫ cast₂ g)
-    where
-    cast₁ = ≡₁-subst (≡₁-sym (fun-Fun-lemma ts₂))
-    cast₂ = ≡₁-subst (fun-Fun-lemma ts₂)
+  B⋆ : forall {A B} Ts₁ Ts₂ ->
+       (A -> Fun Ts₁ B) -> Fun Ts₂ A -> Fun Ts₂ (Fun Ts₁ B)
+  B⋆ Ts₁ Ts₂ f g = f ⟪ Ts₂ ⟫ g
hunk ./Wand.agda 339
-        ⟦ k → c ⟧⋆ -> ⟦ k → v ^ suc n → c ⟧⋆ -> ⟦ k → v ^ n → c ⟧⋆
-  B⋆′ n f g = B⋆ [] (k ∷ replicate n v) f (cast g)
+        (K -> C) -> (K -> V ^ suc n → C) -> (K -> V ^ n → C)
+  B⋆′ n f g = B⋆ []₁ (K ∷₁ replicate₁ n V) f (cast g)
hunk ./Wand.agda 344
-        ⟦ k → v ^ m → c ⟧⋆ -> ⟦ v ^ 1 + n → c ⟧⋆ -> ⟦ v ^ m + n → c ⟧⋆
-  B⋆″ m n f g = cast₁ (B⋆ (replicate m v) (replicate n v) f (cast₂ g))
+        (K -> V ^ m → C) -> (V ^ suc n → C) -> (V ^ m + n → C)
+  B⋆″ m n f g = cast₁ (B⋆ (replicate₁ m V) (replicate₁ n V) f (cast₂ g))
hunk ./Wand.agda 357
-  -- A variant of Step₂′ which uses the universe.
-  --
-  -- Here I have chosen to specialise the types, and to also treat the
-  -- top-level compiler (P).
+  -- Yet another variant of Step₂. Here I have chosen to specialise
+  -- the types, and to include a version of the top-level compiler
+  -- (P).
hunk ./Wand.agda 362
-  open Universe
+  open Stack
hunk ./Wand.agda 364
-  data Exp' : (n : ℕ) -> ⟦ k → v ^ n → c ⟧⋆ -> Set where
+  data Exp' : (n : ℕ) -> (K -> V ^ n → C) -> Set where
hunk ./Wand.agda 370
-  data ToplevelExp : ⟦ c ⟧⋆ -> Set where
+  data ToplevelExp : C -> Set where
hunk ./Wand.agda 380
-  -- B⋆′, which is used to type B above.
+  -- B⋆′, which is used in the type of B above.
hunk ./Wand.agda 389
-  ⟦_⟧ : forall {f} -> ToplevelExp f -> ⟦ c ⟧⋆
+  ⟦_⟧ : forall {f} -> ToplevelExp f -> C
hunk ./Wand.agda 405
-  open Universe
+  open Language
+  open Stack
hunk ./Wand.agda 408
-  data Command : (n : ℕ) -> ⟦ k → v ^ n → c ⟧⋆ -> Set where
+  data Command : (n : ℕ) -> (K -> V ^ n → C) -> Set where
hunk ./Wand.agda 412
-  data LinearExp : (n : ℕ) -> ⟦ v ^ n → c ⟧⋆ -> Set where
+  data LinearExp : (n : ℕ) -> (V ^ n → C) -> Set where
hunk ./Wand.agda 414
-           Command m f -> LinearExp (suc n) g -> LinearExp (m + n) (B⋆″ m n f g)
+           Command m f -> LinearExp (suc n) g ->
+           LinearExp (m + n) (B⋆″ m n f g)
hunk ./Wand.agda 421
-  Cont : (m : ℕ) -> ⟦ k → v ^ m → c ⟧⋆ -> Set
+  Cont : (m : ℕ) -> (K -> V ^ m → C) -> Set
hunk ./Wand.agda 428
-  rot (Step₂″.B {m} {f} {g} e₁ e₂) {n} {h} =
-    \k -> cast (rot e₁ (rot e₂ k)) (rot-lemma m n f g h)
+  rot (Step₂″.B {m} {f} {g} e₁ e₂) {n} {h} = \k ->
+    cast (rot e₁ (rot e₂ k)) (rot-lemma m n f g h)