Change to unicode syntax for behaviour

diff --git a/src/Behaviour.agda b/src/Behaviour.agda
index c60c3e14a67310611832fe9ef37843f8bae9b0b6..0a8010bbbb9cdfac8e792327ac0c806339ca9f6e 100644 (file)
--- a/src/Behaviour.agda
+++ b/src/Behaviour.agda
@@ -8,26 +8,26 @@ open import Expr
 open import Type
 
 
-data Output_ex : Set where
-  notification : Operation → Location → Expr → Output_ex
-  solicitres : Operation → Location → Expr → Variable → Output_ex
+data η̂  : Set where
+  _at_[_] : Operation → Location → Expr → η̂
+  _at_[_][_] : Operation → Location → Expr → Variable → η̂
 
 data Behaviour : Set
 
-data Input_ex : Set where
-  oneway : Operation → Variable → Input_ex
-  reqres : Operation → Variable → Variable → Behaviour → Input_ex
+data η : Set where
+  _[_] : Operation → Variable → η
+  _[_][_]_ : Operation → Variable → Variable → Behaviour → η
 
 data Behaviour where
-  input : Input_ex → Behaviour
-  output : Output_ex → Behaviour
-  if : Expr → Behaviour → Behaviour → Behaviour
-  while : Expr → Behaviour → Behaviour
-  seq : Behaviour → Behaviour → Behaviour
-  par : Behaviour → Behaviour → Behaviour
-  assign : Variable → Expr → Behaviour
+  input : η → Behaviour
+  output : η̂  → Behaviour
+  if_then_else_ : Expr → Behaviour → Behaviour → Behaviour
+  while[_]_ : Expr → Behaviour → Behaviour
+  _∶_ : Behaviour → Behaviour → Behaviour
+  _∣_ : Behaviour → Behaviour → Behaviour
+  _≃_ : Variable → Expr → Behaviour
   nil : Behaviour
-  inputchoice : List (Input_ex × Behaviour) → Behaviour
+  inputchoice : List (η × Behaviour) → Behaviour
   wait : Channel → Operation → Location → Variable → Behaviour
   exec : Channel → Operation → Variable → Behaviour → Behaviour
 

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 38f9d2f4bcf0c8e827304991ecb66b0847ba2a71..427fa4693bd71d70ca5279944ebe017c20d6c298 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -38,16 +38,16 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
        → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
        → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
        --------------------------
-       → ◆ Γ ⊢B if e b1 b2 ▹ ◆ Γ₁
+       → ◆ Γ ⊢B if e then b1 else b2 ▹ ◆ Γ₁
           
   t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr} 
           → Γ ⊢ₑ e ∶ bool
           → ◆ Γ ⊢B b ▹ ◆ Γ
           ------------------------
-          → ◆ Γ ⊢B while e b ▹ ◆ Γ
+          → ◆ Γ ⊢B while[ e ] b ▹ ◆ Γ
           
-  t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
-           → All (λ { (η , b) → ◆ Γ ⊢B seq (input η) b ▹ ◆ Γ₁ }) choices
+  t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (η × Behaviour)}
+           → All (λ { (η , b) → ◆ Γ ⊢B (input η) ∶ b ▹ ◆ Γ₁ }) choices
            -----------------------------------
            → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
 
@@ -56,53 +56,53 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
        → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
        → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
        --------------------------------------
-       → (■ Γ₁ Γ₂) ⊢B par b1 b2 ▹ (■ Γ₁' Γ₂')
+       → (■ Γ₁ Γ₂) ⊢B b1 ∣ b2 ▹ (■ Γ₁' Γ₂')
 
   t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
         → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
         → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂
         -------------------------
-        → ◆ Γ ⊢B seq b1 b2 ▹ ◆ Γ₂
+        → ◆ Γ ⊢B b1 ∶ b2 ▹ ◆ Γ₂
 
   t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
                  → Γ ⊢ e ∶ Tₑ
                  → Tₑ ⊆ T₀
                  ------------------------------------------------
-                 → ◆ Γ ⊢B output (notification o l (var e)) ▹ ◆ Γ
+                 → ◆ Γ ⊢B output (o at l [ var e ]) ▹ ◆ Γ
 
   t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
                → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
                --------------------------------------
-               → ◆ Γ ⊢B assign x e ▹ ◆ (var x Tₑ ∷ Γ)
+               → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
 
   t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
                   → var x Tₓ ∈ Γ
                   → Tₑ ≡ Tₓ
                   -------------------------
-                  → ◆ Γ ⊢B assign x e ▹ ◆ Γ
+                  → ◆ Γ ⊢B x ≃ e ▹ ◆ Γ
 
   t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                → inOneWay o Tᵢ ∈ Γ
                → ¬ (var x Tₓ ∈ Γ)
                ----------------------------------------------
-               → ◆ Γ ⊢B input (oneway o x) ▹ ◆ (var x Tᵢ ∷ Γ)
+               → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
 
   t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → inOneWay o Tᵢ ∈ Γ
                   → var x Tₓ ∈ Γ
                   → Tᵢ ⊆ Tₓ
                   ---------------------------------
-                  → ◆ Γ ⊢B input (oneway o x) ▹ ◆ Γ
+                  → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ Γ
 
   t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                 → outSolRes o l Tₒ Tᵢ ∈ Γ
                 → Tₑ ⊆ Tₒ
                 → ¬ (var x Tₓ ∈ Γ)
                 -------------------------------------------------------
-                → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ (var x Tᵢ ∷ Γ)
+                → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
 
   t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                    → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -110,7 +110,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    → var x Tₓ ∈ Γ
                    → Tᵢ ⊆ Tₓ
                    ------------------------------------------
-                   → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ Γ
+                   → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ Γ
 
   t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
                 → inReqRes o Tᵢ Tₒ ∈ Γ
@@ -119,7 +119,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                 → var a Tₐ ∈ Γ₁
                 → Tₐ ⊆ Tₒ
                 --------------------------------------
-                → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
+                → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
 
   t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
                    → (inReqRes o Tᵢ Tₒ) ∈ Γ
@@ -129,7 +129,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    → var a Tₐ ∈ Γ₁
                    → Tₐ ⊆ Tₒ
                    --------------------------------------
-                   → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
+                   → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
 
   t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
              → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -155,13 +155,13 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
 struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
 struct-congruence t refl = t
 
-struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (seq nil b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
+struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
 struct-cong-nil (t-seq t-nil t) = t
 
-struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
+struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b ∣ nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
 struct-cong-par-nil (t-par t t-nil) = t
 
-struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b1 b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (par b2 b1) ▹ ■ Γ₂' Γ₁'
+struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b1 ∣ b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (b2 ∣ b1) ▹ ■ Γ₂' Γ₁'
 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
 
 data Label : Set where