Rename file and add remaining rules

diff --git a/src/BehaviouralSemantics.agda b/src/BehaviouralSemantics.agda
new file mode 100644 (file)
index 0000000..cbc55ad
--- /dev/null
+++ b/src/BehaviouralSemantics.agda
@@ -0,0 +1,100 @@
+module BehaviouralSemantics where
+
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Data.Vec using (Vec; toList) renaming (_∈_ to _∈-Vec_)
+open import Data.Bool using (true; false)
+open import Data.Product using (_×_; _,_)
+open import Type
+open import Behaviour
+open import Variable
+open import Expr
+
+
+data State : Set where
+
+data _⟨_⟩≔_ : Expr → State → Expr → Set where
+
+data Label : Set where
+  -- Behavioural layer
+  -- x = e
+  lb-assign : Variable → Expr → Label
+
+  -- read t
+  lb-read : State → 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
+
+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
+
+  b-exec : {b b′ : Behaviour} {η : Label} {r : Channel} {o : Operation} {x : Variable}
+         → b ↝ b′ ∶ η
+         ----------------------------------
+         → exec r o x b ↝ exec r o x b′ ∶ η
+
+  b-seq : {b₁ b₂ b₁′ : Behaviour} {η : Label}
+        → b₁ ↝ b₁′ ∶ η
+        -----------------------------
+        → (b₁ ∶ b₂) ↝ (b₁′ ∶ b₂) ∶ η
+
+  b-par : {b₁ b₂ b₁′ : Behaviour} {η : Label}
+        → b₁ ↝ b₁′ ∶ η
+        ----------------------------
+        → (b₁ ∥ b₂) ↝ (b₁′ ∥ b₂) ∶ η
+
+  b-struct : {b₁ b₂ b₁′ b₂′ : Behaviour} {η : Label}
+           → b₁ ≡ b₂
+           → b₂ ↝ b₂′ ∶ η
+           → b₁′ ≡ b₂′
+           --------------
+           → b₁ ↝ b₁′ ∶ η
+
+  b-if-then : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
+            → e ⟨ t ⟩≔ (constant (bool true))
+            → (if e then b₁ else b₂) ↝ b₁ ∶ lb-read t
+
+  b-if-else : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
+            → e ⟨ t ⟩≔ (constant (bool false))
+            → (if e then b₁ else b₂) ↝ b₂ ∶ lb-read t
+
+  b-iteration : {e : Expr} {t : State} {b : Behaviour}
+              → e ⟨ t ⟩≔ (constant (bool true))
+              → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ lb-read t
+
+  b-no-iteration : {e : Expr} {t : State} {b : Behaviour}
+                 → e ⟨ t ⟩≔ (constant (bool false))
+                 → (while[ e ] b) ↝ nil ∶ lb-read t
+
+  b-choice : ∀ {n} {choices : Vec (η × Behaviour) n} {ηⱼ : η} {η : Label} {bⱼ bⱼ′ : Behaviour}
+           → (ηⱼ , bⱼ) ∈-Vec choices
+           → input ηⱼ ↝ bⱼ′ ∶ η
+           → inputchoice (toList choices) ↝ (bⱼ′ ∶ bⱼ) ∶ η

diff --git a/src/Interpreter.agda b/src/Interpreter.agda
deleted file mode 100644 (file)
index 1b29e57..0000000
--- a/src/Interpreter.agda
+++ /dev/null
@@ -1,66 +0,0 @@
-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