[Started on the rotation code.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080305025625
 + In order to continue I need to either generalise the type of the
   resulting linear expressions, or specialise the types of the
   input expressions.
] hunk ./Wand.agda 268
-  infixr 0 _→_
+  infixr 5 _→_
hunk ./Wand.agda 381
+module Step₃ where
+
+  open Universe
+
+  -- Command n represents expressions of type k → vⁿ → c.
+
+  data Command : ℕ -> Set where
+    add   : Command 2
+    fetch : Id -> Command 0
+
+  fun' : ℕ -> Ty
+  fun' zero    = c
+  fun' (suc n) = v → fun' n
+
+  ⟦_⟧c : forall {n} -> Command n -> ⟦ k → fun' n ⟧⋆
+  ⟦ add ⟧c     = Step₁.add
+  ⟦ fetch I ⟧c = Step₁.fetch I
+
+  -- LinearExp n represents expressions of type vⁿ → c.
+
+  data LinearExp : ℕ -> Set where
+    _○_  : forall {m n} ->
+           Command m -> LinearExp (suc n) -> LinearExp (m + n)
+    halt : LinearExp 1
+
+  -- Let's try to implement Wand's rotation.
+
+  Cont : ℕ -> Set
+  Cont m = forall {n} -> LinearExp (suc n) -> LinearExp (m + n)
+
+  rot : forall m {t f} -> Step₂''.Exp' t f -> t ≡ k → fun' m -> Cont m
+  rot 2 Step₂''.add                            ≡-refl = \k -> add ○ k
+  rot 0 (Step₂''.fetch I)                      ≡-refl = \k -> fetch I ○ k
+  rot m (Step₂''.B (k ∷ ts) e₁ e₂)             eq     = \k -> {!rot 0 e₁ !}
+  rot m (Step₂''.B .{b = k → fun' m} [] e₁ e₂) ≡-refl = \k -> {!rot _ e₂ !}
+
+  -- Impossible cases:
+
+  rot 0                   Step₂''.add ()
+  rot 1                   Step₂''.add ()
+  rot (suc (suc (suc _))) Step₂''.add ()
+
+  rot (suc _) (Step₂''.fetch I) ()
+
+  rot 0                   Step₂''.halt ()
+  rot 1                   Step₂''.halt ()
+  rot 2                   Step₂''.halt ()
+  rot (suc (suc (suc _))) Step₂''.halt ()
+