repos / jolie.agda.git

commit

8501ad7

parent

54b8b36

author

Eugene Akentyev

date

2017-01-08 05:39:52 +0400 +04

Added typingnetwork

1@@ -21,7 +21,7 @@ MessageQueue = Queue Message
2 data Process : Set where
3   _∙_∙_ : Behaviour → List Variable → MessageQueue → Process
4   nil : Process
5-  par : Process → Process → Process
6+  _∥_ : Process → Process → Process
7 
8 data AliasingFunction : Set where
9 

 1@@ -0,0 +1,16 @@
 2+module TypingNetwork where
 3+
 4+open import Network
 5+open import Type
 6+
 7+data _⊢N_ : ∀ {n} → Ctx n → Network → Set where
 8+  t-network-nil : ∀ {n} {Γ : Ctx n}
 9+                ----------
10+                → Γ ⊢N nil
11+
12+  -- TODO: implement t-network and t-deployment
13+
14+  t-restriction : ∀ {n} {Γ : Ctx n} {n : Network}
15+                → Γ ⊢N n
16+                -----------
17+                → Γ ⊢N νr n