[Modified the "Kripke"-approach. Nils Anders Danielsson **20101220170727 Ignore-this: c554455fa1dfdcd643fd1b7e3391acca + I realised that this approach is very close to the one which separates the environment and the stack. ] hunk ./CompositionBased/Lambda.agda 168 - open module C = Compositional using (Dom) renaming (⟦_⟧ to ⟦_⟧C) + open module C = Compositional using () renaming (⟦_⟧ to ⟦_⟧C) hunk ./CompositionBased/Lambda.agda 172 - -- The composition operator used below. + -- Semantic domain: stack → environment → result. hunk ./CompositionBased/Lambda.agda 174 - infix 9 [_]_◌_ + Dom : Ctxt → Ctxt → Type → Set + Dom Δ Γ σ = Values Δ ++ Values Γ ⇨ Value σ + + -- A composition operator used below. The first argument gets access + -- only to the environment, while the second one also gets to see + -- the stack: [ Δ ] f ◌ κ ≈ λ ρ s → κ ρ (f ρ , s). TODO: Is this + -- operator related to Kripke models? hunk ./CompositionBased/Lambda.agda 182 - [_]_◌_ : ∀ Γ {Δ σ τ} → - Dom Δ σ → - Values (σ ∷ Γ) ++ Values Δ ⇨ Value τ → - Values Γ ++ Values Δ ⇨ Value τ - [ Γ ] f ◌ g = const⋆ (Values Γ) f ⊙∥ g + infix 9 [_]_◌_ hunk ./CompositionBased/Lambda.agda 184 - -- Lookup. + [_]_◌_ : ∀ {Γ} Δ {σ τ} → C.Dom Γ σ → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ + [ Δ ] f ◌ g = const⋆ (Values Δ) f ⊙∥ g hunk ./CompositionBased/Lambda.agda 187 - top : ∀ Γ {Δ σ τ} → - Values (σ ∷ Γ) ++ Values (σ ∷ Δ) ⇨ Value τ → - Values Γ ++ Values (σ ∷ Δ) ⇨ Value τ - top Γ κ = [ Γ ] identity∥ ◌ κ + -- Lookup. The lookup function doesn't need access to the stack, so + -- C.Dom and _⊙∥_ are used instead of Dom and [_]_◌_. hunk ./CompositionBased/Lambda.agda 190 - const⋆-const⋆′ : ∀ {X : Set} (as bs : List X) {Cs D} - (F : X → Set) (f : Cs ⇨ D) → - const⋆ (List.map F as) (const⋆ (List.map F bs) f) ≈ - const⋆ (List.map F (as ++ bs)) f - const⋆-const⋆′ [] bs F f = refl _ - const⋆-const⋆′ (a ∷ as) bs F f = Λ-cong λ _ → const⋆-const⋆′ as bs F f + top : ∀ {Γ σ τ} → C.Dom (σ ∷ σ ∷ Γ) τ → C.Dom (σ ∷ Γ) τ + top κ = Λ λ v → κ ∙ v ∙ v hunk ./CompositionBased/Lambda.agda 193 - lemma : ∀ Γ {τ Δ} → - Values (Γ ∷ʳ τ) ++ Values Δ ≡ Values Γ ++ Values (τ ∷ Δ) - lemma Γ {τ} {Δ} = begin - Values (Γ ∷ʳ τ) ++ Values Δ ≡⟨ P.cong (λ As → As ++ Values Δ) $ ListProp.map-++-commute Value Γ [ τ ] ⟩′ - (Values Γ ∷ʳ Value τ) ++ Values Δ ≡⟨ Monoid.assoc (List.monoid Set) (Values Γ) _ _ ⟩′ - Values Γ ++ Values (τ ∷ Δ) ∎′ - where - open P.≡-Reasoning - using (begin_) renaming (_≡⟨_⟩_ to _≡⟨_⟩′_; _∎ to _∎′) + push-under : ∀ {Γ σ τ χ} → + C.Dom (σ ∷ τ ∷ Γ) χ → C.Dom (σ ∷ Γ) (τ ⟶ χ) + push-under κ = Λ λ v → push (κ ∙ v) hunk ./CompositionBased/Lambda.agda 199 - lookup : ∀ {Δ σ τ} → Δ ∋ σ → - ∀ Γ → Values (σ ∷ Γ) ++ Values Δ ⇨ Value τ → - Values Γ ++ Values Δ ⇨ Value τ - lookup x Γ κ = witness (lookup′ x Γ κ) + lookup : ∀ {Γ σ τ} → Γ ∋ σ → C.Dom (σ ∷ Γ) τ → C.Dom Γ τ + lookup x κ = witness (lookup′ x κ) hunk ./CompositionBased/Lambda.agda 202 - lookup′ : ∀ {Δ σ τ} - (x : Δ ∋ σ) Γ (κ : Values (σ ∷ Γ) ++ Values Δ ⇨ Value τ) → - EqualTo ([ Γ ] C.lookup x ◌ κ) - lookup′ zero Γ κ = ▷ - [ Γ ] C.lookup zero ◌ κ ≡⟨ P.refl ⟩ - [ Γ ] identity∥ ◌ κ ≡⟨ P.refl ⟩ - top Γ κ ∎ + lookup′ : ∀ {Γ σ τ} (x : Γ ∋ σ) (κ : C.Dom (σ ∷ Γ) τ) → + EqualTo (C.lookup x ⊙∥ κ) + lookup′ zero κ = ▷ + C.lookup zero ⊙∥ κ ≡⟨ P.refl ⟩ + identity∥ ⊙∥ κ ≡⟨ 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 211 - lookup′ (suc {σ = σ} {τ = τ} x) Γ κ = ▷ - [ Γ ] C.lookup (suc x) ◌ κ ≡⟨ P.refl ⟩ - const⋆ (Values Γ) (wk (C.lookup x)) ⊙∥ κ ≈⟨ const⋆-const⋆′ Γ [ τ ] Value (C.lookup x) ⊙∥-cong - sym (Cast.drop lemma′ κ) ⟩ - const⋆ (Values (Γ ∷ʳ τ)) (C.lookup x) ⊙∥ cast lemma′ κ ≈⟨ proof $ lookup′ x (Γ ∷ʳ τ) (cast lemma′ κ) ⟩ - lookup x (Γ ∷ʳ τ) (cast lemma′ κ) ≈⟨ sym $ Cast.drop (lemma Γ) _ ⟩ - cast (lemma Γ) (lookup x (Γ ∷ʳ τ) (cast lemma′ κ)) ∎ - where - lemma′ = P.sym $ lemma (σ ∷ Γ) + 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 227 - closure : ∀ {Δ σ τ} Γ → - Dom (σ ∷ Δ) τ → Values Γ ++ Values Δ ⇨ Value (σ ⟶ τ) - closure Γ = const⋆ (Values Γ) ∘ push + closure : ∀ {Γ σ τ χ} Δ → + Dom [ σ ] Γ τ → Dom (σ ⟶ τ ∷ Δ) Γ χ → Dom Δ Γ χ + closure Δ f κ = const⋆ (Values Δ) (push f) ⊙∥ κ hunk ./CompositionBased/Lambda.agda 231 - ret : ∀ {Γ σ} → Dom (σ ∷ Γ) σ + ret : ∀ {Γ σ} → Dom [ σ ] Γ σ hunk ./CompositionBased/Lambda.agda 234 + weaken : ∀ {Γ σ τ} Δ → + (C.Dom (σ ∷ Γ) τ → C.Dom Γ τ) → + (Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ) + weaken Δ f κ = join {As = Values Δ} (RC.curry λ s → + f (Λ λ v → RC.uncurry (split (Values Δ) (κ ∙ v)) s)) + + weaken-cong : ∀ {Γ σ τ} Δ {f₁ f₂ : C.Dom (σ ∷ Γ) τ → C.Dom Γ τ} → + (∀ κ → f₁ κ ≈ f₂ κ) → + ∀ κ → weaken Δ f₁ κ ≈ weaken Δ f₂ κ + weaken-cong [] f₁≈f₂ κ = f₁≈f₂ κ + weaken-cong (σ ∷ Δ) f₁≈f₂ κ = Λ-cong λ v → + weaken-cong Δ f₁≈f₂ (Λ λ v′ → κ ∙ v′ ∙ v) + + weaken-lemma : ∀ {Γ σ τ} Δ (f : C.Dom Γ σ) (κ : Dom (σ ∷ Δ) Γ τ) → + const⋆ (Values Δ) f ⊙∥ κ ≈ weaken Δ (λ κ → f ⊙∥ κ) κ + weaken-lemma [] f κ = refl (f ⊙∥ κ) + weaken-lemma (σ ∷ Δ) f κ = Λ-cong λ v → + weaken-lemma Δ f (Λ λ v′ → κ ∙ v′ ∙ v) + hunk ./CompositionBased/Lambda.agda 255 - ⟦_⟧ : ∀ {Δ σ τ} → Δ ⊢ σ → - ∀ Γ → Values (σ ∷ Γ) ++ Values Δ ⇨ Value τ → - Values Γ ++ Values Δ ⇨ Value τ - ⟦ t ⟧ Γ f = witness (⟦ t ⟧′ Γ f) + ⟦_⟧ : ∀ {Γ σ τ} → Γ ⊢ σ → ∀ Δ → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ + ⟦ t ⟧ Δ f = witness (⟦ t ⟧′ Δ f) hunk ./CompositionBased/Lambda.agda 258 - ⟦_⟧′ : ∀ {Δ σ τ} - (t : Δ ⊢ σ) Γ (κ : Values (σ ∷ Γ) ++ Values Δ ⇨ Value τ) → - EqualTo ([ Γ ] ⟦ t ⟧C ◌ κ) - ⟦ var x ⟧′ Γ κ = ▷ - [ Γ ] ⟦ var x ⟧C ◌ κ ≡⟨ P.refl ⟩ - [ Γ ] C.lookup x ◌ κ ≈⟨ proof (lookup′ x Γ κ) ⟩ - lookup x Γ κ ∎ + ⟦_⟧′ : ∀ {Γ σ τ} (t : Γ ⊢ σ) Δ (κ : Dom (σ ∷ Δ) Γ τ) → + EqualTo ([ Δ ] ⟦ t ⟧C ◌ κ) + ⟦ var x ⟧′ Δ κ = ▷ + [ Δ ] ⟦ var x ⟧C ◌ κ ≡⟨ P.refl ⟩ + const⋆ (Values Δ) (C.lookup x) ⊙∥ κ ≈⟨ weaken-lemma Δ (C.lookup x) κ ⟩ + weaken Δ (λ κ → C.lookup x ⊙∥ κ) κ ≈⟨ weaken-cong Δ (λ κ → proof $ lookup′ x κ) κ ⟩ + weaken Δ (lookup x) κ ∎ hunk ./CompositionBased/Lambda.agda 266 - ⟦ t₁ · t₂ ⟧′ Γ κ = ▷ - [ Γ ] ⟦ t₁ · t₂ ⟧C ◌ κ ≡⟨ P.refl ⟩ - const⋆ (Values Γ) (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ⊙∥ κ ≈⟨ const⋆-⊛∥ (Values Γ) ⟦ t₁ ⟧C ⟦ t₂ ⟧C ⊙∥-cong refl κ ⟩ - (const⋆ (Values Γ) ⟦ t₁ ⟧C ⊛∥ const⋆ (Values Γ) ⟦ t₂ ⟧C) ⊙∥ κ ≈⟨ Stack.wk-ap (const⋆ (Values Γ) ⟦ t₁ ⟧C) - (const⋆ (Values Γ) ⟦ t₂ ⟧C) κ ⟩ - const⋆ (Values Γ) ⟦ t₂ ⟧C ⊙∥ - wk (const⋆ (Values Γ) ⟦ t₁ ⟧C) ⊙∥ ap κ ≡⟨ P.refl ⟩ - const⋆ (Values Γ) ⟦ t₂ ⟧C ⊙∥ - const⋆ (Values (_ ∷ Γ)) ⟦ t₁ ⟧C ⊙∥ ap κ ≈⟨ refl (const⋆ (Values Γ) ⟦ t₂ ⟧C) ⊙∥-cong - proof (⟦ t₁ ⟧′ (_ ∷ Γ) (ap κ)) ⟩ - const⋆ (Values Γ) ⟦ t₂ ⟧C ⊙∥ ⟦ t₁ ⟧ (_ ∷ Γ) (ap κ) ≈⟨ proof $ ⟦ t₂ ⟧′ Γ (⟦ t₁ ⟧ (_ ∷ Γ) (ap κ)) ⟩ - ⟦ t₂ ⟧ Γ (⟦ t₁ ⟧ (_ ∷ Γ) (ap κ)) ∎ + ⟦ t₁ · t₂ ⟧′ Δ κ = ▷ + [ Δ ] ⟦ t₁ · t₂ ⟧C ◌ κ ≡⟨ P.refl ⟩ + const⋆ (Values Δ) (⟦ t₁ ⟧C ⊛∥ ⟦ t₂ ⟧C) ⊙∥ κ ≈⟨ const⋆-⊛∥ (Values Δ) ⟦ t₁ ⟧C ⟦ t₂ ⟧C ⊙∥-cong refl κ ⟩ + (const⋆ (Values Δ) ⟦ t₁ ⟧C ⊛∥ const⋆ (Values Δ) ⟦ t₂ ⟧C) ⊙∥ κ ≈⟨ Stack.wk-ap (const⋆ (Values Δ) ⟦ t₁ ⟧C) + (const⋆ (Values Δ) ⟦ t₂ ⟧C) κ ⟩ + const⋆ (Values Δ) ⟦ t₂ ⟧C ⊙∥ + wk (const⋆ (Values Δ) ⟦ t₁ ⟧C) ⊙∥ ap κ ≡⟨ P.refl ⟩ + const⋆ (Values Δ) ⟦ t₂ ⟧C ⊙∥ + const⋆ (Values (_ ∷ Δ)) ⟦ t₁ ⟧C ⊙∥ ap κ ≈⟨ refl (const⋆ (Values Δ) ⟦ t₂ ⟧C) ⊙∥-cong + proof (⟦ t₁ ⟧′ (_ ∷ Δ) (ap κ)) ⟩ + const⋆ (Values Δ) ⟦ t₂ ⟧C ⊙∥ ⟦ t₁ ⟧ (_ ∷ Δ) (ap κ) ≈⟨ proof $ ⟦ t₂ ⟧′ Δ (⟦ t₁ ⟧ (_ ∷ Δ) (ap κ)) ⟩ + ⟦ t₂ ⟧ Δ (⟦ t₁ ⟧ (_ ∷ Δ) (ap κ)) ∎ hunk ./CompositionBased/Lambda.agda 279 - ⟦ ƛ t ⟧′ Γ κ = ▷ - [ Γ ] ⟦ ƛ t ⟧C ◌ κ ≡⟨ P.refl ⟩ - const⋆ (Values Γ) (push ⟦ t ⟧C) ⊙∥ κ ≈⟨ const⋆-cong (Values Γ) (Stack.push-cong ext $ sym $ identity-⊙∥ ⟦ t ⟧C) + ⟦ ƛ t ⟧′ Δ κ = ▷ + [ Δ ] ⟦ ƛ t ⟧C ◌ κ ≡⟨ P.refl ⟩ + const⋆ (Values Δ) (push ⟦ t ⟧C) ⊙∥ κ ≈⟨ const⋆-cong (Values Δ) (Stack.push-cong ext $ sym $ identity-⊙∥ ⟦ t ⟧C) hunk ./CompositionBased/Lambda.agda 284 - const⋆ (Values Γ) (push ([ [] ] ⟦ t ⟧C ◌ ret)) ⊙∥ κ ≈⟨ const⋆-cong (Values Γ) (Stack.push-cong ext $ proof $ ⟦ t ⟧′ [] ret) + const⋆ (Values Δ) (push ([ [] ] ⟦ t ⟧C ◌ ret)) ⊙∥ κ ≈⟨ const⋆-cong (Values Δ) (Stack.push-cong ext $ proof $ ⟦ t ⟧′ [] ret) hunk ./CompositionBased/Lambda.agda 287 - const⋆ (Values Γ) (push (⟦ t ⟧ [] ret)) ⊙∥ κ ≡⟨ P.refl ⟩ - closure Γ (⟦ t ⟧ [] ret) ⊙∥ κ ∎ + const⋆ (Values Δ) (push (⟦ t ⟧ [] ret)) ⊙∥ κ ≡⟨ P.refl ⟩ + closure Δ (⟦ t ⟧ [] ret) κ ∎ hunk ./CompositionBased/Lambda.agda 290 - correct : ∀ {Δ σ} (t : Δ ⊢ σ) → - ∃₂ λ Γ (κ : Values (σ ∷ Γ) ++ Values Δ ⇨ Value σ) → - RC.curry {As = Values Δ} ⟦ t ⟧S ≈ ⟦ t ⟧ Γ κ - correct t = [] , ret , ( - RC.curry ⟦ t ⟧S ≈⟨ proof $ Compositional.⟦_⟧′ t ⟩ - ⟦ t ⟧C ≈⟨ sym $ identity-⊙∥ _ ⟩ - ⟦ t ⟧C ⊙∥ ret ≈⟨ proof $ ⟦ t ⟧′ [] ret ⟩ - ⟦ t ⟧ [] ret ∎) - --- What happens if we continue with the code above? I don't know, but --- rather than having only two components in the resulting machine --- (code + stack), I think it seems nicer to have three (code + stack --- + environment). Let's try this. - -module CPS₂ where - - private - open module S = Semantics - using (Env) renaming (⟦_⟧ to ⟦_⟧S) - open Derivation - open P.≡-Reasoning - - Cont : Type → Set - Cont σ = ∀ Δ {τ} → S.Dom (σ ∷ Δ) τ → S.Dom Δ τ - - ret : ∀ {Γ σ} → S.Dom (σ ∷ Γ) σ - ret = proj₁ - - Dom : Ctxt → Type → Set - Dom Γ σ = Env Γ → Cont σ - - closure : ∀ Γ {σ τ} → Dom (σ ∷ Γ) τ → S.Dom Γ (σ ⟶ τ) - closure _ d ρ = λ v → d (v , ρ) [] proj₁ (lift tt) - - app : ∀ Γ {σ τ χ} → S.Dom (τ ∷ Γ) χ → S.Dom (σ ⟶ τ ∷ σ ∷ Γ) χ - app _ κ (f , x , ρ) = κ (f x , ρ) - - mutual - - ⟦_⟧ : ∀ {Γ σ} → Γ ⊢ σ → Dom Γ σ - ⟦ t ⟧ ρ Δ κ s = witness (⟦ t ⟧′ ρ Δ κ s) - - ⟦_⟧′ : ∀ {Γ σ τ} - (t : Γ ⊢ σ) (ρ : Env Γ) - Δ (κ : S.Dom (σ ∷ Δ) τ) (s : Env Δ) → - EqualTo (κ (⟦ t ⟧S ρ , s)) - ⟦ var x ⟧′ ρ Δ κ s = ▷ begin - κ (S.lookup x ρ , s) ∎ - - ⟦_⟧′ {Γ = Γ} (ƛ t) ρ Δ κ s = ▷ begin - κ (⟦ ƛ t ⟧S ρ , s) ≡⟨ P.refl ⟩ - κ ((λ v → ⟦ t ⟧S (v , ρ)) , s) ≡⟨ P.refl ⟩ - κ ((λ v → proj₁ {b = zero} {B = λ _ → Lift ⊤} - (⟦ t ⟧S (v , ρ) , lift tt)) , s) ≡⟨ P.cong (λ f → κ (f , s)) (ext λ v → - proof $ ⟦ t ⟧′ (v , ρ) [] proj₁ (lift tt)) ⟩ - κ ((λ v → ⟦ t ⟧ (v , ρ) [] proj₁ (lift tt)) , s) ≡⟨ P.refl ⟩ - κ (closure Γ ⟦ t ⟧ ρ , s) ∎ - - ⟦ t₁ · t₂ ⟧′ ρ Δ κ s = ▷ begin - κ (⟦ t₁ · t₂ ⟧S ρ , s) ≡⟨ P.refl ⟩ - κ (⟦ t₁ ⟧S ρ (⟦ t₂ ⟧S ρ) , s) ≡⟨ P.refl ⟩ - app Δ κ (⟦ t₁ ⟧S ρ , ⟦ t₂ ⟧S ρ , s) ≡⟨ proof $ ⟦ t₁ ⟧′ ρ (_ ∷ Δ) (app Δ κ) _ ⟩ - ⟦ t₁ ⟧ ρ (_ ∷ Δ) (app Δ κ) (⟦ t₂ ⟧S ρ , s) ≡⟨ proof $ ⟦ t₂ ⟧′ ρ Δ (⟦ t₁ ⟧ ρ (_ ∷ Δ) (app Δ κ)) s ⟩ - ⟦ t₂ ⟧ ρ Δ (⟦ t₁ ⟧ ρ (_ ∷ Δ) (app Δ κ)) s ∎ + correct : ∀ {Γ σ} (t : Γ ⊢ σ) ρ → + ⟦ t ⟧S ρ ≡ RC.uncurry (⟦ t ⟧ [] ret) ρ + correct {Γ} t ρ = begin + ⟦ 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) ρ ≡⟨ uncurry-cong (proof $ ⟦ t ⟧′ [] ret) ρ ⟩′ + RC.uncurry (⟦ t ⟧ [] ret) ρ ∎′ + where + open CurryLaws + open P.≡-Reasoning renaming (_≡⟨_⟩_ to _≡⟨_⟩′_; _∎ to _∎′)