Add semantics rules for behavioural layer.

diff --git a/src/Interpreter.agda b/src/Interpreter.agda
new file mode 100644 (file)
index 0000000..1b29e57
--- /dev/null
+++ b/src/Interpreter.agda
@@ -0,0 +1,66 @@
+module Interpreter where
+
+open import Type
+open import Behaviour
+open import Variable
+open import Expr
+
+
+data Label : Set where
+  -- Behavioural layer
+  -- x = e
+  lb-assign : Variable → Expr → Label
+
+  -- read t
+  -- TODO: t - state of underlying process
+  lb-read : Label
+
+  -- νr o@l(e)
+  lb-send : Channel → Operation → Location → Expr → Label
+
+  -- r : o(x)
+  lb-store : Channel → Operation → Variable → Label
+
+  -- (r, o)!x
+  lb-write : Channel → Operation → Variable → Label
+
+  -- (r, o@l)?x
+  lb-read-write : Channel → Operation → Location → Variable → Label
+
+  -- Service layer
+  -- τ
+  ls-interal : Label
+
+  -- νr o@l(t)
+  ls-send : Channel → Operation → Location → Label
+
+  -- νr o(t)
+  ls-store : Channel → Operation → Label
+
+  -- (r, o)!t
+  ls-write : Channel → Operation → Label
+
+  -- (r, o@l)?t
+  ls-read-write : Channel → Operation → Location → Label
+
+data _↝_∶_ : Behaviour → Behaviour → Label → Set where
+  b-assign : {x : Variable} {e : Expr}
+           → (x ≃ e) ↝ nil ∶ lb-assign x e
+
+  b-wait : {r : Channel} {o : Operation} {l : Location} {x : Variable}
+         → wait r o l x ↝ nil ∶ lb-read-write r o l x
+ 
+  b-oneway : {o : Operation} {x : Variable} {r : Channel}
+           → input (o [ x ]) ↝ nil ∶ lb-store r o x
+
+  b-notification : {r : Channel} {o : Operation} {l : Location} {e : Expr}
+                 → output (o at l [ e ]) ↝ nil ∶ lb-send r o l e
+
+  b-solresp : {r : Channel} {o : Operation} {l : Location} {e : Expr} {x : Variable}
+            → output (o at l [ e ][ x ]) ↝ wait r o l x ∶ lb-send r o l e
+
+  b-reqresp : {r : Channel} {o : Operation} {x x′ : Variable} {b : Behaviour}
+            → input (o [ x ][ x′ ] b) ↝ exec r o x′ b ∶ lb-store r o x
+
+  b-end-exec : {r : Channel} {o : Operation} {x : Variable}
+             → exec r o x nil ↝ nil ∶ lb-write r o x