[Tried using _⊛∥_ for the accumulator composition. Still stuck. Nils Anders Danielsson **20101211122538 Ignore-this: 41b4ad6a663b464af058e6f9eca6dd59 ] hunk ./CompositionBased/Lambda.agda 101 - top : ∀ Γ {σ} → Dom (σ ∷ Γ) σ - top _ = Λ λ v → return∥ v + top : ∀ {Γ σ} → Dom (σ ∷ Γ) σ + top = Λ λ v → return∥ v hunk ./CompositionBased/Lambda.agda 118 - top Γ ∎ + top ∎ hunk ./CompositionBased/Lambda.agda 179 - open Semantics using (Value; Values) + open Semantics using (Value; Values) renaming (⟦_⟧ to ⟦_⟧S) hunk ./CompositionBased/Lambda.agda 186 - top⊙ : ∀ Γ {Δ σ τ} → - Dom (σ ∷ Δ) τ → Values (σ ∷ Γ) ++ Values Δ ⇨ Value τ - top⊙ Γ κ = Λ λ v → const⋆ (Values Γ) (κ ∙ v) + top : ∀ {Γ σ τ} → Dom (σ ∷ Γ) (σ ⟶ τ) → Dom (σ ∷ Γ) τ + top f = Λ λ v → RC.map (λ g → g v) (f ∙ v) hunk ./CompositionBased/Lambda.agda 189 - pop : ∀ {As} {A B : Set} → As ⇨ (A → B) → A ∷ As ⇨ B - pop f = Λ λ v → RC.map (λ g → g v) f - - drop : ∀ {As} {B C : Set} → As ⇨ C → As ⇨ (B → C) - drop = RC.map const - - pop-cong : ∀ {As} {A B : Set} {f₁ f₂ : As ⇨ (A → B)} → - f₁ ≈ f₂ → pop f₁ ≈ pop f₂ - pop-cong f₁≈f₂ = Λ-cong λ v → MoreLaws∥.map-cong (λ f → P.refl {x = f v}) f₁≈f₂ - - pop-drop : ∀ {Γ Δ σ τ χ} (f : Dom Γ σ) (κ : Dom (σ ∷ Δ) τ) → - C.drop {τ = χ} f ⊙ κ ≈ pop {A = Value χ} (f ⊙ drop κ) - pop-drop f κ = Λ-cong λ v → - f ⊙ κ ≈⟨ sym $ map-id (f ⊙ κ) ⟩ - RC.map id (f ⊙ κ) ≈⟨ sym $ map-∘ (λ g → g v) const (f ⊙ κ) ⟩ - RC.map (λ g → g v) (RC.map const (f ⊙ κ)) ≈⟨ map-cong (λ f → P.refl {x = f v}) (map-⊙ const f κ) ⟩ - RC.map (λ g → g v) (f ⊙ RC.map const κ) ∎ - where open MoreLaws∥ + drop : ∀ {Γ σ τ χ} → + (Dom Γ σ → Dom Γ τ) → (Dom (χ ∷ Γ) σ → Dom (χ ∷ Γ) τ) + drop g f = Λ λ v → g (f ∙ v) hunk ./CompositionBased/Lambda.agda 195 - lookup : ∀ {Γ Δ σ τ} → Γ ∋ σ → Dom (σ ∷ Δ) τ → - Values Γ ++ Values Δ ⇨ Value τ + lookup : ∀ {Γ σ τ} → Γ ∋ σ → Dom Γ (σ ⟶ τ) → Dom Γ τ hunk ./CompositionBased/Lambda.agda 198 - lookup′ : ∀ {Γ Δ σ τ} (x : Γ ∋ σ) (κ : Dom (σ ∷ Δ) τ) → - EqualTo (C.lookup x ⊙ κ) - lookup′ (zero {Γ = Γ}) κ = ▷ - C.lookup (zero {Γ = Γ}) ⊙ κ ≡⟨ P.refl ⟩ - C.top Γ ⊙ κ ≈⟨ (Λ-cong λ v → MoreLaws∥.return∥->>= (Values Γ) v (_∙_ κ)) ⟩ - top⊙ Γ κ ∎ + lookup′ : ∀ {Γ σ τ} (x : Γ ∋ σ) (f : Dom Γ (σ ⟶ τ)) → + EqualTo (f ⊛∥ C.lookup x) + lookup′ (zero {Γ = Γ}) f = ▷ + f ⊛∥ C.lookup (zero {Γ = Γ}) ≡⟨ P.refl ⟩ + f ⊛∥ C.top ≡⟨ P.refl ⟩ + Λ (λ v → f ∙ v) ⊛∥ (Λ λ v → return∥ v) ≡⟨ P.refl ⟩ + Λ (λ v → f ∙ v ⊛∥ return∥ v) ≈⟨ Λ-cong (λ v → MoreLaws∥.⊛∥-return∥ (f ∙ v) v) ⟩ + Λ (λ v → RC.map (λ g → g v) (f ∙ v)) ≡⟨ P.refl ⟩ + top f ∎ hunk ./CompositionBased/Lambda.agda 208 - lookup′ (suc {τ = τ} x) κ = ▷ - C.lookup (suc x) ⊙ κ ≡⟨ P.refl ⟩ - C.drop (C.lookup x) ⊙ κ ≈⟨ pop-drop (C.lookup x) κ ⟩ - pop (C.lookup x ⊙ drop κ) ≈⟨ pop-cong (proof (lookup′ x (drop κ))) ⟩ - pop (lookup x (drop κ)) ∎ + lookup′ (suc {τ = τ} x) f = ▷ + f ⊛∥ C.lookup (suc x) ≡⟨ P.refl ⟩ + f ⊛∥ C.drop (C.lookup x) ≡⟨ P.refl ⟩ + f ⊛∥ (Λ λ _ → C.lookup x) ≡⟨ P.refl ⟩ + (Λ λ v → f ∙ v ⊛∥ C.lookup x) ≈⟨ Λ-cong (λ v → proof (lookup′ x (f ∙ v))) ⟩ + (Λ λ v → lookup x (f ∙ v)) ≡⟨ P.refl ⟩ + drop (lookup x) f ∎ hunk ./CompositionBased/Lambda.agda 216 + -- Note that defunctionalisation of the last case above leads to + -- tree-structured code. + hunk ./CompositionBased/Lambda.agda 223 - ⟦_⟧ : ∀ {Γ Δ σ τ} → Γ ⊢ σ → Dom (σ ∷ Δ) τ → - Values Γ ++ Values Δ ⇨ Value τ - ⟦ t ⟧ κ = witness (⟦ t ⟧′ κ) + ⟦_⟧ : ∀ {Γ σ τ} → Γ ⊢ σ → Dom Γ (σ ⟶ τ) → Dom Γ τ + ⟦ t ⟧ f = witness (⟦ t ⟧′ f) hunk ./CompositionBased/Lambda.agda 226 - ⟦_⟧′ : ∀ {Γ Δ σ τ} (t : Γ ⊢ σ) (κ : Dom (σ ∷ Δ) τ) → - EqualTo (⟦ t ⟧C ⊙ κ) - ⟦ var x ⟧′ κ = ▷ - ⟦ var x ⟧C ⊙ κ ≡⟨ P.refl ⟩ - C.lookup x ⊙ κ ≈⟨ proof (lookup′ x κ) ⟩ - lookup x κ ∎ + ⟦_⟧′ : ∀ {Γ σ τ} (t : Γ ⊢ σ) (f : Dom Γ (σ ⟶ τ)) → + EqualTo (f ⊛∥ ⟦ t ⟧C) + ⟦ var x ⟧′ f = ▷ + f ⊛∥ ⟦ var x ⟧C ≡⟨ P.refl ⟩ + f ⊛∥ C.lookup x ≈⟨ proof (lookup′ x f) ⟩ + lookup x f ∎ hunk ./CompositionBased/Lambda.agda 233 - ⟦_⟧′ {Γ = Γ} {Δ = Δ} (ƛ t) κ = ▷ - ⟦ ƛ t ⟧C ⊙ κ ≡⟨ P.refl ⟩ - C.push ⟦ t ⟧C ⊙ κ ≈⟨ {!!} ⟩ - {!!} ∎ + ⟦ t₁ · t₂ ⟧′ f = ▷ + f ⊛∥ ⟦ t₁ · t₂ ⟧C ≡⟨ P.refl ⟩ + f ⊛∥ (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ≈⟨ sym $ composition _ _ _ ⟩ + RC.map _∘′_ f ⊛∥ ⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C ≈⟨ proof (⟦ t₁ ⟧′ _) ⊛∥-cong refl _ ⟩ + ⟦ t₁ ⟧ (RC.map _∘′_ f) ⊛∥ ⟦ t₂ ⟧C ≈⟨ proof (⟦ t₂ ⟧′ _) ⟩ + ⟦ t₂ ⟧ (⟦ t₁ ⟧ (RC.map _∘′_ f)) ∎ + where open MoreLaws∥ hunk ./CompositionBased/Lambda.agda 241 - ⟦ t₁ · t₂ ⟧′ κ = ▷ - ⟦ t₁ · t₂ ⟧C ⊙ κ ≡⟨ P.refl ⟩ - (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ⊙ κ ≈⟨ {!!} ⟩ - {!!} ∎ + ⟦_⟧′ {Γ = Γ} (ƛ t) f = ▷ + f ⊛∥ ⟦ ƛ t ⟧C ≡⟨ P.refl ⟩ + f ⊛∥ C.push ⟦ t ⟧C ≈⟨ ⊛∥-curry-uncurry f (C.push ⟦ t ⟧C) ⟩ + RC.curry (λ ρ → + RC.uncurry f ρ (RC.uncurry (C.push ⟦ t ⟧C) ρ)) ≡⟨ P.refl ⟩ + RC.curry (λ ρ → + RC.uncurry f ρ (RC.uncurry (RC.curry {As = Values Γ} + (λ ρ v → RC.uncurry ⟦ t ⟧C (v , ρ))) ρ)) ≈⟨ curry-cong (λ ρ → P.cong (RC.uncurry f ρ) $ + uncurry∘curry (Values Γ) _ ρ) ⟩ + RC.curry (λ ρ → RC.uncurry f ρ (λ v → RC.uncurry ⟦ t ⟧C (v , ρ))) ≈⟨ {!!} ⟩ + {!!} ∎ + where + open MoreLaws∥ + open CurryLaws + + -- My goal is to find f′ and ρ′ which solve the following + -- equation: + -- + -- f ρ (λ v → g (v , ρ)) ≈ f′ ρ′ (g ρ′) + -- + -- In that case I can apply the inductive hypothesis to ⟦ t ⟧C. + -- However, this equation does not seem to have a solution. + + halt : ∀ {Γ σ} → Dom Γ (σ ⟶ σ) + halt = return∥ id + + correct : ∀ {Γ σ} (t : Γ ⊢ σ) → + ∃ λ f → RC.curry {As = Values Γ} ⟦ t ⟧S ≈ ⟦ t ⟧ f + correct t = halt , ( + RC.curry ⟦ t ⟧S ≈⟨ proof $ Compositional.⟦_⟧′ t ⟩ + ⟦ t ⟧C ≈⟨ sym $ identity-⊛∥ ⟦ t ⟧C ⟩ + halt ⊛∥ ⟦ t ⟧C ≈⟨ proof $ ⟦ t ⟧′ (halt) ⟩ + ⟦ t ⟧ (halt) ∎) + where open MoreLaws∥