Simplified variables and finished typing rules for behaviour.

diff --git a/src/Behaviour.agda b/src/Behaviour.agda
index 474861740dff4d635f4e5d5feb6f45554982158a..8c78720897b7ee009ec6283035f0f860e25792e9 100644 (file)
--- a/src/Behaviour.agda
+++ b/src/Behaviour.agda
@@ -11,13 +11,13 @@ open import Type
 
 data Output_ex : Set where
   notification : Operation → Location → Expr → Output_ex
-  solicitRes : Operation → Location → Expr → Variable → Output_ex
+  solicitres : Operation → Location → Expr → Variable → Output_ex
 
 data Behaviour : Set
 
 data Input_ex : Set where
   oneway : Operation → Variable → Input_ex
-  reqRes : Operation → Variable → Variable → Behaviour → Input_ex
+  reqres : Operation → Variable → Variable → Behaviour → Input_ex
 
 data Behaviour where
   input : Input_ex → Behaviour

diff --git a/src/Type.agda b/src/Type.agda
index 0b2b9a59374083a146ff1cc15ced43a0f022deba..a6fba822aeedf88cefcab94ad89688798468cec3 100644 (file)
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -4,12 +4,13 @@ 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 (ℕ)
 open import Data.Empty
 open import Data.String using (String)
-open import Data.List using (List)
-open import Data.Vec using (Vec)
+open import Data.List using (List; filter)
+open import Data.Vec using (Vec; toList)
 open import Expr
 open import Variable
 
@@ -23,68 +24,20 @@ Location = String
 Channel : Set
 Channel = String
 
-data Cardinality : Set where
-  oo oi ii : Cardinality
-
-data BasicType : Set where
-  bool int double long string raw void : BasicType
-
-data TypeTree : Set
-
-data ChildType : Set where
-  child : String → Cardinality → TypeTree → ChildType
-
-data TypeTree where
-  leaf : BasicType → TypeTree
-  node : BasicType → List ChildType → TypeTree
-
-get-basic : TypeTree → BasicType
-get-basic (leaf b) = b
-get-basic (node b _) = b
+data Type : Set where
+  bool int double long string raw void : Type
 
 data TypeDecl : Set where
-  outNotify : Operation → Location → TypeTree → TypeDecl
-  outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl
-  inOneWay : Operation → TypeTree → TypeDecl
-  inReqRes : Operation → TypeTree → TypeTree → TypeDecl
-  var : Variable → TypeTree → TypeDecl
+  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
 
-data _⊆_ : TypeTree → TypeTree → Set where
-  sub : {T₁ T₂ : TypeTree} → T₁ ⊆ T₂
+data _⊆_ : Type → Type → Set where
+  sub : {T₁ T₂ : Type} → T₁ ⊆ T₂
 
 Ctx : ℕ → Set
 Ctx = Vec TypeDecl
-
-roots : {n : ℕ} → Ctx n → List Name
-roots xs = go xs
-  where
-    open import Data.List using ([]; _∷_)
-
-    go : {n : ℕ} → Ctx n → List Name
-    go Vec.[] = []
-    go (Vec._∷_ x xs) =
-      case x of λ
-        { (var v t) → (root v) ∷ (roots xs)
-        ; _ → roots xs
-        }
-
-intersect-roots : List Name → List Name → List Name
-intersect-roots xs ys = intersect xs ys
-  where
-    open import Data.List using ([]; _∷_)
-    open import Data.String using (_≟_)
-
-    intersect : List Name → List Name → List Name
-    intersect [] _ = []
-    intersect _ [] = []
-    intersect (x ∷ xs) (y ∷ ys) with x ≟ y
-    ... | yes x≡y = x ∷ intersect xs ys
-    ... | no _ = intersect xs ys
-
-
-upd : {n m : ℕ} → Ctx n → Variable → TypeTree → Ctx m
-upd Γ x Tₓ =
-  let r = root x in
-  {!!}

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index ad70c02edbf0dba6b6ee5bfdaeb9077aa0ceb003..97d9173f32595a79043eda36e9faf3be5ebf090b 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,77 +1,143 @@
+
 module Typecheck where
 
 import Data.List as List
 import Data.Vec.Equality as VecEq
 open import Relation.Nullary using (¬_)
+open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
-open import Data.Nat using (ℕ; _+_)
-open import Data.Vec using (Vec; _∈_; zip)
+open import Data.Nat using (ℕ; _+_; suc)
+open import Data.Vec using (Vec; _∈_; zip; _∷_)
 open import Expr
 open import Type
 open import Behaviour
 open import Variable
 
 
-data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → TypeTree → Set where
-  var-t : {s : Variable} {b : TypeTree} 
+data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
+  var-t : {s : Variable} {b : Type}
         → Γ ⊢ s of b
 
-data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → TypeTree → Set where
-  expr-t : {s : Expr} {b : TypeTree}
+data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
+  expr-t : {s : Expr} {b : Type}
          → Γ ⊢ₑ s of b
 
-data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where 
+data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where 
   t-nil : {Γ₁ : Ctx m}
         → n ≡ m
         --------------
-        → Γ ⊢ nil ▹ Γ₁
+        → Γ ⊢B nil ▹ Γ₁
           
   t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
-       → Γ ⊢ e of (leaf bool) -- Γ ⊢ e : bool
-       → Γ ⊢ b1 ▹ Γ₁
-       → Γ ⊢ b2 ▹ Γ₁
+       → Γ ⊢ e of bool -- Γ ⊢ e : bool
+       → Γ ⊢B b1 ▹ Γ₁
+       → Γ ⊢B b2 ▹ Γ₁
        ---------------------------
-       → Γ ⊢ if (var e) b1 b2 ▹ Γ₁
+       → Γ ⊢B if (var e) b1 b2 ▹ Γ₁
           
   t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
-          → Γ ⊢ e of (leaf bool)
-          → Γ ⊢ b ▹ Γ₁
+          → Γ ⊢ e of bool
+          → Γ ⊢B b ▹ Γ₁
           --------------------------
-          → Γ ⊢ while (var e) b ▹ Γ₁
+          → Γ ⊢B while (var e) b ▹ Γ₁
           
   t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
              {b : Behaviour} {behaviours : Vec Behaviour n}
            → η ∈ inputs
            → b ∈ behaviours
-           → Γ ⊢ seq (input η) b ▹ Γ₁
+           → Γ ⊢B seq (input η) b ▹ Γ₁
            ----------------------------------------------
-           → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁
+           → Γ ⊢B inputchoice (zip inputs behaviours) ▹ Γ₁
 
   t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
           {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
-        → Γ₁ ⊢ b1 ▹ Γ₁'
-        → Γ₂ ⊢ b2 ▹ Γ₂'
-        → intersect-roots (roots Γ₁') (roots Γ₂') ≡ List.[]
+        → Γ₁ ⊢B b1 ▹ Γ₁'
+        → Γ₂ ⊢B b2 ▹ Γ₂'
         -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
         --------------------
-        → Γ ⊢ par b1 b2 ▹ Γ'
+        → Γ ⊢B par b1 b2 ▹ Γ'
 
   t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
-        → Γ ⊢ b1 ▹ Γ₁
-        → Γ₁ ⊢ b2 ▹ Γ₂
+        → Γ ⊢B b1 ▹ Γ₁
+        → Γ₁ ⊢B b2 ▹ Γ₂
         --------------------
-        → Γ ⊢ seq b1 b2 ▹ Γ₂
+        → Γ ⊢B seq b1 b2 ▹ Γ₂
 
-  t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : TypeTree}
+  t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
                  → Γ ⊢ e of Tₑ
                  → Tₑ ⊆ T₀
-                 -------------------------------------------
                  → n ≡ m
-                 → Γ ⊢ output (notification o l (var e)) ▹ Γ₁
+                 -------------------------------------------
+                 → Γ ⊢B output (notification o l (var e)) ▹ Γ₁
 
-  t-assign-new : {Î\93â\82\81 : Ctx m} {x : Variable} {e : Expr} {Tâ\82\80 : TypeTree} {Tâ\82\93 : TypeTree}
-               â\86\92 Î\93 â\8a¢â\82\91 e of Tâ\82\80 -- Γ ⊢ e : bool
+  t-assign-new : {Î\93â\82\81 : Ctx m} {x : Variable} {e : Expr} {Tâ\82\93 Tâ\82\91 : Type}
+               â\86\92 Î\93 â\8a¢â\82\91 e of Tâ\82\91 -- Γ ⊢ e : bool
                → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
+               → (var x Tₑ) ∈ Γ₁
                ---------------------
-               → Γ ⊢ assign x e ▹ upd Γ x (bt Tₑ)
+               → Γ ⊢B assign x e ▹ Γ₁
+
+  t-assign-exists : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+                  → Γ ⊢ₑ e of Tₑ
+                  → (var x Tₓ) ∈ Γ
+                  → Tₑ ≡ Tₓ
+                  → n ≡ m -- TODO Γ ≡ Γ₁
+                  ---------------------
+                  → Γ ⊢B assign x e ▹ Γ₁
+
+  t-oneway-new : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+               → (inOneWay o Tᵢ) ∈ Γ
+               → ¬ ((var x Tₓ) ∈ Γ)
+               → (var x Tᵢ) ∈ Γ₁
+               -------------------------------
+               → Γ ⊢B (input (oneway o x)) ▹ Γ₁
+
+  t-oneway-exists : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+                  → (inOneWay o Tᵢ) ∈ Γ
+                  → ((var x Tₓ) ∈ Γ)
+                  → Tᵢ ⊆ Tₓ
+                  → n ≡ m -- TODO Γ ≡ Γ₁
+                  --------------------------------
+                  → Γ ⊢B (input (oneway o x)) ▹ Γ₁
+
+  t-solresp-new : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+                → (outSolRes o l Tₒ Tᵢ) ∈ Γ
+                → Tₑ ⊆ Tₒ
+                → ¬ (var x Tₓ ∈ Γ)
+                → (var x Tᵢ) ∈ Γ₁
+                -----------------------------------------
+                → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
+
+  t-solresp-exists : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+                   → (outSolRes o l Tₒ Tᵢ) ∈ Γ
+                   → Tₑ ⊆ Tₒ
+                   → (var x Tₓ) ∈ Γ
+                   → Tᵢ ⊆ Tₓ
+                   → n ≡ m -- TODO Γ ≡ Γ₁
+                   -----------------------------------------
+                   → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
+
+  t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
+                → (inReqRes o Tᵢ Tₒ) ∈ Γ
+                → ¬ (var x Tₓ ∈ Γ)
+                → (var x Tₓ) ∈ Γₓ
+                → Γₓ ⊢B b ▹ Γ₁
+                → (var a Tₐ) ∈ Γ₁
+                → Tₐ ⊆ Tₒ
+                -----------------------------------
+                → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
+
+  t-reqresp-exists : {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
+                   → (inReqRes o Tᵢ Tₒ) ∈ Γ
+                   → (var x Tₓ) ∈ Γ
+                   → Tᵢ ⊆ Tₓ
+                   → Γ ⊢B b ▹ Γ₁
+                   → (var a Tₐ) ∈ Γ₁
+                   → Tₐ ⊆ Tₒ
+                   ------------------------------------
+                   → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
+
+
+check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (B : Behaviour) → Dec (Γ ⊢B B ▹ Γ₁)
+check-B = {!!}

diff --git a/src/Variable.agda b/src/Variable.agda
index 71aa4747dfd39c73d4d9550fb3759462a5a13268..33b0f60f6ca2f2b3070d6ca01e9665948b89c236 100644 (file)
--- a/src/Variable.agda
+++ b/src/Variable.agda
@@ -6,10 +6,11 @@ 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 (ℕ)
 
 
-Name : Set
-Name = String
+Variable : Set
+Variable = ℕ
 
 data Value : Set where
   string : String → Value
@@ -17,11 +18,4 @@ data Value : Set where
   bool : Bool → Value
   double : ℤ × ℤ → Value
   long : ℤ → Value
-
-data Variable : Set where
-  leaf : Name → Value → Variable
-  node : Name → Maybe Value → List Variable → Variable
-
-root : Variable → Name
-root (leaf n _) = n
-root (node n _ _) = n
+  void : Value