From 1aa59ad2ea6ea45a23d270fc49b9631262a5ee92 Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Wed, 9 Nov 2016 02:01:07 +0300
Subject: [PATCH] Add t-assign-new

---
 src/Type.agda      |  6 ++++++
 src/Typecheck.agda | 25 ++++++++++++++++++-------
 2 files changed, 24 insertions(+), 7 deletions(-)

diff --git a/src/Type.agda b/src/Type.agda
index d3b1ee9..0b2b9a5 100644
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -82,3 +82,9 @@ intersect-roots xs ys = intersect xs ys
     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 c9fe2e4..ad70c02 100644
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -2,6 +2,7 @@ module Typecheck where
 
 import Data.List as List
 import Data.Vec.Equality as VecEq
+open import Relation.Nullary using (¬_)
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 open import Data.Nat using (ℕ; _+_)
 open import Data.Vec using (Vec; _∈_; zip)
@@ -15,23 +16,27 @@ data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → TypeTree → Set where
   var-t : {s : Variable} {b : TypeTree} 
         → Γ ⊢ s of b
 
+data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → TypeTree → Set where
+  expr-t : {s : Expr} {b : TypeTree}
+         → Γ ⊢ₑ s of b
+
 data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where 
   t-nil : {Γ₁ : Ctx m}
         → n ≡ m
-        -------------
+        --------------
         → Γ ⊢ nil ▹ Γ₁
           
   t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
        → Γ ⊢ e of (leaf bool) -- Γ ⊢ e : bool
        → Γ ⊢ b1 ▹ Γ₁
        → Γ ⊢ b2 ▹ Γ₁
-       -------------
+       ---------------------------
        → Γ ⊢ if (var e) b1 b2 ▹ Γ₁
           
   t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
           → Γ ⊢ e of (leaf bool)
           → Γ ⊢ b ▹ Γ₁
-          ----------------------
+          --------------------------
           → Γ ⊢ while (var e) b ▹ Γ₁
           
   t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
@@ -39,7 +44,7 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
            → η ∈ inputs
            → b ∈ behaviours
            → Γ ⊢ seq (input η) b ▹ Γ₁
-           --------------------------
+           ----------------------------------------------
            → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁
 
   t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
@@ -48,19 +53,25 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
         → Γ₂ ⊢ b2 ▹ Γ₂'
         → intersect-roots (roots Γ₁') (roots Γ₂') ≡ List.[]
         -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
-        ---------------
+        --------------------
         → Γ ⊢ par b1 b2 ▹ Γ'
 
   t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
         → Γ ⊢ b1 ▹ Γ₁
         → Γ₁ ⊢ b2 ▹ Γ₂
-        --------------
+        --------------------
         → Γ ⊢ seq b1 b2 ▹ Γ₂
 
   t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : TypeTree}
                  → (outNotify o l T₀) ∈ Γ
                  → Γ ⊢ e of Tₑ
                  → Tₑ ⊆ T₀
-                 -------------
+                 -------------------------------------------
                  → n ≡ m
                  → Γ ⊢ output (notification o l (var e)) ▹ Γ₁
+
+  t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {T₀ : TypeTree} {Tₓ : TypeTree}
+               → Γ ⊢ₑ e of T₀ -- Γ ⊢ e : bool
+               → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
+               ---------------------
+               → Γ ⊢ assign x e ▹ upd Γ x (bt Tₑ)
-- 
2.50.1