repos / jolie.agda.git

commit

e643ac1

parent

2d07c59

author

Eugene Akentyev

date

2016-11-05 21:12:16 +0400 +04

Add condition for t-par

 1@@ -56,3 +56,29 @@ data _⊆_ : TypeTree → TypeTree → Set where
 2 
 3 Ctx : ℕ → Set
 4 Ctx = Vec TypeDecl
 5+
 6+roots : {n : ℕ} → Ctx n → List Name
 7+roots xs = go xs
 8+  where
 9+    open import Data.List using ([]; _∷_)
10+
11+    go : {n : ℕ} → Ctx n → List Name
12+    go Vec.[] = []
13+    go (Vec._∷_ x xs) =
14+      case x of λ
15+        { (var v t) → (root v) ∷ (roots xs)
16+        ; _ → roots xs
17+        }
18+
19+intersect-roots : List Name → List Name → List Name
20+intersect-roots xs ys = intersect xs ys
21+  where
22+    open import Data.List using ([]; _∷_)
23+    open import Data.String using (_≟_)
24+
25+    intersect : List Name → List Name → List Name
26+    intersect [] _ = []
27+    intersect _ [] = []
28+    intersect (x ∷ xs) (y ∷ ys) with x ≟ y
29+    ... | yes x≡y = x ∷ intersect xs ys
30+    ... | no _ = intersect xs ys

 1@@ -1,5 +1,6 @@
 2 module Typecheck where
 3 
 4+import Data.List as List
 5 import Data.Vec.Equality as VecEq
 6 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 7 open import Data.Nat using (ℕ; _+_)
 8@@ -45,7 +46,8 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
 9           {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
10         → Γ₁ ⊢ b1 ▹ Γ₁'
11         → Γ₂ ⊢ b2 ▹ Γ₂'
12-        -- TODO: Express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
13+        → intersect-roots (roots Γ₁') (roots Γ₂') ≡ List.[]
14+        -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
15         ---------------
16         → Γ ⊢ par b1 b2 ▹ Γ'
17 

1@@ -22,3 +22,6 @@ data Variable : Set where
2   leaf : Name → Value → Variable
3   node : Name → Maybe Value → List Variable → Variable
4 
5+root : Variable → Name
6+root (leaf n _) = n
7+root (node n _ _) = n