repos / jolie.agda.git

commit

1aa59ad

parent

e643ac1

author

Eugene Akentyev

date

2016-11-09 03:01:07 +0400 +04

Add t-assign-new

 1@@ -82,3 +82,9 @@ intersect-roots xs ys = intersect xs ys
 2     intersect (x ∷ xs) (y ∷ ys) with x ≟ y
 3     ... | yes x≡y = x ∷ intersect xs ys
 4     ... | no _ = intersect xs ys
 5+
 6+
 7+upd : {n m : ℕ} → Ctx n → Variable → TypeTree → Ctx m
 8+upd Γ x Tₓ =
 9+  let r = root x in
10+  {!!}

 1@@ -2,6 +2,7 @@ module Typecheck where
 2 
 3 import Data.List as List
 4 import Data.Vec.Equality as VecEq
 5+open import Relation.Nullary using (¬_)
 6 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 7 open import Data.Nat using (ℕ; _+_)
 8 open import Data.Vec using (Vec; _∈_; zip)
 9@@ -15,23 +16,27 @@ data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → TypeTree → Set where
10   var-t : {s : Variable} {b : TypeTree} 
11         → Γ ⊢ s of b
12 
13+data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → TypeTree → Set where
14+  expr-t : {s : Expr} {b : TypeTree}
15+         → Γ ⊢ₑ s of b
16+
17 data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where 
18   t-nil : {Γ₁ : Ctx m}
19         → n ≡ m
20-        -------------
21+        --------------
22         → Γ ⊢ nil ▹ Γ₁
23           
24   t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
25        → Γ ⊢ e of (leaf bool) -- Γ ⊢ e : bool
26        → Γ ⊢ b1 ▹ Γ₁
27        → Γ ⊢ b2 ▹ Γ₁
28-       -------------
29+       ---------------------------
30        → Γ ⊢ if (var e) b1 b2 ▹ Γ₁
31           
32   t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
33           → Γ ⊢ e of (leaf bool)
34           → Γ ⊢ b ▹ Γ₁
35-          ----------------------
36+          --------------------------
37           → Γ ⊢ while (var e) b ▹ Γ₁
38           
39   t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
40@@ -39,7 +44,7 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
41            → η ∈ inputs
42            → b ∈ behaviours
43            → Γ ⊢ seq (input η) b ▹ Γ₁
44-           --------------------------
45+           ----------------------------------------------
46            → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁
47 
48   t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
49@@ -48,19 +53,25 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
50         → Γ₂ ⊢ b2 ▹ Γ₂'
51         → intersect-roots (roots Γ₁') (roots Γ₂') ≡ List.[]
52         -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
53-        ---------------
54+        --------------------
55         → Γ ⊢ par b1 b2 ▹ Γ'
56 
57   t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
58         → Γ ⊢ b1 ▹ Γ₁
59         → Γ₁ ⊢ b2 ▹ Γ₂
60-        --------------
61+        --------------------
62         → Γ ⊢ seq b1 b2 ▹ Γ₂
63 
64   t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : TypeTree}
65                  → (outNotify o l T₀) ∈ Γ
66                  → Γ ⊢ e of Tₑ
67                  → Tₑ ⊆ T₀
68-                 -------------
69+                 -------------------------------------------
70                  → n ≡ m
71                  → Γ ⊢ output (notification o l (var e)) ▹ Γ₁
72+
73+  t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {T₀ : TypeTree} {Tₓ : TypeTree}
74+               → Γ ⊢ₑ e of T₀ -- Γ ⊢ e : bool
75+               → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
76+               ---------------------
77+               → Γ ⊢ assign x e ▹ upd Γ x (bt Tₑ)