Eugene Akentyev
·
2017-01-16
Behaviour.agda
1module Behaviour where
2
3open import Data.String using (String)
4open import Data.List using (List)
5open import Data.Product using (_×_)
6open import Variable
7open import Expr
8open import Type
9
10-- Output
11data η̂ : Set where
12 -- o@l(e) -- Notification
13 _at_[_] : Operation → Location → Expr → η̂
14
15 -- o@l(e)(x) -- Solicit-response
16 _at_[_][_] : Operation → Location → Expr → Variable → η̂
17
18data Behaviour : Set
19
20-- Input
21data η : Set where
22 -- o(x) -- One-way
23 _[_] : Operation → Variable → η
24
25 -- o(x)(x'){B} -- Request-response
26 _[_][_]_ : Operation → Variable → Variable → Behaviour → η
27
28data Behaviour where
29 input : η → Behaviour
30 output : η̂ → Behaviour
31 if_then_else_ : Expr → Behaviour → Behaviour → Behaviour
32 while[_]_ : Expr → Behaviour → Behaviour
33
34 -- Sequence
35 _∶_ : Behaviour → Behaviour → Behaviour
36
37 -- Parallel
38 _∥_ : Behaviour → Behaviour → Behaviour
39
40 -- Assign
41 _≃_ : Variable → Expr → Behaviour
42
43 nil : Behaviour
44
45 -- [η₁]{B₁}⋯[ηₐ]{Bₐ} -- Input choice
46 inputchoice : List (η × Behaviour) → Behaviour
47
48 wait : Channel → Operation → Location → Variable → Behaviour
49 exec : Channel → Operation → Variable → Behaviour → Behaviour
50