Rename side effect. Add comments.

diff --git a/src/Behaviour.agda b/src/Behaviour.agda
index 0a8010bbbb9cdfac8e792327ac0c806339ca9f6e..addfb76fe5f1d646fa5bf61993de3544253465e2 100644 (file)
--- a/src/Behaviour.agda
+++ b/src/Behaviour.agda
@@ -7,15 +7,22 @@ open import Variable
 open import Expr
 open import Type
 
-
-data η̂  : Set where
+-- Output
+data η̂ : Set where
+  -- o@l(e) -- Notification
   _at_[_] : Operation → Location → Expr → η̂
+
+  -- o@l(e)(x) -- Solicit-response
   _at_[_][_] : Operation → Location → Expr → Variable → η̂
 
 data Behaviour : Set
 
+-- Input
 data η : Set where
+  -- o(x) -- One-way
   _[_] : Operation → Variable → η
+
+  -- o(x)(x'){B} -- Request-response
   _[_][_]_ : Operation → Variable → Variable → Behaviour → η
 
 data Behaviour where
@@ -23,11 +30,21 @@ data Behaviour where
   output : η̂  → Behaviour
   if_then_else_ : Expr → Behaviour → Behaviour → Behaviour
   while[_]_ : Expr → Behaviour → Behaviour
+  
+  -- Sequence
   _∶_ : Behaviour → Behaviour → Behaviour
-  _∣_ : Behaviour → Behaviour → Behaviour
+
+  -- Parallel
+  _∥_ : Behaviour → Behaviour → Behaviour
+
+  -- Assign
   _≃_ : Variable → Expr → Behaviour
+
   nil : Behaviour
+
+  -- [η₁]{B₁}⋯[ηₐ]{Bₐ} -- Input choice
   inputchoice : List (η × Behaviour) → Behaviour
+
   wait : Channel → Operation → Location → Variable → Behaviour
   exec : Channel → Operation → Variable → Behaviour → Behaviour
 

diff --git a/src/Network.agda b/src/Network.agda
index a02f9b7daf929dc1f480ccc157c4ef4adde11851..b413c91601b1c4bfce95e55d1f9dab964bd73ba5 100644 (file)
--- a/src/Network.agda
+++ b/src/Network.agda
@@ -7,5 +7,5 @@ open import Service
 data Network : Set where
   [_]_ : Service → Location → Network
   νr : Network → Network
-  _||_ : Network → Network → Network
+  _∥_ : Network → Network → Network
   nil : Network

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index a9cd0efd8fccbaf55a115382d58f39c291522527..ee808692b2509b4349fb5f60c6222b00af6e7b17 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -14,10 +14,9 @@ open import Behaviour
 open import Variable
 
 
-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 [] []
+data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour → Set where
+  upd : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} → Γ ⊢ b₁ ↦ Γ₁ ⊢ b₂
+  idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b
 
 data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
   expr-t : {s : Expr} {b : Type}
@@ -32,12 +31,12 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
         ------------------
         → ◆ Γ ⊢B nil ▹ ◆ Γ
           
-  t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
+  t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} {e : Expr}
        → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
-       → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
-       → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
+       → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
+       → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁
        --------------------------
-       → ◆ Γ ⊢B if e then b1 else b2 ▹ ◆ Γ₁
+       → ◆ Γ ⊢B if e then b₁ else b₂ ▹ ◆ Γ₁
           
   t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr} 
           → Γ ⊢ₑ e ∶ bool
@@ -55,13 +54,13 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
        → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
        → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
        --------------------------------------
-       â\86\92 (â\96  Î\93â\82\81 Î\93â\82\82) â\8a¢B b1 â\88£ b2 ▹ (■ Γ₁' Γ₂')
+       â\86\92 (â\96  Î\93â\82\81 Î\93â\82\82) â\8a¢B b1 â\88¥ b2 ▹ (■ Γ₁' Γ₂')
 
-  t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
-        → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
-        → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂
+  t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b₁ b₂ : Behaviour}
+        → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
+        → ◆ Γ₁ ⊢B b₂ ▹ ◆ Γ₂
         -------------------------
-        → ◆ Γ ⊢B b1 ∶ b2 ▹ ◆ Γ₂
+        → ◆ Γ ⊢B b₁ ∶ b₂ ▹ ◆ Γ₂
 
   t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
@@ -151,25 +150,36 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
          ----------------------------
          → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
 
-  t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b : Behaviour}
-           → SideEffect Γ Γₐ
-           → ◆ Γ ⊢B b ▹ ◆ Γ₁
+  t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b₁ b₂ : Behaviour}
+           → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂
+           → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
            ------------------
-           → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
+           → ◆ Γₐ ⊢B 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} {b₁ b₂ : Behaviour}
+                  → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
+                  → b₁ ≡ b₂
+                  → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁
 struct-congruence t refl = t
 
-struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
-struct-cong-nil (t-seq x x₁) = t-mutate updated x₁
-struct-cong-nil (t-mutate x x₁) = t-mutate updated (struct-cong-nil x₁)
-
-struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b ∣ nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
+struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour}
+                    → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
+                    → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
 struct-cong-par-nil (t-par x _) = x
 
-struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b1 ∣ b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (b2 ∣ b1) ▹ ■ Γ₂' Γ₁'
+struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b₁ b₂ : Behaviour}
+                    → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
+                    → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
 
-preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
+struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour}
+                → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁
+                → ◆ Γ ⊢B b ▹ ◆ Γ₁
+struct-cong-nil = t-mutate upd
+
+preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour}
+             → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
+             → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂
+             → ◆ Γₐ ⊢B b₂ ▹ ◆ Γ₁
 preservation x s = t-mutate s x