repos / jolie.agda.git

commit

ced78ed

parent

d435954

author

Eugene Akentyev

date

2017-01-19 23:38:12 +0400 +04

Update typing rules for network and service layers.

 1@@ -21,15 +21,15 @@ data _⊢N_ : Context → Network → Set where
 2                --------------------------
 3                → Γ ⊢N ([ b ▹ d - p ] l)
 4 
 5-  t-network : ∀ {n} {m} {Γ₁ : Ctx n} {Γ₂ : Ctx m} {N₁ N₂ : Network} {l : Location}
 6-            → ◆ Γ₁ ⊢N N₁
 7-            → ◆ Γ₂ ⊢N N₂
 8+  t-network : {Γ₁ Γ₂ : Context} {N₁ N₂ : Network} {l : Location}
 9+            → Γ₁ ⊢N N₁
10+            → Γ₂ ⊢N N₂
11 --            →  , ¬ (l ∈ fromList (locs N₁))
12             → ¬ (l ∈-Vec fromList (locs N₂))
13             ----------------------
14-            → ■ (◆ Γ₁) (◆ Γ₂) ⊢N (N₁ ∥ N₂)
15+            → & Γ₁ Γ₂ ⊢N (N₁ ∥ N₂)
16 
17-  t-restriction : ∀ {n} {Γ : Ctx n} {n : Network}
18-                → ◆ Γ ⊢N n
19+  t-restriction : {Γ : Context} {n : Network}
20+                → Γ ⊢N n
21                 -------------
22-                → ◆ Γ ⊢N νr n
23+                → Γ ⊢N νr n

 1@@ -20,12 +20,12 @@ data _⊢BSL_▹_ : Context → Behaviour → Context → Set where
 2 
 3   -- TODO
 4   t-bsl-choice : ∀ {m k} {Γ : Context} {contexts : Vec (Ctx m) k} {choices : List (η × Behaviour)} {Tₐ Tₓ : Type} {x : Variable}
 5-               → All (λ { (Γ₁ , (η , b)) → Γ ⊢B input η ∶ b ▹ ◆ Γ₁ }) (zip (toList contexts) choices)
 6-               → ¬ (var x Tₓ ∈ ◆ (concat contexts))
 7-               → ¬ (var x Tₐ ∈ ◆ (concat contexts))
 8+               → All (λ { (Γ₁ , (η , b)) → Γ ⊢B input η ∶ b ▹ ⋆ Γ₁ }) (zip (toList contexts) choices)
 9+               → ¬ (var x Tₓ ∈ ⋆ (concat contexts))
10+               → ¬ (var x Tₐ ∈ ⋆ (concat contexts))
11                → Tₓ ≢ Tₐ
12                ----------------------------------------------
13-               → Γ ⊢BSL inputchoice choices ▹ ◆ (concat contexts)
14+               → Γ ⊢BSL inputchoice choices ▹ ⋆ (concat contexts)
15 
16 data _⊢state_ : Context → Process → Set where
17