[Tried to use _⊙∥_ as the composition operation. Nils Anders Danielsson **20101216163954 Ignore-this: d4b4a345637e3833d12a1a62c44eb1e ] hunk ./CompositionBased/Lambda.agda 22 - hiding (module Derivation; app; push) + hiding (module Derivation; app) hunk ./CompositionBased/Lambda.agda 170 - open Derivation + open RC.Derivation hunk ./CompositionBased/Lambda.agda 177 - -- κ ◌ (λ ρ v → ⟦ t ⟧S (v , ρ)) + -- (λ ρ v → ⟦ t ⟧S (v , ρ)) ◌ κ hunk ./CompositionBased/Lambda.agda 182 - -- κ′ (κ″ ◌ ⟦ t ⟧S) - -- - -- 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 + -- κ′ (⟦ t ⟧S ◌ κ″) hunk ./CompositionBased/Lambda.agda 184 - -- ⟦ t ⟧ κ = λ ρ → κ ⟦ t ⟧S ρ = κ ⟦ t ⟧S. + -- for some κ′ and κ″. Note that the environment changes above. hunk ./CompositionBased/Lambda.agda 188 - top : ∀ {Γ σ B} → (Dom (σ ∷ Γ) σ → B) → B - top κ = κ C.top + top : ∀ {Γ σ τ} → Dom (σ ∷ σ ∷ Γ) τ → Dom (σ ∷ Γ) τ + top κ = Λ λ v → κ ∙ v ∙ v hunk ./CompositionBased/Lambda.agda 191 - drop : ∀ {Γ σ τ} {B : Set} → - (Dom (σ ∷ Γ) τ → B) → (Dom Γ τ → B) - drop κ d = κ (wk d) + push-under : ∀ {Γ σ τ χ} → Dom (σ ∷ τ ∷ Γ) χ → Dom (σ ∷ Γ) (τ ⟶ χ) + push-under κ = Λ λ v → push (κ ∙ v) hunk ./CompositionBased/Lambda.agda 196 - lookup : ∀ {Γ σ B} → Γ ∋ σ → (Dom Γ σ → B) → B + lookup : ∀ {Γ σ τ} → Γ ∋ σ → Dom (σ ∷ Γ) τ → Dom Γ τ hunk ./CompositionBased/Lambda.agda 199 - lookup′ : ∀ {Γ σ B} (x : Γ ∋ σ) (κ : Dom Γ σ → B) → - EqualTo (κ (C.lookup x)) - lookup′ zero κ = ▷ begin - κ (C.lookup zero) ≡⟨ P.refl ⟩ - κ C.top ≡⟨ P.refl ⟩ - top κ ∎ - where open P.≡-Reasoning + lookup′ : ∀ {Γ σ τ} (x : Γ ∋ σ) (κ : Dom (σ ∷ Γ) τ) → + EqualTo (C.lookup x ⊙∥ κ) + lookup′ (zero {Γ = Γ}) κ = ▷ + C.lookup zero ⊙∥ κ ≡⟨ P.refl ⟩ + C.top ⊙∥ κ ≡⟨ P.refl ⟩ + (Λ λ v → return∥ v) ⊙∥ κ ≡⟨ P.refl ⟩ + (Λ λ v → return∥ v >>=∥ λ x → κ ∙ x ∙ v) ≈⟨ Λ-cong (λ v → MonadLaws∥.left-identity (λ x → κ ∙ x ∙ v) v) ⟩ + top κ ∎ hunk ./CompositionBased/Lambda.agda 208 - lookup′ (suc x) κ = ▷ begin - κ (C.lookup (suc x)) ≡⟨ P.refl ⟩ - κ (wk (C.lookup x)) ≡⟨ P.refl ⟩ - drop κ (C.lookup x) ≡⟨ proof (lookup′ x (drop κ)) ⟩ - lookup x (drop κ) ∎ - where open P.≡-Reasoning + 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 224 - app : ∀ {Γ σ τ B} → - (Dom Γ τ → B) → (Dom Γ σ → Dom Γ (σ ⟶ τ) → B) - app κ x f = κ (f ⊛∥ x) - - push : ∀ {Γ σ τ B} → - (Dom Γ (σ ⟶ τ) → B) → (Dom (σ ∷ Γ) τ → B) - push κ f = κ (RC.push f) - hunk ./CompositionBased/Lambda.agda 226 - ⟦_⟧ : ∀ {Γ σ B} → Γ ⊢ σ → (Dom Γ σ → B) → B + ⟦_⟧ : ∀ {Γ σ τ} → Γ ⊢ σ → Dom (σ ∷ Γ) τ → Dom Γ τ hunk ./CompositionBased/Lambda.agda 229 - ⟦_⟧′ : ∀ {Γ σ B} (t : Γ ⊢ σ) (κ : Dom Γ σ → B) → - EqualTo (κ ⟦ t ⟧C) - ⟦ var x ⟧′ κ = ▷ begin - κ ⟦ var x ⟧C ≡⟨ P.refl ⟩ - κ (C.lookup x) ≡⟨ proof (lookup′ x κ) ⟩ - lookup x κ ∎ - where open P.≡-Reasoning + ⟦_⟧′ : ∀ {Γ σ τ} (t : Γ ⊢ σ) (κ : Dom (σ ∷ Γ) τ) → + EqualTo (⟦ t ⟧C ⊙∥ κ) + ⟦ var x ⟧′ κ = ▷ + ⟦ var x ⟧C ⊙∥ κ ≡⟨ P.refl ⟩ + C.lookup x ⊙∥ κ ≈⟨ proof (lookup′ x κ) ⟩ + lookup x κ ∎ hunk ./CompositionBased/Lambda.agda 236 - ⟦ 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 + ⟦ t₁ · t₂ ⟧′ κ = ▷ + ⟦ t₁ · t₂ ⟧C ⊙∥ κ ≡⟨ P.refl ⟩ + (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ⊙∥ κ ≈⟨ Stack.wk-reverse-app ⟦ t₁ ⟧C ⟦ t₂ ⟧C κ ⟩ + ⟦ t₁ ⟧C ⊙∥ wk ⟦ t₂ ⟧C ⊙∥ reverse-app κ ≈⟨ proof $ ⟦ t₁ ⟧′ (wk ⟦ t₂ ⟧C ⊙∥ reverse-app κ) ⟩ + ⟦ t₁ ⟧ (wk ⟦ t₂ ⟧C ⊙∥ reverse-app κ) ≈⟨ {!!} ⟩ + ? ∎ hunk ./CompositionBased/Lambda.agda 243 - ⟦ ƛ t ⟧′ κ = ▷ begin - κ ⟦ ƛ t ⟧C ≡⟨ P.refl ⟩ - κ (RC.push ⟦ t ⟧C) ≡⟨ P.refl ⟩ - push κ ⟦ t ⟧C ≡⟨ proof (⟦ t ⟧′ (push κ)) ⟩ - ⟦ t ⟧ (push κ) ∎ - where open P.≡-Reasoning + ⟦ ƛ t ⟧′ κ = ▷ + ⟦ ƛ t ⟧C ⊙∥ κ ≡⟨ P.refl ⟩ + push ⟦ t ⟧C ⊙∥ κ ≈⟨ {!!} ⟩ + ? ∎ hunk ./CompositionBased/Lambda.agda 248 - halt : ∀ {Γ σ} → (Dom Γ σ → Dom Γ σ) - halt = id + halt : ∀ {Γ σ} → Dom (σ ∷ Γ) σ + halt = identity∥ hunk ./CompositionBased/Lambda.agda 254 - RC.curry ⟦ t ⟧S ≈⟨ RC.Derivation.proof $ Compositional.⟦_⟧′ t ⟩ - ⟦ t ⟧C ≡⟨ P.refl ⟩ - halt ⟦ t ⟧C ≡⟨ proof $ ⟦ t ⟧′ halt ⟩ + RC.curry ⟦ t ⟧S ≈⟨ proof $ Compositional.⟦_⟧′ t ⟩ + ⟦ t ⟧C ≈⟨ sym $ identity-⊙∥ _ ⟩ + ⟦ t ⟧C ⊙∥ halt ≈⟨ proof $ ⟦ t ⟧′ halt ⟩ hunk ./CompositionBased/Lambda.agda 258 - where open ≈-Reasoning hunk ./CompositionBased/Lambda.agda 259 - -- As an aside, note that the right-hand sides of lookup and ⟦_⟧ can - -- be written as compositions: - - private - - lookup″ : ∀ {Γ σ B} → Γ ∋ σ → (Dom Γ σ → B) → B - lookup″ zero = top - lookup″ (suc x) = lookup″ x ∘ drop - - ⟦_⟧″ : ∀ {Γ σ B} → Γ ⊢ σ → (Dom Γ σ → B) → B - ⟦ var x ⟧″ = lookup″ x - ⟦ t₁ · t₂ ⟧″ = ⟦ t₁ ⟧″ ∘ ⟦ t₂ ⟧″ ∘ app - ⟦ ƛ t ⟧″ = ⟦ t ⟧″ ∘ push - - -- However, we have a problem: defunctionalisation of the code above - -- doesn't seem to give us anything useful. -