- commit
- a27ccbf
- parent
- 417008d
- author
- Eugene Akentyev
- date
- 2016-11-05 18:18:36 +0400 +04
Express typing rules in types
3 files changed,
+43,
-158
+3,
-2
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@@ -27,7 +28,7 @@ data Behaviour where
12 par : Behaviour → Behaviour → Behaviour
13 assign : Variable → Expr → Behaviour
14 nil : Behaviour
15- inputchoice : List (Input_ex × Behaviour) → Behaviour
16+ inputchoice : {n : ℕ} → Vec (Input_ex × Behaviour) n → Behaviour
17 wait : Channel → Operation → Location → Variable → Behaviour
18 exec : Channel → Operation → Variable → Behaviour → Behaviour
19
+2,
-118
1@@ -1,9 +1,10 @@
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 Function
10 open import Data.Nat using (ℕ)
11 open import Data.Empty
12 open import Data.String using (String)
13@@ -28,58 +29,6 @@ data Cardinality : Set where
14 data BasicType : Set where
15 bool int double long string raw void : BasicType
16
17-module BasicTypeEq where
18- _≟_ : Decidable {A = BasicType} _≡_
19- bool ≟ bool = yes refl
20- int ≟ int = yes refl
21- double ≟ double = yes refl
22- long ≟ long = yes refl
23- string ≟ string = yes refl
24- raw ≟ raw = yes refl
25- void ≟ void = yes refl
26- bool ≟ int = no λ()
27- bool ≟ double = no λ()
28- bool ≟ long = no λ()
29- bool ≟ string = no λ()
30- bool ≟ raw = no λ()
31- bool ≟ void = no λ()
32- int ≟ bool = no λ()
33- int ≟ double = no λ()
34- int ≟ long = no λ()
35- int ≟ string = no λ()
36- int ≟ raw = no λ()
37- int ≟ void = no λ()
38- double ≟ bool = no λ()
39- double ≟ int = no λ()
40- double ≟ long = no λ()
41- double ≟ string = no λ()
42- double ≟ raw = no λ()
43- double ≟ void = no λ()
44- long ≟ bool = no λ()
45- long ≟ int = no λ()
46- long ≟ double = no λ()
47- long ≟ string = no λ()
48- long ≟ raw = no λ()
49- long ≟ void = no λ()
50- string ≟ bool = no λ()
51- string ≟ int = no λ()
52- string ≟ double = no λ()
53- string ≟ long = no λ()
54- string ≟ raw = no λ()
55- string ≟ void = no λ()
56- raw ≟ bool = no λ()
57- raw ≟ int = no λ()
58- raw ≟ double = no λ()
59- raw ≟ long = no λ()
60- raw ≟ string = no λ()
61- raw ≟ void = no λ()
62- void ≟ bool = no λ()
63- void ≟ int = no λ()
64- void ≟ double = no λ()
65- void ≟ long = no λ()
66- void ≟ string = no λ()
67- void ≟ raw = no λ()
68-
69 data TypeTree : Set
70
71 data ChildType : Set where
72@@ -93,15 +42,6 @@ get-basic : TypeTree → BasicType
73 get-basic (leaf b) = b
74 get-basic (node b _) = b
75
76-module TypeTreeEq where
77- _≟_ : Decidable {A = TypeTree} _≡_
78- (leaf b1) ≟ (leaf b2) with BasicTypeEq._≟_ b1 b2
79- ... | yes b1≡b2 = yes (cong leaf b1≡b2)
80- ... | no b1≢b2 = no {!!} -- ¬ leaf b1 ≡ leaf b2
81- (node b1 cts) ≟ (node b2 cts') = {!!}
82- (leaf _) ≟ (node _ _) = no λ ()
83- (node _ _) ≟ (leaf _) = no λ ()
84-
85 data TypeDecl : Set where
86 outNotify : Operation → Location → TypeTree → TypeDecl
87 outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl
88@@ -111,61 +51,5 @@ data TypeDecl : Set where
89 empty : TypeDecl
90 pair : TypeDecl → TypeDecl → TypeDecl
91
92-module TypeDeclEq where
93- _≟_ : Decidable {A = TypeDecl} _≡_
94- (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) = {!!}
95- (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') = {!!}
96- (inOneWay o1 t1) ≟ (inOneWay o2 t2) = {!!}
97- (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') = {!!}
98- (var v1 t1) ≟ (var v2 t2) = {!!}
99- (pair t1 t1') ≟ (pair t2 t2') = {!!}
100- empty ≟ empty = yes refl
101- empty ≟ (outNotify _ _ _) = no λ()
102- empty ≟ (outSolRes _ _ _ _) = no λ()
103- empty ≟ (inOneWay _ _) = no λ()
104- empty ≟ (inReqRes _ _ _) = no λ()
105- empty ≟ (var _ _) = no λ()
106- empty ≟ (pair _ _) = no λ()
107- (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
108- (outNotify _ _ _) ≟ (inOneWay _ _) = no λ()
109- (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ()
110- (outNotify _ _ _) ≟ (var _ _) = no λ()
111- (outNotify _ _ _) ≟ empty = no λ()
112- (outNotify _ _ _) ≟ (pair _ _) = no λ()
113- (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ()
114- (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ()
115- (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ()
116- (outSolRes _ _ _ _) ≟ (var _ _) = no λ()
117- (outSolRes _ _ _ _) ≟ empty = no λ()
118- (outSolRes _ _ _ _) ≟ (pair _ _) = no λ()
119- (inOneWay _ _) ≟ (outNotify _ _ _) = no λ()
120- (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ()
121- (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ()
122- (inOneWay _ _) ≟ (var _ _) = no λ()
123- (inOneWay _ _) ≟ empty = no λ()
124- (inOneWay _ _) ≟ (pair _ _) = no λ()
125- (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ()
126- (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
127- (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ()
128- (inReqRes _ _ _) ≟ (var _ _) = no λ()
129- (inReqRes _ _ _) ≟ empty = no λ()
130- (inReqRes _ _ _) ≟ (pair _ _) = no λ()
131- (var _ _) ≟ (outNotify _ _ _) = no λ()
132- (var _ _) ≟ (outSolRes _ _ _ _) = no λ()
133- (var _ _) ≟ (inOneWay _ _) = no λ()
134- (var _ _) ≟ (inReqRes _ _ _) = no λ()
135- (var _ _) ≟ empty = no λ()
136- (var _ _) ≟ (pair _ _) = no λ()
137- (pair _ _) ≟ (outNotify _ _ _) = no λ()
138- (pair _ _) ≟ (outSolRes _ _ _ _) = no λ()
139- (pair _ _) ≟ (inOneWay _ _) = no λ()
140- (pair _ _) ≟ (inReqRes _ _ _) = no λ()
141- (pair _ _) ≟ (var _ _) = no λ()
142- (pair _ _) ≟ empty = no λ()
143-
144- decSetoid : DecSetoid _ _
145- decSetoid = PropEq.decSetoid _≟_
146-
147-
148 Ctx : ℕ → Set
149 Ctx = Vec TypeDecl
+38,
-38
1@@ -1,51 +1,51 @@
2 module Typecheck where
3
4 import Data.Vec.Equality as VecEq
5-open import Relation.Binary.PropositionalEquality as PropEq using (decSetoid)
6-open import Relation.Nullary.Decidable using (⌊_⌋)
7-open import Data.Maybe using (Maybe; just; nothing)
8+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
9 open import Data.Nat using (ℕ)
10-open import Data.Bool using (if_then_else_)
11-open import Data.Product using (_,_)
12-open import Function
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-type_of_value : Value → BasicType
21-type_of_value (Value.string _) = Type.string
22-type_of_value (Value.int _) = Type.int
23-type_of_value (Value.bool _) = Type.bool
24-type_of_value (Value.double _) = Type.double
25-type_of_value (Value.long _) = Type.long
26+data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → TypeTree → Set where
27+ var-t : {s : Variable} {b : TypeTree}
28+ → Γ ⊢ s of b
29
30-type_of_var : Variable → Maybe BasicType
31-type_of_var (leaf _ v) = just $ type_of_value v
32-type_of_var _ = nothing
33+data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where
34+ t-nil : {Γ₁ : Ctx m}
35+ → n ≡ m
36+ -------------
37+ → Γ ⊢ nil ▹ Γ₁
38+
39+ t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
40+ → Γ ⊢ e of (leaf bool) -- Γ ⊢ e : bool
41+ → Γ ⊢ b1 ▹ Γ₁
42+ → Γ ⊢ b2 ▹ Γ₁
43+ -------------
44+ → Γ ⊢ if (var e) b1 b2 ▹ Γ₁
45+
46+ t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
47+ → Γ ⊢ e of (leaf bool)
48+ → Γ ⊢ b ▹ Γ₁
49+ ----------------------
50+ → Γ ⊢ while (var e) b ▹ Γ₁
51+
52+ t-choice : {Γ₁ : Ctx m} {k n : ℕ} {η : Input_ex} {inputs : Vec Input_ex n} {b : Behaviour} {behaviours : Vec Behaviour n}
53+ → η ∈ inputs
54+ → b ∈ behaviours
55+ → Γ ⊢ seq (input η) b ▹ Γ₁
56+ --------------------------
57+ → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁
58
59-data Check {n} (Γ : Ctx n) : Behaviour → Set where
60- yes : {b : Behaviour} → Check Γ b
61- no : {b : Behaviour} → Check Γ b
62+ --t-par
63
64-typecheck_behaviour : {n : ℕ} (Γ : Ctx n) → (b : Behaviour) → Check Γ b
65-typecheck_behaviour ctx nil = yes
66-typecheck_behaviour ctx (if e b1 b2) =
67- case e of λ
68- {
69- -- If conditional expression is variable
70- (var v) →
71- let ctx1 = typecheck_behaviour ctx b1 in
72- case (type_of_var v) of λ
73- -- If e : bool
74- { (just bool) →
75- let ctx2 = typecheck_behaviour ctx b2 in
76- let module CtxEq = VecEq.DecidableEquality Data.Bool.decSetoid in
77- if ⌊ ctx1 CtxEq.≟ ctx2 ⌋ then yes else no
78- ; _ → no
79- }
80- --case ()
81- ; _ → no
82- }
83-typecheck_behaviour _ _ = no
84+ t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
85+ → Γ ⊢ b1 ▹ Γ₁
86+ → Γ₁ ⊢ b2 ▹ Γ₂
87+ --------------
88+ → Γ ⊢ seq b1 b2 ▹ Γ₂
89+
90+