repos / jolie.agda.git

commit

321ab46

parent

84fbee9

author

Eugene Akentyev

date

2017-02-22 23:44:19 +0400 +04

Add type preservation cases

1@@ -103,3 +103,4 @@ data _↝_∶_ : Behaviour → Behaviour → Label → Set where
2            → input ηⱼ ↝ bⱼ′ ∶ η
3            ----------------------------------------------
4            → inputchoice (toList choices) ↝ (bⱼ′ ∶ bⱼ) ∶ η
5+

 1@@ -29,6 +29,7 @@ Ctx = Vec TypeDecl
 2 data Context : Set where
 3   ⋆ : ∀ {n} → Ctx n → Context
 4   & : Context → Context → Context
 5+--  sideEffect : {Γ Γ′ : Context}
 6 
 7 infix 4 _∈_
 8 
 9@@ -40,3 +41,6 @@ data _∈_ : TypeDecl → Context → Set where
10   there-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
11   there-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
12 
13+appendContext : TypeDecl → Context → Context
14+appendContext t (⋆ Γ) = ⋆ (t ∷ Γ)
15+appendContext t (& Γ₁ Γ₂) = & (appendContext t Γ₁) Γ₂

 1@@ -7,6 +7,7 @@ open import Data.Nat using (ℕ)
 2 open import Data.List using (List)
 3 open import Data.Vec using ([]; _++_; _∷_)
 4 open import Data.Product using (_,_; _×_)
 5+open import BehaviouralSemantics
 6 open import Function
 7 open import Expr
 8 open import Type
 9@@ -14,18 +15,24 @@ open import Behaviour
10 open import Variable
11 
12 
13--- Side effect
14-data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour → Set where
15-  -- Updated
16-  upd : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} → Γ ⊢ b₁ ↦ Γ₁ ⊢ b₂
17-
18-  -- Identity
19-  idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b
20-
21 data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where
22   expr-t : {s : Expr} {b : Type}
23          → Γ ⊢ₑ s ∶ b
24 
25+-- Side effect
26+data _↦⟨_⟩_ : Context → Label → Context → Set where
27+  s-assign : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
28+           → Γ ⊢ₑ e ∶ Tₑ
29+           → var x Tₓ ∈ Γ
30+           → Tₓ ≡ Tₑ
31+           ---------------------------------
32+           → Γ ↦⟨ lb-assign x e ⟩ Γ
33+
34+  s-assign-upd : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
35+               → Γ ⊢ₑ e ∶ Tₑ
36+               → ¬ (var x Tₓ ∈ Γ)
37+               → Γ ↦⟨ lb-assign x e ⟩ (appendContext (var x Tₓ) Γ)
38+
39 data _⊢B_▹_ : Context → Behaviour → Context → Set where
40   t-nil : {Γ : Context}
41         --------------
42@@ -242,3 +249,48 @@ struct-cong-par-assoc : {Γ₁ Γ₂ Γ₃ Γ₁' Γ₂' Γ₃' : Context} {b₁
43                       → & (& Γ₁ Γ₂) Γ₃ ⊢B (b₁ ∥ b₂) ∥ b₃ ▹ & (& Γ₁' Γ₂') Γ₃'
44                       → & Γ₁ (& Γ₂ Γ₃) ⊢B b₁ ∥ (b₂ ∥ b₃) ▹ & Γ₁' (& Γ₂' Γ₃')
45 struct-cong-par-assoc (t-par (t-par t1 t2) t3) = t-par t1 (t-par t2 t3)
46+
47+--type-preservation : {Γ Γ′ Γ′′ : Context} {b b′ : Behaviour} {η : Label}
48+--                  → Γ ⊢B b ▹ Γ′
49+--                  → b ↝ b′ ∶ η
50+--                  → Γ ↦⟨ η ⟩ Γ′′
51+--                  → Γ′′ ⊢B b′ ▹ Γ′
52+--type-preservation _ = {!-c -t 30!}
53+
54+type-preservation-if-then : {Γ Γ′ : Context} {b₁ b₂ : Behaviour} {t : State} {e : Expr}
55+                  → Γ ⊢B if e then b₁ else b₂ ▹ Γ′
56+                  → (if e then b₁ else b₂) ↝ b₁ ∶ (lb-read t)
57+                  → Γ ↦⟨ lb-read t ⟩ Γ
58+                  → Γ ⊢B b₁ ▹ Γ′
59+type-preservation-if-then (t-if et t1 t2) _ _ = t1
60+
61+type-preservation-if-else : {Γ Γ′ : Context} {b₁ b₂ : Behaviour} {t : State} {e : Expr}
62+                  → Γ ⊢B if e then b₁ else b₂ ▹ Γ′
63+                  → (if e then b₁ else b₂) ↝ b₂ ∶ (lb-read t)
64+                  → Γ ↦⟨ lb-read t ⟩ Γ
65+                  → Γ ⊢B b₂ ▹ Γ′
66+type-preservation-if-else (t-if et t1 t2) _ _ = t2
67+
68+type-preservation-iter : {Γ Γ′ : Context} {b : Behaviour} {t : State} {e : Expr}
69+                  → Γ ⊢B while[ e ] b ▹ Γ′
70+                  → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ (lb-read t)
71+                  → Γ ↦⟨ lb-read t ⟩ Γ
72+                  → Γ ⊢B (b ∶ (while[ e ] b)) ▹ Γ′
73+type-preservation-iter (t-while te t) _ _ = t-seq t (t-while te t)
74+
75+type-preservation-no-iter : {Γ Γ′ : Context} {b : Behaviour} {t : State} {e : Expr}
76+                  → Γ ⊢B while[ e ] b ▹ Γ′
77+                  → (while[ e ] b) ↝ nil ∶ (lb-read t)
78+                  → Γ ↦⟨ lb-read t ⟩ Γ
79+                  → Γ ⊢B (nil ∶ (while[ e ] b)) ▹ Γ
80+type-preservation-no-iter (t-while te t) _ _ = t-seq t-nil (t-while te t)
81+
82+type-preservation-assign : {Γ Γ′ Γ′′ : Context} {x : Variable} {t : State} {e : Expr} {Tₑ : Type}
83+                  → Γ ⊢B x ≃ e ▹ Γ′
84+                  → (x ≃ e) ↝ nil ∶ (lb-assign x e)
85+                  → Γ ↦⟨ lb-assign x e ⟩ Γ′′
86+                  → Γ′′ ⊢B x ≃ e ▹ Γ′
87+type-preservation-assign (t-assign-new x₁ x₂) _ _ = {!!}
88+type-preservation-assign (t-assign-new-left x₁ x₂) _ _ = {!!}
89+type-preservation-assign (t-assign-new-right x₁ x₂) _ _ = {!!}
90+type-preservation-assign (t-assign-exists x₁ x₂ x₃) _ _ = {!!}