- commit
- 485cdaf
- parent
- 30b45bc
- author
- Eugene Akentyev
- date
- 2016-11-02 18:09:53 +0400 +04
First steps with Equality
3 files changed,
+135,
-21
+1,
-5
1@@ -6,11 +6,7 @@ open import Variable
2
3 -- TODO: add logic operations and, or
4 data BinOp : Set where
5- plus : BinOp
6- minus : BinOp
7- mult : BinOp
8- div : BinOp
9- power : BinOp
10+ plus minus mult div power : BinOp
11
12 data Expr : Set where
13 var : Variable → Expr
+126,
-12
1@@ -1,7 +1,12 @@
2 module Type where
3
4+open import Relation.Nullary
5+open import Relation.Binary
6+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)
7+open import Data.Nat using (ℕ)
8 open import Data.String using (String)
9 open import Data.List using (List)
10+open import Data.Vec using (Vec)
11 open import Expr
12 open import Variable
13
14@@ -16,18 +21,62 @@ Channel : Set
15 Channel = String
16
17 data Cardinality : Set where
18- oo : Cardinality
19- oi : Cardinality
20- ii : Cardinality
21+ oo oi ii : Cardinality
22
23 data BasicType : Set where
24- bool : BasicType
25- int : BasicType
26- double : BasicType
27- long : BasicType
28- string : BasicType
29- raw : BasicType
30- void : BasicType
31+ bool int double long string raw void : BasicType
32+
33+module BasicTypeEq where
34+ _≟_ : Decidable {A = BasicType} _≡_
35+ bool ≟ bool = yes refl
36+ int ≟ int = yes refl
37+ double ≟ double = yes refl
38+ long ≟ long = yes refl
39+ string ≟ string = yes refl
40+ raw ≟ raw = yes refl
41+ void ≟ void = yes refl
42+ bool ≟ int = no λ()
43+ bool ≟ double = no λ()
44+ bool ≟ long = no λ()
45+ bool ≟ string = no λ()
46+ bool ≟ raw = no λ()
47+ bool ≟ void = no λ()
48+ int ≟ bool = no λ()
49+ int ≟ double = no λ()
50+ int ≟ long = no λ()
51+ int ≟ string = no λ()
52+ int ≟ raw = no λ()
53+ int ≟ void = no λ()
54+ double ≟ bool = no λ()
55+ double ≟ int = no λ()
56+ double ≟ long = no λ()
57+ double ≟ string = no λ()
58+ double ≟ raw = no λ()
59+ double ≟ void = no λ()
60+ long ≟ bool = no λ()
61+ long ≟ int = no λ()
62+ long ≟ double = no λ()
63+ long ≟ string = no λ()
64+ long ≟ raw = no λ()
65+ long ≟ void = no λ()
66+ string ≟ bool = no λ()
67+ string ≟ int = no λ()
68+ string ≟ double = no λ()
69+ string ≟ long = no λ()
70+ string ≟ raw = no λ()
71+ string ≟ void = no λ()
72+ raw ≟ bool = no λ()
73+ raw ≟ int = no λ()
74+ raw ≟ double = no λ()
75+ raw ≟ long = no λ()
76+ raw ≟ string = no λ()
77+ raw ≟ void = no λ()
78+ void ≟ bool = no λ()
79+ void ≟ int = no λ()
80+ void ≟ double = no λ()
81+ void ≟ long = no λ()
82+ void ≟ string = no λ()
83+ void ≟ raw = no λ()
84
85 data TypeTree : Set
86
87@@ -38,6 +87,15 @@ data TypeTree where
88 leaf : BasicType → TypeTree
89 node : BasicType → List ChildType → TypeTree
90
91+module TypeTreeEq where
92+ _≟_ : Decidable {A = TypeTree} _≡_
93+ (leaf b1) ≟ (leaf b2) with BasicTypeEq._≟_ b1 b2
94+ ... | yes b1≡b2 = {!!}
95+ ... | no ¬b1≡b2 = no {!!}
96+ (node b1 cts) ≟ (node b2 cts') = {!!}
97+ (leaf _) ≟ (node _ _) = no λ ()
98+ (node _ _) ≟ (leaf _) = no λ ()
99+
100 data TypeDecl : Set where
101 outNotify : Operation → Location → TypeTree → TypeDecl
102 outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl
103@@ -47,5 +105,61 @@ data TypeDecl : Set where
104 empty : TypeDecl
105 pair : TypeDecl → TypeDecl → TypeDecl
106
107-Ctx : Set
108-Ctx = List TypeDecl
109+module TypeDeclEq where
110+ _≟_ : Decidable {A = TypeDecl} _≡_
111+ (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) = {!!}
112+ (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') = {!!}
113+ (inOneWay o1 t1) ≟ (inOneWay o2 t2) = {!!}
114+ (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') = {!!}
115+ (var v1 t1) ≟ (var v2 t2) = {!!}
116+ (pair t1 t1') ≟ (pair t2 t2') = {!!}
117+ empty ≟ empty = yes refl
118+ empty ≟ (outNotify _ _ _) = no λ()
119+ empty ≟ (outSolRes _ _ _ _) = no λ()
120+ empty ≟ (inOneWay _ _) = no λ()
121+ empty ≟ (inReqRes _ _ _) = no λ()
122+ empty ≟ (var _ _) = no λ()
123+ empty ≟ (pair _ _) = no λ()
124+ (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
125+ (outNotify _ _ _) ≟ (inOneWay _ _) = no λ()
126+ (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ()
127+ (outNotify _ _ _) ≟ (var _ _) = no λ()
128+ (outNotify _ _ _) ≟ empty = no λ()
129+ (outNotify _ _ _) ≟ (pair _ _) = no λ()
130+ (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ()
131+ (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ()
132+ (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ()
133+ (outSolRes _ _ _ _) ≟ (var _ _) = no λ()
134+ (outSolRes _ _ _ _) ≟ empty = no λ()
135+ (outSolRes _ _ _ _) ≟ (pair _ _) = no λ()
136+ (inOneWay _ _) ≟ (outNotify _ _ _) = no λ()
137+ (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ()
138+ (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ()
139+ (inOneWay _ _) ≟ (var _ _) = no λ()
140+ (inOneWay _ _) ≟ empty = no λ()
141+ (inOneWay _ _) ≟ (pair _ _) = no λ()
142+ (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ()
143+ (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
144+ (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ()
145+ (inReqRes _ _ _) ≟ (var _ _) = no λ()
146+ (inReqRes _ _ _) ≟ empty = no λ()
147+ (inReqRes _ _ _) ≟ (pair _ _) = no λ()
148+ (var _ _) ≟ (outNotify _ _ _) = no λ()
149+ (var _ _) ≟ (outSolRes _ _ _ _) = no λ()
150+ (var _ _) ≟ (inOneWay _ _) = no λ()
151+ (var _ _) ≟ (inReqRes _ _ _) = no λ()
152+ (var _ _) ≟ empty = no λ()
153+ (var _ _) ≟ (pair _ _) = no λ()
154+ (pair _ _) ≟ (outNotify _ _ _) = no λ()
155+ (pair _ _) ≟ (outSolRes _ _ _ _) = no λ()
156+ (pair _ _) ≟ (inOneWay _ _) = no λ()
157+ (pair _ _) ≟ (inReqRes _ _ _) = no λ()
158+ (pair _ _) ≟ (var _ _) = no λ()
159+ (pair _ _) ≟ empty = no λ()
160+
161+ decSetoid : DecSetoid _ _
162+ decSetoid = PropEq.decSetoid _≟_
163+
164+
165+Ctx : ℕ → Set
166+Ctx = Vec TypeDecl
+8,
-4
1@@ -1,7 +1,10 @@
2 module Typecheck where
3
4-import Relation.Binary.PropositionalEquality as PropEq
5+import Data.Vec.Equality as VecEq
6+open import Relation.Binary.PropositionalEquality as PropEq using (decSetoid)
7+open import Relation.Nullary.Decidable using (⌊_⌋)
8 open import Data.Maybe using (Maybe; just; nothing)
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@@ -22,11 +25,11 @@ type_of_var : Variable → Maybe BasicType
14 type_of_var (leaf _ v) = just $ type_of_value v
15 type_of_var _ = nothing
16
17-data Check (Γ : Ctx) : Behaviour → Set where
18+data Check {n} (Γ : Ctx n) : Behaviour → Set where
19 yes : {b : Behaviour} → Check Γ b
20 no : {b : Behaviour} → Check Γ b
21
22-typecheck_behaviour : (Γ : Ctx) → (b : Behaviour) → Check Γ b
23+typecheck_behaviour : {n : ℕ} (Γ : Ctx n) → (b : Behaviour) → Check Γ b
24 typecheck_behaviour ctx nil = yes
25 typecheck_behaviour ctx (if e b1 b2) =
26 case e of λ
27@@ -38,7 +41,8 @@ typecheck_behaviour ctx (if e b1 b2) =
28 -- If e : bool
29 { (just bool) →
30 let ctx2 = typecheck_behaviour ctx b2 in
31- {!!}
32+ let module CtxEq = VecEq.DecidableEquality Data.Bool.decSetoid in
33+ if ⌊ ctx1 CtxEq.≟ ctx2 ⌋ then yes else no
34 ; _ → no
35 }
36 --case ()