[Simplified things. Identified a problem. Nils Anders Danielsson **20101211175728 Ignore-this: 3bdb2a1077ac4afc5b53334b77ca4690 ] hunk ./CompositionBased/Lambda.agda 20 +import Derivation hunk ./CompositionBased/Lambda.agda 176 --- Rewrite the evaluator in accumulator style +-- Rewrite the evaluator in continuation-passing style hunk ./CompositionBased/Lambda.agda 178 --- TODO: Is accumulator really the right term? - -module Accumulator where +module CPS where hunk ./CompositionBased/Lambda.agda 183 - open RC.Derivation + open Derivation hunk ./CompositionBased/Lambda.agda 186 - -- We need to decide what kind of accumulator/composition to use. ƛ + -- We need to decide what kind of continuation/composition to use. ƛ hunk ./CompositionBased/Lambda.agda 190 - -- f ◌ (λ ρ v → ⟦ t ⟧S (v , ρ)) + -- κ ◌ (λ ρ v → ⟦ t ⟧S (v , ρ)) hunk ./CompositionBased/Lambda.agda 192 - -- (for some notion of accumulator f and composition _◌_) can be + -- (for some notion of continuation κ and composition _◌_) can be hunk ./CompositionBased/Lambda.agda 195 - -- f′ (f″ ◌ ⟦ t ⟧S) - -- - -- for some f′ and f″. Note that the environment changes above. For - -- this reason I've found it useful if the accumulator - -- (continuation?) gets direct access to the environment, as in + -- κ′ (κ″ ◌ ⟦ t ⟧S) hunk ./CompositionBased/Lambda.agda 197 - -- ⟦ t ⟧′ κ = λ ρ → κ ⟦ t ⟧ ρ = κ ⟦ t ⟧. + -- for some κ′ and κ″. Note that the environment changes above. For + -- this reason I've found it useful if the continuation gets direct + -- access to the environment, as in hunk ./CompositionBased/Lambda.agda 201 - -- With this specification of ⟦_⟧′ we get the following result: - -- - -- ⟦ t₁ · t₂ ⟧′ κ = - -- κ (λ ρ → (⟦ t₁ ⟧ ρ) (⟦ t₂ ⟧ ρ)) = - -- ⟦ t₁ ⟧′ (λ f → ⟦ t₂ ⟧′ (λ g → κ (λ ρ → (f ρ) (g ρ)))) - -- - -- Note that ⟦ t₂ ⟧′ occurs under a lambda. I want to incorporate - -- this lambda in the definition of composition, so I'm defining - -- composition as follows: - - infixr 9 _◌_ - - _◌_ : ∀ {As} {A B : Set} → A → As ⇨ (A → B) → As ⇨ B - x ◌ f = RC.map (λ g → g x) f - - -- With As = [] we get reverse application, and with As = C ∷ [] we - -- get (roughly) x ◌ f = λ v → f v x. - - -- TODO: As seems to stay constant in the computations below, so I - -- think I've made some kind of mistake. - - -- A lemma related to _◌_. - - ◌-cong : ∀ {As A B} (x : A) {f₁ f₂ : As ⇨ (A → B)} → - f₁ ≈ f₂ → x ◌ f₁ ≈ x ◌ f₂ - ◌-cong x f₁≈f₂ = map-cong (λ g → P.refl {x = g x}) f₁≈f₂ + -- ⟦ t ⟧ κ = λ ρ → κ ⟦ t ⟧S ρ = κ ⟦ t ⟧S. hunk ./CompositionBased/Lambda.agda 205 - -- TODO: Simplify things? The moral code for top is - -- - -- top κ = λ ρ → κ ρ (λ (v , ρ) → v). + top : ∀ {Γ σ B} → (Dom (σ ∷ Γ) σ → B) → B + top κ = κ C.top hunk ./CompositionBased/Lambda.agda 208 - top : ∀ {Γ σ As B} → As ⇨ (Dom (σ ∷ Γ) σ → B) → As ⇨ B - top = RC.map (λ f → f (Λ λ v → return∥ v)) - - drop : ∀ {Γ σ τ As} {B : Set} → - As ⇨ (Dom (σ ∷ Γ) τ → B) → As ⇨ (Dom Γ τ → B) - drop = RC.map (λ f g → f (Λ λ _ → g)) - - drop-lemma : ∀ {Γ σ τ As B} - (f : Dom Γ τ) (κ : As ⇨ (Dom (σ ∷ Γ) τ → B)) → - C.drop f ◌ κ ≈ f ◌ drop κ - drop-lemma {B = B} f κ = - C.drop f ◌ κ ≡⟨ P.refl ⟩ - RC.map (λ g → g (Λ λ _ → f)) κ ≈⟨ sym $ map-∘ (λ (g : _ → B) → g f) (λ f g → f (Λ (λ _ → g))) κ ⟩ - RC.map (λ (g : _ → B) → g f) (RC.map (λ f g → f (Λ λ _ → g)) κ) ≡⟨ P.refl ⟩ - f ◌ drop κ ∎ + drop : ∀ {Γ σ τ} {B : Set} → + (Dom (σ ∷ Γ) τ → B) → (Dom Γ τ → B) + drop κ d = κ (C.drop d) hunk ./CompositionBased/Lambda.agda 214 - lookup : ∀ {Γ σ As B} → Γ ∋ σ → As ⇨ (Dom Γ σ → B) → As ⇨ B + lookup : ∀ {Γ σ B} → Γ ∋ σ → (Dom Γ σ → B) → B hunk ./CompositionBased/Lambda.agda 217 - lookup′ : ∀ {Γ σ As B} (x : Γ ∋ σ) (κ : As ⇨ (Dom Γ σ → B)) → - EqualTo (C.lookup x ◌ κ) - lookup′ zero κ = ▷ - C.lookup zero ◌ κ ≡⟨ P.refl ⟩ - C.top ◌ κ ≡⟨ P.refl ⟩ + lookup′ : ∀ {Γ σ B} (x : Γ ∋ σ) (κ : Dom Γ σ → B) → + EqualTo (κ (C.lookup x)) + lookup′ zero κ = ▷ begin + κ (C.lookup zero) ≡⟨ P.refl ⟩ + κ C.top ≡⟨ P.refl ⟩ hunk ./CompositionBased/Lambda.agda 223 + where open P.≡-Reasoning hunk ./CompositionBased/Lambda.agda 225 - lookup′ (suc x) κ = ▷ - C.lookup (suc x) ◌ κ ≡⟨ P.refl ⟩ - C.drop (C.lookup x) ◌ κ ≈⟨ drop-lemma (C.lookup x) κ ⟩ - C.lookup x ◌ drop κ ≈⟨ proof (lookup′ x _) ⟩ + lookup′ (suc x) κ = ▷ begin + κ (C.lookup (suc x)) ≡⟨ P.refl ⟩ + κ (C.drop (C.lookup x)) ≡⟨ P.refl ⟩ + drop κ (C.lookup x) ≡⟨ proof (lookup′ x (drop κ)) ⟩ hunk ./CompositionBased/Lambda.agda 230 + where open P.≡-Reasoning hunk ./CompositionBased/Lambda.agda 234 - app : ∀ {Γ σ τ As B} → - As ⇨ (Dom Γ τ → B) → As ⇨ (Dom Γ σ → Dom Γ (σ ⟶ τ) → B) - app = RC.map (λ κ x f → κ (f ⊛∥ x)) - - app-lemma : ∀ {Γ σ τ As B} - (f : Dom Γ (σ ⟶ τ)) (g : Dom Γ σ) - (κ : As ⇨ (Dom Γ τ → B)) → - (f ⊛∥ g) ◌ κ ≈ f ◌ g ◌ app κ - app-lemma {B = B} f g κ = - (f ⊛∥ g) ◌ κ ≡⟨ P.refl ⟩ - RC.map (λ h → h (f ⊛∥ g)) κ ≈⟨ sym $ map-∘ (λ (h : _ → B) → h f) (λ κ f → κ (f ⊛∥ g)) κ ⟩ - RC.map (λ (h : _ → B) → h f) - (RC.map (λ κ f → κ (f ⊛∥ g)) κ) ≡⟨ P.refl ⟩ - f ◌ RC.map (λ κ f → κ (f ⊛∥ g)) κ ≈⟨ sym $ ◌-cong f $ map-∘ (λ (h : _ → _ → B) → h g) (λ κ x f → κ (f ⊛∥ x)) κ ⟩ - f ◌ RC.map (λ (h : _ → _ → B) → h g) - (RC.map (λ κ x f → κ (f ⊛∥ x)) κ) ≡⟨ P.refl ⟩ - f ◌ g ◌ app κ ∎ + app : ∀ {Γ σ τ B} → + (Dom Γ τ → B) → (Dom Γ σ → Dom Γ (σ ⟶ τ) → B) + app κ x f = κ (f ⊛∥ x) hunk ./CompositionBased/Lambda.agda 238 - push : ∀ {Γ σ τ As B} → - As ⇨ (Dom Γ (σ ⟶ τ) → B) → As ⇨ (Dom (σ ∷ Γ) τ → B) - push = RC.map (λ κ f → κ (C.push f)) - - push-lemma : ∀ {Γ σ τ As B} - (f : Dom (σ ∷ Γ) τ) (κ : As ⇨ (Dom Γ (σ ⟶ τ) → B)) → - C.push f ◌ κ ≈ f ◌ push κ - push-lemma {B = B} f κ = - C.push f ◌ κ ≡⟨ P.refl ⟩ - RC.map (λ g → g (C.push f)) κ ≈⟨ sym $ map-∘ (λ (g : _ → B) → g f) (λ κ f → κ (C.push f)) κ ⟩ - RC.map (λ (g : _ → B) → g f) (RC.map (λ κ f → κ (C.push f)) κ) ≡⟨ P.refl ⟩ - f ◌ push κ ∎ + push : ∀ {Γ σ τ B} → + (Dom Γ (σ ⟶ τ) → B) → (Dom (σ ∷ Γ) τ → B) + push κ f = κ (C.push f) hunk ./CompositionBased/Lambda.agda 244 - ⟦_⟧ : ∀ {Γ σ As B} → Γ ⊢ σ → As ⇨ (Dom Γ σ → B) → As ⇨ B + ⟦_⟧ : ∀ {Γ σ B} → Γ ⊢ σ → (Dom Γ σ → B) → B hunk ./CompositionBased/Lambda.agda 247 - ⟦_⟧′ : ∀ {Γ σ As B} (t : Γ ⊢ σ) (κ : As ⇨ (Dom Γ σ → B)) → - EqualTo (⟦ t ⟧C ◌ κ) - ⟦ var x ⟧′ κ = ▷ - ⟦ var x ⟧C ◌ κ ≡⟨ P.refl ⟩ - C.lookup x ◌ κ ≈⟨ proof (lookup′ x κ) ⟩ + ⟦_⟧′ : ∀ {Γ σ B} (t : Γ ⊢ σ) (κ : Dom Γ σ → B) → + EqualTo (κ ⟦ t ⟧C) + ⟦ var x ⟧′ κ = ▷ begin + κ ⟦ var x ⟧C ≡⟨ P.refl ⟩ + κ (C.lookup x) ≡⟨ proof (lookup′ x κ) ⟩ hunk ./CompositionBased/Lambda.agda 253 + where open P.≡-Reasoning hunk ./CompositionBased/Lambda.agda 255 - ⟦ t₁ · t₂ ⟧′ κ = ▷ - ⟦ t₁ · t₂ ⟧C ◌ κ ≡⟨ P.refl ⟩ - (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ◌ κ ≈⟨ app-lemma ⟦ t₁ ⟧C ⟦ t₂ ⟧C κ ⟩ - ⟦ t₁ ⟧C ◌ ⟦ t₂ ⟧C ◌ app κ ≈⟨ ◌-cong ⟦ t₁ ⟧C (proof (⟦ t₂ ⟧′ _)) ⟩ - ⟦ t₁ ⟧C ◌ ⟦ t₂ ⟧ (app κ) ≈⟨ proof (⟦ t₁ ⟧′ _) ⟩ - ⟦ t₁ ⟧ (⟦ t₂ ⟧ (app κ)) ∎ + ⟦ t₁ · t₂ ⟧′ κ = ▷ begin + κ ⟦ t₁ · t₂ ⟧C ≡⟨ P.refl ⟩ + κ (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ≡⟨ P.refl ⟩ + app κ ⟦ t₂ ⟧C ⟦ t₁ ⟧C ≡⟨ P.cong (λ f → f ⟦ t₁ ⟧C) (proof (⟦ t₂ ⟧′ (app κ))) ⟩ + ⟦ t₂ ⟧ (app κ) ⟦ t₁ ⟧C ≡⟨ proof (⟦ t₁ ⟧′ (⟦ t₂ ⟧ (app κ))) ⟩ + ⟦ t₁ ⟧ (⟦ t₂ ⟧ (app κ)) ∎ + where open P.≡-Reasoning hunk ./CompositionBased/Lambda.agda 263 - ⟦ ƛ t ⟧′ κ = ▷ - ⟦ ƛ t ⟧C ◌ κ ≡⟨ P.refl ⟩ - C.push ⟦ t ⟧C ◌ κ ≈⟨ push-lemma ⟦ t ⟧C κ ⟩ - ⟦ t ⟧C ◌ push κ ≈⟨ proof (⟦ t ⟧′ _) ⟩ + ⟦ ƛ t ⟧′ κ = ▷ begin + κ ⟦ ƛ t ⟧C ≡⟨ P.refl ⟩ + κ (C.push ⟦ t ⟧C) ≡⟨ P.refl ⟩ + push κ ⟦ t ⟧C ≡⟨ proof (⟦ t ⟧′ (push κ)) ⟩ hunk ./CompositionBased/Lambda.agda 268 + where open P.≡-Reasoning hunk ./CompositionBased/Lambda.agda 270 - halt : ∀ {Γ σ} → [] ⇨ (Dom Γ σ → Dom Γ σ) - halt = return id + halt : ∀ {Γ σ} → (Dom Γ σ → Dom Γ σ) + halt = id hunk ./CompositionBased/Lambda.agda 274 - ∃ λ κ → RC.curry {As = Values Γ} ⟦ t ⟧S ≈ run (⟦ t ⟧ κ) + ∃ λ κ → RC.curry {As = Values Γ} ⟦ t ⟧S ≈ ⟦ t ⟧ κ hunk ./CompositionBased/Lambda.agda 276 - RC.curry ⟦ t ⟧S ≈⟨ proof $ Compositional.⟦_⟧′ t ⟩ - ⟦ t ⟧C ≡⟨ P.refl ⟩ - run (⟦ t ⟧C ◌ halt) ≡⟨ run-cong $ proof $ ⟦ t ⟧′ halt ⟩ - run (⟦ t ⟧ halt) ∎) - - -- lookup and ⟦_⟧ preserve equality of the accumulator. - - top-cong : ∀ {Γ σ As B} {κ₁ κ₂ : As ⇨ (Dom (σ ∷ Γ) σ → B)} → - κ₁ ≈ κ₂ → top κ₁ ≈ top κ₂ - top-cong = map-cong (λ f → P.refl {x = f (Λ λ v → return∥ v)}) - - drop-cong : ∀ {Γ σ τ As B} {κ₁ κ₂ : As ⇨ (Dom (σ ∷ Γ) τ → B)} → - κ₁ ≈ κ₂ → drop κ₁ ≈ drop κ₂ - drop-cong = map-cong (λ f → P.refl {x = λ g → f (Λ λ _ → g)}) - - app-cong : ∀ {Γ σ τ As B} {κ₁ κ₂ : As ⇨ (Dom Γ τ → B)} → - κ₁ ≈ κ₂ → app {σ = σ} κ₁ ≈ app {σ = σ} κ₂ - app-cong = map-cong (λ κ → P.refl {x = λ x f → κ (f ⊛∥ x)}) - - push-cong : ∀ {Γ σ τ As B} {κ₁ κ₂ : As ⇨ (Dom Γ (σ ⟶ τ) → B)} → - κ₁ ≈ κ₂ → push κ₁ ≈ push κ₂ - push-cong = map-cong (λ κ → P.refl {x = λ f → κ (C.push f)}) - - lookup-cong : ∀ {Γ σ As B} (x : Γ ∋ σ) {κ₁ κ₂ : As ⇨ (Dom Γ σ → B)} → - κ₁ ≈ κ₂ → lookup x κ₁ ≈ lookup x κ₂ - lookup-cong zero = top-cong - lookup-cong (suc x) = lookup-cong x ∘ drop-cong - - ⟦_⟧-cong : ∀ {Γ σ As B} (t : Γ ⊢ σ) {κ₁ κ₂ : As ⇨ (Dom Γ σ → B)} → - κ₁ ≈ κ₂ → ⟦ t ⟧ κ₁ ≈ ⟦ t ⟧ κ₂ - ⟦ var x ⟧-cong = lookup-cong x - ⟦ t₁ · t₂ ⟧-cong = ⟦ t₁ ⟧-cong ∘ ⟦ t₂ ⟧-cong ∘ app-cong - ⟦ ƛ t ⟧-cong = ⟦ t ⟧-cong ∘ push-cong + RC.curry ⟦ t ⟧S ≈⟨ RC.Derivation.proof $ Compositional.⟦_⟧′ t ⟩ + ⟦ t ⟧C ≡⟨ P.refl ⟩ + halt ⟦ t ⟧C ≡⟨ proof $ ⟦ t ⟧′ halt ⟩ + ⟦ t ⟧ halt ∎) + where open ≈-Reasoning hunk ./CompositionBased/Lambda.agda 287 - lookup″ : ∀ {Γ σ As B} → Γ ∋ σ → As ⇨ (Dom Γ σ → B) → As ⇨ B + lookup″ : ∀ {Γ σ B} → Γ ∋ σ → (Dom Γ σ → B) → B hunk ./CompositionBased/Lambda.agda 291 - ⟦_⟧″ : ∀ {Γ σ As B} → Γ ⊢ σ → As ⇨ (Dom Γ σ → B) → As ⇨ B + ⟦_⟧″ : ∀ {Γ σ B} → Γ ⊢ σ → (Dom Γ σ → B) → B hunk ./CompositionBased/Lambda.agda 296 + -- However, we have a problem: defunctionalisation of the code above + -- doesn't seem to give us anything useful. +