[Stopped using ReverseComposition. Simplified the code considerably. Nils Anders Danielsson **20101220233224 Ignore-this: 9213272da68b3eedb3337a1291f13894 ] hunk ./CompositionBased/Lambda.agda 14 -open import Algebra -open import Data.List as List hiding (drop) -import Data.List.Properties as ListProp +open import Data.List hunk ./CompositionBased/Lambda.agda 18 -import Relation.Binary.HeterogeneousEquality as H - -import Derivation -open import ReverseComposition as RC - hiding (module Derivation; app) - renaming (_·_ to _∙_) hunk ./CompositionBased/Lambda.agda 53 - -- Semantic domains. + -- Parametrised interpretation of contexts. + + Ctxt-interpretation : (Type → Set) → (Ctxt → Set) + Ctxt-interpretation ⟦_⟧ [] = ⊤ + Ctxt-interpretation ⟦_⟧ (σ ∷ Γ) = + Σ[ x ∶ ⟦ σ ⟧ ] Ctxt-interpretation ⟦_⟧ Γ + + -- Interpretation of types. hunk ./CompositionBased/Lambda.agda 65 - Values : Ctxt → List Set - Values = List.map Value + -- Environments. hunk ./CompositionBased/Lambda.agda 67 - Env : Ctxt → Set - Env = Args ∘ Values + Env = Ctxt-interpretation Value + + -- Semantic domains. hunk ./CompositionBased/Lambda.agda 86 --- Rewrite the evaluator in "compositional" style +-- Functions taking a well-typed stack and a well-typed environment to +-- a value hunk ./CompositionBased/Lambda.agda 89 -module Compositional where +module StackEnv where hunk ./CompositionBased/Lambda.agda 91 - private - open module S = Semantics - using (Value; Values) renaming (⟦_⟧ to ⟦_⟧S) - open RC.Derivation - open CurryLaws + open Semantics public using (Value; Env) hunk ./CompositionBased/Lambda.agda 93 - -- Semantic domains. + -- Stacks. hunk ./CompositionBased/Lambda.agda 95 - Dom : Ctxt → Type → Set - Dom Γ σ = Values Γ ⇨ Value σ + Stack : Ctxt → Set + Stack = Env hunk ./CompositionBased/Lambda.agda 98 - -- One could calculate/devise some other definition of the lookup - -- function, but allowing the unary representation of variables to - -- affect the design of the machine/compiler seems like a bad idea. + -- Semantic domains: stack → environment → result. hunk ./CompositionBased/Lambda.agda 100 - lookup : ∀ {Γ σ} → Γ ∋ σ → Dom Γ σ - lookup x = RC.curry (S.lookup x) + Dom : Ctxt → Ctxt → Type → Set + Dom Δ Γ σ = Stack Δ → Env Γ → Value σ hunk ./CompositionBased/Lambda.agda 103 - -- Compositional semantics. + -- Equality. hunk ./CompositionBased/Lambda.agda 105 - private + infix 4 _≈_ hunk ./CompositionBased/Lambda.agda 107 - uc : ∀ Γ {σ} → Semantics.Dom Γ σ → Semantics.Dom Γ σ - uc Γ = RC.uncurry {As = Values Γ} ∘ RC.curry + _≈_ : ∀ {Δ Γ σ} → Dom Δ Γ σ → Dom Δ Γ σ → Set + f ≈ g = ∀ s ρ → f s ρ ≡ g s ρ hunk ./CompositionBased/Lambda.agda 110 - mutual + -- Equational reasoning. hunk ./CompositionBased/Lambda.agda 112 - ⟦_⟧ : ∀ {Γ σ} → Γ ⊢ σ → Dom Γ σ - ⟦ t ⟧ = witness ⟦ t ⟧′ + infix 2 _∎ + infixr 2 _≈⟨_⟩_ _≈⟨⟩_ hunk ./CompositionBased/Lambda.agda 115 - ⟦_⟧′ : ∀ {Γ σ} (t : Γ ⊢ σ) → EqualTo (RC.curry ⟦ t ⟧S) - ⟦ var x ⟧′ = ▷ - RC.curry ⟦ var x ⟧S ≡⟨ P.refl ⟩ - RC.curry (S.lookup x) ≡⟨ P.refl ⟩ - lookup x ∎ + _≈⟨_⟩_ : ∀ {Δ Γ σ} (f : Dom Δ Γ σ) {g h : Dom Δ Γ σ} → + f ≈ g → g ≈ h → f ≈ h + _ ≈⟨ f≈g ⟩ g≈h = λ s ρ → P.trans (f≈g s ρ) (g≈h s ρ) hunk ./CompositionBased/Lambda.agda 119 - ⟦_⟧′ {Γ = Γ} (ƛ t) = ▷ - RC.curry ⟦ ƛ t ⟧S ≡⟨ P.refl ⟩ - RC.curry (λ ρ v → ⟦ t ⟧S (v , ρ)) ≈⟨ sym (curry-cong λ ρ → ext λ v → uncurry∘curry (Values Γ) _ _) ⟩ - RC.curry (λ ρ v → uc (_ ∷ Γ) ⟦ t ⟧S (v , ρ)) ≡⟨ P.refl ⟩ - push (RC.curry ⟦ t ⟧S) ≈⟨ Stack.push-cong ext (proof ⟦ t ⟧′) ⟩ - push ⟦ t ⟧ ∎ + _≈⟨⟩_ : ∀ {Δ Γ σ} (f : Dom Δ Γ σ) {g : Dom Δ Γ σ} → + f ≈ g → f ≈ g + _ ≈⟨⟩ g≈h = g≈h hunk ./CompositionBased/Lambda.agda 123 - ⟦_⟧′ {Γ = Γ} (t₁ · t₂) = ▷ - RC.curry ⟦ t₁ · t₂ ⟧S ≡⟨ P.refl ⟩ - RC.curry (λ ρ → ⟦ t₁ ⟧S ρ (⟦ t₂ ⟧S ρ)) ≈⟨ sym (curry-cong λ ρ → - P.cong₂ _$_ - (uncurry∘curry (Values Γ) ⟦ t₁ ⟧S ρ) - (uncurry∘curry (Values Γ) ⟦ t₂ ⟧S ρ)) ⟩ - RC.curry (λ ρ → uc Γ ⟦ t₁ ⟧S ρ (uc Γ ⟦ t₂ ⟧S ρ)) ≈⟨ curry-cong (λ ρ → P.cong₂ _$_ - (uncurry-cong (proof ⟦ t₁ ⟧′) ρ) - (uncurry-cong (proof ⟦ t₂ ⟧′) ρ)) ⟩ - RC.curry (λ ρ → (RC.uncurry ⟦ t₁ ⟧ ρ) - (RC.uncurry ⟦ t₂ ⟧ ρ)) ≈⟨ sym $ MoreLaws∥.⊛∥-curry-uncurry ⟦ t₁ ⟧ ⟦ t₂ ⟧ ⟩ - ⟦ t₁ ⟧ ⊛∥ ⟦ t₂ ⟧ ∎ + _∎ : ∀ {Δ Γ σ} (f : Dom Δ Γ σ) → f ≈ f + f ∎ = λ s ρ → P.refl + + sym : ∀ {Δ Γ σ} {f g : Dom Δ Γ σ} → f ≈ g → g ≈ f + sym f≈g = λ s ρ → P.sym (f≈g s ρ) + + -- Helper functions for derivations. + + EqualTo : ∀ {Δ Γ σ} → Dom Δ Γ σ → Set + EqualTo f = ∃ (λ g → f ≈ g) + + infix 0 ▷_ + + ▷_ : ∀ {Δ Γ σ} {f g : Dom Δ Γ σ} → f ≈ g → EqualTo f + ▷ f≈g = (_ , f≈g) hunk ./CompositionBased/Lambda.agda 144 - open Semantics using (Value; Values; Env) renaming (⟦_⟧ to ⟦_⟧S) hunk ./CompositionBased/Lambda.agda 145 - open module C = Compositional using () renaming (⟦_⟧ to ⟦_⟧C) - open RC.Derivation - open MoreLaws∥ - - -- Semantic domain: stack → environment → result. + open module S = Semantics using () renaming (⟦_⟧ to ⟦_⟧S) + open StackEnv hunk ./CompositionBased/Lambda.agda 148 - Dom : Ctxt → Ctxt → Type → Set - Dom Δ Γ σ = Env Δ → Values Γ ⇨ Value σ - - -- A CPS-transformed variant of the semantic domain. + -- A CPS-transformed variant of Dom. hunk ./CompositionBased/Lambda.agda 151 - DomCPS Γ σ = ∀ Δ {τ} → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ + DomCPS Γ σ = ∀ {Δ τ} → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ hunk ./CompositionBased/Lambda.agda 153 - -- A composition operator used below. The first argument gets access - -- only to the environment, while the second one also gets to see - -- the stack. TODO: Is this operator related to Kripke models? (See - -- the application case below, for instance.) + -- A composition operator used to specify ⟦_⟧. The first argument + -- gets access only to the environment, while the second one also + -- gets to see the stack. TODO: Is this operator related to Kripke + -- models? (Observe how the contexts change in the lambda and + -- application cases below.) hunk ./CompositionBased/Lambda.agda 159 - infixr 9 _⟪_⟫_ _⟪_⟫-cong_ + infixr 9 _⊙_ _⊙-cong_ hunk ./CompositionBased/Lambda.agda 161 - _⟪_⟫_ : ∀ {Γ σ} → C.Dom Γ σ → DomCPS Γ σ - (f ⟪ _ ⟫ κ) s = f >>=∥ λ v → κ (v , s) + _⊙_ : ∀ {Γ σ} → S.Dom Γ σ → DomCPS Γ σ + (f ⊙ κ) s ρ = κ (f ρ , s) ρ hunk ./CompositionBased/Lambda.agda 164 - _⟪_⟫-cong_ : ∀ {Γ σ} {f₁ f₂ : C.Dom Γ σ} → - f₁ ≈ f₂ → - ∀ Δ {τ} {κ₁ κ₂ : Dom (σ ∷ Δ) Γ τ} → - (∀ s → κ₁ s ≈ κ₂ s) → - ∀ {s} → (f₁ ⟪ Δ ⟫ κ₁) s ≈ (f₂ ⟪ Δ ⟫ κ₂) s - (f₁≈f₂ ⟪ Δ ⟫-cong κ₁≈κ₂) {s} = f₁≈f₂ >>=∥-cong′ λ v → κ₁≈κ₂ (v , s) - where open MonadLaws∥ + _⊙-cong_ : ∀ {Γ σ} {f₁ f₂ : S.Dom Γ σ} → + (∀ ρ → f₁ ρ ≡ f₂ ρ) → + ∀ {Δ τ} {κ₁ κ₂ : Dom (σ ∷ Δ) Γ τ} → + κ₁ ≈ κ₂ → + f₁ ⊙ κ₁ ≈ f₂ ⊙ κ₂ + _⊙-cong_ {f₁ = f₁} {f₂} f₁≈f₂ {κ₁ = κ₁} {κ₂} κ₁≈κ₂ = + f₁ ⊙ κ₁ ≈⟨ (λ s ρ → P.cong (λ x → κ₁ (x , s) ρ) (f₁≈f₂ ρ)) ⟩ + f₂ ⊙ κ₁ ≈⟨ (λ s ρ → κ₁≈κ₂ (f₂ ρ , s) ρ) ⟩ + f₂ ⊙ κ₂ ∎ hunk ./CompositionBased/Lambda.agda 176 + -- One could calculate/devise some other definition of the lookup + -- function, but allowing the unary representation of variables to + -- affect the design of the machine/compiler seems like a bad idea. + hunk ./CompositionBased/Lambda.agda 181 - lookup x _ κ = λ s → C.lookup x >>=∥ λ v → κ (v , s) + lookup x κ = S.lookup x ⊙ κ hunk ./CompositionBased/Lambda.agda 184 - closure f Δ κ = push (f (lift tt)) ⟪ Δ ⟫ κ + closure f κ = (λ ρ v → f _ (v , ρ)) ⊙ κ + + closure-cong : ∀ {Γ σ τ} {f₁ f₂ : Dom [] (σ ∷ Γ) τ} → f₁ ≈ f₂ → + ∀ {Δ χ} (κ : Dom (σ ⟶ τ ∷ Δ) Γ χ) → + closure f₁ κ ≈ closure f₂ κ + closure-cong f₁≈f₂ κ = + (λ ρ → ext λ v → f₁≈f₂ _ (v , ρ)) ⊙-cong (κ ∎) hunk ./CompositionBased/Lambda.agda 192 - ret : ∀ {Γ σ} → Dom [ σ ] Γ σ - ret (v , s) = return∥ v + top : ∀ {Γ σ} → Dom [ σ ] Γ σ + top (v , s) ρ = v hunk ./CompositionBased/Lambda.agda 195 - app : ∀ {Γ σ τ χ} Δ → Dom (τ ∷ Δ) Γ χ → Dom (σ ⟶ τ ∷ σ ∷ Δ) Γ χ - app _ κ (f , x , s) = κ (f x , s) + app : ∀ {Γ Δ σ τ χ} → Dom (τ ∷ Δ) Γ χ → Dom (σ ∷ σ ⟶ τ ∷ Δ) Γ χ + app κ (x , f , s) = κ (f x , s) hunk ./CompositionBased/Lambda.agda 201 - ⟦ t ⟧ Δ κ s = witness (⟦ t ⟧′ Δ κ s) + ⟦ t ⟧ κ = proj₁ (⟦ t ⟧′ κ) hunk ./CompositionBased/Lambda.agda 203 - ⟦_⟧′ : ∀ {Γ σ} (t : Γ ⊢ σ) Δ {τ} (κ : Dom (σ ∷ Δ) Γ τ) (s : Env Δ) → - EqualTo ((⟦ t ⟧C ⟪ Δ ⟫ κ) s) - ⟦ var x ⟧′ Δ κ s = ▷ - (⟦ var x ⟧C ⟪ Δ ⟫ κ) s ≡⟨ P.refl ⟩ - C.lookup x >>=∥ (λ v → κ (v , s)) ≡⟨ P.refl ⟩ - lookup x Δ κ s ∎ + ⟦_⟧′ : ∀ {Γ σ} (t : Γ ⊢ σ) {Δ τ} (κ : Dom (σ ∷ Δ) Γ τ) → + EqualTo (⟦ t ⟧S ⊙ κ) + ⟦ var x ⟧′ κ = ▷ + ⟦ var x ⟧S ⊙ κ ≈⟨⟩ + S.lookup x ⊙ κ ≈⟨⟩ + lookup x κ ∎ hunk ./CompositionBased/Lambda.agda 210 - ⟦ ƛ t ⟧′ Δ κ s = ▷ - (⟦ ƛ t ⟧C ⟪ Δ ⟫ κ) s ≡⟨ P.refl ⟩ - (push ⟦ t ⟧C ⟪ Δ ⟫ κ) s ≈⟨ Stack.push-cong ext (sym $ identity-⊙∥ ⟦ t ⟧C) ⟪ Δ ⟫-cong refl ∘ κ ⟩ - (push ((⟦ t ⟧C ⟪ [] ⟫ ret) (lift tt)) ⟪ Δ ⟫ κ) s ≈⟨ Stack.push-cong ext (proof $ ⟦ t ⟧′ [] ret (lift tt)) ⟪ Δ ⟫-cong refl ∘ κ ⟩ - (push (⟦ t ⟧ [] ret (lift tt)) ⟪ Δ ⟫ κ) s ≡⟨ P.refl ⟩ - (closure (⟦ t ⟧ [] ret) Δ κ) s ∎ + ⟦ ƛ t ⟧′ κ = ▷ + ⟦ ƛ t ⟧S ⊙ κ ≈⟨⟩ + (λ ρ v → ⟦ t ⟧S (v , ρ)) ⊙ κ ≈⟨⟩ + closure (⟦ t ⟧S ⊙ top) κ ≈⟨ closure-cong (proj₂ $ ⟦ t ⟧′ top) κ ⟩ + closure (⟦ t ⟧ top) κ ∎ hunk ./CompositionBased/Lambda.agda 216 - ⟦ t₁ · t₂ ⟧′ Δ κ s = ▷ - (⟦ t₁ · t₂ ⟧C ⟪ Δ ⟫ κ) s ≡⟨ P.refl ⟩ - (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ⊙∥ (Λ λ v → κ (v , s)) ≈⟨ Stack.wk-ap (⟦ t₁ ⟧C) (⟦ t₂ ⟧C) (Λ λ v → κ (v , s)) ⟩ - ⟦ t₂ ⟧C ⊙∥ wk ⟦ t₁ ⟧C ⊙∥ ap (Λ λ v → κ (v , s)) ≡⟨ P.refl ⟩ - (⟦ t₂ ⟧C >>=∥ λ x → ⟦ t₁ ⟧C >>=∥ λ f → κ (f x , s)) ≡⟨ P.refl ⟩ - (⟦ t₂ ⟧C ⟪ Δ ⟫ ⟦ t₁ ⟧C ⟪ _ ∷ Δ ⟫ app Δ κ) s ≈⟨ refl ⟦ t₂ ⟧C ⟪ Δ ⟫-cong (proof ∘ ⟦ t₁ ⟧′ (_ ∷ Δ) (app Δ κ)) ⟩ - (⟦ t₂ ⟧C ⟪ Δ ⟫ ⟦ t₁ ⟧ (_ ∷ Δ) (app Δ κ)) s ≈⟨ proof $ ⟦ t₂ ⟧′ Δ (⟦ t₁ ⟧ (_ ∷ Δ) (app Δ κ)) s ⟩ - ⟦ t₂ ⟧ Δ (⟦ t₁ ⟧ (_ ∷ Δ) (app Δ κ)) s ∎ + ⟦ t₁ · t₂ ⟧′ κ = ▷ + ⟦ t₁ · t₂ ⟧S ⊙ κ ≈⟨⟩ + (λ ρ → ⟦ t₁ ⟧S ρ (⟦ t₂ ⟧S ρ)) ⊙ κ ≈⟨⟩ + ⟦ t₁ ⟧S ⊙ ⟦ t₂ ⟧S ⊙ app κ ≈⟨ (λ _ → P.refl) ⊙-cong proj₂ (⟦ t₂ ⟧′ (app κ)) ⟩ + ⟦ t₁ ⟧S ⊙ ⟦ t₂ ⟧ (app κ) ≈⟨ proj₂ $ ⟦ t₁ ⟧′ (⟦ t₂ ⟧ (app κ)) ⟩ + ⟦ t₁ ⟧ (⟦ t₂ ⟧ (app κ)) ∎ hunk ./CompositionBased/Lambda.agda 223 - correct : ∀ {Γ σ} (t : Γ ⊢ σ) ρ → - ⟦ t ⟧S ρ ≡ RC.uncurry (⟦ t ⟧ [] ret (lift tt)) ρ + correct : ∀ {Γ σ} (t : Γ ⊢ σ) ρ → ⟦ t ⟧S ρ ≡ ⟦ t ⟧ top _ ρ hunk ./CompositionBased/Lambda.agda 225 - ⟦ t ⟧S ρ ≡⟨ P.sym $ uncurry∘curry (Values Γ) ⟦ t ⟧S ρ ⟩′ - RC.uncurry (RC.curry {As = Values Γ} ⟦ t ⟧S) ρ ≡⟨ uncurry-cong (proof $ C.⟦_⟧′ t) ρ ⟩′ - RC.uncurry ⟦ t ⟧C ρ ≡⟨ uncurry-cong (sym $ identity-⊙∥ ⟦ t ⟧C) ρ ⟩′ - RC.uncurry ((⟦ t ⟧C ⟪ [] ⟫ ret) (lift tt)) ρ ≡⟨ uncurry-cong (proof $ ⟦ t ⟧′ [] ret (lift tt)) ρ ⟩′ - RC.uncurry (⟦ t ⟧ [] ret (lift tt)) ρ ∎′ - where - open CurryLaws - open P.≡-Reasoning renaming (_≡⟨_⟩_ to _≡⟨_⟩′_; _∎ to _∎′) + ⟦ t ⟧S ρ ≡⟨ P.refl ⟩ + (⟦ t ⟧S ⊙ top) _ ρ ≡⟨ proj₂ (⟦ t ⟧′ top) _ ρ ⟩ + ⟦ t ⟧ top _ ρ □ + where open P.≡-Reasoning renaming (_∎ to _□) hunk ./CompositionBased/Lambda.agda 232 - ⟦_⟧-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 ∘ κ) + ⟦_⟧-cong : ∀ {Γ σ} (t : Γ ⊢ σ) {Δ τ} {κ₁ κ₂ : Dom (σ ∷ Δ) Γ τ} → + κ₁ ≈ κ₂ → ⟦ t ⟧ κ₁ ≈ ⟦ t ⟧ κ₂ + ⟦_⟧-cong t {κ₁ = κ₁} {κ₂} κ₁≈κ₂ = + ⟦ t ⟧ κ₁ ≈⟨ sym $ proj₂ $ ⟦ t ⟧′ κ₁ ⟩ + ⟦ t ⟧S ⊙ κ₁ ≈⟨ (λ _ → P.refl) ⊙-cong κ₁≈κ₂ ⟩ + ⟦ t ⟧S ⊙ κ₂ ≈⟨ proj₂ $ ⟦ t ⟧′ κ₂ ⟩ + ⟦ t ⟧ κ₂ ∎ hunk ./CompositionBased/Lambda.agda 245 - open Semantics using () renaming (⟦_⟧ to ⟦_⟧S) + private + open module S = Semantics using () renaming (⟦_⟧ to ⟦_⟧S) hunk ./CompositionBased/Lambda.agda 248 - open ≈-Reasoning + open StackEnv hunk ./CompositionBased/Lambda.agda 250 + -- I defunctionalise with respect to Dom. + hunk ./CompositionBased/Lambda.agda 258 - ret : ∀ {Γ σ} → Term [ σ ] Γ σ + top : ∀ {Γ σ} → Term [ σ ] Γ σ hunk ./CompositionBased/Lambda.agda 260 - (t : Term (τ ∷ Δ) Γ χ) → Term (σ ⟶ τ ∷ σ ∷ Δ) Γ χ + (t : Term (τ ∷ Δ) Γ χ) → Term (σ ∷ σ ⟶ τ ∷ Δ) Γ χ hunk ./CompositionBased/Lambda.agda 263 + -- + -- Note that exec is /not/ a virtual machine: in the closure case + -- there is a non-tail call. hunk ./CompositionBased/Lambda.agda 267 - 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) + exec : ∀ {Γ Δ σ} → Term Δ Γ σ → Dom Δ Γ σ + exec (lookup x t) s ρ = exec t (S.lookup x ρ , s) ρ + exec (closure t₁ t₂) s ρ = exec t₂ ((λ v → exec t₁ _ (v , ρ)) , s) ρ + exec top (v , s) ρ = v + exec (app t) (x , f , s) ρ = exec t (f x , s) ρ hunk ./CompositionBased/Lambda.agda 280 - 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 + comp′ : ∀ {Γ Δ σ τ} (t : Γ ⊢ σ) (κ : Term (σ ∷ Δ) Γ τ) → + ∃ λ (t′ : Term Δ Γ τ) → ⟦ t ⟧CPS (exec κ) ≈ exec t′ + comp′ (var x) κ = lookup x κ , ( + ⟦ var x ⟧CPS (exec κ) ≈⟨⟩ + CPS.lookup x (exec κ) ≈⟨⟩ + exec (lookup x κ) ∎) hunk ./CompositionBased/Lambda.agda 287 - exec : ∀ {Γ Δ σ} → Term Δ Γ σ → Dom Δ Γ σ - exec t s ρ = witness $ exec′ t s ρ + comp′ (ƛ t) κ = closure (comp t top) κ , ( + ⟦ ƛ t ⟧CPS (exec κ) ≈⟨⟩ + CPS.closure (⟦ t ⟧CPS CPS.top) (exec κ) ≈⟨ CPS.closure-cong (proj₂ $ comp′ t top) (exec κ) ⟩ + exec (closure (comp t top) κ) ∎) hunk ./CompositionBased/Lambda.agda 292 - 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. + comp′ (t₁ · t₂) κ = comp t₁ (comp t₂ (app κ)) , ( + ⟦ t₁ · t₂ ⟧CPS (exec κ) ≈⟨⟩ + ⟦ t₁ ⟧CPS (⟦ t₂ ⟧CPS (CPS.app (exec κ))) ≈⟨⟩ + ⟦ t₁ ⟧CPS (⟦ t₂ ⟧CPS (exec (app κ))) ≈⟨ ⟦ t₁ ⟧CPS-cong (proj₂ $ comp′ t₂ (app κ)) ⟩ + ⟦ t₁ ⟧CPS (exec (comp t₂ (app κ))) ≈⟨ proj₂ (comp′ t₁ (comp t₂ (app κ))) ⟩ + exec (comp t₁ (comp t₂ (app κ))) ∎) hunk ./CompositionBased/Lambda.agda 300 - ⟦ t ⟧S ρ ≡ exec (D.comp t ret) (lift tt) ρ + ⟦ t ⟧S ρ ≡ exec (comp t top) _ ρ hunk ./CompositionBased/Lambda.agda 302 - ⟦ 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) ρ ∎ + ⟦ t ⟧S ρ ≡⟨ CPS.correct t ρ ⟩ + ⟦ t ⟧CPS CPS.top _ ρ ≡⟨ proj₂ (comp′ t top) _ ρ ⟩ + exec (comp t top) _ ρ □ + where open P.≡-Reasoning renaming (_∎ to _□)