Clean up

diff --git a/src/Expr.agda b/src/Expr.agda
index ff1f59fbdc406dda27c00d36471f51e8c35005ab..1cdf67c1f2e573b522e65bdf4ec281c307e50ae6 100644 (file)
--- a/src/Expr.agda
+++ b/src/Expr.agda
@@ -1,14 +1,15 @@
 module Expr where
 
-open import Data.Maybe using (Maybe; just; nothing)
 open import Variable
 
 
--- TODO: add logic operations and, or
 data BinOp : Set where
+  -- Arithmetics
   plus minus mult div power : BinOp
+  -- Logical operations
+  and or : BinOp
 
 data Expr : Set where
   var : Variable → Expr
   binary : BinOp → Expr → Expr → Expr
-  constant : Variable.Value → Expr
+  constant : Value → Expr

diff --git a/src/Service.agda b/src/Service.agda
index 45bce0c2ad41120630f24aee3924f3147c59df04..e2745af2a9c1d340724769c5ab347fb1f44b6411 100644 (file)
--- a/src/Service.agda
+++ b/src/Service.agda
@@ -8,6 +8,7 @@ open import Type
 open import Behaviour
 open import Variable
 
+
 Queue : (A : Set) → Set
 Queue A = List A
 

diff --git a/src/Type.agda b/src/Type.agda
index 421eba6d1762e57a8700b56d3ac0b223bfbd0cf8..a275abef083f1b8e3d130436cd92192a3c4a9994 100644 (file)
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -1,18 +1,8 @@
 module Type where
 
-import Data.Vec.Equality as VecEq
-open import Level
-open import Relation.Nullary
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
-open import Relation.Nullary.Decidable using (⌊_⌋)
-open import Function
-open import Data.Nat using (ℕ) renaming (_≟_ to _≟-Nat_)
-open import Data.Empty
-open import Data.String using (String) renaming (_≟_ to _≟-String_)
-open import Data.List using (List; filter)
-open import Data.Vec using (Vec; toList)
-open import Expr
+open import Data.Nat using (ℕ)
+open import Data.String using (String)
+open import Data.Vec using (Vec)
 open import Variable
 
 
@@ -28,157 +18,15 @@ Channel = String
 data Type : Set where
   bool int double long string raw void : Type
 
-module TypeEq where
-  _≟_ : Decidable {A = Type} _≡_
-  bool ≟ bool = yes refl
-  int ≟ int = yes refl
-  double ≟ double = yes refl
-  long ≟ long = yes refl
-  string ≟ string = yes refl
-  raw ≟ raw = yes refl
-  void ≟ void = yes refl
-  bool ≟ int = no λ()
-  bool ≟ double = no λ()
-  bool ≟ long = no λ()
-  bool ≟ string = no λ()
-  bool ≟ raw = no λ()
-  bool ≟ void = no λ()
-  int ≟ bool = no λ()
-  int ≟ double = no λ()
-  int ≟ long = no λ()
-  int ≟ string = no λ()
-  int ≟ raw = no λ()
-  int ≟ void = no λ()
-  double ≟ bool = no λ()
-  double ≟ int = no λ()
-  double ≟ long = no λ()
-  double ≟ string = no λ()
-  double ≟ raw = no λ()
-  double ≟ void = no λ()
-  long ≟ bool = no λ()
-  long ≟ int = no λ()
-  long ≟ double = no λ()
-  long ≟ string = no λ()
-  long ≟ raw = no λ()
-  long ≟ void = no λ()
-  string ≟ bool = no λ()
-  string ≟ int = no λ()
-  string ≟ double = no λ()
-  string ≟ long = no λ()
-  string ≟ raw = no λ()
-  string ≟ void = no λ()
-  raw ≟ bool = no λ()
-  raw ≟ int = no λ()
-  raw ≟ double = no λ()
-  raw ≟ long = no λ()
-  raw ≟ string = no λ()
-  raw ≟ void = no λ()
-  void ≟ bool = no λ()
-  void ≟ int = no λ()
-  void ≟ double = no λ()
-  void ≟ long = no λ()
-  void ≟ string = no λ()
-  void ≟ raw = no λ()
-
 data TypeDecl : Set where
   outNotify : Operation → Location → Type → TypeDecl
   outSolRes : Operation → Location → Type → Type → TypeDecl
   inOneWay : Operation → Type → TypeDecl
   inReqRes : Operation → Type → Type → TypeDecl
   var : Variable → Type → TypeDecl
-  empty : TypeDecl
-  pair : TypeDecl → TypeDecl → TypeDecl
-
-cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
-        (f : A → B → C → D) {x y u v m n} → x ≡ y → u ≡ v → m ≡ n → f x u m ≡ f y v n
-cong₃ f refl refl refl = refl
-
-cong₄ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e}
-        (f : A → B → C → D → E) {x y u v m n k l} → x ≡ y → u ≡ v → m ≡ n → k ≡ l → f x u m k ≡ f y v n l
-cong₄ f refl refl refl refl = refl
-
-module TypeDeclEq where
-  _≟_ : Decidable {A = TypeDecl} _≡_
-  (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) with o1 ≟-String o2 | l1 ≟-String l2 | t1 TypeEq.≟ t2
-  ... | yes o | yes l | yes t = yes (cong₃ outNotify o l t)
-  ... | no ¬p | _ | _ = no (λ { refl → ¬p refl})
-  ... | _ | no ¬p | _ = no (λ { refl → ¬p refl})
-  ... | _ | _ | no ¬p = no (λ { refl → ¬p refl})
-  (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') with o1 ≟-String o2 | l1 ≟-String l2 | t1 TypeEq.≟ t2 | t1' TypeEq.≟ t2'
-  ... | yes o | yes l | yes t | yes t' = yes (cong₄ outSolRes o l t t')
-  ... | no ¬p | _ | _ | _ = no (λ { refl → ¬p refl})
-  ... | _ | no ¬p | _ | _ = no (λ { refl → ¬p refl})
-  ... | _ | _ | no ¬p | _ = no (λ { refl → ¬p refl})
-  ... | _ | _ | _ | no ¬p = no (λ { refl → ¬p refl})
-  (inOneWay o1 t1) ≟ (inOneWay o2 t2) with o1 ≟-String o2 | t1 TypeEq.≟ t2
-  ... | yes o | yes t = yes (cong₂ inOneWay o t)
-  ... | no ¬p | _ = no (λ { refl → ¬p refl})
-  ... | _ | no ¬p = no (λ { refl → ¬p refl})
-  (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') with o1 ≟-String o2 | t1 TypeEq.≟ t2 | t1' TypeEq.≟ t2'
-  ... | yes o | yes l | yes t = yes (cong₃ inReqRes o l t)
-  ... | no ¬p | _ | _ = no (λ { refl → ¬p refl})
-  ... | _ | no ¬p | _ = no (λ { refl → ¬p refl})
-  ... | _ | _ | no ¬p = no (λ { refl → ¬p refl})
-  (var v1 t1) ≟ (var v2 t2) with v1 ≟-Nat v2 | t1 TypeEq.≟ t2
-  ... | yes v | yes t = yes (cong₂ var v t)
-  ... | no ¬p | _ = no (λ { refl → ¬p refl})
-  ... | _ | no ¬p = no (λ { refl → ¬p refl})
-  (pair t1 t1') ≟ (pair t2 t2') with t1 ≟ t2 | t1' ≟ t2'
-  ... | yes t | yes t' = yes (cong₂ pair t t')
-  ... | no ¬p | _ = no (λ { refl → ¬p refl})
-  ... | _ | no ¬p = no (λ { refl → ¬p refl})
-  empty ≟ empty = yes refl
-  empty ≟ (outNotify _ _ _) = no λ()
-  empty ≟ (outSolRes _ _ _ _) = no λ()
-  empty ≟ (inOneWay _ _) = no λ()
-  empty ≟ (inReqRes _ _ _) = no λ()
-  empty ≟ (var _ _) = no λ()
-  empty ≟ (pair _ _) = no λ()
-  (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
-  (outNotify _ _ _) ≟ (inOneWay _ _) = no λ()
-  (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ()
-  (outNotify _ _ _) ≟ (var _ _) = no λ()
-  (outNotify _ _ _) ≟ empty = no λ()
-  (outNotify _ _ _) ≟ (pair _ _) = no λ()
-  (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ()
-  (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ()
-  (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ()
-  (outSolRes _ _ _ _) ≟ (var _ _) = no λ()
-  (outSolRes _ _ _ _) ≟ empty = no λ()
-  (outSolRes _ _ _ _) ≟ (pair _ _) = no λ()
-  (inOneWay _ _) ≟ (outNotify _ _ _) = no λ()
-  (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ()
-  (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ()
-  (inOneWay _ _) ≟ (var _ _) = no λ()
-  (inOneWay _ _) ≟ empty = no λ()
-  (inOneWay _ _) ≟ (pair _ _) = no λ()
-  (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ()
-  (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
-  (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ()
-  (inReqRes _ _ _) ≟ (var _ _) = no λ()
-  (inReqRes _ _ _) ≟ empty = no λ()
-  (inReqRes _ _ _) ≟ (pair _ _) = no λ()
-  (var _ _) ≟ (outNotify _ _ _) = no λ()
-  (var _ _) ≟ (outSolRes _ _ _ _) = no λ()
-  (var _ _) ≟ (inOneWay _ _) = no λ()
-  (var _ _) ≟ (inReqRes _ _ _) = no λ()
-  (var _ _) ≟ empty = no λ()
-  (var _ _) ≟ (pair _ _) = no λ()
-  (pair _ _) ≟ (outNotify _ _ _) = no λ()
-  (pair _ _) ≟ (outSolRes _ _ _ _) = no λ()
-  (pair _ _) ≟ (inOneWay _ _) = no λ()
-  (pair _ _) ≟ (inReqRes _ _ _) = no λ()
-  (pair _ _) ≟ (var _ _) = no λ()
-  (pair _ _) ≟ empty = no λ()
-  
-  decSetoid : DecSetoid _ _
-  decSetoid = PropEq.decSetoid _≟_
 
 data _⊆_ : Type → Type → Set where
   sub : {T₁ T₂ : Type} → T₁ ⊆ T₂
 
 Ctx : ℕ → Set
 Ctx = Vec TypeDecl
-
-module CtxEq = VecEq.DecidableEquality TypeDeclEq.decSetoid
-module CtxPropEq = VecEq.PropositionalEquality

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 73fea3695f2f9e33391a06234a6efe7193c4d2d7..38f9d2f4bcf0c8e827304991ecb66b0847ba2a71 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -30,25 +30,25 @@ data Context : Set where
 
 data _⊢B_▹_ : Context → Behaviour → Context → Set where
   t-nil : ∀ {n} {Γ : Ctx n}
-        --------------
+        ------------------
         → ◆ Γ ⊢B nil ▹ ◆ Γ
           
   t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
        → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
        → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
        → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
-       ----------------------
+       --------------------------
        → ◆ Γ ⊢B if e b1 b2 ▹ ◆ Γ₁
           
   t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr} 
           → Γ ⊢ₑ e ∶ bool
           → ◆ Γ ⊢B 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
-           -------------------------------
+           -----------------------------------
            → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
 
   t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁}
@@ -61,47 +61,47 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
   t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
         → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
         → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂
-        ---------------------
+        -------------------------
         → ◆ Γ ⊢B seq 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)) ▹ ◆ Γ
 
   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ₑ ∷ Γ)
 
   t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
                   → var x Tₓ ∈ Γ
                   → Tₑ ≡ Tₓ
-                  ----------------------
+                  -------------------------
                   → ◆ Γ ⊢B assign 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ᵢ ∷ Γ)
 
   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) ▹ ◆ Γ
 
   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ᵢ ∷ Γ)
 
   t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
@@ -109,7 +109,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    → Tₑ ⊆ Tₒ
                    → var x Tₓ ∈ Γ
                    → Tᵢ ⊆ Tₓ
-                   ---------------------------------------
+                   ------------------------------------------
                    → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ Γ
 
   t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
@@ -118,7 +118,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                 → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
                 → var a Tₐ ∈ Γ₁
                 → Tₐ ⊆ Tₒ
-                ----------------------------------
+                --------------------------------------
                 → ◆ Γ ⊢B input (reqres 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}
@@ -128,20 +128,20 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    → ◆ Γ ⊢B b ▹ ◆ Γ₁
                    → var a Tₐ ∈ Γ₁
                    → Tₐ ⊆ Tₒ
-                   ----------------------------------
+                   --------------------------------------
                    → ◆ Γ ⊢B input (reqres 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ᵢ ∈ Γ
              → ¬ (var x Tₓ ∈ Γ)
-             ------------------------------------
+             ----------------------------------------
              → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
 
   t-wait-exists : ∀ {n} {Γ : Ctx n} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
                 → outSolRes o l Tₒ Tᵢ ∈ Γ
                 → var x Tₓ ∈ Γ
                 → Tᵢ ⊆ Tₓ
-                ------------------------
+                ---------------------------
                 → ◆ Γ ⊢B wait r o l x ▹ ◆ Γ
 
   t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
@@ -149,7 +149,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
          → ◆ Γ ⊢B b ▹ ◆ Γ₁
          → var x Tₓ ∈ Γ
          → Tₓ ⊆ Tₒ
-         ------------------------
+         ----------------------------
          → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
 
 struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
@@ -164,13 +164,16 @@ 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 (t-par t₁ t₂) = t-par t₂ t₁
 
+data Label : Set where
+  x=e readt νr r:o r,o r,ol : Label
+
 data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
   updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
   identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
   undefined : SideEffect [] []
 
-preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
-preservation t undefined = t
-preservation t (identity γ) = t
+--preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
+--preservation t undefined = t
+--preservation t (identity γ) = t
 --preservation t-nil (updated {_} {k} Γ Γₐ) = {!!}
-preservation = {!!}
+--preservation = {!!}

diff --git a/src/TypingService.agda b/src/TypingService.agda
index 0006a18490b42fd5c1df20b75fb239ce822bc2ff..9da969e27e9f8744081e2ba4ca010103d2a1731a 100644 (file)
--- a/src/TypingService.agda
+++ b/src/TypingService.agda
@@ -8,6 +8,7 @@ open import Type
 open import Service
 open import Behaviour
 
+
 data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
   t-bsl-nil : ∀ {n} {Γ : Ctx n}
             ----------------

diff --git a/src/Variable.agda b/src/Variable.agda
index 33b0f60f6ca2f2b3070d6ca01e9665948b89c236..f3b08cc1d4bc45bd97cbd53f5d877f33f52ab133 100644 (file)
--- a/src/Variable.agda
+++ b/src/Variable.agda
@@ -3,8 +3,6 @@ module Variable where
 open import Data.Integer using (ℤ)
 open import Data.String using (String)
 open import Data.Product using (_×_)
-open import Data.Maybe using (Maybe)
-open import Data.List using (List)
 open import Data.Bool using (Bool)
 open import Data.Nat using (ℕ)