[Finished the code for rotation.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080305040437
 + Did this by specialising types. The code is currently a bit ugly. I
   would prefer more general types.
 + No correctness proof yet.
] hunk ./Wand.agda 259
+module Examples (X Y Z : Id) where
+
+  open Language
+  open Step₂'
+
+  -- Fig. 2(b) in Wand's paper.
+
+  fig2b : Exp' {C} _
+  fig2b = B []₁ l halt
+    where
+    llr : Exp' {K -> V -> C} _
+    llr = B (K ∷₁ V ∷₁ []₁) (fetch Y) add
+
+    ll : Exp' {K -> C} _
+    ll = B (K ∷₁ []₁) (fetch X) llr
+
+    lr : Exp' {K -> V -> C} _
+    lr = B (K ∷₁ V ∷₁ []₁) (fetch Z) add
+
+    l : Exp' {K -> C} _
+    l = B (K ∷₁ []₁) ll lr
+
+  -- Fig. 2(c) in Wand's paper.
+
+  fig2c : Exp' {C} _
+  fig2c = B []₁ (fetch X) step₂
+    where
+    step₆ : Exp' {V -> C} _
+    step₆ = halt
+
+    step₅ : Exp' {V -> V -> C} _
+    step₅ = B []₁ add step₆
+
+    step₄ : Exp' {V -> C} _
+    step₄ = B (V ∷₁ []₁) (fetch Z) step₅
+
+    step₃ : Exp' {V -> V -> C} _
+    step₃ = B []₁ add step₄
+
+    step₂ : Exp' {V -> C} _
+    step₂ = B (V ∷₁ []₁) (fetch Y) step₃
+
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).
+
hunk ./Wand.agda 344
-  -- A variant of Step₂' which uses the universe.
+  v^_→c : ℕ -> Ty
+  v^ n →c = fun (replicate n v) c
hunk ./Wand.agda 347
-  _⟪_⟫'_ : forall {a b} ->
-           ⟦ a → b ⟧⋆ -> (ts : [ Ty ]) -> ⟦ fun ts a ⟧⋆ -> ⟦ fun ts b ⟧⋆
-  f ⟪ τs ⟫' g = ≡₁-subst (≡₁-sym (lemma τs))
-                         (f ⟪ map₀₁ ⟦_⟧⋆ τs ⟫ ≡₁-subst (lemma τs) g)
+  _⟪_⟫'_ : ⟦ k → c ⟧⋆ -> (n : ℕ) -> ⟦ k → v^ suc n →c ⟧⋆ ->
+           ⟦ k → v^ n →c ⟧⋆
+  f ⟪ n ⟫' g = ≡₁-subst lem (f ⟪ map₀₁ ⟦_⟧⋆ ts ⟫ ≡₁-subst lem' g)
+    where
+    ts = k ∷ replicate n v
hunk ./Wand.agda 353
-  -- Step₂ can be simplified by indexing the Exp' type on the
-  -- semantics of expressions:
+    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)
hunk ./Wand.agda 358
-  data Exp' : (t : Ty) -> ⟦ t ⟧⋆ -> Set where
-    B     : forall {a b} ts {f g} ->
-            Exp' (a → b) f -> Exp' (fun ts a) g ->
-            Exp' (fun ts b) (f ⟪ ts ⟫' g)
-    add   : Exp' (k → v → v → c) Step₁.add
-    fetch : (I : Id) -> Exp' (k → c) (Step₁.fetch I)
-    halt  : Exp' k Step₁.halt
+    lem  = ≡₁-sym (lemma ts)
+    lem' = ≡₁-cong (\t -> K -> t) (lemma₂ n)
hunk ./Wand.agda 361
-  -- The semantics is encoded in the type:
+  data Exp' : (n : ℕ) -> ⟦ k → v^ n →c ⟧⋆ -> Set where
+    B     : forall {n f g} ->
+            Exp' 0 f -> Exp' (suc n) g -> Exp' n (f ⟪ n ⟫' g)
+    add   : Exp' 2 Step₁.add
+    fetch : (I : Id) -> Exp' 0 (Step₁.fetch I)
hunk ./Wand.agda 367
-  ⟦_⟧ : forall {t f} -> Exp' t f -> ⟦ t ⟧⋆
-  ⟦_⟧ {f = f} _ = f
+  data ToplevelExp : (t : Ty) -> ⟦ t ⟧⋆ -> Set where
+    Bhalt : forall {f} -> Exp' 0 f -> ToplevelExp c (f Step₁.halt)
hunk ./Wand.agda 372
-  comp : (e : Exp) -> Exp' (k → c) (Step₁.E' e)
-  comp (id I)      = fetch I
-  comp [ e₁ + e₂ ] = B (k ∷ []) (comp e₁) (B (k ∷ v ∷ []) (comp e₂) add)
+  comp' : (e : Exp) -> Exp' 0 (Step₁.E' e)
+  comp' (id I)      = fetch I
+  comp' [ e₁ + e₂ ] = B (comp' e₁) (B (comp' e₂) add)
hunk ./Wand.agda 378
-  -- We can still combine the proofs:
+  -- Top-level compiler:
+
+  comp : (e : Exp) -> ToplevelExp c (Step₁.P' e)
+  comp e = Bhalt (comp' e)
+
+  -- Correctness:
hunk ./Wand.agda 385
-  correct : forall e -> E e ≡ ⟦ comp e ⟧
+  ⟦_⟧ : forall {t f} -> ToplevelExp t f -> ⟦ t ⟧⋆
+  ⟦_⟧ {f = f} _ = f
+
+  correct : forall e -> P e ≡ ⟦ comp e ⟧
hunk ./Wand.agda 390
-    E e
-      ≡⟨ proof (Step₁.E'P e) ⟩
-    Step₁.E' e
+    P e
+      ≡⟨ proof (Step₁.P'P e) ⟩
+    Step₁.P' e
hunk ./Wand.agda 397
-module Examples (X Y Z : Id) where
-
-  open Universe
-  open Step₂''
-
-  -- Fig. 2(b) in Wand's paper.
-
-  fig2b : Exp' c _
-  fig2b = B [] l halt
-    where
-    llr : Exp' (k → v → c) _
-    llr = B (k ∷ v ∷ []) (fetch Y) add
-
-    ll : Exp' (k → c) _
-    ll = B (k ∷ []) (fetch X) llr
-
-    lr : Exp' (k → v → c) _
-    lr = B (k ∷ v ∷ []) (fetch Z) add
-
-    l : Exp' (k → c) _
-    l = B (k ∷ []) ll lr
-
-  -- Fig. 2(c) in Wand's paper.
-
-  fig2c : Exp' c _
-  fig2c = B [] (fetch X) step₂
-    where
-    step₆ : Exp' (v → c) _
-    step₆ = halt
-
-    step₅ : Exp' (v → v → c) _
-    step₅ = B [] add step₆
-
-    step₄ : Exp' (v → c) _
-    step₄ = B (v ∷ []) (fetch Z) step₅
-
-    step₃ : Exp' (v → v → c) _
-    step₃ = B [] add step₄
-
-    step₂ : Exp' (v → c) _
-    step₂ = B (v ∷ []) (fetch Y) step₃
-
hunk ./Wand.agda 400
+  open Step₂'' using (v^_→c)
hunk ./Wand.agda 408
-  fun' : ℕ -> Ty
-  fun' zero    = c
-  fun' (suc n) = v → fun' n
-
-  ⟦_⟧c : forall {n} -> Command n -> ⟦ k → fun' n ⟧⋆
+  ⟦_⟧c : forall {n} -> Command n -> ⟦ k → v^ n →c ⟧⋆
hunk ./Wand.agda 419
-  -- Let's try to implement Wand's rotation.
+  -- Wand's rotation implemented in a continuation-passing style to
+  -- ensure that it is well-typed and structurally recursive.
hunk ./Wand.agda 425
-  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 : 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)
+
+  toplevelRot : forall {t f} -> Step₂''.ToplevelExp t f -> LinearExp 0
+  toplevelRot (Step₂''.Bhalt e) = rot e halt
hunk ./Wand.agda 433
-  rot 0                   Step₂''.halt ()
-  rot 1                   Step₂''.halt ()
-  rot 2                   Step₂''.halt ()
-  rot (suc (suc (suc _))) Step₂''.halt ()
+  -- TODO: Correctness.