From 321ab466cfedb850d2ec129b78840294075d08ad Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Wed, 22 Feb 2017 22:44:19 +0300
Subject: [PATCH] Add type preservation cases

---
 src/BehaviouralSemantics.agda |  1 +
 src/Type.agda                 |  4 +++
 src/TypingBehaviour.agda      | 68 ++++++++++++++++++++++++++++++-----
 3 files changed, 65 insertions(+), 8 deletions(-)

diff --git a/src/BehaviouralSemantics.agda b/src/BehaviouralSemantics.agda
index 276d93c..0956bdb 100644
--- a/src/BehaviouralSemantics.agda
+++ b/src/BehaviouralSemantics.agda
@@ -103,3 +103,4 @@ data _↝_∶_ : Behaviour → Behaviour → Label → Set where
            → input ηⱼ ↝ bⱼ′ ∶ η
            ----------------------------------------------
            → inputchoice (toList choices) ↝ (bⱼ′ ∶ bⱼ) ∶ η
+
diff --git a/src/Type.agda b/src/Type.agda
index 255f3e2..8fe0cf7 100644
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -29,6 +29,7 @@ Ctx = Vec TypeDecl
 data Context : Set where
   ⋆ : ∀ {n} → Ctx n → Context
   & : Context → Context → Context
+--  sideEffect : {Γ Γ′ : Context}
 
 infix 4 _∈_
 
@@ -40,3 +41,6 @@ data _∈_ : TypeDecl → Context → Set where
   there-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
   there-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
 
+appendContext : TypeDecl → Context → Context
+appendContext t (⋆ Γ) = ⋆ (t ∷ Γ)
+appendContext t (& Γ₁ Γ₂) = & (appendContext t Γ₁) Γ₂
diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index f4c1915..f24def3 100644
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -7,6 +7,7 @@ open import Data.Nat using (ℕ)
 open import Data.List using (List)
 open import Data.Vec using ([]; _++_; _∷_)
 open import Data.Product using (_,_; _×_)
+open import BehaviouralSemantics
 open import Function
 open import Expr
 open import Type
@@ -14,18 +15,24 @@ open import Behaviour
 open import Variable
 
 
--- Side effect
-data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour → Set where
-  -- Updated
-  upd : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} → Γ ⊢ b₁ ↦ Γ₁ ⊢ b₂
-
-  -- Identity
-  idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b
-
 data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where
   expr-t : {s : Expr} {b : Type}
          → Γ ⊢ₑ s ∶ b
 
+-- Side effect
+data _↦⟨_⟩_ : Context → Label → Context → Set where
+  s-assign : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+           → Γ ⊢ₑ e ∶ Tₑ
+           → var x Tₓ ∈ Γ
+           → Tₓ ≡ Tₑ
+           ---------------------------------
+           → Γ ↦⟨ lb-assign x e ⟩ Γ
+
+  s-assign-upd : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+               → Γ ⊢ₑ e ∶ Tₑ
+               → ¬ (var x Tₓ ∈ Γ)
+               → Γ ↦⟨ lb-assign x e ⟩ (appendContext (var x Tₓ) Γ)
+
 data _⊢B_▹_ : Context → Behaviour → Context → Set where
   t-nil : {Γ : Context}
         --------------
@@ -242,3 +249,48 @@ struct-cong-par-assoc : {Γ₁ Γ₂ Γ₃ Γ₁' Γ₂' Γ₃' : Context} {b₁
                       → & (& Γ₁ Γ₂) Γ₃ ⊢B (b₁ ∥ b₂) ∥ b₃ ▹ & (& Γ₁' Γ₂') Γ₃'
                       → & Γ₁ (& Γ₂ Γ₃) ⊢B b₁ ∥ (b₂ ∥ b₃) ▹ & Γ₁' (& Γ₂' Γ₃')
 struct-cong-par-assoc (t-par (t-par t1 t2) t3) = t-par t1 (t-par t2 t3)
+
+--type-preservation : {Γ Γ′ Γ′′ : Context} {b b′ : Behaviour} {η : Label}
+--                  → Γ ⊢B b ▹ Γ′
+--                  → b ↝ b′ ∶ η
+--                  → Γ ↦⟨ η ⟩ Γ′′
+--                  → Γ′′ ⊢B b′ ▹ Γ′
+--type-preservation _ = {!-c -t 30!}
+
+type-preservation-if-then : {Γ Γ′ : Context} {b₁ b₂ : Behaviour} {t : State} {e : Expr}
+                  → Γ ⊢B if e then b₁ else b₂ ▹ Γ′
+                  → (if e then b₁ else b₂) ↝ b₁ ∶ (lb-read t)
+                  → Γ ↦⟨ lb-read t ⟩ Γ
+                  → Γ ⊢B b₁ ▹ Γ′
+type-preservation-if-then (t-if et t1 t2) _ _ = t1
+
+type-preservation-if-else : {Γ Γ′ : Context} {b₁ b₂ : Behaviour} {t : State} {e : Expr}
+                  → Γ ⊢B if e then b₁ else b₂ ▹ Γ′
+                  → (if e then b₁ else b₂) ↝ b₂ ∶ (lb-read t)
+                  → Γ ↦⟨ lb-read t ⟩ Γ
+                  → Γ ⊢B b₂ ▹ Γ′
+type-preservation-if-else (t-if et t1 t2) _ _ = t2
+
+type-preservation-iter : {Γ Γ′ : Context} {b : Behaviour} {t : State} {e : Expr}
+                  → Γ ⊢B while[ e ] b ▹ Γ′
+                  → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ (lb-read t)
+                  → Γ ↦⟨ lb-read t ⟩ Γ
+                  → Γ ⊢B (b ∶ (while[ e ] b)) ▹ Γ′
+type-preservation-iter (t-while te t) _ _ = t-seq t (t-while te t)
+
+type-preservation-no-iter : {Γ Γ′ : Context} {b : Behaviour} {t : State} {e : Expr}
+                  → Γ ⊢B while[ e ] b ▹ Γ′
+                  → (while[ e ] b) ↝ nil ∶ (lb-read t)
+                  → Γ ↦⟨ lb-read t ⟩ Γ
+                  → Γ ⊢B (nil ∶ (while[ e ] b)) ▹ Γ
+type-preservation-no-iter (t-while te t) _ _ = t-seq t-nil (t-while te t)
+
+type-preservation-assign : {Γ Γ′ Γ′′ : Context} {x : Variable} {t : State} {e : Expr} {Tₑ : Type}
+                  → Γ ⊢B x ≃ e ▹ Γ′
+                  → (x ≃ e) ↝ nil ∶ (lb-assign x e)
+                  → Γ ↦⟨ lb-assign x e ⟩ Γ′′
+                  → Γ′′ ⊢B x ≃ e ▹ Γ′
+type-preservation-assign (t-assign-new x₁ x₂) _ _ = {!!}
+type-preservation-assign (t-assign-new-left x₁ x₂) _ _ = {!!}
+type-preservation-assign (t-assign-new-right x₁ x₂) _ _ = {!!}
+type-preservation-assign (t-assign-exists x₁ x₂ x₃) _ _ = {!!}
-- 
2.50.1