Expand behaviour's typing rules. Add network and service typing rules.

diff --git a/src/Network.agda b/src/Network.agda
index b413c91601b1c4bfce95e55d1f9dab964bd73ba5..34631bb5f89b76185f8e5e397218f7e77eacd038 100644 (file)
--- a/src/Network.agda
+++ b/src/Network.agda
@@ -1,5 +1,6 @@
 module Network where
 
+open import Data.List using (List; []; [_]; _++_)
 open import Type
 open import Service
 
@@ -9,3 +10,9 @@ data Network : Set where
   νr : Network → Network
   _∥_ : Network → Network → Network
   nil : Network
+
+locs : Network → List Location
+locs (νr n) = locs n
+locs (n₁ ∥ n₂) = locs n₁ ++ locs n₂
+locs nil = []
+locs ([ s ] l) = [ l ]

diff --git a/src/Type.agda b/src/Type.agda
index a275abef083f1b8e3d130436cd92192a3c4a9994..f5c31303ce8056aaba6d49ea725f8d703dad25a5 100644 (file)
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -2,18 +2,13 @@ module Type where
 
 open import Data.Nat using (ℕ)
 open import Data.String using (String)
-open import Data.Vec using (Vec)
+open import Data.Vec using (Vec) renaming (_∷_ to _∷-Vec_)
 open import Variable
 
 
-Operation : Set
-Operation = String
-
-Location : Set
-Location = String
-
-Channel : Set
-Channel = String
+data Operation : Set where
+data Location : Set where
+data Channel : Set where
 
 data Type : Set where
   bool int double long string raw void : Type
@@ -30,3 +25,21 @@ data _⊆_ : Type → Type → Set where
 
 Ctx : ℕ → Set
 Ctx = Vec TypeDecl
+
+data Context : Set where
+  ◆ : ∀ {n} → Ctx n → Context
+  ■ : ∀ {n m} → Ctx n → Ctx m → Context
+
+infix 4 _∈_
+
+data _∈_ : TypeDecl → Context → Set where
+  here-◆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ◆ (x ∷-Vec xs)
+  there-◆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ◆ xs) → x ∈ ◆ (y ∷-Vec xs)
+  here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (x ∷-Vec xs) ys
+  here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ xs (x ∷-Vec ys)
+  there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ (x ∷-Vec xs) ys
+  there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ xs (x ∷-Vec ys)
+
+_∷_ : TypeDecl → Context → Context
+t ∷ ◆ xs = ◆ (t ∷-Vec xs)
+x ∷ ■ xs ys = ■ (x ∷-Vec xs) ys

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 642c23f60ecad267e6bf3212c2e792c2453b482e..7d82a792cc914652ba161e233bae4562a2fdca3a 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -5,7 +5,7 @@ open import Relation.Nullary using (¬_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Data.Nat using (ℕ)
 open import Data.List using (List)
-open import Data.Vec using (_∈_; []; _++_; _∷_; here; there)
+open import Data.Vec using ([]; _++_)
 open import Data.Product using (_,_; _×_)
 open import Function
 open import Expr
@@ -22,143 +22,132 @@ data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour 
   -- Identity
   idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b
 
-data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
+data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where
   expr-t : {s : Expr} {b : Type}
          → Γ ⊢ₑ s ∶ b
 
-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}
+  t-nil : {Γ : Context}
         ------------------
-        → ◆ Γ ⊢B nil ▹ ◆ Γ
+        → Γ ⊢B nil ▹ Γ
           
-  t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} {e : Expr}
+  t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr}
        → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
-       → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
-       → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁
+       → Γ ⊢B b₁ ▹ Γ₁
+       → Γ ⊢B b₂ ▹ Γ₁
        --------------------------
-       → ◆ Γ ⊢B if e then b₁ else b₂ ▹ ◆ Γ₁
+       → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁
           
-  t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr} 
+  t-while : {Γ : Context} {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 (η × Behaviour)}
-           → All (λ { (η , b) → ◆ Γ ⊢B (input η) ∶ b ▹ ◆ Γ₁ }) choices
+  t-choice : {Γ Γ₁ : Context} {choices : List (η × Behaviour)}
+           → All (λ { (η , b) → Γ ⊢B (input η) ∶ b ▹ Γ₁ }) choices
            -----------------------------------
-           → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
+           → Γ ⊢B inputchoice choices ▹ Γ₁
 
   t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour}
         → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
         → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
-        --------------------------------------
+        ------------------------------------
         → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
 
-  t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b₁ b₂ : Behaviour}
-        → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
-        → ◆ Γ₁ ⊢B b₂ ▹ ◆ Γ₂
-        -------------------------
-        → ◆ Γ ⊢B b₁ ∶ b₂ ▹ ◆ Γ₂
+  t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
+        → Γ ⊢B b₁ ▹ Γ₁
+        → Γ₁ ⊢B b₂ ▹ Γ₂
+        -----------------------
+        → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂
 
-  t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
+  t-notification : {Γ : Context} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
                  → var e Tₑ ∈ Γ
                  → Tₑ ⊆ T₀
                  ------------------------------------------------
-                 → ◆ Γ ⊢B output (o at l [ var e ]) ▹ ◆ Γ
+                 → Γ ⊢B output (o at l [ var e ]) ▹ Γ
 
-  t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+  t-assign-new : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
                → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
                --------------------------------------
-               → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
+               → Γ ⊢B x ≃ e ▹ (var x Tₑ ∷ Γ)
 
-  t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+  t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
                   → var x Tₓ ∈ Γ
                   → Tₑ ≡ Tₓ
                   -------------------------
-                  → ◆ Γ ⊢B x ≃ e ▹ ◆ Γ
+                  → Γ ⊢B x ≃ e ▹ Γ
 
-  t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+  t-oneway-new : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                → inOneWay o Tᵢ ∈ Γ
                → ¬ (var x Tₓ ∈ Γ)
-               ----------------------------------------------
-               → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
+               ---------------------------------------
+               → Γ ⊢B input (o [ x ]) ▹ (var x Tᵢ ∷ Γ)
 
-  t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+  t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → inOneWay o Tᵢ ∈ Γ
                   → var x Tₓ ∈ Γ
                   → Tᵢ ⊆ Tₓ
-                  ---------------------------------
-                  → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ Γ
+                  --------------------------
+                  → Γ ⊢B input (o [ x ]) ▹ Γ
 
-  t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+  t-solresp-new : {Γ : Context} {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 (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
+                --------------------------------------------------
+                → Γ ⊢B output (o at 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}
+  t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                    → outSolRes o l Tₒ Tᵢ ∈ Γ
                    → Tₑ ⊆ Tₒ
                    → var x Tₓ ∈ Γ
                    → Tᵢ ⊆ Tₓ
-                   ------------------------------------------
-                   → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ Γ
+                   -------------------------------------
+                   → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ
 
-  t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
+  t-reqresp-new : {Γ Γ₁ : Context} {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 (o [ x ][ a ] b) ▹ ◆ Γ₁
+                ----------------------------------
+                → Γ ⊢B input (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}
+  t-reqresp-exists : {Γ Γ₁ : Context} {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 (o [ x ][ a ] b) ▹ ◆ Γ₁
+                   ----------------------------------
+                   → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
 
-  t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
+  t-wait-new : {Γ : Context} {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}
+  t-wait-exists : {Γ : Context} {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}
+  t-exec : {Γ Γ₁ : Context} {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 ▹ ◆ Γ₁
-
-  t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b₁ b₂ : Behaviour}
-           → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂
-           → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
-           ------------------
-           → ◆ Γₐ ⊢B b₂ ▹ ◆ Γ₁
-
+         ------------------------
+         → Γ ⊢B exec r o x b ▹ Γ₁
 
 struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour}
                   → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
@@ -171,18 +160,7 @@ struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁
                     → ◆ Γ₁ ⊢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₁} {b₁ b₂ : Behaviour}
-                    → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
-                    → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
-struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
-
-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
+--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₁

diff --git a/src/TypingNetwork.agda b/src/TypingNetwork.agda
index 3816edd20593403042977ed5047384b5bfa6b694..be79b1ab7d917b5cb024df27cc88fa94a4c5fc7b 100644 (file)
--- a/src/TypingNetwork.agda
+++ b/src/TypingNetwork.agda
@@ -1,16 +1,35 @@
 module TypingNetwork where
 
+open import Relation.Nullary using (¬_)
+open import Data.Vec using (_∈_; fromList)
+open import Data.Product using (_,_)
+open import TypingService
+open import Service
 open import Network
 open import Type
+open import Behaviour
 
-data _⊢N_ : ∀ {n} → Ctx n → Network → Set where
+
+data _⊢N_ : Context → Network → Set where
   t-network-nil : ∀ {n} {Γ : Ctx n}
-                ----------
-                → Γ ⊢N nil
+                ------------
+                → ◆ Γ ⊢N nil
+
+  t-deployment : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {l : Location} {o : Operation} {p : Process} {d : Deployment m} {Tₒ : Type}
+               → Γ ⊢S (b ▹ d - p)
+               → ¬ (outNotify o l Tₒ ∈ Γ)
+               --------------------------
+               → ◆ Γ ⊢N ([ b ▹ d - p ] l)
 
-  -- TODO: implement t-network and t-deployment
+  t-network : ∀ {n} {m} {Γ₁ : Ctx n} {Γ₂ : Ctx m} {N₁ N₂ : Network} {l : Location}
+            → ◆ Γ₁ ⊢N N₁
+            → ◆ Γ₂ ⊢N N₂
+--            →  , ¬ (l ∈ fromList (locs N₁))
+            → ¬ (l ∈ fromList (locs N₂))
+            ----------------------
+            → ■ Γ₁ Γ₂ ⊢N (N₁ ∥ N₂)
 
   t-restriction : ∀ {n} {Γ : Ctx n} {n : Network}
-                → Γ ⊢N n
-                -----------
-                → Γ ⊢N νr n
+                → ◆ Γ ⊢N n
+                -------------
+                → ◆ Γ ⊢N νr n

diff --git a/src/TypingService.agda b/src/TypingService.agda
index 7e2dc36295f46c5a33126f71bc38a660ce6b1500..eeefc58f5935c725c2c5034f392fab5e5d638623 100644 (file)
--- a/src/TypingService.agda
+++ b/src/TypingService.agda
@@ -6,7 +6,7 @@ open import Data.List.All using (All)
 open import Data.Vec using (Vec; toList; concat; _∈_)
 open import Data.List using (List; zip)
 open import Data.Product using (_×_; _,_)
-open import TypingBehaviour using (_⊢B_▹_; ◆)
+open import TypingBehaviour using (_⊢B_▹_)
 open import Type
 open import Service
 open import Behaviour
@@ -41,6 +41,8 @@ data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
 
 
 data _⊢S_ : ∀ {n} → Ctx n → Service → Set where
-  t-service : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {d : Deployment m} {p : Process}
+  t-service : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {b : Behaviour} {d : Deployment m} {p : Process}            
+            → Γ ⊢BSL b ▹ Γ₁
+            → Γ ⊢P p
             ------------------
             → Γ ⊢S (b ▹ d - p)