- commit
- 80305d1
- parent
- 1aa59ad
- author
- Eugene Akentyev
- date
- 2016-12-03 19:37:13 +0400 +04
Simplified variables and finished typing rules for behaviour.
4 files changed,
+114,
-101
+2,
-2
1@@ -11,13 +11,13 @@ open import Type
2
3 data Output_ex : Set where
4 notification : Operation → Location → Expr → Output_ex
5- solicitRes : Operation → Location → Expr → Variable → Output_ex
6+ solicitres : Operation → Location → Expr → Variable → Output_ex
7
8 data Behaviour : Set
9
10 data Input_ex : Set where
11 oneway : Operation → Variable → Input_ex
12- reqRes : Operation → Variable → Variable → Behaviour → Input_ex
13+ reqres : Operation → Variable → Variable → Behaviour → Input_ex
14
15 data Behaviour where
16 input : Input_ex → Behaviour
+12,
-59
1@@ -4,12 +4,13 @@ open import Level
2 open import Relation.Nullary
3 open import Relation.Binary
4 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
5+open import Relation.Nullary.Decidable using (⌊_⌋)
6 open import Function
7 open import Data.Nat using (ℕ)
8 open import Data.Empty
9 open import Data.String using (String)
10-open import Data.List using (List)
11-open import Data.Vec using (Vec)
12+open import Data.List using (List; filter)
13+open import Data.Vec using (Vec; toList)
14 open import Expr
15 open import Variable
16
17@@ -23,68 +24,20 @@ Location = String
18 Channel : Set
19 Channel = String
20
21-data Cardinality : Set where
22- oo oi ii : Cardinality
23-
24-data BasicType : Set where
25- bool int double long string raw void : BasicType
26-
27-data TypeTree : Set
28-
29-data ChildType : Set where
30- child : String → Cardinality → TypeTree → ChildType
31-
32-data TypeTree where
33- leaf : BasicType → TypeTree
34- node : BasicType → List ChildType → TypeTree
35-
36-get-basic : TypeTree → BasicType
37-get-basic (leaf b) = b
38-get-basic (node b _) = b
39+data Type : Set where
40+ bool int double long string raw void : Type
41
42 data TypeDecl : Set where
43- outNotify : Operation → Location → TypeTree → TypeDecl
44- outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl
45- inOneWay : Operation → TypeTree → TypeDecl
46- inReqRes : Operation → TypeTree → TypeTree → TypeDecl
47- var : Variable → TypeTree → TypeDecl
48+ outNotify : Operation → Location → Type → TypeDecl
49+ outSolRes : Operation → Location → Type → Type → TypeDecl
50+ inOneWay : Operation → Type → TypeDecl
51+ inReqRes : Operation → Type → Type → TypeDecl
52+ var : Variable → Type → TypeDecl
53 empty : TypeDecl
54 pair : TypeDecl → TypeDecl → TypeDecl
55
56-data _⊆_ : TypeTree → TypeTree → Set where
57- sub : {T₁ T₂ : TypeTree} → T₁ ⊆ T₂
58+data _⊆_ : Type → Type → Set where
59+ sub : {T₁ T₂ : Type} → T₁ ⊆ T₂
60
61 Ctx : ℕ → Set
62 Ctx = Vec TypeDecl
63-
64-roots : {n : ℕ} → Ctx n → List Name
65-roots xs = go xs
66- where
67- open import Data.List using ([]; _∷_)
68-
69- go : {n : ℕ} → Ctx n → List Name
70- go Vec.[] = []
71- go (Vec._∷_ x xs) =
72- case x of λ
73- { (var v t) → (root v) ∷ (roots xs)
74- ; _ → roots xs
75- }
76-
77-intersect-roots : List Name → List Name → List Name
78-intersect-roots xs ys = intersect xs ys
79- where
80- open import Data.List using ([]; _∷_)
81- open import Data.String using (_≟_)
82-
83- intersect : List Name → List Name → List Name
84- intersect [] _ = []
85- intersect _ [] = []
86- intersect (x ∷ xs) (y ∷ ys) with x ≟ y
87- ... | yes x≡y = x ∷ intersect xs ys
88- ... | no _ = intersect xs ys
89-
90-
91-upd : {n m : ℕ} → Ctx n → Variable → TypeTree → Ctx m
92-upd Γ x Tₓ =
93- let r = root x in
94- {!!}
+96,
-30
1@@ -1,77 +1,143 @@
2+
3 module Typecheck where
4
5 import Data.List as List
6 import Data.Vec.Equality as VecEq
7 open import Relation.Nullary using (¬_)
8+open import Relation.Nullary
9 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
10-open import Data.Nat using (ℕ; _+_)
11-open import Data.Vec using (Vec; _∈_; zip)
12+open import Data.Nat using (ℕ; _+_; suc)
13+open import Data.Vec using (Vec; _∈_; zip; _∷_)
14 open import Expr
15 open import Type
16 open import Behaviour
17 open import Variable
18
19
20-data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → TypeTree → Set where
21- var-t : {s : Variable} {b : TypeTree}
22+data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
23+ var-t : {s : Variable} {b : Type}
24 → Γ ⊢ s of b
25
26-data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → TypeTree → Set where
27- expr-t : {s : Expr} {b : TypeTree}
28+data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
29+ expr-t : {s : Expr} {b : Type}
30 → Γ ⊢ₑ s of b
31
32-data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where
33+data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where
34 t-nil : {Γ₁ : Ctx m}
35 → n ≡ m
36 --------------
37- → Γ ⊢ nil ▹ Γ₁
38+ → Γ ⊢B nil ▹ Γ₁
39
40 t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
41- → Γ ⊢ e of (leaf bool) -- Γ ⊢ e : bool
42- → Γ ⊢ b1 ▹ Γ₁
43- → Γ ⊢ b2 ▹ Γ₁
44+ → Γ ⊢ e of bool -- Γ ⊢ e : bool
45+ → Γ ⊢B b1 ▹ Γ₁
46+ → Γ ⊢B b2 ▹ Γ₁
47 ---------------------------
48- → Γ ⊢ if (var e) b1 b2 ▹ Γ₁
49+ → Γ ⊢B if (var e) b1 b2 ▹ Γ₁
50
51 t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
52- → Γ ⊢ e of (leaf bool)
53- → Γ ⊢ b ▹ Γ₁
54+ → Γ ⊢ e of bool
55+ → Γ ⊢B b ▹ Γ₁
56 --------------------------
57- → Γ ⊢ while (var e) b ▹ Γ₁
58+ → Γ ⊢B while (var e) b ▹ Γ₁
59
60 t-choice : {Γ₁ : Ctx m} {k n : ℕ} {η : Input_ex} {inputs : Vec Input_ex n}
61 {b : Behaviour} {behaviours : Vec Behaviour n}
62 → η ∈ inputs
63 → b ∈ behaviours
64- → Γ ⊢ seq (input η) b ▹ Γ₁
65+ → Γ ⊢B seq (input η) b ▹ Γ₁
66 ----------------------------------------------
67- → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁
68+ → Γ ⊢B inputchoice (zip inputs behaviours) ▹ Γ₁
69
70 t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
71 {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
72- → Γ₁ ⊢ b1 ▹ Γ₁'
73- → Γ₂ ⊢ b2 ▹ Γ₂'
74- → intersect-roots (roots Γ₁') (roots Γ₂') ≡ List.[]
75+ → Γ₁ ⊢B b1 ▹ Γ₁'
76+ → Γ₂ ⊢B b2 ▹ Γ₂'
77 -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
78 --------------------
79- → Γ ⊢ par b1 b2 ▹ Γ'
80+ → Γ ⊢B par b1 b2 ▹ Γ'
81
82 t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
83- → Γ ⊢ b1 ▹ Γ₁
84- → Γ₁ ⊢ b2 ▹ Γ₂
85+ → Γ ⊢B b1 ▹ Γ₁
86+ → Γ₁ ⊢B b2 ▹ Γ₂
87 --------------------
88- → Γ ⊢ seq b1 b2 ▹ Γ₂
89+ → Γ ⊢B seq b1 b2 ▹ Γ₂
90
91- t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : TypeTree}
92+ t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
93 → (outNotify o l T₀) ∈ Γ
94 → Γ ⊢ e of Tₑ
95 → Tₑ ⊆ T₀
96- -------------------------------------------
97 → n ≡ m
98- → Γ ⊢ output (notification o l (var e)) ▹ Γ₁
99+ -------------------------------------------
100+ → Γ ⊢B output (notification o l (var e)) ▹ Γ₁
101
102- t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {T₀ : TypeTree} {Tₓ : TypeTree}
103- → Γ ⊢ₑ e of T₀ -- Γ ⊢ e : bool
104+ t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
105+ → Γ ⊢ₑ e of Tₑ -- Γ ⊢ e : bool
106 → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
107+ → (var x Tₑ) ∈ Γ₁
108 ---------------------
109- → Γ ⊢ assign x e ▹ upd Γ x (bt Tₑ)
110+ → Γ ⊢B assign x e ▹ Γ₁
111+
112+ t-assign-exists : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
113+ → Γ ⊢ₑ e of Tₑ
114+ → (var x Tₓ) ∈ Γ
115+ → Tₑ ≡ Tₓ
116+ → n ≡ m -- TODO Γ ≡ Γ₁
117+ ---------------------
118+ → Γ ⊢B assign x e ▹ Γ₁
119+
120+ t-oneway-new : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
121+ → (inOneWay o Tᵢ) ∈ Γ
122+ → ¬ ((var x Tₓ) ∈ Γ)
123+ → (var x Tᵢ) ∈ Γ₁
124+ -------------------------------
125+ → Γ ⊢B (input (oneway o x)) ▹ Γ₁
126+
127+ t-oneway-exists : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
128+ → (inOneWay o Tᵢ) ∈ Γ
129+ → ((var x Tₓ) ∈ Γ)
130+ → Tᵢ ⊆ Tₓ
131+ → n ≡ m -- TODO Γ ≡ Γ₁
132+ --------------------------------
133+ → Γ ⊢B (input (oneway o x)) ▹ Γ₁
134+
135+ t-solresp-new : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
136+ → (outSolRes o l Tₒ Tᵢ) ∈ Γ
137+ → Tₑ ⊆ Tₒ
138+ → ¬ (var x Tₓ ∈ Γ)
139+ → (var x Tᵢ) ∈ Γ₁
140+ -----------------------------------------
141+ → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
142+
143+ t-solresp-exists : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
144+ → (outSolRes o l Tₒ Tᵢ) ∈ Γ
145+ → Tₑ ⊆ Tₒ
146+ → (var x Tₓ) ∈ Γ
147+ → Tᵢ ⊆ Tₓ
148+ → n ≡ m -- TODO Γ ≡ Γ₁
149+ -----------------------------------------
150+ → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
151+
152+ t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
153+ → (inReqRes o Tᵢ Tₒ) ∈ Γ
154+ → ¬ (var x Tₓ ∈ Γ)
155+ → (var x Tₓ) ∈ Γₓ
156+ → Γₓ ⊢B b ▹ Γ₁
157+ → (var a Tₐ) ∈ Γ₁
158+ → Tₐ ⊆ Tₒ
159+ -----------------------------------
160+ → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
161+
162+ t-reqresp-exists : {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
163+ → (inReqRes o Tᵢ Tₒ) ∈ Γ
164+ → (var x Tₓ) ∈ Γ
165+ → Tᵢ ⊆ Tₓ
166+ → Γ ⊢B b ▹ Γ₁
167+ → (var a Tₐ) ∈ Γ₁
168+ → Tₐ ⊆ Tₒ
169+ ------------------------------------
170+ → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
171+
172+
173+check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (B : Behaviour) → Dec (Γ ⊢B B ▹ Γ₁)
174+check-B = {!!}
+4,
-10
1@@ -6,10 +6,11 @@ open import Data.Product using (_×_)
2 open import Data.Maybe using (Maybe)
3 open import Data.List using (List)
4 open import Data.Bool using (Bool)
5+open import Data.Nat using (ℕ)
6
7
8-Name : Set
9-Name = String
10+Variable : Set
11+Variable = ℕ
12
13 data Value : Set where
14 string : String → Value
15@@ -17,11 +18,4 @@ data Value : Set where
16 bool : Bool → Value
17 double : ℤ × ℤ → Value
18 long : ℤ → Value
19-
20-data Variable : Set where
21- leaf : Name → Value → Variable
22- node : Name → Maybe Value → List Variable → Variable
23-
24-root : Variable → Name
25-root (leaf n _) = n
26-root (node n _ _) = n
27+ void : Value