First steps with Equality

diff --git a/src/Expr.agda b/src/Expr.agda
index b6360f32703d35136d83d507a92731b6ef4b354d..ff1f59fbdc406dda27c00d36471f51e8c35005ab 100644 (file)
--- a/src/Expr.agda
+++ b/src/Expr.agda
@@ -6,11 +6,7 @@ open import Variable
 
 -- TODO: add logic operations and, or
 data BinOp : Set where
-  plus : BinOp
-  minus : BinOp
-  mult : BinOp
-  div : BinOp
-  power : BinOp
+  plus minus mult div power : BinOp
 
 data Expr : Set where
   var : Variable → Expr

diff --git a/src/Type.agda b/src/Type.agda
index 2d8cf33659cb8d79e83b93d0f6227883d73adf55..48a00af0279f6ee14861b522454371e4bae80234 100644 (file)
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -1,7 +1,12 @@
 module Type where
 
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)
+open import Data.Nat using (ℕ)
 open import Data.String using (String)
 open import Data.List using (List)
+open import Data.Vec using (Vec)
 open import Expr
 open import Variable
 
@@ -16,18 +21,62 @@ Channel : Set
 Channel = String
 
 data Cardinality : Set where
-  oo : Cardinality
-  oi : Cardinality
-  ii : Cardinality
+  oo oi ii : Cardinality
 
 data BasicType : Set where
-  bool : BasicType
-  int : BasicType
-  double : BasicType
-  long : BasicType
-  string : BasicType
-  raw : BasicType
-  void : BasicType
+  bool int double long string raw void : BasicType
+
+module BasicTypeEq where
+  _≟_ : Decidable {A = BasicType} _≡_
+  bool ≟ bool = yes refl
+  int ≟ int = yes refl
+  double ≟ double = yes refl
+  long ≟ long = yes refl
+  string ≟ string = yes refl
+  raw ≟ raw = yes refl
+  void ≟ void = yes refl
+  bool ≟ int = no λ()
+  bool ≟ double = no λ()
+  bool ≟ long = no λ()
+  bool ≟ string = no λ()
+  bool ≟ raw = no λ()
+  bool ≟ void = no λ()
+  int ≟ bool = no λ()
+  int ≟ double = no λ()
+  int ≟ long = no λ()
+  int ≟ string = no λ()
+  int ≟ raw = no λ()
+  int ≟ void = no λ()
+  double ≟ bool = no λ()
+  double ≟ int = no λ()
+  double ≟ long = no λ()
+  double ≟ string = no λ()
+  double ≟ raw = no λ()
+  double ≟ void = no λ()
+  long ≟ bool = no λ()
+  long ≟ int = no λ()
+  long ≟ double = no λ()
+  long ≟ string = no λ()
+  long ≟ raw = no λ()
+  long ≟ void = no λ()
+  string ≟ bool = no λ()
+  string ≟ int = no λ()
+  string ≟ double = no λ()
+  string ≟ long = no λ()
+  string ≟ raw = no λ()
+  string ≟ void = no λ()
+  raw ≟ bool = no λ()
+  raw ≟ int = no λ()
+  raw ≟ double = no λ()
+  raw ≟ long = no λ()
+  raw ≟ string = no λ()
+  raw ≟ void = no λ()
+  void ≟ bool = no λ()
+  void ≟ int = no λ()
+  void ≟ double = no λ()
+  void ≟ long = no λ()
+  void ≟ string = no λ()
+  void ≟ raw = no λ()
 
 data TypeTree : Set
 
@@ -38,6 +87,15 @@ data TypeTree where
   leaf : BasicType → TypeTree
   node : BasicType → List ChildType → TypeTree
 
+module TypeTreeEq where
+  _≟_ : Decidable {A = TypeTree} _≡_
+  (leaf b1) ≟ (leaf b2) with BasicTypeEq._≟_ b1 b2
+  ... | yes b1≡b2 = {!!}
+  ... | no ¬b1≡b2 = no {!!}
+  (node b1 cts) ≟ (node b2 cts') = {!!}
+  (leaf _) ≟ (node _ _) = no λ ()
+  (node _ _) ≟ (leaf _) = no λ ()
+
 data TypeDecl : Set where
   outNotify : Operation → Location → TypeTree → TypeDecl
   outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl
@@ -47,5 +105,61 @@ data TypeDecl : Set where
   empty : TypeDecl
   pair : TypeDecl → TypeDecl → TypeDecl
 
-Ctx : Set
-Ctx = List TypeDecl
+module TypeDeclEq where
+  _≟_ : Decidable {A = TypeDecl} _≡_
+  (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) = {!!}
+  (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') = {!!}
+  (inOneWay o1 t1) ≟ (inOneWay o2 t2) = {!!}
+  (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') = {!!}
+  (var v1 t1) ≟ (var v2 t2) = {!!}
+  (pair t1 t1') ≟ (pair t2 t2') = {!!}
+  empty ≟ empty = yes refl
+  empty ≟ (outNotify _ _ _) = no λ()
+  empty ≟ (outSolRes _ _ _ _) = no λ()
+  empty ≟ (inOneWay _ _) = no λ()
+  empty ≟ (inReqRes _ _ _) = no λ()
+  empty ≟ (var _ _) = no λ()
+  empty ≟ (pair _ _) = no λ()
+  (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
+  (outNotify _ _ _) ≟ (inOneWay _ _) = no λ()
+  (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ()
+  (outNotify _ _ _) ≟ (var _ _) = no λ()
+  (outNotify _ _ _) ≟ empty = no λ()
+  (outNotify _ _ _) ≟ (pair _ _) = no λ()
+  (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ()
+  (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ()
+  (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ()
+  (outSolRes _ _ _ _) ≟ (var _ _) = no λ()
+  (outSolRes _ _ _ _) ≟ empty = no λ()
+  (outSolRes _ _ _ _) ≟ (pair _ _) = no λ()
+  (inOneWay _ _) ≟ (outNotify _ _ _) = no λ()
+  (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ()
+  (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ()
+  (inOneWay _ _) ≟ (var _ _) = no λ()
+  (inOneWay _ _) ≟ empty = no λ()
+  (inOneWay _ _) ≟ (pair _ _) = no λ()
+  (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ()
+  (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
+  (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ()
+  (inReqRes _ _ _) ≟ (var _ _) = no λ()
+  (inReqRes _ _ _) ≟ empty = no λ()
+  (inReqRes _ _ _) ≟ (pair _ _) = no λ()
+  (var _ _) ≟ (outNotify _ _ _) = no λ()
+  (var _ _) ≟ (outSolRes _ _ _ _) = no λ()
+  (var _ _) ≟ (inOneWay _ _) = no λ()
+  (var _ _) ≟ (inReqRes _ _ _) = no λ()
+  (var _ _) ≟ empty = no λ()
+  (var _ _) ≟ (pair _ _) = no λ()
+  (pair _ _) ≟ (outNotify _ _ _) = no λ()
+  (pair _ _) ≟ (outSolRes _ _ _ _) = no λ()
+  (pair _ _) ≟ (inOneWay _ _) = no λ()
+  (pair _ _) ≟ (inReqRes _ _ _) = no λ()
+  (pair _ _) ≟ (var _ _) = no λ()
+  (pair _ _) ≟ empty = no λ()
+
+  decSetoid : DecSetoid _ _
+  decSetoid = PropEq.decSetoid _≟_
+
+
+Ctx : ℕ → Set
+Ctx = Vec TypeDecl

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 26b280047071660ba4e671e3bf69900648ec67fb..e5f7e3a7d6ba7f12faf44a9b9eaf4a1de29970f4 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,7 +1,10 @@
 module Typecheck where
 
-import Relation.Binary.PropositionalEquality as PropEq
+import Data.Vec.Equality as VecEq
+open import Relation.Binary.PropositionalEquality as PropEq using (decSetoid)
+open import Relation.Nullary.Decidable using (⌊_⌋)
 open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Nat using (ℕ)
 open import Data.Bool using (if_then_else_)
 open import Data.Product using (_,_)
 open import Function
@@ -22,11 +25,11 @@ type_of_var : Variable → Maybe BasicType
 type_of_var (leaf _ v) = just $ type_of_value v
 type_of_var _ = nothing
 
-data Check (Γ : Ctx) : Behaviour → Set where
+data Check {n} (Γ : Ctx n) : Behaviour → Set where
   yes : {b : Behaviour} → Check Γ b
   no : {b : Behaviour} → Check Γ b
 
-typecheck_behaviour : (Γ : Ctx) → (b : Behaviour) → Check Γ b
+typecheck_behaviour : {n : ℕ} (Γ : Ctx n) → (b : Behaviour) → Check Γ b
 typecheck_behaviour ctx nil = yes
 typecheck_behaviour ctx (if e b1 b2) =
   case e of λ
@@ -38,7 +41,8 @@ typecheck_behaviour ctx (if e b1 b2) =
       -- If e : bool
       { (just bool) →
         let ctx2 = typecheck_behaviour ctx b2 in
-        {!!}
+        let module CtxEq = VecEq.DecidableEquality Data.Bool.decSetoid in
+        if ⌊ ctx1 CtxEq.≟ ctx2 ⌋ then yes else no
       ; _ → no
       }
       --case ()