repos / jolie.agda.git

commit

eb93f60

parent

fdb342f

author

Eugene Akentyev

date

2017-01-26 11:20:40 +0400 +04

Rename file and add remaining rules

  1@@ -0,0 +1,100 @@
  2+module BehaviouralSemantics where
  3+
  4+open import Relation.Binary.PropositionalEquality using (_≡_)
  5+open import Data.Vec using (Vec; toList) renaming (_∈_ to _∈-Vec_)
  6+open import Data.Bool using (true; false)
  7+open import Data.Product using (_×_; _,_)
  8+open import Type
  9+open import Behaviour
 10+open import Variable
 11+open import Expr
 12+
 13+
 14+data State : Set where
 15+
 16+data _⟨_⟩≔_ : Expr → State → Expr → Set where
 17+
 18+data Label : Set where
 19+  -- Behavioural layer
 20+  -- x = e
 21+  lb-assign : Variable → Expr → Label
 22+
 23+  -- read t
 24+  lb-read : State → Label
 25+
 26+  -- νr o@l(e)
 27+  lb-send : Channel → Operation → Location → Expr → Label
 28+
 29+  -- r : o(x)
 30+  lb-store : Channel → Operation → Variable → Label
 31+
 32+  -- (r, o)!x
 33+  lb-write : Channel → Operation → Variable → Label
 34+
 35+  -- (r, o@l)?x
 36+  lb-read-write : Channel → Operation → Location → Variable → Label
 37+
 38+data _↝_∶_ : Behaviour → Behaviour → Label → Set where
 39+  b-assign : {x : Variable} {e : Expr}
 40+           → (x ≃ e) ↝ nil ∶ lb-assign x e
 41+
 42+  b-wait : {r : Channel} {o : Operation} {l : Location} {x : Variable}
 43+         → wait r o l x ↝ nil ∶ lb-read-write r o l x
 44+ 
 45+  b-oneway : {o : Operation} {x : Variable} {r : Channel}
 46+           → input (o [ x ]) ↝ nil ∶ lb-store r o x
 47+
 48+  b-notification : {r : Channel} {o : Operation} {l : Location} {e : Expr}
 49+                 → output (o at l [ e ]) ↝ nil ∶ lb-send r o l e
 50+
 51+  b-solresp : {r : Channel} {o : Operation} {l : Location} {e : Expr} {x : Variable}
 52+            → output (o at l [ e ][ x ]) ↝ wait r o l x ∶ lb-send r o l e
 53+
 54+  b-reqresp : {r : Channel} {o : Operation} {x x′ : Variable} {b : Behaviour}
 55+            → input (o [ x ][ x′ ] b) ↝ exec r o x′ b ∶ lb-store r o x
 56+
 57+  b-end-exec : {r : Channel} {o : Operation} {x : Variable}
 58+             → exec r o x nil ↝ nil ∶ lb-write r o x
 59+
 60+  b-exec : {b b′ : Behaviour} {η : Label} {r : Channel} {o : Operation} {x : Variable}
 61+         → b ↝ b′ ∶ η
 62+         ----------------------------------
 63+         → exec r o x b ↝ exec r o x b′ ∶ η
 64+
 65+  b-seq : {b₁ b₂ b₁′ : Behaviour} {η : Label}
 66+        → b₁ ↝ b₁′ ∶ η
 67+        -----------------------------
 68+        → (b₁ ∶ b₂) ↝ (b₁′ ∶ b₂) ∶ η
 69+
 70+  b-par : {b₁ b₂ b₁′ : Behaviour} {η : Label}
 71+        → b₁ ↝ b₁′ ∶ η
 72+        ----------------------------
 73+        → (b₁ ∥ b₂) ↝ (b₁′ ∥ b₂) ∶ η
 74+
 75+  b-struct : {b₁ b₂ b₁′ b₂′ : Behaviour} {η : Label}
 76+           → b₁ ≡ b₂
 77+           → b₂ ↝ b₂′ ∶ η
 78+           → b₁′ ≡ b₂′
 79+           --------------
 80+           → b₁ ↝ b₁′ ∶ η
 81+
 82+  b-if-then : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
 83+            → e ⟨ t ⟩≔ (constant (bool true))
 84+            → (if e then b₁ else b₂) ↝ b₁ ∶ lb-read t
 85+
 86+  b-if-else : {e : Expr} {t : State} {b₁ b₂ : Behaviour}
 87+            → e ⟨ t ⟩≔ (constant (bool false))
 88+            → (if e then b₁ else b₂) ↝ b₂ ∶ lb-read t
 89+
 90+  b-iteration : {e : Expr} {t : State} {b : Behaviour}
 91+              → e ⟨ t ⟩≔ (constant (bool true))
 92+              → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ lb-read t
 93+
 94+  b-no-iteration : {e : Expr} {t : State} {b : Behaviour}
 95+                 → e ⟨ t ⟩≔ (constant (bool false))
 96+                 → (while[ e ] b) ↝ nil ∶ lb-read t
 97+
 98+  b-choice : ∀ {n} {choices : Vec (η × Behaviour) n} {ηⱼ : η} {η : Label} {bⱼ bⱼ′ : Behaviour}
 99+           → (ηⱼ , bⱼ) ∈-Vec choices
100+           → input ηⱼ ↝ bⱼ′ ∶ η
101+           → inputchoice (toList choices) ↝ (bⱼ′ ∶ bⱼ) ∶ η

 1@@ -1,66 +0,0 @@
 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