- commit
- bba29dc
- parent
- 417008d
- author
- Eugene Akentyev
- date
- 2016-12-07 17:42:16 +0400 +04
Merge pull request #1 from ak3n/in_types In types version
5 files changed,
+161,
-198
+5,
-4
1@@ -1,7 +1,8 @@
2 module Behaviour where
3
4+open import Data.Nat using (ℕ)
5 open import Data.String using (String)
6-open import Data.List using (List)
7+open import Data.Vec using (Vec)
8 open import Data.Product using (_×_)
9 open import Variable
10 open import Expr
11@@ -10,13 +11,13 @@ open import Type
12
13 data Output_ex : Set where
14 notification : Operation → Location → Expr → Output_ex
15- solicitRes : Operation → Location → Expr → Variable → Output_ex
16+ solicitres : Operation → Location → Expr → Variable → Output_ex
17
18 data Behaviour : Set
19
20 data Input_ex : Set where
21 oneway : Operation → Variable → Input_ex
22- reqRes : Operation → Variable → Variable → Behaviour → Input_ex
23+ reqres : Operation → Variable → Variable → Behaviour → Input_ex
24
25 data Behaviour where
26 input : Input_ex → Behaviour
27@@ -27,7 +28,7 @@ data Behaviour where
28 par : Behaviour → Behaviour → Behaviour
29 assign : Variable → Expr → Behaviour
30 nil : Behaviour
31- inputchoice : List (Input_ex × Behaviour) → Behaviour
32+ inputchoice : {n : ℕ} → Vec (Input_ex × Behaviour) n → Behaviour
33 wait : Channel → Operation → Location → Variable → Behaviour
34 exec : Channel → Operation → Variable → Behaviour → Behaviour
35
+4,
-3
1@@ -1,5 +1,6 @@
2 module Service where
3
4+open import Data.Nat using (ℕ)
5 open import Data.List using (List)
6 open import Data.String using (String)
7 open import Data.Product using (_×_)
8@@ -22,8 +23,8 @@ data Process : Set where
9
10 data AliasingFunction : Set where
11
12-Deployment : Set
13-Deployment = AliasingFunction × Γ
14+Deployment : {m : ℕ} → Set
15+Deployment {m} = AliasingFunction × Ctx m
16
17 data Service : Set where
18- service : Behaviour → Deployment → Process → Service
19+ service : {m : ℕ} → Behaviour → Deployment {m} → Process → Service
+14,
-142
1@@ -1,14 +1,16 @@
2 module Type where
3
4+open import Level
5 open import Relation.Nullary
6 open import Relation.Binary
7 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
8-open import Function using (_∘_)
9+open import Relation.Nullary.Decidable using (⌊_⌋)
10+open import Function
11 open import Data.Nat using (ℕ)
12 open import Data.Empty
13 open import Data.String using (String)
14-open import Data.List using (List)
15-open import Data.Vec using (Vec)
16+open import Data.List using (List; filter)
17+open import Data.Vec using (Vec; toList)
18 open import Expr
19 open import Variable
20
21@@ -22,150 +24,20 @@ Location = String
22 Channel : Set
23 Channel = String
24
25-data Cardinality : Set where
26- oo oi ii : Cardinality
27-
28-data BasicType : Set where
29- bool int double long string raw void : BasicType
30-
31-module BasicTypeEq where
32- _≟_ : Decidable {A = BasicType} _≡_
33- bool ≟ bool = yes refl
34- int ≟ int = yes refl
35- double ≟ double = yes refl
36- long ≟ long = yes refl
37- string ≟ string = yes refl
38- raw ≟ raw = yes refl
39- void ≟ void = yes refl
40- bool ≟ int = no λ()
41- bool ≟ double = no λ()
42- bool ≟ long = no λ()
43- bool ≟ string = no λ()
44- bool ≟ raw = no λ()
45- bool ≟ void = no λ()
46- int ≟ bool = no λ()
47- int ≟ double = no λ()
48- int ≟ long = no λ()
49- int ≟ string = no λ()
50- int ≟ raw = no λ()
51- int ≟ void = no λ()
52- double ≟ bool = no λ()
53- double ≟ int = no λ()
54- double ≟ long = no λ()
55- double ≟ string = no λ()
56- double ≟ raw = no λ()
57- double ≟ void = no λ()
58- long ≟ bool = no λ()
59- long ≟ int = no λ()
60- long ≟ double = no λ()
61- long ≟ string = no λ()
62- long ≟ raw = no λ()
63- long ≟ void = no λ()
64- string ≟ bool = no λ()
65- string ≟ int = no λ()
66- string ≟ double = no λ()
67- string ≟ long = no λ()
68- string ≟ raw = no λ()
69- string ≟ void = no λ()
70- raw ≟ bool = no λ()
71- raw ≟ int = no λ()
72- raw ≟ double = no λ()
73- raw ≟ long = no λ()
74- raw ≟ string = no λ()
75- raw ≟ void = no λ()
76- void ≟ bool = no λ()
77- void ≟ int = no λ()
78- void ≟ double = no λ()
79- void ≟ long = no λ()
80- void ≟ string = no λ()
81- void ≟ raw = no λ()
82-
83-data TypeTree : Set
84-
85-data ChildType : Set where
86- child : String → Cardinality → TypeTree → ChildType
87-
88-data TypeTree where
89- leaf : BasicType → TypeTree
90- node : BasicType → List ChildType → TypeTree
91-
92-get-basic : TypeTree → BasicType
93-get-basic (leaf b) = b
94-get-basic (node b _) = b
95-
96-module TypeTreeEq where
97- _≟_ : Decidable {A = TypeTree} _≡_
98- (leaf b1) ≟ (leaf b2) with BasicTypeEq._≟_ b1 b2
99- ... | yes b1≡b2 = yes (cong leaf b1≡b2)
100- ... | no b1≢b2 = no {!!} -- ¬ leaf b1 ≡ leaf b2
101- (node b1 cts) ≟ (node b2 cts') = {!!}
102- (leaf _) ≟ (node _ _) = no λ ()
103- (node _ _) ≟ (leaf _) = no λ ()
104+data Type : Set where
105+ bool int double long string raw void : Type
106
107 data TypeDecl : Set where
108- outNotify : Operation → Location → TypeTree → TypeDecl
109- outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl
110- inOneWay : Operation → TypeTree → TypeDecl
111- inReqRes : Operation → TypeTree → TypeTree → TypeDecl
112- var : Variable → TypeTree → TypeDecl
113+ outNotify : Operation → Location → Type → TypeDecl
114+ outSolRes : Operation → Location → Type → Type → TypeDecl
115+ inOneWay : Operation → Type → TypeDecl
116+ inReqRes : Operation → Type → Type → TypeDecl
117+ var : Variable → Type → TypeDecl
118 empty : TypeDecl
119 pair : TypeDecl → TypeDecl → TypeDecl
120
121-module TypeDeclEq where
122- _≟_ : Decidable {A = TypeDecl} _≡_
123- (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) = {!!}
124- (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') = {!!}
125- (inOneWay o1 t1) ≟ (inOneWay o2 t2) = {!!}
126- (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') = {!!}
127- (var v1 t1) ≟ (var v2 t2) = {!!}
128- (pair t1 t1') ≟ (pair t2 t2') = {!!}
129- empty ≟ empty = yes refl
130- empty ≟ (outNotify _ _ _) = no λ()
131- empty ≟ (outSolRes _ _ _ _) = no λ()
132- empty ≟ (inOneWay _ _) = no λ()
133- empty ≟ (inReqRes _ _ _) = no λ()
134- empty ≟ (var _ _) = no λ()
135- empty ≟ (pair _ _) = no λ()
136- (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
137- (outNotify _ _ _) ≟ (inOneWay _ _) = no λ()
138- (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ()
139- (outNotify _ _ _) ≟ (var _ _) = no λ()
140- (outNotify _ _ _) ≟ empty = no λ()
141- (outNotify _ _ _) ≟ (pair _ _) = no λ()
142- (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ()
143- (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ()
144- (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ()
145- (outSolRes _ _ _ _) ≟ (var _ _) = no λ()
146- (outSolRes _ _ _ _) ≟ empty = no λ()
147- (outSolRes _ _ _ _) ≟ (pair _ _) = no λ()
148- (inOneWay _ _) ≟ (outNotify _ _ _) = no λ()
149- (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ()
150- (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ()
151- (inOneWay _ _) ≟ (var _ _) = no λ()
152- (inOneWay _ _) ≟ empty = no λ()
153- (inOneWay _ _) ≟ (pair _ _) = no λ()
154- (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ()
155- (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
156- (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ()
157- (inReqRes _ _ _) ≟ (var _ _) = no λ()
158- (inReqRes _ _ _) ≟ empty = no λ()
159- (inReqRes _ _ _) ≟ (pair _ _) = no λ()
160- (var _ _) ≟ (outNotify _ _ _) = no λ()
161- (var _ _) ≟ (outSolRes _ _ _ _) = no λ()
162- (var _ _) ≟ (inOneWay _ _) = no λ()
163- (var _ _) ≟ (inReqRes _ _ _) = no λ()
164- (var _ _) ≟ empty = no λ()
165- (var _ _) ≟ (pair _ _) = no λ()
166- (pair _ _) ≟ (outNotify _ _ _) = no λ()
167- (pair _ _) ≟ (outSolRes _ _ _ _) = no λ()
168- (pair _ _) ≟ (inOneWay _ _) = no λ()
169- (pair _ _) ≟ (inReqRes _ _ _) = no λ()
170- (pair _ _) ≟ (var _ _) = no λ()
171- (pair _ _) ≟ empty = no λ()
172-
173- decSetoid : DecSetoid _ _
174- decSetoid = PropEq.decSetoid _≟_
175-
176+data _⊆_ : Type → Type → Set where
177+ sub : {T₁ T₂ : Type} → T₁ ⊆ T₂
178
179 Ctx : ℕ → Set
180 Ctx = Vec TypeDecl
+134,
-42
1@@ -1,51 +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.Binary.PropositionalEquality as PropEq using (decSetoid)
8-open import Relation.Nullary.Decidable using (⌊_⌋)
9-open import Data.Maybe using (Maybe; just; nothing)
10-open import Data.Nat using (ℕ)
11-open import Data.Bool using (if_then_else_)
12-open import Data.Product using (_,_)
13-open import Function
14+open import Relation.Nullary using (¬_)
15+open import Relation.Nullary
16+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
17+open import Data.Nat using (ℕ; _+_; suc)
18+open import Data.Vec using (Vec; _∈_; zip; _∷_)
19 open import Expr
20 open import Type
21 open import Behaviour
22 open import Variable
23
24
25-type_of_value : Value → BasicType
26-type_of_value (Value.string _) = Type.string
27-type_of_value (Value.int _) = Type.int
28-type_of_value (Value.bool _) = Type.bool
29-type_of_value (Value.double _) = Type.double
30-type_of_value (Value.long _) = Type.long
31-
32-type_of_var : Variable → Maybe BasicType
33-type_of_var (leaf _ v) = just $ type_of_value v
34-type_of_var _ = nothing
35-
36-data Check {n} (Γ : Ctx n) : Behaviour → Set where
37- yes : {b : Behaviour} → Check Γ b
38- no : {b : Behaviour} → Check Γ b
39-
40-typecheck_behaviour : {n : ℕ} (Γ : Ctx n) → (b : Behaviour) → Check Γ b
41-typecheck_behaviour ctx nil = yes
42-typecheck_behaviour ctx (if e b1 b2) =
43- case e of λ
44- {
45- -- If conditional expression is variable
46- (var v) →
47- let ctx1 = typecheck_behaviour ctx b1 in
48- case (type_of_var v) of λ
49- -- If e : bool
50- { (just bool) →
51- let ctx2 = typecheck_behaviour ctx b2 in
52- let module CtxEq = VecEq.DecidableEquality Data.Bool.decSetoid in
53- if ⌊ ctx1 CtxEq.≟ ctx2 ⌋ then yes else no
54- ; _ → no
55- }
56- --case ()
57- ; _ → no
58- }
59-typecheck_behaviour _ _ = no
60+data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
61+ var-t : {s : Variable} {b : Type}
62+ → Γ ⊢ s of b
63+
64+data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
65+ expr-t : {s : Expr} {b : Type}
66+ → Γ ⊢ₑ s of b
67+
68+data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where
69+ t-nil : {Γ₁ : Ctx m}
70+ → n ≡ m
71+ --------------
72+ → Γ ⊢B nil ▹ Γ₁
73+
74+ t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
75+ → Γ ⊢ e of bool -- Γ ⊢ e : bool
76+ → Γ ⊢B b1 ▹ Γ₁
77+ → Γ ⊢B b2 ▹ Γ₁
78+ ---------------------------
79+ → Γ ⊢B if (var e) b1 b2 ▹ Γ₁
80+
81+ t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
82+ → Γ ⊢ e of bool
83+ → Γ ⊢B b ▹ Γ₁
84+ --------------------------
85+ → Γ ⊢B while (var e) b ▹ Γ₁
86+
87+ t-choice : {Γ₁ : Ctx m} {k n : ℕ} {η : Input_ex} {inputs : Vec Input_ex n}
88+ {b : Behaviour} {behaviours : Vec Behaviour n}
89+ → η ∈ inputs
90+ → b ∈ behaviours
91+ → Γ ⊢B seq (input η) b ▹ Γ₁
92+ ----------------------------------------------
93+ → Γ ⊢B inputchoice (zip inputs behaviours) ▹ Γ₁
94+
95+ t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
96+ {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
97+ → Γ₁ ⊢B b1 ▹ Γ₁'
98+ → Γ₂ ⊢B b2 ▹ Γ₂'
99+ -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
100+ --------------------
101+ → Γ ⊢B par b1 b2 ▹ Γ'
102+
103+ t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
104+ → Γ ⊢B b1 ▹ Γ₁
105+ → Γ₁ ⊢B b2 ▹ Γ₂
106+ --------------------
107+ → Γ ⊢B seq b1 b2 ▹ Γ₂
108+
109+ t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
110+ → (outNotify o l T₀) ∈ Γ
111+ → Γ ⊢ e of Tₑ
112+ → Tₑ ⊆ T₀
113+ → n ≡ m
114+ -------------------------------------------
115+ → Γ ⊢B output (notification o l (var e)) ▹ Γ₁
116+
117+ t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
118+ → Γ ⊢ₑ e of Tₑ -- Γ ⊢ e : bool
119+ → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
120+ → (var x Tₑ) ∈ Γ₁
121+ ---------------------
122+ → Γ ⊢B assign x e ▹ Γ₁
123+
124+ t-assign-exists : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
125+ → Γ ⊢ₑ e of Tₑ
126+ → (var x Tₓ) ∈ Γ
127+ → Tₑ ≡ Tₓ
128+ → n ≡ m -- TODO Γ ≡ Γ₁
129+ ---------------------
130+ → Γ ⊢B assign x e ▹ Γ₁
131+
132+ t-oneway-new : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
133+ → (inOneWay o Tᵢ) ∈ Γ
134+ → ¬ ((var x Tₓ) ∈ Γ)
135+ → (var x Tᵢ) ∈ Γ₁
136+ -------------------------------
137+ → Γ ⊢B (input (oneway o x)) ▹ Γ₁
138+
139+ t-oneway-exists : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
140+ → (inOneWay o Tᵢ) ∈ Γ
141+ → ((var x Tₓ) ∈ Γ)
142+ → Tᵢ ⊆ Tₓ
143+ → n ≡ m -- TODO Γ ≡ Γ₁
144+ --------------------------------
145+ → Γ ⊢B (input (oneway o x)) ▹ Γ₁
146+
147+ t-solresp-new : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
148+ → (outSolRes o l Tₒ Tᵢ) ∈ Γ
149+ → Tₑ ⊆ Tₒ
150+ → ¬ (var x Tₓ ∈ Γ)
151+ → (var x Tᵢ) ∈ Γ₁
152+ -----------------------------------------
153+ → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
154+
155+ t-solresp-exists : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
156+ → (outSolRes o l Tₒ Tᵢ) ∈ Γ
157+ → Tₑ ⊆ Tₒ
158+ → (var x Tₓ) ∈ Γ
159+ → Tᵢ ⊆ Tₓ
160+ → n ≡ m -- TODO Γ ≡ Γ₁
161+ -----------------------------------------
162+ → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
163+
164+ t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
165+ → (inReqRes o Tᵢ Tₒ) ∈ Γ
166+ → ¬ (var x Tₓ ∈ Γ)
167+ → (var x Tₓ) ∈ Γₓ
168+ → Γₓ ⊢B b ▹ Γ₁
169+ → (var a Tₐ) ∈ Γ₁
170+ → Tₐ ⊆ Tₒ
171+ -----------------------------------
172+ → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
173+
174+ t-reqresp-exists : {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
175+ → (inReqRes o Tᵢ Tₒ) ∈ Γ
176+ → (var x Tₓ) ∈ Γ
177+ → Tᵢ ⊆ Tₓ
178+ → Γ ⊢B b ▹ Γ₁
179+ → (var a Tₐ) ∈ Γ₁
180+ → Tₐ ⊆ Tₒ
181+ ------------------------------------
182+ → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
183+
184+
185+check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (B : Behaviour) → Dec (Γ ⊢B B ▹ Γ₁)
186+check-B = {!!}
+4,
-7
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,8 +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+ void : Value