repos / jolie.agda.git

commit

9fbadb5

parent

f6b8752

author

Eugene Akentyev

date

2016-12-08 23:53:08 +0400 +04

Add context equality

  1@@ -1,14 +1,15 @@
  2 module Type where
  3 
  4+import Data.Vec.Equality as VecEq
  5 open import Level
  6 open import Relation.Nullary
  7 open import Relation.Binary
  8 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
  9 open import Relation.Nullary.Decidable using (⌊_⌋)
 10 open import Function
 11-open import Data.Nat using (ℕ)
 12+open import Data.Nat using (ℕ) renaming (_≟_ to _≟-Nat_)
 13 open import Data.Empty
 14-open import Data.String using (String)
 15+open import Data.String using (String) renaming (_≟_ to _≟-String_)
 16 open import Data.List using (List; filter)
 17 open import Data.Vec using (Vec; toList)
 18 open import Expr
 19@@ -27,6 +28,58 @@ Channel = String
 20 data Type : Set where
 21   bool int double long string raw void : Type
 22 
 23+module TypeEq where
 24+  _≟_ : Decidable {A = Type} _≡_
 25+  bool ≟ bool = yes refl
 26+  int ≟ int = yes refl
 27+  double ≟ double = yes refl
 28+  long ≟ long = yes refl
 29+  string ≟ string = yes refl
 30+  raw ≟ raw = yes refl
 31+  void ≟ void = yes refl
 32+  bool ≟ int = no λ()
 33+  bool ≟ double = no λ()
 34+  bool ≟ long = no λ()
 35+  bool ≟ string = no λ()
 36+  bool ≟ raw = no λ()
 37+  bool ≟ void = no λ()
 38+  int ≟ bool = no λ()
 39+  int ≟ double = no λ()
 40+  int ≟ long = no λ()
 41+  int ≟ string = no λ()
 42+  int ≟ raw = no λ()
 43+  int ≟ void = no λ()
 44+  double ≟ bool = no λ()
 45+  double ≟ int = no λ()
 46+  double ≟ long = no λ()
 47+  double ≟ string = no λ()
 48+  double ≟ raw = no λ()
 49+  double ≟ void = no λ()
 50+  long ≟ bool = no λ()
 51+  long ≟ int = no λ()
 52+  long ≟ double = no λ()
 53+  long ≟ string = no λ()
 54+  long ≟ raw = no λ()
 55+  long ≟ void = no λ()
 56+  string ≟ bool = no λ()
 57+  string ≟ int = no λ()
 58+  string ≟ double = no λ()
 59+  string ≟ long = no λ()
 60+  string ≟ raw = no λ()
 61+  string ≟ void = no λ()
 62+  raw ≟ bool = no λ()
 63+  raw ≟ int = no λ()
 64+  raw ≟ double = no λ()
 65+  raw ≟ long = no λ()
 66+  raw ≟ string = no λ()
 67+  raw ≟ void = no λ()
 68+  void ≟ bool = no λ()
 69+  void ≟ int = no λ()
 70+  void ≟ double = no λ()
 71+  void ≟ long = no λ()
 72+  void ≟ string = no λ()
 73+  void ≟ raw = no λ()
 74+
 75 data TypeDecl : Set where
 76   outNotify : Operation → Location → Type → TypeDecl
 77   outSolRes : Operation → Location → Type → Type → TypeDecl
 78@@ -36,8 +89,95 @@ data TypeDecl : Set where
 79   empty : TypeDecl
 80   pair : TypeDecl → TypeDecl → TypeDecl
 81 
 82+cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
 83+        (f : A → B → C → D) {x y u v m n} → x ≡ y → u ≡ v → m ≡ n → f x u m ≡ f y v n
 84+cong₃ f refl refl refl = refl
 85+
 86+cong₄ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e}
 87+        (f : A → B → C → D → E) {x y u v m n k l} → x ≡ y → u ≡ v → m ≡ n → k ≡ l → f x u m k ≡ f y v n l
 88+cong₄ f refl refl refl refl = refl
 89+
 90+module TypeDeclEq where
 91+  _≟_ : Decidable {A = TypeDecl} _≡_
 92+  (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) with o1 ≟-String o2 | l1 ≟-String l2 | t1 TypeEq.≟ t2
 93+  ... | yes o | yes l | yes t = yes (cong₃ outNotify o l t)
 94+  ... | no ¬p | _ | _ = no (λ { refl → ¬p refl})
 95+  ... | _ | no ¬p | _ = no (λ { refl → ¬p refl})
 96+  ... | _ | _ | no ¬p = no (λ { refl → ¬p refl})
 97+  (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') with o1 ≟-String o2 | l1 ≟-String l2 | t1 TypeEq.≟ t2 | t1' TypeEq.≟ t2'
 98+  ... | yes o | yes l | yes t | yes t' = yes (cong₄ outSolRes o l t t')
 99+  ... | no ¬p | _ | _ | _ = no (λ { refl → ¬p refl})
100+  ... | _ | no ¬p | _ | _ = no (λ { refl → ¬p refl})
101+  ... | _ | _ | no ¬p | _ = no (λ { refl → ¬p refl})
102+  ... | _ | _ | _ | no ¬p = no (λ { refl → ¬p refl})
103+  (inOneWay o1 t1) ≟ (inOneWay o2 t2) with o1 ≟-String o2 | t1 TypeEq.≟ t2
104+  ... | yes o | yes t = yes (cong₂ inOneWay o t)
105+  ... | no ¬p | _ = no (λ { refl → ¬p refl})
106+  ... | _ | no ¬p = no (λ { refl → ¬p refl})
107+  (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') with o1 ≟-String o2 | t1 TypeEq.≟ t2 | t1' TypeEq.≟ t2'
108+  ... | yes o | yes l | yes t = yes (cong₃ inReqRes o l t)
109+  ... | no ¬p | _ | _ = no (λ { refl → ¬p refl})
110+  ... | _ | no ¬p | _ = no (λ { refl → ¬p refl})
111+  ... | _ | _ | no ¬p = no (λ { refl → ¬p refl})
112+  (var v1 t1) ≟ (var v2 t2) with v1 ≟-Nat v2 | t1 TypeEq.≟ t2
113+  ... | yes v | yes t = yes (cong₂ var v t)
114+  ... | no ¬p | _ = no (λ { refl → ¬p refl})
115+  ... | _ | no ¬p = no (λ { refl → ¬p refl})
116+  (pair t1 t1') ≟ (pair t2 t2') with t1 ≟ t2 | t1' ≟ t2'
117+  ... | yes t | yes t' = yes (cong₂ pair t t')
118+  ... | no ¬p | _ = no (λ { refl → ¬p refl})
119+  ... | _ | no ¬p = no (λ { refl → ¬p refl})
120+  empty ≟ empty = yes refl
121+  empty ≟ (outNotify _ _ _) = no λ()
122+  empty ≟ (outSolRes _ _ _ _) = no λ()
123+  empty ≟ (inOneWay _ _) = no λ()
124+  empty ≟ (inReqRes _ _ _) = no λ()
125+  empty ≟ (var _ _) = no λ()
126+  empty ≟ (pair _ _) = no λ()
127+  (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
128+  (outNotify _ _ _) ≟ (inOneWay _ _) = no λ()
129+  (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ()
130+  (outNotify _ _ _) ≟ (var _ _) = no λ()
131+  (outNotify _ _ _) ≟ empty = no λ()
132+  (outNotify _ _ _) ≟ (pair _ _) = no λ()
133+  (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ()
134+  (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ()
135+  (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ()
136+  (outSolRes _ _ _ _) ≟ (var _ _) = no λ()
137+  (outSolRes _ _ _ _) ≟ empty = no λ()
138+  (outSolRes _ _ _ _) ≟ (pair _ _) = no λ()
139+  (inOneWay _ _) ≟ (outNotify _ _ _) = no λ()
140+  (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ()
141+  (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ()
142+  (inOneWay _ _) ≟ (var _ _) = no λ()
143+  (inOneWay _ _) ≟ empty = no λ()
144+  (inOneWay _ _) ≟ (pair _ _) = no λ()
145+  (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ()
146+  (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
147+  (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ()
148+  (inReqRes _ _ _) ≟ (var _ _) = no λ()
149+  (inReqRes _ _ _) ≟ empty = no λ()
150+  (inReqRes _ _ _) ≟ (pair _ _) = no λ()
151+  (var _ _) ≟ (outNotify _ _ _) = no λ()
152+  (var _ _) ≟ (outSolRes _ _ _ _) = no λ()
153+  (var _ _) ≟ (inOneWay _ _) = no λ()
154+  (var _ _) ≟ (inReqRes _ _ _) = no λ()
155+  (var _ _) ≟ empty = no λ()
156+  (var _ _) ≟ (pair _ _) = no λ()
157+  (pair _ _) ≟ (outNotify _ _ _) = no λ()
158+  (pair _ _) ≟ (outSolRes _ _ _ _) = no λ()
159+  (pair _ _) ≟ (inOneWay _ _) = no λ()
160+  (pair _ _) ≟ (inReqRes _ _ _) = no λ()
161+  (pair _ _) ≟ (var _ _) = no λ()
162+  (pair _ _) ≟ empty = no λ()
163+  
164+  decSetoid : DecSetoid _ _
165+  decSetoid = PropEq.decSetoid _≟_
166+
167 data _⊆_ : Type → Type → Set where
168   sub : {T₁ T₂ : Type} → T₁ ⊆ T₂
169 
170 Ctx : ℕ → Set
171 Ctx = Vec TypeDecl
172+
173+module CtxEq = VecEq.DecidableEquality TypeDeclEq.decSetoid