Added typingnetwork

diff --git a/src/Service.agda b/src/Service.agda
index e2745af2a9c1d340724769c5ab347fb1f44b6411..7c65e06e0aa7993400acde9a2078459d0f52b978 100644 (file)
--- 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 (file)
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