From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Sat, 5 Nov 2016 17:12:16 +0000 (+0300)
Subject: Add condition for t-par
X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=e643ac14ceec03a11ec1e77caf4eae1cae406802;p=jolie.agda.git

Add condition for t-par
---

diff --git a/src/Type.agda b/src/Type.agda
index 0490a32..d3b1ee9 100644
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -56,3 +56,29 @@ data _⊆_ : TypeTree → TypeTree → Set where
 
 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
diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 72e98b3..c9fe2e4 100644
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,5 +1,6 @@
 module Typecheck where
 
+import Data.List as List
 import Data.Vec.Equality as VecEq
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 open import Data.Nat using (ℕ; _+_)
@@ -45,7 +46,8 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
           {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
         → Γ₁ ⊢ b1 ▹ Γ₁'
         → Γ₂ ⊢ b2 ▹ Γ₂'
-        -- TODO: Express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
+        → intersect-roots (roots Γ₁') (roots Γ₂') ≡ List.[]
+        -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
         ---------------
         → Γ ⊢ par b1 b2 ▹ Γ'
 
diff --git a/src/Variable.agda b/src/Variable.agda
index 2f92269..71aa474 100644
--- a/src/Variable.agda
+++ b/src/Variable.agda
@@ -22,3 +22,6 @@ 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