repos / jolie.agda.git

commit

dd77c46

parent

8501ad7

author

Eugene Akentyev

date

2017-01-08 20:52:36 +0400 +04

Added t-mutate

 1@@ -2,8 +2,8 @@ module TypingBehaviour where
 2 
 3 open import Data.List.All using (All)
 4 open import Relation.Nullary using (¬_)
 5-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl; sym; trans)
 6-open import Data.Nat using (ℕ; _+_; suc; _≟_)
 7+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 8+open import Data.Nat using (ℕ)
 9 open import Data.List using (List)
10 open import Data.Vec using (_∈_; []; _++_; _∷_; here; there)
11 open import Data.Product using (_,_; _×_)
12@@ -14,11 +14,10 @@ open import Behaviour
13 open import Variable
14 
15 
16-data _⊢_∶_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
17-  var-t : {s : Variable} {b : Type}
18-        → (var s b) ∈ Γ
19-        ------------
20-        → Γ ⊢ s ∶ b
21+data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
22+  updated : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} → SideEffect Γ Γ₁
23+  identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
24+  undefined : SideEffect [] []
25 
26 data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
27   expr-t : {s : Expr} {b : Type}
28@@ -66,7 +65,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
29 
30   t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
31                  → (outNotify o l T₀) ∈ Γ
32-                 → Γ ⊢ e ∶ Tₑ
33+                 → var e Tₑ ∈ Γ
34                  → Tₑ ⊆ T₀
35                  ------------------------------------------------
36                  → ◆ Γ ⊢B output (o at l [ var e ]) ▹ ◆ Γ
37@@ -152,28 +151,25 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
38          ----------------------------
39          → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
40 
41+  t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b : Behaviour}
42+           → SideEffect Γ Γₐ
43+           → ◆ Γ ⊢B b ▹ ◆ Γ₁
44+           ------------------
45+           → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
46+
47+
48 struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
49 struct-congruence t refl = t
50 
51 struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
52-struct-cong-nil (t-seq t-nil t) = t
53+struct-cong-nil (t-seq x x₁) = t-mutate updated x₁
54+struct-cong-nil (t-mutate x x₁) = t-mutate updated (struct-cong-nil x₁)
55 
56 struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b ∣ nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
57-struct-cong-par-nil (t-par t t-nil) = t
58+struct-cong-par-nil (t-par x _) = x
59 
60 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) ▹ ■ Γ₂' Γ₁'
61 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
62 
63-data Label : Set where
64-  x=e readt νr r:o r,o r,ol : Label
65-
66-data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
67-  updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
68-  identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
69-  undefined : SideEffect [] []
70-
71---preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
72---preservation t undefined = t
73---preservation t (identity γ) = t
74---preservation t-nil (updated {_} {k} Γ Γₐ) = {!!}
75---preservation = {!!}
76+preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
77+preservation x s = t-mutate s x