[Made the separation of the stack and the environment more obvious. Nils Anders Danielsson **20101220191930 Ignore-this: 1542b47af89d33e8c7f0be10e744bd4 ] hunk ./CompositionBased/Lambda.agda 152 - open Semantics using (Value; Values) renaming (⟦_⟧ to ⟦_⟧S) + open Semantics using (Value; Values; Env) renaming (⟦_⟧ to ⟦_⟧S) hunk ./CompositionBased/Lambda.agda 161 - Dom Δ Γ σ = Values Δ ++ Values Γ ⇨ Value σ + Dom Δ Γ σ = Env Δ → Values Γ ⇨ Value σ + + -- A CPS-transformed variant of the semantic domain. + + DomCPS : Ctxt → Type → Set + DomCPS Γ σ = ∀ Δ {τ} → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ hunk ./CompositionBased/Lambda.agda 170 - -- the stack: [ Δ ] f ◌ κ ≈ λ ρ s → κ ρ (f ρ , s). TODO: Is this - -- operator related to Kripke models? + -- the stack. TODO: Is this operator related to Kripke models? (See + -- the application case below, for instance.) hunk ./CompositionBased/Lambda.agda 173 - infix 9 [_]_◌_ + infixr 9 _⟪_⟫_ _⟪_⟫-cong_ hunk ./CompositionBased/Lambda.agda 175 - [_]_◌_ : ∀ {Γ} Δ {σ τ} → C.Dom Γ σ → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ - [ Δ ] f ◌ g = const⋆ (Values Δ) f ⊙∥ g + _⟪_⟫_ : ∀ {Γ σ} → C.Dom Γ σ → DomCPS Γ σ + (f ⟪ _ ⟫ κ) s = f >>=∥ λ v → κ (v , s) + + _⟪_⟫-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∥ hunk ./CompositionBased/Lambda.agda 188 - lookup : ∀ {Γ σ τ} → Γ ∋ σ → ∀ Δ → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ - lookup x Δ κ = const⋆ (Values Δ) (C.lookup x) ⊙∥ κ + lookup : ∀ {Γ σ} → Γ ∋ σ → DomCPS Γ σ + lookup x _ κ = λ s → C.lookup x >>=∥ λ v → κ (v , s) hunk ./CompositionBased/Lambda.agda 191 - closure : ∀ {Γ σ τ χ} Δ → - Dom [ σ ] Γ τ → Dom (σ ⟶ τ ∷ Δ) Γ χ → Dom Δ Γ χ - closure Δ f κ = const⋆ (Values Δ) (push f) ⊙∥ κ + closure : ∀ {Γ σ τ} → Dom [] (σ ∷ Γ) τ → DomCPS Γ (σ ⟶ τ) + closure f Δ κ = push (f (lift tt)) ⟪ Δ ⟫ κ hunk ./CompositionBased/Lambda.agda 195 - ret = identity∥ + ret (v , s) = return∥ v + + app : ∀ {Γ σ τ χ} Δ → Dom (τ ∷ Δ) Γ χ → Dom (σ ⟶ τ ∷ σ ∷ Δ) Γ χ + app _ κ (f , x , s) = κ (f x , s) hunk ./CompositionBased/Lambda.agda 202 - ⟦_⟧ : ∀ {Γ σ τ} → Γ ⊢ σ → ∀ Δ → Dom (σ ∷ Δ) Γ τ → Dom Δ Γ τ - ⟦ t ⟧ Δ f = witness (⟦ t ⟧′ Δ f) + ⟦_⟧ : ∀ {Γ σ} → Γ ⊢ σ → DomCPS Γ σ + ⟦ t ⟧ Δ κ s = witness (⟦ t ⟧′ Δ κ s) hunk ./CompositionBased/Lambda.agda 205 - ⟦_⟧′ : ∀ {Γ σ τ} (t : Γ ⊢ σ) Δ (κ : Dom (σ ∷ Δ) Γ τ) → - EqualTo ([ Δ ] ⟦ t ⟧C ◌ κ) - ⟦ var x ⟧′ Δ κ = ▷ - [ Δ ] ⟦ var x ⟧C ◌ κ ≡⟨ P.refl ⟩ - const⋆ (Values Δ) (C.lookup x) ⊙∥ κ ≡⟨ P.refl ⟩ - lookup x Δ κ ∎ + ⟦_⟧′ : ∀ {Γ σ} (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 ∎ hunk ./CompositionBased/Lambda.agda 212 - ⟦ 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 ⟧′ Δ κ 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 ∎ hunk ./CompositionBased/Lambda.agda 219 - ⟦ ƛ t ⟧′ Δ κ = ▷ - [ Δ ] ⟦ ƛ t ⟧C ◌ κ ≡⟨ P.refl ⟩ - const⋆ (Values Δ) (push ⟦ t ⟧C) ⊙∥ κ ≈⟨ const⋆-cong (Values Δ) (Stack.push-cong ext $ sym $ identity-⊙∥ ⟦ t ⟧C) - ⊙∥-cong - refl κ ⟩ - const⋆ (Values Δ) (push ([ [] ] ⟦ t ⟧C ◌ ret)) ⊙∥ κ ≈⟨ const⋆-cong (Values Δ) (Stack.push-cong ext $ proof $ ⟦ t ⟧′ [] ret) - ⊙∥-cong - refl κ ⟩ - const⋆ (Values Δ) (push (⟦ t ⟧ [] ret)) ⊙∥ κ ≡⟨ P.refl ⟩ - closure Δ (⟦ t ⟧ [] ret) κ ∎ + ⟦ 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 ∎ hunk ./CompositionBased/Lambda.agda 229 - ⟦ t ⟧S ρ ≡ RC.uncurry (⟦ t ⟧ [] ret) ρ + ⟦ t ⟧S ρ ≡ RC.uncurry (⟦ t ⟧ [] ret (lift tt)) ρ hunk ./CompositionBased/Lambda.agda 234 - RC.uncurry ([ [] ] ⟦ t ⟧C ◌ ret) ρ ≡⟨ uncurry-cong (proof $ ⟦ t ⟧′ [] ret) ρ ⟩′ - RC.uncurry (⟦ t ⟧ [] ret) ρ ∎′ + RC.uncurry ((⟦ t ⟧C ⟪ [] ⟫ ret) (lift tt)) ρ ≡⟨ uncurry-cong (proof $ ⟦ t ⟧′ [] ret (lift tt)) ρ ⟩′ + RC.uncurry (⟦ t ⟧ [] ret (lift tt)) ρ ∎′