repos / jolie.agda.git

commit

fdb342f

parent

ced78ed

author

Eugene Akentyev

date

2017-01-26 10:32:27 +0400 +04

Add semantics rules for behavioural layer.

 1@@ -0,0 +1,66 @@
 2+module Interpreter where
 3+
 4+open import Type
 5+open import Behaviour
 6+open import Variable
 7+open import Expr
 8+
 9+
10+data Label : Set where
11+  -- Behavioural layer
12+  -- x = e
13+  lb-assign : Variable → Expr → Label
14+
15+  -- read t
16+  -- TODO: t - state of underlying process
17+  lb-read : Label
18+
19+  -- νr o@l(e)
20+  lb-send : Channel → Operation → Location → Expr → Label
21+
22+  -- r : o(x)
23+  lb-store : Channel → Operation → Variable → Label
24+
25+  -- (r, o)!x
26+  lb-write : Channel → Operation → Variable → Label
27+
28+  -- (r, o@l)?x
29+  lb-read-write : Channel → Operation → Location → Variable → Label
30+
31+  -- Service layer
32+  -- τ
33+  ls-interal : Label
34+
35+  -- νr o@l(t)
36+  ls-send : Channel → Operation → Location → Label
37+
38+  -- νr o(t)
39+  ls-store : Channel → Operation → Label
40+
41+  -- (r, o)!t
42+  ls-write : Channel → Operation → Label
43+
44+  -- (r, o@l)?t
45+  ls-read-write : Channel → Operation → Location → Label
46+
47+data _↝_∶_ : Behaviour → Behaviour → Label → Set where
48+  b-assign : {x : Variable} {e : Expr}
49+           → (x ≃ e) ↝ nil ∶ lb-assign x e
50+
51+  b-wait : {r : Channel} {o : Operation} {l : Location} {x : Variable}
52+         → wait r o l x ↝ nil ∶ lb-read-write r o l x
53+ 
54+  b-oneway : {o : Operation} {x : Variable} {r : Channel}
55+           → input (o [ x ]) ↝ nil ∶ lb-store r o x
56+
57+  b-notification : {r : Channel} {o : Operation} {l : Location} {e : Expr}
58+                 → output (o at l [ e ]) ↝ nil ∶ lb-send r o l e
59+
60+  b-solresp : {r : Channel} {o : Operation} {l : Location} {e : Expr} {x : Variable}
61+            → output (o at l [ e ][ x ]) ↝ wait r o l x ∶ lb-send r o l e
62+
63+  b-reqresp : {r : Channel} {o : Operation} {x x′ : Variable} {b : Behaviour}
64+            → input (o [ x ][ x′ ] b) ↝ exec r o x′ b ∶ lb-store r o x
65+
66+  b-end-exec : {r : Channel} {o : Operation} {x : Variable}
67+             → exec r o x nil ↝ nil ∶ lb-write r o x