repos / jolie.agda.git

commit

eacd202

parent

91d804c

author

Eugene Akentyev

date

2017-01-16 16:51:58 +0400 +04

Add t-bsl-choice

 1@@ -14,8 +14,12 @@ open import Behaviour
 2 open import Variable
 3 
 4 
 5+-- Side effect
 6 data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour → Set where
 7+  -- Updated
 8   upd : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} → Γ ⊢ b₁ ↦ Γ₁ ⊢ b₂
 9+
10+  -- Identity
11   idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b
12 
13 data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
14@@ -49,12 +53,11 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
15            -----------------------------------
16            → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
17 
18-  t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁}
19-          {b1 b2 : Behaviour}
20-       → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
21-       → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
22-       --------------------------------------
23-       → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
24+  t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour}
25+        → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
26+        → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
27+        --------------------------------------
28+        → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
29 
30   t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b₁ b₂ : Behaviour}
31         → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁

 1@@ -1,12 +1,16 @@
 2 module TypingService where
 3 
 4+open import Relation.Binary.PropositionalEquality using (_≢_)
 5+open import Relation.Nullary using (¬_)
 6 open import Data.List.All using (All)
 7-open import Data.List using (List)
 8+open import Data.Vec using (Vec; toList; concat; _∈_)
 9+open import Data.List using (List; zip)
10 open import Data.Product using (_×_; _,_)
11-open import TypingBehaviour using (_⊢B_▹_)
12+open import TypingBehaviour using (_⊢B_▹_; ◆)
13 open import Type
14 open import Service
15 open import Behaviour
16+open import Variable
17 
18 
19 data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
20@@ -14,10 +18,13 @@ data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
21             ----------------
22             → Γ ⊢BSL nil ▹ Γ
23 
24--- TODO: finish
25---  t-bsl-choice : ∀ {n} {Γ : Ctx n} {Γ₁ : Ctx n} {choices : List (Input_ex × Behaviour)}
26---               → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
27---               → Γ ⊢BSL 
28+  t-bsl-choice : ∀ {n m k} {Γ : Ctx n} {contexts : Vec (Ctx m) k} {choices : List (η × Behaviour)} {Tₐ Tₓ : Type} {x : Variable}
29+               → All (λ { (Γ₁ , (η , b)) → ◆ Γ ⊢B input η ∶ b ▹ ◆ Γ₁ }) (zip (toList contexts) choices)
30+               → ¬ (var x Tₓ ∈ concat contexts)
31+               → ¬ (var x Tₐ ∈ concat contexts)
32+               → Tₓ ≢ Tₐ
33+               ----------------------------------------------
34+               → Γ ⊢BSL inputchoice choices ▹ concat contexts
35 
36 data _⊢state_ : ∀ {n} → Ctx n → Process → Set where
37 
38@@ -30,7 +37,7 @@ data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
39                 → Γ ⊢P p₁
40                 → Γ ⊢P p₂
41                 ----------------
42-                → Γ ⊢P par p₁ p₂
43+                → Γ ⊢P (p₁ ∥ p₂)
44 
45 
46 data _⊢S_ : ∀ {n} → Ctx n → Service → Set where