[Tried to separate the environment and the stack.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101220121504
 Ignore-this: 55fae5ba7357ad0d3fb0e5899442b544
] hunk ./CompositionBased/Lambda.agda 288
-  -- What happens if we continue with the code above? I don't know,
-  -- but rather than having only two components in the resulting
-  -- machine (code + stack), I think it seems nicer to have three
-  -- (code + stack + environment).
+-- What happens if we continue with the code above? I don't know, but
+-- rather than having only two components in the resulting machine
+-- (code + stack), I think it seems nicer to have three (code + stack
+-- + environment). Let's try this.
+
+module CPS₂ where
+
+  private
+    open module S = Semantics
+      using (Env) renaming (⟦_⟧ to ⟦_⟧S)
+  open Derivation
+  open P.≡-Reasoning
+
+  Cont : Type → Set
+  Cont σ = ∀ Δ {τ} → S.Dom (σ ∷ Δ) τ → S.Dom Δ τ
+
+  ret : ∀ {Γ σ} → S.Dom (σ ∷ Γ) σ
+  ret = proj₁
+
+  Dom : Ctxt → Type → Set
+  Dom Γ σ = Env Γ → Cont σ
+
+  closure : ∀ Γ {σ τ} → Dom (σ ∷ Γ) τ → S.Dom Γ (σ ⟶ τ)
+  closure _ d ρ = λ v → d (v , ρ) [] proj₁ (lift tt)
+
+  app : ∀ Γ {σ τ χ} → S.Dom (τ ∷ Γ) χ → S.Dom (σ ⟶ τ ∷ σ ∷ Γ) χ
+  app _ κ (f , x , ρ) = κ (f x , ρ)
+
+  mutual
+
+    ⟦_⟧ : ∀ {Γ σ} → Γ ⊢ σ → Dom Γ σ
+    ⟦ t ⟧ ρ Δ κ s = witness (⟦ t ⟧′ ρ Δ κ s)
+
+    ⟦_⟧′ : ∀ {Γ σ τ}
+           (t : Γ ⊢ σ) (ρ : Env Γ)
+           Δ (κ : S.Dom (σ ∷ Δ) τ) (s : Env Δ) →
+           EqualTo (κ (⟦ t ⟧S ρ , s))
+    ⟦ var x ⟧′ ρ Δ κ s = ▷ begin
+      κ (S.lookup x ρ , s) ∎
+
+    ⟦_⟧′ {Γ = Γ} (ƛ t) ρ Δ κ s = ▷ begin
+      κ (⟦ ƛ t ⟧S ρ , s)                                ≡⟨ P.refl ⟩
+      κ ((λ v → ⟦ t ⟧S (v , ρ)) , s)                    ≡⟨ P.refl ⟩
+      κ ((λ v → proj₁ {b = zero} {B = λ _ → Lift ⊤}
+                      (⟦ t ⟧S (v , ρ) , lift tt)) , s)  ≡⟨ P.cong (λ f → κ (f , s)) (ext λ v →
+                                                             proof $ ⟦ t ⟧′ (v , ρ) [] proj₁ (lift tt)) ⟩
+      κ ((λ v → ⟦ t ⟧ (v , ρ) [] proj₁ (lift tt)) , s)  ≡⟨ P.refl ⟩
+      κ (closure Γ ⟦ t ⟧ ρ , s)                         ∎
+
+    ⟦ t₁ · t₂ ⟧′ ρ Δ κ s = ▷ begin
+      κ (⟦ t₁ · t₂ ⟧S ρ , s)                      ≡⟨ P.refl ⟩
+      κ (⟦ t₁ ⟧S ρ (⟦ t₂ ⟧S ρ) , s)               ≡⟨ P.refl ⟩
+      app Δ κ (⟦ t₁ ⟧S ρ , ⟦ t₂ ⟧S ρ , s)         ≡⟨ proof $ ⟦ t₁ ⟧′ ρ (_ ∷ Δ) (app Δ κ) _ ⟩
+      ⟦ t₁ ⟧ ρ (_ ∷ Δ) (app Δ κ) (⟦ t₂ ⟧S ρ , s)  ≡⟨ proof $ ⟦ t₂ ⟧′ ρ Δ (⟦ t₁ ⟧ ρ (_ ∷ Δ) (app Δ κ)) s ⟩
+      ⟦ t₂ ⟧ ρ Δ (⟦ t₁ ⟧ ρ (_ ∷ Δ) (app Δ κ)) s   ∎