[Added some combinators which manipulate the "stack" of arguments.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101216163215
 Ignore-this: ec329f09f53ecb94459e9c732ca3a46b
] hunk ./CompositionBased/Lambda.agda 22
-  hiding (module Derivation; app)
+  hiding (module Derivation; app; push)
hunk ./CompositionBased/Lambda.agda 105
-  drop : ∀ {Γ σ τ} → Dom Γ σ → Dom (τ ∷ Γ) σ
-  drop d = Λ λ _ → d
-
hunk ./CompositionBased/Lambda.agda 122
-      drop (lookup x)                  ∎
+      wk (lookup x)                    ∎
hunk ./CompositionBased/Lambda.agda 126
-  push : ∀ {Bs} {A C : Set} → A ∷ Bs ⇨ C → Bs ⇨ (A → C)
-  push f = RC.curry (λ bs a → RC.uncurry f (a , bs))
-
-  push-cong : ∀ {Bs} {A C : Set} {f₁ f₂ : A ∷ Bs ⇨ C} →
-              f₁ ≈ f₂ → push f₁ ≈ push f₂
-  push-cong f₁≈f₂ =
-    curry-cong λ bs →
-    ext λ a →
-    uncurry-cong f₁≈f₂ (a , bs)
-
hunk ./CompositionBased/Lambda.agda 146
-      push (RC.curry ⟦ t ⟧S)                        ≈⟨ push-cong (proof ⟦ t ⟧′) ⟩
-      push ⟦ t ⟧                                    ∎
+      RC.push (RC.curry ⟦ t ⟧S)                     ≈⟨ Stack.push-cong ext (proof ⟦ t ⟧′) ⟩
+      RC.push ⟦ t ⟧                                 ∎
hunk ./CompositionBased/Lambda.agda 197
-  drop κ d = κ (C.drop d)
+  drop κ d = κ (wk d)
hunk ./CompositionBased/Lambda.agda 214
-      κ (C.drop (C.lookup x))  ≡⟨ P.refl ⟩
+      κ (wk (C.lookup x))      ≡⟨ P.refl ⟩
hunk ./CompositionBased/Lambda.agda 227
-  push κ f = κ (C.push f)
+  push κ f = κ (RC.push f)
hunk ./CompositionBased/Lambda.agda 251
-      κ ⟦ ƛ t ⟧C         ≡⟨ P.refl ⟩
-      κ (C.push ⟦ t ⟧C)  ≡⟨ P.refl ⟩
-      push κ ⟦ t ⟧C      ≡⟨ proof (⟦ t ⟧′ (push κ)) ⟩
-      ⟦ t ⟧ (push κ)     ∎
+      κ ⟦ ƛ t ⟧C          ≡⟨ P.refl ⟩
+      κ (RC.push ⟦ t ⟧C)  ≡⟨ P.refl ⟩
+      push κ ⟦ t ⟧C       ≡⟨ proof (⟦ t ⟧′ (push κ)) ⟩
+      ⟦ t ⟧ (push κ)      ∎
hunk ./ReverseComposition.agda 628
+
+------------------------------------------------------------------------
+-- Some combinators which manipulate the "stack" of arguments
+
+-- Discards the top-most stack element.
+
+wk : ∀ {ℓ As} {A B : Set ℓ} → As ⇨ B → A ∷ As ⇨ B
+wk f = Λ λ _ → f
+
+-- Reverse application.
+
+reverse-app : ∀ {ℓ As} {B C D : Set ℓ} →
+              C ∷ As ⇨ D → B ∷ (B → C) ∷ As ⇨ D
+reverse-app g = Λ λ x → Λ λ f → g · f x
+
+-- Pushes an argument onto the stack.
+
+push : ∀ {ℓ Bs} {A C : Set ℓ} → A ∷ Bs ⇨ C → Bs ⇨ (A → C)
+push f = curry (λ bs a → uncurry f (a , bs))
+
+-- Pops the stack.
+
+pop : ∀ {ℓ Bs} {A C : Set ℓ} → Bs ⇨ (A → C) → A ∷ Bs ⇨ C
+pop f = Λ λ x → map (λ g → g x) f
+
+module Stack {ℓ} where
+
+  open ≈-Reasoning
+
+  wk-reverse-app :
+    ∀ {As} {B C D : Set ℓ}
+    (f : As ⇨ (B → C)) (g : As ⇨ B) (h : C ∷ As ⇨ D) →
+    (f ⊛∥ g) ⊙∥ h ≈ f ⊙∥ wk g ⊙∥ reverse-app h
+  wk-reverse-app f g h =
+    (f ⊛∥ g) ⊙∥ h                      ≡⟨ P.refl ⟩
+    (f >>=∥ λ f → map f g) >>=∥ _·_ h  ≈⟨ assoc f (λ f → map f g) (_·_ h) ⟩
+    (f >>=∥ λ f → map f g >>=∥ _·_ h)  ≈⟨ (refl f >>=∥-cong′ λ f → MoreLaws∥.map->>=∥ f g (_·_ h)) ⟩
+    (f >>=∥ λ f → g >>=∥ _·_ h ∘ f)    ≡⟨ P.refl ⟩
+    f ⊙∥ wk g ⊙∥ reverse-app h         ∎
+    where open MonadLaws∥
+
+  map-push : ∀ {Bs} {A C : Set ℓ} (f : A ∷ Bs ⇨ C) x →
+             map (λ f → f x) (push f) ≈ f · x
+  map-push {Bs} f x =
+    map (λ f → f x) (push f)                             ≈⟨ MoreLaws∥.map-curry-uncurry (λ f → f x) (push f) ⟩
+    curry (λ bs → uncurry (push f) bs x)                 ≡⟨ P.refl ⟩
+    curry (λ bs →
+      uncurry {B = _ → _}
+        (curry {As = Bs} (λ bs x → uncurry f (x , bs)))
+        bs x)                                            ≈⟨ curry-cong (λ bs → P.cong (λ (f : _ → _) → f x) $
+                                                              uncurry∘curry Bs (λ bs x → uncurry f (x , bs)) bs) ⟩
+    curry (λ bs → uncurry f (x , bs))                    ≈⟨ curry∘uncurry (f · x) ⟩
+    f · x                                                ∎
+    where open CurryLaws
+
+  push-cong : P.Extensionality ℓ ℓ →
+              ∀ {Bs} {A C : Set ℓ} {f₁ f₂ : A ∷ Bs ⇨ C} →
+              f₁ ≈ f₂ → push f₁ ≈ push f₂
+  push-cong ext f₁≈f₂ =
+    curry-cong λ bs →
+    ext λ a →
+    uncurry-cong f₁≈f₂ (a , bs)
hunk ./ReverseComposition.agda 692
+  pop-cong : ∀ {Bs} {A C : Set ℓ} {f₁ f₂ : Bs ⇨ (A → C)} →
+             f₁ ≈ f₂ → pop f₁ ≈ pop f₂
+  pop-cong f₁≈f₂ = Λ-cong λ x →
+    MoreLaws∥.map-cong (λ g → P.refl {x = g x}) f₁≈f₂
+
+  push-pop : P.Extensionality ℓ ℓ →
+             ∀ {Bs} {A C : Set ℓ} (f : Bs ⇨ (A → C)) →
+             push (pop f) ≈ f
+  push-pop ext {Bs} f =
+    push (pop f)                                             ≡⟨ P.refl ⟩
+    push (Λ λ a → map (λ g → g a) f)                         ≈⟨ push-cong ext (Λ-cong λ a → MoreLaws∥.map-curry-uncurry (λ g → g a) f) ⟩
+    push (Λ λ a → curry (λ bs → uncurry f bs a))             ≡⟨ P.refl ⟩
+    curry (λ bs a →
+      uncurry (curry {As = Bs} (λ bs → uncurry f bs a)) bs)  ≈⟨ curry-cong (λ bs → ext λ a →
+                                                                  uncurry∘curry Bs (λ bs → uncurry f bs a) bs) ⟩
+    curry (λ bs a → uncurry f bs a)                          ≡⟨ P.refl ⟩
+    curry (uncurry f)                                        ≈⟨ curry∘uncurry f ⟩
+    f                                                        ∎
+    where open CurryLaws
+
+  pop-push : ∀ {Bs} {A C : Set ℓ} (f : A ∷ Bs ⇨ C) →
+             pop (push f) ≈ f
+  pop-push f = Λ-cong λ a →
+    map (λ g → g a) (push f)  ≈⟨ map-push f a ⟩
+    f · a                     ∎
+