[Set the stage to prove correctness of rotation.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080305143644
 + Cleaned up the code, proved some lemmas, stated correctness.
] hunk ./Wand.agda 30
+open import Algebra.Structures
+open import Data.Nat.Properties
hunk ./Wand.agda 222
-module Step₂' where
+module Step₂′ where
hunk ./Wand.agda 264
-  open Step₂'
+  open Step₂′
hunk ./Wand.agda 306
-  open import Data.List
hunk ./Wand.agda 311
+  -- TODO: Is this actually used in the final version of the code?
+
hunk ./Wand.agda 332
-  lemma : forall σs {τ} ->
-          ⟦ fun σs τ ⟧⋆ ≡₁ Fun (map₀₁ ⟦_⟧⋆ σs) ⟦ τ ⟧⋆
-  lemma []       = ≡₁-refl
-  lemma (σ ∷ σs) = ≡₁-cong (\t -> ⟦ σ ⟧⋆ -> t) (lemma σs)
+  -- The following type constructor is used a lot below.
hunk ./Wand.agda 334
-module Step₂'' where
+  infixr 5 _^_→_
hunk ./Wand.agda 336
-  -- 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).
+  _^_→_ : Ty -> ℕ -> Ty -> Ty
+  a ^ n → b = fun (replicate n a) b
hunk ./Wand.agda 339
-  open Language
-  open Universe
+  -- A bunch of lemmas about it.
+
+  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)
+
+  shift-lemma : forall {a b} n ->
+                ⟦ a ^ suc n → b ⟧⋆ ≡₁ ⟦ a ^ n → (a → b) ⟧⋆
+  shift-lemma     zero    = ≡₁-refl
+  shift-lemma {a} (suc n) = ≡₁-cong (\t -> ⟦ a ⟧⋆ -> t) (shift-lemma n)
+
+  merge-lemma : forall {a b} m n ->
+                ⟦ a ^ m → a ^ n → b ⟧⋆ ≡₁ ⟦ a ^ m + n → b ⟧⋆
+  merge-lemma     zero    n = ≡₁-refl
+  merge-lemma {a} (suc m) n =
+    ≡₁-cong (\t -> ⟦ a ⟧⋆ -> t) (merge-lemma m n)
+
+  swap-lemma : forall {a b} m n ->
+               ⟦ a ^ m + n → b ⟧⋆ ≡₁ ⟦ a ^ n + m → b ⟧⋆
+  swap-lemma m n with n + m | +-comm m n
+    where open IsCommutativeSemiring _ ℕ-isCommutativeSemiring
+  ... | ._ | ≡-refl = ≡₁-refl
+
+  -- Variants of _⟪_⟫_.
+
+  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₂)
hunk ./Wand.agda 373
-  v^_→c : ℕ -> Ty
-  v^ n →c = fun (replicate n v) c
+  B⋆′ : forall n ->
+        ⟦ k → c ⟧⋆ -> ⟦ k → v ^ suc n → c ⟧⋆ -> ⟦ k → v ^ n → c ⟧⋆
+  B⋆′ n f g = B⋆ [] (k ∷ replicate n v) f (cast g)
+    where cast = ≡₁-subst (≡₁-cong (\t -> K -> t) (shift-lemma n))
hunk ./Wand.agda 378
-  _⟪_⟫'_ : ⟦ k → c ⟧⋆ -> (n : ℕ) -> ⟦ k → v^ suc n →c ⟧⋆ ->
-           ⟦ k → v^ n →c ⟧⋆
-  f ⟪ n ⟫' g = ≡₁-subst lem (f ⟪ map₀₁ ⟦_⟧⋆ ts ⟫ ≡₁-subst lem' g)
+  B⋆″ : forall m n ->
+        ⟦ 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))
hunk ./Wand.agda 382
-    ts = k ∷ replicate n v
+    cast₁ = ≡₁-subst (≡₁-trans (merge-lemma n m) (swap-lemma n m))
+    cast₂ = ≡₁-subst (shift-lemma n)
hunk ./Wand.agda 385
-    lemma₂ : forall n -> ⟦ fun (replicate (suc n) v) c ⟧⋆ ≡₁
-                         Fun (map₀₁ ⟦_⟧⋆ (replicate n v)) K
-    lemma₂ zero    = ≡₁-refl
-    lemma₂ (suc n) = ≡₁-cong (\t -> ℕ -> t) (lemma₂ n)
+  rot-lemma
+    : forall m n f g h ->
+      B⋆″ 0 (m + n) f (B⋆″ (suc m) n g h) ≡ B⋆″ m n (B⋆′ m f g) h
+  rot-lemma = {! !}
hunk ./Wand.agda 390
-    lem  = ≡₁-sym (lemma ts)
-    lem' = ≡₁-cong (\t -> K -> t) (lemma₂ n)
+module Step₂″ where
hunk ./Wand.agda 392
-  data Exp' : (n : ℕ) -> ⟦ k → v^ n →c ⟧⋆ -> Set where
+  -- 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).
+
+  open Language
+  open Universe
+
+  data Exp' : (n : ℕ) -> ⟦ k → v ^ n → c ⟧⋆ -> Set where
hunk ./Wand.agda 402
-            Exp' 0 f -> Exp' (suc n) g -> Exp' n (f ⟪ n ⟫' g)
+            Exp' 0 f -> Exp' (suc n) g -> Exp' n (B⋆′ n f g)
hunk ./Wand.agda 406
-  data ToplevelExp : (t : Ty) -> ⟦ t ⟧⋆ -> Set where
-    Bhalt : forall {f} -> Exp' 0 f -> ToplevelExp c (f Step₁.halt)
+  data ToplevelExp : ⟦ c ⟧⋆ -> Set where
+    Bhalt : forall {f} -> Exp' 0 f -> ToplevelExp (f Step₁.halt)
hunk ./Wand.agda 415
-  -- Note: Now we are using some proof code. See _⟪_⟫'_ above.
+  -- Note: Now we are using some proof code. See the definition of
+  -- B⋆′, which is used to type B above.
hunk ./Wand.agda 420
-  comp : (e : Exp) -> ToplevelExp c (Step₁.P' e)
+  comp : (e : Exp) -> ToplevelExp (Step₁.P' e)
hunk ./Wand.agda 425
-  ⟦_⟧ : forall {t f} -> ToplevelExp t f -> ⟦ t ⟧⋆
+  ⟦_⟧ : forall {f} -> ToplevelExp f -> ⟦ c ⟧⋆
hunk ./Wand.agda 439
-  open Universe
-  open Step₂'' using (v^_→c)
-
-  -- Command n represents expressions of type k → vⁿ → c.
-
-  data Command : ℕ -> Set where
-    add   : Command 2
-    fetch : Id -> Command 0
+  -- Let's implement Wand's rotation.
hunk ./Wand.agda 441
-  ⟦_⟧c : forall {n} -> Command n -> ⟦ k → v^ n →c ⟧⋆
-  ⟦ add ⟧c     = Step₁.add
-  ⟦ fetch I ⟧c = Step₁.fetch I
+  open Universe
hunk ./Wand.agda 443
-  -- LinearExp n represents expressions of type vⁿ → c.
+  data Command : (n : ℕ) -> ⟦ k → v ^ n → c ⟧⋆ -> Set where
+    add   : Command 2 Step₁.add
+    fetch : (I : Id) -> Command 0 (Step₁.fetch I)
hunk ./Wand.agda 447
-  data LinearExp : ℕ -> Set where
-    _○_  : forall {m n} ->
-           Command m -> LinearExp (suc n) -> LinearExp (m + n)
-    halt : LinearExp 1
+  data LinearExp : (n : ℕ) -> ⟦ v ^ n → c ⟧⋆ -> Set where
+    _○_  : forall {m n f g} ->
+           Command m f -> LinearExp (suc n) g -> LinearExp (m + n) (B⋆″ m n f g)
+    halt : LinearExp 1 Step₁.halt
hunk ./Wand.agda 455
-  Cont : ℕ -> Set
-  Cont m = forall {n} -> LinearExp (suc n) -> LinearExp (m + n)
-
-  rot : forall {m f} -> Step₂''.Exp' m f -> Cont m
-  rot Step₂''.add       = \k -> add ○ k
-  rot (Step₂''.fetch I) = \k -> fetch I ○ k
-  rot (Step₂''.B e₁ e₂) = \k -> rot e₁ (rot e₂ k)
+  Cont : (m : ℕ) -> ⟦ k → v ^ m → c ⟧⋆ -> Set
+  Cont m f = forall {n g} ->
+             LinearExp (suc n) g -> LinearExp (m + n) (B⋆″ m n f g)
hunk ./Wand.agda 459
-  toplevelRot : forall {t f} -> Step₂''.ToplevelExp t f -> LinearExp 0
-  toplevelRot (Step₂''.Bhalt e) = rot e halt
+  rot : forall {m f} -> Step₂″.Exp' m f -> Cont m f
+  rot Step₂″.add                           = \k -> add ○ k
+  rot (Step₂″.fetch I)                     = \k -> fetch I ○ k
+  rot (Step₂″.B {m} {f} {g} e₁ e₂) {n} {h} =
+    \k -> cast (rot e₁ (rot e₂ k)) (rot-lemma m n f g h)
+    where
+    cast : forall {n f g} -> LinearExp n f -> f ≡ g -> LinearExp n g
+    cast e ≡-refl = e
hunk ./Wand.agda 468
-  -- TODO: Correctness.
+  toplevelRot : forall {f} -> Step₂″.ToplevelExp f -> LinearExp 0 f
+  toplevelRot (Step₂″.Bhalt e) = rot e halt