[Defunctionalised and switched to an explicit environment. Nils Anders Danielsson **20101220202403 Ignore-this: d4cb538204768c8328294691c5359c4b ] hunk ./CompositionBased/Lambda.agda 240 + -- ⟦_⟧ preserves equality in its continuation argument. + + ⟦_⟧-cong : ∀ {Γ σ} (t : Γ ⊢ σ) Δ {τ} {κ₁ κ₂ : Dom (σ ∷ Δ) Γ τ} → + (∀ s → κ₁ s ≈ κ₂ s) → ∀ {s} → ⟦ t ⟧ Δ κ₁ s ≈ ⟦ t ⟧ Δ κ₂ s + ⟦_⟧-cong t Δ {κ₁ = κ₁} {κ₂} κ₁≈κ₂ {s} = + ⟦ t ⟧ Δ κ₁ s ≈⟨ sym $ proof $ ⟦ t ⟧′ Δ κ₁ s ⟩ + (⟦ t ⟧C ⟪ Δ ⟫ κ₁) s ≈⟨ refl ⟦ t ⟧C ⟪ Δ ⟫-cong κ₁≈κ₂ ⟩ + (⟦ t ⟧C ⟪ Δ ⟫ κ₂) s ≈⟨ proof $ ⟦ t ⟧′ Δ κ₂ s ⟩ + ⟦ t ⟧ Δ κ₂ s ∎ + + -- The closure combinator preserves equality in (at least) its first + -- continuation argument. + + closure-cong : ∀ {Γ σ τ} {f₁ f₂ : C.Dom (σ ∷ Γ) τ} → + f₁ ≈ f₂ → + ∀ Δ {χ} (κ : Dom (σ ⟶ τ ∷ Δ) Γ χ) {s} → + closure (λ _ → f₁) Δ κ s ≈ closure (λ _ → f₂) Δ κ s + closure-cong f₁≈f₂ Δ κ = + Stack.push-cong ext f₁≈f₂ ⟪ Δ ⟫-cong (refl ∘ κ) + +------------------------------------------------------------------------ +-- Defunctionalise + +module Defunctionalised where + + open Semantics using () renaming (⟦_⟧ to ⟦_⟧S) + open CPS using () renaming (⟦_⟧ to ⟦_⟧CPS; ⟦_⟧-cong to ⟦_⟧CPS-cong) + open ≈-Reasoning + + data Term : Ctxt → Ctxt → Type → Set where + lookup : ∀ {Γ Δ σ τ} + (x : Γ ∋ σ) (t : Term (σ ∷ Δ) Γ τ) → Term Δ Γ τ + closure : ∀ {Γ Δ σ τ χ} + (t₁ : Term [] (σ ∷ Γ) τ) (t₂ : Term (σ ⟶ τ ∷ Δ) Γ χ) → + Term Δ Γ χ + ret : ∀ {Γ σ} → Term [ σ ] Γ σ + app : ∀ {Γ Δ σ τ χ} + (t : Term (τ ∷ Δ) Γ χ) → Term (σ ⟶ τ ∷ σ ∷ Δ) Γ χ + + -- The semantics of Term. + + exec : ∀ {Γ Δ σ} → Term Δ Γ σ → CPS.Dom Δ Γ σ + exec (lookup x t) s = Compositional.lookup x >>=∥ λ v → + exec t (v , s) + exec (closure t₁ t₂) s = push (exec t₁ (lift tt)) >>=∥ λ v → + exec t₂ (v , s) + exec ret (v , s) = return∥ v + exec (app t) (f , x , s) = exec t (f x , s) + + -- Compiler. + + mutual + + comp : ∀ {Γ Δ σ τ} → Γ ⊢ σ → Term (σ ∷ Δ) Γ τ → Term Δ Γ τ + comp t κ = proj₁ (comp′ t κ) + + comp′ : ∀ {Γ σ τ} (t : Γ ⊢ σ) {Δ} (κ : Term (σ ∷ Δ) Γ τ) → + ∃ λ (t′ : Term Δ Γ τ) → + ∀ s → ⟦ t ⟧CPS Δ (exec κ) s ≈ exec t′ s + comp′ (var x) {Δ} κ = lookup x κ , λ s → + ⟦ var x ⟧CPS Δ (exec κ) s ≡⟨ P.refl ⟩ + CPS.lookup x Δ (exec κ) s ≡⟨ P.refl ⟩ + exec (lookup x κ) s ∎ + + comp′ (ƛ t) {Δ} κ = closure (comp t ret) κ , λ s → + ⟦ ƛ t ⟧CPS Δ (exec κ) s ≡⟨ P.refl ⟩ + CPS.closure (⟦ t ⟧CPS [] CPS.ret) Δ (exec κ) s ≈⟨ CPS.closure-cong (proj₂ (comp′ t ret) _) Δ (exec κ) ⟩ + exec (closure (comp t ret) κ) s ∎ + + comp′ (t₁ · t₂) {Δ} κ = comp t₂ (comp t₁ (app κ)) , λ s → + ⟦ t₁ · t₂ ⟧CPS Δ (exec κ) s ≡⟨ P.refl ⟩ + ⟦ t₂ ⟧CPS Δ (⟦ t₁ ⟧CPS (_ ∷ Δ) (CPS.app Δ (exec κ))) s ≡⟨ P.refl ⟩ + ⟦ t₂ ⟧CPS Δ (⟦ t₁ ⟧CPS (_ ∷ Δ) (exec (app κ))) s ≈⟨ ⟦ t₂ ⟧CPS-cong Δ (proj₂ $ comp′ t₁ (app κ)) ⟩ + ⟦ t₂ ⟧CPS Δ (exec (comp t₁ (app κ))) s ≈⟨ proj₂ (comp′ t₂ (comp t₁ (app κ))) s ⟩ + exec (comp t₂ (comp t₁ (app κ))) s ∎ + + correct : ∀ {Γ σ} (t : Γ ⊢ σ) ρ → + ⟦ t ⟧S ρ ≡ RC.uncurry (exec (comp t ret) (lift tt)) ρ + correct t ρ = begin + ⟦ t ⟧S ρ ≡⟨ CPS.correct t ρ ⟩′ + RC.uncurry (⟦ t ⟧CPS [] CPS.ret (lift tt)) ρ ≡⟨ uncurry-cong (proj₂ (comp′ t ret) _) ρ ⟩′ + RC.uncurry (exec (comp t ret) (lift tt)) ρ ∎′ + where + open CurryLaws + open P.≡-Reasoning renaming (_≡⟨_⟩_ to _≡⟨_⟩′_; _∎ to _∎′) + +------------------------------------------------------------------------ +-- Switch to an explicit environment + +module Environment where + + private + module C = Compositional + open module D = Defunctionalised using (Term); open D.Term + open module S = Semantics using (Value; Env) renaming (⟦_⟧ to ⟦_⟧S) + open Derivation + open P.≡-Reasoning + open CurryLaws + + Dom : Ctxt → Ctxt → Type → Set + Dom Δ Γ σ = Env Δ → Env Γ → Value σ + + mutual + + exec : ∀ {Γ Δ σ} → Term Δ Γ σ → Dom Δ Γ σ + exec t s ρ = witness $ exec′ t s ρ + + exec′ : ∀ {Γ Δ σ} (t : Term Δ Γ σ) (s : Env Δ) (ρ : Env Γ) → + EqualTo (RC.uncurry (D.exec t s) ρ) + exec′ {Γ} (lookup x t) s ρ = ▷ begin + RC.uncurry (D.exec (lookup x t) s) ρ ≡⟨ P.refl ⟩ + RC.uncurry (C.lookup x >>=∥ λ v → D.exec t (v , s)) ρ ≡⟨ uncurry∘curry (S.Values Γ) + (λ ρ → RC.uncurry (D.exec t (RC.uncurry (C.lookup x) ρ , s)) ρ) ρ ⟩ + RC.uncurry (D.exec t (RC.uncurry (C.lookup x) ρ , s)) ρ ≡⟨ proof $ exec′ t _ _ ⟩ + exec t (RC.uncurry (C.lookup x) ρ , s) ρ ≡⟨ P.cong (λ x → exec t (x , s) ρ) $ + uncurry∘curry (S.Values Γ) (S.lookup x) ρ ⟩ + exec t (S.lookup x ρ , s) ρ ∎ + + exec′ {Γ} (closure t₁ t₂) s ρ = ▷ begin + RC.uncurry (D.exec (closure t₁ t₂) s) ρ ≡⟨ P.refl ⟩ + RC.uncurry (push (D.exec t₁ (lift tt)) >>=∥ λ v → + D.exec t₂ (v , s)) ρ ≡⟨ uncurry∘curry (S.Values Γ) + (λ ρ → RC.uncurry (D.exec t₂ + (RC.uncurry (push (D.exec t₁ (lift tt))) ρ , s)) ρ) + ρ ⟩ + RC.uncurry + (D.exec t₂ (RC.uncurry (push (D.exec t₁ (lift tt))) ρ , s)) ρ ≡⟨ proof $ exec′ t₂ _ _ ⟩ + exec t₂ (RC.uncurry (push (D.exec t₁ (lift tt))) ρ , s) ρ ≡⟨ P.cong (λ x → exec t₂ (x , s) ρ) $ + uncurry∘curry (S.Values Γ) + (λ ρ v → RC.uncurry (D.exec t₁ _ ∙ v) ρ) ρ ⟩ + exec t₂ ((λ v → RC.uncurry (D.exec t₁ (lift tt)) (v , ρ)) , s) ρ ≡⟨ (P.cong (λ x → exec t₂ (x , s) ρ) $ ext λ v → + proof $ exec′ t₁ _ _) ⟩ + exec t₂ ((λ v → exec t₁ (lift tt) (v , ρ)) , s) ρ ∎ + + exec′ {Γ} ret (v , s) ρ = ▷ begin + RC.uncurry {As = S.Values Γ} (D.exec ret (v , s)) ρ ≡⟨ P.refl ⟩ + RC.uncurry {As = S.Values Γ} (return∥ v) ρ ≡⟨ uncurry∘curry (S.Values Γ) (const v) ρ ⟩ + v ∎ + + exec′ {Γ} (app t) (f , x , s) ρ = ▷ begin + RC.uncurry (D.exec (app t) (f , x , s)) ρ ≡⟨ P.refl ⟩ + RC.uncurry (D.exec t (f x , s)) ρ ≡⟨ proof $ exec′ t _ _ ⟩ + exec t (f x , s) ρ ∎ + + -- Note that exec is /not/ a virtual machine: in the closure case + -- there is a non-tail call. + + correct : ∀ {Γ σ} (t : Γ ⊢ σ) ρ → + ⟦ t ⟧S ρ ≡ exec (D.comp t ret) (lift tt) ρ + correct t ρ = begin + ⟦ t ⟧S ρ ≡⟨ D.correct t ρ ⟩ + RC.uncurry (D.exec (D.comp t ret) (lift tt)) ρ ≡⟨ proof $ exec′ (D.comp t ret) _ ρ ⟩ + exec (D.comp t ret) (lift tt) ρ ∎ +