From 1d23c479cd2ca14c8b64719c134373f272be7e2b Mon Sep 17 00:00:00 2001 From: Eugene Akentyev Date: Tue, 3 Jan 2017 03:49:52 +0500 Subject: [PATCH] Added disjoint union --- src/TypingBehaviour.agda | 96 ++++++++++++++++++++-------------------- src/TypingService.agda | 3 ++ 2 files changed, 51 insertions(+), 48 deletions(-) diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda index efef10e..73fea36 100644 --- a/src/TypingBehaviour.agda +++ b/src/TypingBehaviour.agda @@ -24,82 +24,85 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where expr-t : {s : Expr} {b : Type} → Γ ⊢ₑ s ∶ b -data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where +data Context : Set where + ◆ : ∀ {n} → Ctx n → Context + ■ : ∀ {n m} → Ctx n → Ctx m → Context + +data _⊢B_▹_ : Context → Behaviour → Context → Set where t-nil : ∀ {n} {Γ : Ctx n} -------------- - → Γ ⊢B nil ▹ Γ + → ◆ Γ ⊢B nil ▹ ◆ Γ t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool - → Γ ⊢B b1 ▹ Γ₁ - → Γ ⊢B b2 ▹ Γ₁ + → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ + → ◆ Γ ⊢B b2 ▹ ◆ Γ₁ ---------------------- - → Γ ⊢B if e b1 b2 ▹ Γ₁ + → ◆ Γ ⊢B if e b1 b2 ▹ ◆ Γ₁ t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool - → Γ ⊢B b ▹ Γ + → ◆ Γ ⊢B b ▹ ◆ Γ --------------------- - → Γ ⊢B while e b ▹ Γ + → ◆ Γ ⊢B while e b ▹ ◆ Γ t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)} - → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices + → All (λ { (η , b) → ◆ Γ ⊢B seq (input η) b ▹ ◆ Γ₁ }) choices ------------------------------- - → Γ ⊢B inputchoice choices ▹ Γ₁ + → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁ - t-par : ∀ {n m} {Γ : Ctx n} {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour} - {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m} - → Γ₁ ⊢B b1 ▹ Γ₁' - → Γ₂ ⊢B b2 ▹ Γ₂' - -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions - ---------------------------------------- - → (Γ₁ ++ Γ₂) ⊢B par b1 b2 ▹ (Γ₁' ++ Γ₂') + t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} + {b1 b2 : Behaviour} + → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁' + → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂' + -------------------------------------- + → (■ Γ₁ Γ₂) ⊢B par b1 b2 ▹ (■ Γ₁' Γ₂') t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour} - → Γ ⊢B b1 ▹ Γ₁ - → Γ₁ ⊢B b2 ▹ Γ₂ + → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ + → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂ --------------------- - → Γ ⊢B seq b1 b2 ▹ Γ₂ + → ◆ Γ ⊢B seq b1 b2 ▹ ◆ Γ₂ t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type} → (outNotify o l T₀) ∈ Γ → Γ ⊢ e ∶ Tₑ → Tₑ ⊆ T₀ --------------------------------------------- - → Γ ⊢B output (notification o l (var e)) ▹ Γ + → ◆ Γ ⊢B output (notification o l (var e)) ▹ ◆ Γ t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ ----------------------------------- - → Γ ⊢B assign x e ▹ (var x Tₑ ∷ Γ) + → ◆ Γ ⊢B assign x e ▹ ◆ (var x Tₑ ∷ Γ) t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ → var x Tₓ ∈ Γ → Tₑ ≡ Tₓ ---------------------- - → Γ ⊢B assign x e ▹ Γ + → ◆ Γ ⊢B assign x e ▹ ◆ Γ t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} → inOneWay o Tᵢ ∈ Γ → ¬ (var x Tₓ ∈ Γ) ------------------------------------------ - → Γ ⊢B input (oneway o x) ▹ (var x Tᵢ ∷ Γ) + → ◆ Γ ⊢B input (oneway o x) ▹ ◆ (var x Tᵢ ∷ Γ) t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} → inOneWay o Tᵢ ∈ Γ → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ ------------------------------ - → Γ ⊢B input (oneway o x) ▹ Γ + → ◆ Γ ⊢B input (oneway o x) ▹ ◆ Γ t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → Tₑ ⊆ Tₒ → ¬ (var x Tₓ ∈ Γ) -------------------------------------------------- - → Γ ⊢B output (solicitres o l e x) ▹ (var x Tᵢ ∷ Γ) + → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ (var x Tᵢ ∷ Γ) t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ @@ -107,70 +110,67 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ --------------------------------------- - → Γ ⊢B output (solicitres o l e x) ▹ Γ + → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ Γ t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour} → inReqRes o Tᵢ Tₒ ∈ Γ → ¬ (var x Tₓ ∈ Γ) - → (var x Tₓ ∷ Γ) ⊢B b ▹ Γ₁ + → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁ → var a Tₐ ∈ Γ₁ → Tₐ ⊆ Tₒ ---------------------------------- - → Γ ⊢B input (reqres o x a b) ▹ Γ₁ + → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁ t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable} → (inReqRes o Tᵢ Tₒ) ∈ Γ → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ - → Γ ⊢B b ▹ Γ₁ + → ◆ Γ ⊢B b ▹ ◆ Γ₁ → var a Tₐ ∈ Γ₁ → Tₐ ⊆ Tₒ ---------------------------------- - → Γ ⊢B input (reqres o x a b) ▹ Γ₁ + → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁ t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → ¬ (var x Tₓ ∈ Γ) ------------------------------------ - → Γ ⊢B wait r o l x ▹ (var x Tᵢ ∷ Γ) + → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ) t-wait-exists : ∀ {n} {Γ : Ctx n} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ ------------------------ - → Γ ⊢B wait r o l x ▹ Γ + → ◆ Γ ⊢B wait r o l x ▹ ◆ Γ t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable} → inReqRes o Tᵢ Tₒ ∈ Γ - → Γ ⊢B b ▹ Γ₁ + → ◆ Γ ⊢B b ▹ ◆ Γ₁ → var x Tₓ ∈ Γ → Tₓ ⊆ Tₒ ------------------------ - → Γ ⊢B exec r o x b ▹ Γ₁ + → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁ -struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → b1 ≡ b2 → Γ ⊢B b2 ▹ Γ₁ +struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁ struct-congruence t refl = t -struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (seq nil b) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁ +struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (seq nil b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁ struct-cong-nil (t-seq t-nil t) = t ---struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁ ---struct-cong-par-nil (t-par t t-nil) = {!!} - ---struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁ ---struct-cong-par-sym (t-par t₁ t₂) = {!!} +struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁' +struct-cong-par-nil (t-par t t-nil) = t ---struct-cong-par-assoc : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 b3 : Behaviour} → Γ ⊢B par (par b1 b2) b3 ▹ Γ₁ → Γ ⊢B par b1 (par b2 b3) ▹ Γ₁ ---struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!} +struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b1 b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (par b2 b1) ▹ ■ Γ₂' Γ₁' +struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁ data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁ identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ undefined : SideEffect [] [] ---preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁ ---preservation t undefined = t ---preservation t (identity γ) = t ---preservation t-nil (updated {_} {k} Γ Γₐ) = t-nil {k} {Γₐ} ---preservation = {!!} +preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁ +preservation t undefined = t +preservation t (identity γ) = t +--preservation t-nil (updated {_} {k} Γ Γₐ) = {!!} +preservation = {!!} diff --git a/src/TypingService.agda b/src/TypingService.agda index 1eb1d4e..0006a18 100644 --- a/src/TypingService.agda +++ b/src/TypingService.agda @@ -18,6 +18,8 @@ data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where -- → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices -- → Γ ⊢BSL +data _⊢state_ : ∀ {n} → Ctx n → Process → Set where + data _⊢P_ : ∀ {n} → Ctx n → Process → Set where t-process-nil : ∀ {n} {Γ : Ctx n} ---------- @@ -29,6 +31,7 @@ data _⊢P_ : ∀ {n} → Ctx n → Process → Set where ---------------- → Γ ⊢P par p₁ p₂ + data _⊢S_ : ∀ {n} → Ctx n → Service → Set where t-service : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {d : Deployment m} {p : Process} ------------------ -- 2.50.1