[Replaced calculated lookup functions with simpler ones.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101220170739
 Ignore-this: 2249827b2473ee03dd8edd14f36d1c48
] hunk ./CompositionBased/Lambda.agda 102
-  -- Compositional lookup.
+  -- One could calculate/devise some other definition of the lookup
+  -- function, but allowing the unary representation of variables to
+  -- affect the design of the machine/compiler seems like a bad idea.
hunk ./CompositionBased/Lambda.agda 106
-  mutual
-
-    lookup : ∀ {Γ σ} → Γ ∋ σ → Dom Γ σ
-    lookup x = witness (lookup′ x)
-
-    lookup′ : ∀ {Γ σ} (x : Γ ∋ σ) →
-              EqualTo (RC.curry (S.lookup x))
-    lookup′ (zero {Γ = Γ}) = ▷
-      RC.curry (S.lookup (zero {Γ = Γ}))  ≡⟨ P.refl ⟩
-      (Λ λ v → RC.curry (const v))        ≡⟨ P.refl ⟩
-      (Λ λ v → return∥ v)                 ≡⟨ P.refl ⟩
-      identity∥                           ∎
-
-    lookup′ (suc x) = ▷
-      RC.curry (S.lookup (suc x))      ≡⟨ P.refl ⟩
-      (Λ λ _ → RC.curry (S.lookup x))  ≈⟨ Λ-cong (λ _ → proof (lookup′ x)) ⟩
-      (Λ λ _ → lookup x)               ≡⟨ P.refl ⟩
-      wk (lookup x)                    ∎
+  lookup : ∀ {Γ σ} → Γ ∋ σ → Dom Γ σ
+  lookup x = RC.curry (S.lookup x)
hunk ./CompositionBased/Lambda.agda 124
-      RC.curry (S.lookup x)  ≈⟨ proof (lookup′ x) ⟩
+      RC.curry (S.lookup x)  ≡⟨ P.refl ⟩
hunk ./CompositionBased/Lambda.agda 173
-  -- Lookup. The lookup function doesn't need access to the stack, so
-  -- C.Dom and _⊙∥_ are used instead of Dom and [_]_◌_.
-
-  top : ∀ {Γ σ τ} → C.Dom (σ ∷ σ ∷ Γ) τ → C.Dom (σ ∷ Γ) τ
-  top κ = Λ λ v → κ ∙ v ∙ v
-
-  push-under : ∀ {Γ σ τ χ} →
-               C.Dom (σ ∷ τ ∷ Γ) χ → C.Dom (σ ∷ Γ) (τ ⟶ χ)
-  push-under κ = Λ λ v → push (κ ∙ v)
-
-  mutual
-
-    lookup : ∀ {Γ σ τ} → Γ ∋ σ → C.Dom (σ ∷ Γ) τ → C.Dom Γ τ
-    lookup x κ = witness (lookup′ x κ)
-
-    lookup′ : ∀ {Γ σ τ} (x : Γ ∋ σ) (κ : C.Dom (σ ∷ Γ) τ) →
-              EqualTo (C.lookup x ⊙∥ κ)
-    lookup′ zero κ = ▷
-      C.lookup zero ⊙∥ κ                        ≡⟨ P.refl ⟩
-      identity∥ ⊙∥ κ                            ≡⟨ P.refl ⟩
-      (Λ λ v → return∥ v) ⊙∥ κ                  ≡⟨ P.refl ⟩
-      (Λ λ v → return∥ v >>=∥ λ x → κ ∙ x ∙ v)  ≈⟨ Λ-cong (λ v → MonadLaws∥.left-identity (λ x → κ ∙ x ∙ v) v) ⟩
-      top κ                                     ∎
-
-    lookup′ (suc x) κ = ▷
-      C.lookup (suc x) ⊙∥ κ                               ≡⟨ P.refl ⟩
-      wk (C.lookup x) ⊙∥ κ                                ≡⟨ P.refl ⟩
-      (Λ λ v → C.lookup x >>=∥ λ x → κ ∙ x ∙ v)           ≈⟨ Λ-cong (λ v → refl (C.lookup x) >>=∥-cong′ λ x →
-                                                                           sym $ Stack.map-push (κ ∙ x) v) ⟩
-      (Λ λ v → C.lookup x >>=∥ λ x →
-               RC.map (λ f → f v) (push (κ ∙ x)))         ≈⟨ Λ-cong (λ v → sym $
-                                                               map->>=∥′ (λ f → f v) (C.lookup x) (λ x → push (κ ∙ x))) ⟩
-      (Λ λ v → RC.map (λ f → f v) (C.lookup x >>=∥ λ x →
-                                   push (κ ∙ x)))         ≡⟨ P.refl ⟩
-      pop (C.lookup x ⊙∥ push-under κ)                    ≈⟨ Stack.pop-cong $ proof $ lookup′ x (push-under κ) ⟩
-      pop (lookup x (push-under κ))                       ∎
-      where open MonadLaws∥
-
hunk ./CompositionBased/Lambda.agda 175
+  lookup : ∀ {Γ σ τ} → Γ ∋ σ → ∀ Δ → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ
+  lookup x Δ κ = const⋆ (Values Δ) (C.lookup x) ⊙∥ κ
+
hunk ./CompositionBased/Lambda.agda 185
-  weaken : ∀ {Γ σ τ} Δ →
-           (C.Dom (σ ∷ Γ) τ → C.Dom Γ τ) →
-           (Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ)
-  weaken Δ f κ = join {As = Values Δ} (RC.curry λ s →
-                   f (Λ λ v → RC.uncurry (split (Values Δ) (κ ∙ v)) s))
-
-  weaken-cong : ∀ {Γ σ τ} Δ {f₁ f₂ : C.Dom (σ ∷ Γ) τ → C.Dom Γ τ} →
-                (∀ κ → f₁ κ ≈ f₂ κ) →
-                ∀ κ → weaken Δ f₁ κ ≈ weaken Δ f₂ κ
-  weaken-cong []      f₁≈f₂ κ = f₁≈f₂ κ
-  weaken-cong (σ ∷ Δ) f₁≈f₂ κ = Λ-cong λ v →
-    weaken-cong Δ f₁≈f₂ (Λ λ v′ → κ ∙ v′ ∙ v)
-
-  weaken-lemma : ∀ {Γ σ τ} Δ (f : C.Dom Γ σ) (κ : Dom (σ ∷ Δ) Γ τ) →
-                 const⋆ (Values Δ) f ⊙∥ κ ≈ weaken Δ (λ κ → f ⊙∥ κ) κ
-  weaken-lemma []      f κ = refl (f ⊙∥ κ)
-  weaken-lemma (σ ∷ Δ) f κ = Λ-cong λ v →
-    weaken-lemma Δ f (Λ λ v′ → κ ∙ v′ ∙ v)
-
hunk ./CompositionBased/Lambda.agda 194
-      const⋆ (Values Δ) (C.lookup x) ⊙∥ κ  ≈⟨ weaken-lemma Δ (C.lookup x) κ ⟩
-      weaken Δ (λ κ → C.lookup x ⊙∥ κ) κ   ≈⟨ weaken-cong Δ (λ κ → proof $ lookup′ x κ) κ ⟩
-      weaken Δ (lookup x) κ                ∎
+      const⋆ (Values Δ) (C.lookup x) ⊙∥ κ  ≡⟨ P.refl ⟩
+      lookup x Δ κ                         ∎