repos / jolie.agda.git

Service.agda

 1module Service where
 2
 3open import Data.Nat using (ℕ)
 4open import Data.List using (List)
 5open import Data.String using (String)
 6open import Data.Product using (_×_)
 7open import Type
 8open import Behaviour
 9open import Variable
10
11
12Queue : (A : Set) → Set
13Queue A = List A
14
15Message : Set
16Message = Channel × Operation × String
17
18MessageQueue : Set
19MessageQueue = Queue Message
20
21data Process : Set where
22  _∙_∙_ : Behaviour → List Variable → MessageQueue → Process
23  nil : Process
24  _∥_ : Process → Process → Process
25
26data AliasingFunction : Set where
27
28Deployment : (m : ℕ) → Set
29Deployment m = AliasingFunction × Ctx m
30
31data Service : Set where
32  _▹_-_ : {m : ℕ} → Behaviour → Deployment m → Process → Service