From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Sun, 8 Jan 2017 01:39:52 +0000 (+0500)
Subject: Added typingnetwork
X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=8501ad7f372d8e16a2830cf126fb58863799a564;p=jolie.agda.git

Added typingnetwork
---

diff --git a/src/Service.agda b/src/Service.agda
index e2745af..7c65e06 100644
--- a/src/Service.agda
+++ b/src/Service.agda
@@ -21,7 +21,7 @@ MessageQueue = Queue Message
 data Process : Set where
   _∙_∙_ : Behaviour → List Variable → MessageQueue → Process
   nil : Process
-  par : Process → Process → Process
+  _∥_ : Process → Process → Process
 
 data AliasingFunction : Set where
 
diff --git a/src/TypingNetwork.agda b/src/TypingNetwork.agda
new file mode 100644
index 0000000..3816edd
--- /dev/null
+++ b/src/TypingNetwork.agda
@@ -0,0 +1,16 @@
+module TypingNetwork where
+
+open import Network
+open import Type
+
+data _⊢N_ : ∀ {n} → Ctx n → Network → Set where
+  t-network-nil : ∀ {n} {Γ : Ctx n}
+                ----------
+                → Γ ⊢N nil
+
+  -- TODO: implement t-network and t-deployment
+
+  t-restriction : ∀ {n} {Γ : Ctx n} {n : Network}
+                → Γ ⊢N n
+                -----------
+                → Γ ⊢N νr n