Add condition for t-par

diff --git a/src/Type.agda b/src/Type.agda
index 0490a328f3dfc7d640b683c4f93224f97fbd1d34..d3b1ee97351672c22641e7ae08a6b61f16019147 100644 (file)
--- 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 72e98b3f02b6fdb6931ddcf7ea0398e82db63bfb..c9fe2e438d6d7d7d41cb926278098982ecd1847e 100644 (file)
--- 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 2f922692f99eb2480ae67674f08c309a437b69cc..71aa4747dfd39c73d4d9550fb3759462a5a13268 100644 (file)
--- 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