- commit
- d75b931
- parent
- d26f7fc
- author
- Eugene Akentyev
- date
- 2016-12-21 01:20:45 +0400 +04
Change direction to theorems. Add t-wait and t-exec.
1 files changed,
+31,
-33
+31,
-33
1@@ -1,13 +1,11 @@
2 module Typecheck where
3
4-open import Data.List.All using (All; all) renaming ([] to []-All; _∷_ to _∷-All_)
5-import Data.Vec.Equality as VecEq
6+open import Data.List.All using (All)
7 open import Relation.Nullary using (¬_)
8-open import Relation.Nullary
9 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
10 open import Data.Nat using (ℕ; _+_; suc; _≟_)
11-open import Data.List using (List; []; _∷_; foldl)
12-open import Data.Vec using (Vec; _∈_; zip; _∷_; here; fromList; toList) renaming ([] to []-Vec)
13+open import Data.List using (List)
14+open import Data.Vec using (_∈_)
15 open import Data.Product using (_,_; _×_)
16 open import Function
17 open import Expr
18@@ -89,14 +87,14 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
19 → ¬ ((var x Tₓ) ∈ Γ)
20 → (var x Tᵢ) ∈ Γ₁
21 -------------------------------
22- → Γ ⊢B (input (oneway o x)) ▹ Γ₁
23+ → Γ ⊢B input (oneway o x) ▹ Γ₁
24
25 t-oneway-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
26 → (inOneWay o Tᵢ) ∈ Γ
27 → ((var x Tₓ) ∈ Γ)
28 → Tᵢ ⊆ Tₓ
29 --------------------------------
30- → Γ ⊢B (input (oneway o x)) ▹ subst Ctx n≡m Γ
31+ → Γ ⊢B input (oneway o x) ▹ subst Ctx n≡m Γ
32
33 t-solresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
34 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
35@@ -104,7 +102,7 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
36 → ¬ (var x Tₓ ∈ Γ)
37 → (var x Tᵢ) ∈ Γ₁
38 -----------------------------------------
39- → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
40+ → Γ ⊢B output (solicitres o l e x) ▹ Γ₁
41
42 t-solresp-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
43 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
44@@ -112,7 +110,7 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
45 → (var x Tₓ) ∈ Γ
46 → Tᵢ ⊆ Tₓ
47 -----------------------------------------
48- → Γ ⊢B (output (solicitres o l e x)) ▹ subst Ctx n≡m Γ
49+ → Γ ⊢B output (solicitres o l e x) ▹ subst Ctx n≡m Γ
50
51 t-reqresp-new : ∀ {n m} {Γ : Ctx n} {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
52 → (inReqRes o Tᵢ Tₒ) ∈ Γ
53@@ -122,7 +120,7 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
54 → (var a Tₐ) ∈ Γ₁
55 → Tₐ ⊆ Tₒ
56 -----------------------------------
57- → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
58+ → Γ ⊢B input (reqres o x a b) ▹ Γ₁
59
60 t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
61 → (inReqRes o Tᵢ Tₒ) ∈ Γ
62@@ -132,26 +130,26 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
63 → (var a Tₐ) ∈ Γ₁
64 → Tₐ ⊆ Tₒ
65 ------------------------------------
66- → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
67-
68-
69-{-# NON_TERMINATING #-}
70-check-B : ∀ {n m} → (Γ : Ctx n) → (b : Behaviour) → (Γ₁ : Ctx m) → Dec (Γ ⊢B b ▹ Γ₁)
71-check-B {n} {m} Γ nil Γ₁ with Γ CtxEq.≟ Γ₁
72-... | yes Γ≡Γ₁ = yes (t-nil {n} {m} {Γ} {Γ₁} {Γ≡Γ₁})
73-... | no ¬p = no (λ {(t-nil {_} {_} {_} {_} {Γ≡Γ₁}) → ¬p Γ≡Γ₁})
74-check-B {n} {m} Γ (if e b1 b2) Γ₁ with check-B Γ b1 Γ₁ | check-B Γ b2 Γ₁
75-... | yes ctx₁ | yes ctx₂ = yes (t-if expr-t ctx₁ ctx₂)
76-... | yes _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
77-... | no ¬p | yes _ = no (λ {(t-if _ c₁ _) → ¬p c₁})
78-... | no _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
79-check-B {n} {m} Γ (while e b) Γ₁ with Γ CtxEq.≟ Γ₁
80-... | yes Γ≡Γ₁ = case (check-B {n} {m} Γ b Γ₁) of λ
81- { (yes ctx) → yes (t-while {n} {m} {Γ} {Γ₁} {Γ≡Γ₁} expr-t ctx)
82- ; (no ¬p) → no (λ {(t-while _ ctx) → ¬p ctx})
83- }
84-... | no ¬p = no (λ {(t-while {_} {_} {_} {_} {Γ≡Γ₁} _ _) → ¬p Γ≡Γ₁})
85-check-B {n} {m} Γ (inputchoice pairs) Γ₁ with all (λ { (η , b) → check-B {n} {m} Γ (seq (input η) b) Γ₁ }) pairs
86-... | yes checked = yes (t-choice checked)
87-... | no ¬p = no (λ { (t-choice checked) → ¬p checked })
88-check-B Γ b Γ₁ = {!!}
89+ → Γ ⊢B input (reqres o x a b) ▹ Γ₁
90+
91+ t-wait-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
92+ → (outSolRes o l Tₒ Tᵢ) ∈ Γ
93+ → ¬ ((var x Tₓ) ∈ Γ)
94+ → (var x Tᵢ) ∈ Γ₁
95+ ------------------------
96+ → Γ ⊢B wait r o l x ▹ Γ₁
97+
98+ t-wait-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
99+ → (outSolRes o l Tₒ Tᵢ) ∈ Γ
100+ → ((var x Tₓ) ∈ Γ)
101+ → Tᵢ ⊆ Tₓ
102+ ------------------------
103+ → Γ ⊢B wait r o l x ▹ Γ₁
104+
105+ t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
106+ → (inReqRes o Tᵢ Tₒ) ∈ Γ
107+ → Γ ⊢B b ▹ Γ₁
108+ → (var x Tₓ) ∈ Γ
109+ → Tₓ ⊆ Tₒ
110+ ------------------------
111+ → Γ ⊢B exec r o x b ▹ Γ₁