From ced78ed921120218332215dd57032d3f0e8790d8 Mon Sep 17 00:00:00 2001 From: Eugene Akentyev Date: Thu, 19 Jan 2017 22:38:12 +0300 Subject: [PATCH] Update typing rules for network and service layers. --- src/TypingNetwork.agda | 14 +++++++------- src/TypingService.agda | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/TypingNetwork.agda b/src/TypingNetwork.agda index ad77cc3..c3d1b90 100644 --- a/src/TypingNetwork.agda +++ b/src/TypingNetwork.agda @@ -21,15 +21,15 @@ data _⊢N_ : Context → Network → Set where -------------------------- → Γ ⊢N ([ b ▹ d - p ] l) - t-network : ∀ {n} {m} {Γ₁ : Ctx n} {Γ₂ : Ctx m} {N₁ N₂ : Network} {l : Location} - → ◆ Γ₁ ⊢N N₁ - → ◆ Γ₂ ⊢N N₂ + t-network : {Γ₁ Γ₂ : Context} {N₁ N₂ : Network} {l : Location} + → Γ₁ ⊢N N₁ + → Γ₂ ⊢N N₂ -- → , ¬ (l ∈ fromList (locs N₁)) → ¬ (l ∈-Vec fromList (locs N₂)) ---------------------- - → ■ (◆ Γ₁) (◆ Γ₂) ⊢N (N₁ ∥ N₂) + → & Γ₁ Γ₂ ⊢N (N₁ ∥ N₂) - t-restriction : ∀ {n} {Γ : Ctx n} {n : Network} - → ◆ Γ ⊢N n + t-restriction : {Γ : Context} {n : Network} + → Γ ⊢N n ------------- - → ◆ Γ ⊢N νr n + → Γ ⊢N νr n diff --git a/src/TypingService.agda b/src/TypingService.agda index efe748f..3953627 100644 --- a/src/TypingService.agda +++ b/src/TypingService.agda @@ -20,12 +20,12 @@ data _⊢BSL_▹_ : Context → Behaviour → Context → Set where -- TODO t-bsl-choice : ∀ {m k} {Γ : Context} {contexts : Vec (Ctx m) k} {choices : List (η × Behaviour)} {Tₐ Tₓ : Type} {x : Variable} - → All (λ { (Γ₁ , (η , b)) → Γ ⊢B input η ∶ b ▹ ◆ Γ₁ }) (zip (toList contexts) choices) - → ¬ (var x Tₓ ∈ ◆ (concat contexts)) - → ¬ (var x Tₐ ∈ ◆ (concat contexts)) + → All (λ { (Γ₁ , (η , b)) → Γ ⊢B input η ∶ b ▹ ⋆ Γ₁ }) (zip (toList contexts) choices) + → ¬ (var x Tₓ ∈ ⋆ (concat contexts)) + → ¬ (var x Tₐ ∈ ⋆ (concat contexts)) → Tₓ ≢ Tₐ ---------------------------------------------- - → Γ ⊢BSL inputchoice choices ▹ ◆ (concat contexts) + → Γ ⊢BSL inputchoice choices ▹ ⋆ (concat contexts) data _⊢state_ : Context → Process → Set where -- 2.50.1