Added t-mutate

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 427fa4693bd71d70ca5279944ebe017c20d6c298..a9cd0efd8fccbaf55a115382d58f39c291522527 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -2,8 +2,8 @@ module TypingBehaviour where
 
 open import Data.List.All using (All)
 open import Relation.Nullary using (¬_)
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl; sym; trans)
-open import Data.Nat using (ℕ; _+_; suc; _≟_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Data.Nat using (ℕ)
 open import Data.List using (List)
 open import Data.Vec using (_∈_; []; _++_; _∷_; here; there)
 open import Data.Product using (_,_; _×_)
@@ -14,11 +14,10 @@ open import Behaviour
 open import Variable
 
 
-data _⊢_∶_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
-  var-t : {s : Variable} {b : Type}
-        → (var s b) ∈ Γ
-        ------------
-        → Γ ⊢ s ∶ b
+data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
+  updated : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} → SideEffect Γ Γ₁
+  identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
+  undefined : SideEffect [] []
 
 data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
   expr-t : {s : Expr} {b : Type}
@@ -66,7 +65,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
 
   t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
-                 → Γ ⊢ e ∶ Tₑ
+                 → var e Tₑ ∈ Γ
                  → Tₑ ⊆ T₀
                  ------------------------------------------------
                  → ◆ Γ ⊢B output (o at l [ var e ]) ▹ ◆ Γ
@@ -152,28 +151,25 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
          ----------------------------
          → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
 
+  t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b : Behaviour}
+           → SideEffect Γ Γₐ
+           → ◆ Γ ⊢B b ▹ ◆ Γ₁
+           ------------------
+           → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
+
+
 struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
 struct-congruence t refl = t
 
 struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
-struct-cong-nil (t-seq t-nil t) = t
+struct-cong-nil (t-seq x x₁) = t-mutate updated x₁
+struct-cong-nil (t-mutate x x₁) = t-mutate updated (struct-cong-nil x₁)
 
 struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b ∣ nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
-struct-cong-par-nil (t-par t t-nil) = t
+struct-cong-par-nil (t-par x _) = x
 
 struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b1 ∣ b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (b2 ∣ b1) ▹ ■ Γ₂' Γ₁'
 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
 
-data Label : Set where
-  x=e readt νr r:o r,o r,ol : Label
-
-data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
-  updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
-  identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
-  undefined : SideEffect [] []
-
---preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
---preservation t undefined = t
---preservation t (identity γ) = t
---preservation t-nil (updated {_} {k} Γ Γₐ) = {!!}
---preservation = {!!}
+preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
+preservation x s = t-mutate s x