From a27ccbfc07041113b88033604ad25478bed596ec Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Sat, 5 Nov 2016 17:18:36 +0300
Subject: [PATCH] Express typing rules in types

---
 src/Behaviour.agda |   5 +-
 src/Type.agda      | 120 +--------------------------------------------
 src/Typecheck.agda |  76 ++++++++++++++--------------
 3 files changed, 43 insertions(+), 158 deletions(-)

diff --git a/src/Behaviour.agda b/src/Behaviour.agda
index 09091ac..4748617 100644
--- a/src/Behaviour.agda
+++ b/src/Behaviour.agda
@@ -1,7 +1,8 @@
 module Behaviour where
 
+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 Data.Product using (_×_)
 open import Variable
 open import Expr
@@ -27,7 +28,7 @@ data Behaviour where
   par : Behaviour → Behaviour → Behaviour
   assign : Variable → Expr → Behaviour
   nil : Behaviour
-  inputchoice : List (Input_ex × Behaviour) → Behaviour
+  inputchoice : {n : ℕ} → Vec (Input_ex × Behaviour) n → Behaviour
   wait : Channel → Operation → Location → Variable → Behaviour
   exec : Channel → Operation → Variable → Behaviour → Behaviour
 
diff --git a/src/Type.agda b/src/Type.agda
index 0d0da46..20c4d8c 100644
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -1,9 +1,10 @@
 module Type where
 
+open import Level
 open import Relation.Nullary
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
-open import Function using (_∘_)
+open import Function
 open import Data.Nat using (ℕ)
 open import Data.Empty
 open import Data.String using (String)
@@ -28,58 +29,6 @@ data Cardinality : Set where
 data BasicType : Set where
   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
 
 data ChildType : Set where
@@ -93,15 +42,6 @@ get-basic : TypeTree → BasicType
 get-basic (leaf b) = b
 get-basic (node b _) = b
 
-module TypeTreeEq where
-  _≟_ : Decidable {A = TypeTree} _≡_
-  (leaf b1) ≟ (leaf b2) with BasicTypeEq._≟_ b1 b2
-  ... | yes b1≡b2 = yes (cong leaf b1≡b2)
-  ... | no b1≢b2 = no {!!} -- ¬ leaf b1 ≡ leaf b2
-  (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
@@ -111,61 +51,5 @@ data TypeDecl : Set where
   empty : TypeDecl
   pair : TypeDecl → TypeDecl → 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 e5f7e3a..9dbd535 100644
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,51 +1,51 @@
 module Typecheck where
 
 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 Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 open import Data.Nat using (ℕ)
-open import Data.Bool using (if_then_else_)
-open import Data.Product using (_,_)
-open import Function
+open import Data.Vec using (Vec; _∈_; zip)
 open import Expr
 open import Type
 open import Behaviour
 open import Variable
 
 
-type_of_value : Value → BasicType
-type_of_value (Value.string _) = Type.string
-type_of_value (Value.int _) = Type.int
-type_of_value (Value.bool _) = Type.bool
-type_of_value (Value.double _) = Type.double
-type_of_value (Value.long _) = Type.long
+data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → TypeTree → Set where
+  var-t : {s : Variable} {b : TypeTree} 
+        → Γ ⊢ s of b
 
-type_of_var : Variable → Maybe BasicType
-type_of_var (leaf _ v) = just $ type_of_value v
-type_of_var _ = nothing
+data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where 
+  t-nil : {Γ₁ : Ctx m}
+        → n ≡ m
+        -------------
+        → Γ ⊢ nil ▹ Γ₁
+          
+  t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
+       → Γ ⊢ e of (leaf bool) -- Γ ⊢ e : bool
+       → Γ ⊢ b1 ▹ Γ₁
+       → Γ ⊢ b2 ▹ Γ₁
+       -------------
+       → Γ ⊢ if (var e) b1 b2 ▹ Γ₁
+          
+  t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
+          → Γ ⊢ e of (leaf bool)
+          → Γ ⊢ b ▹ Γ₁
+          ----------------------
+          → Γ ⊢ while (var e) b ▹ Γ₁
+          
+  t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n} {b : Behaviour} {behaviours : Vec Behaviour n}
+           → η ∈ inputs
+           → b ∈ behaviours
+           → Γ ⊢ seq (input η) b ▹ Γ₁
+           --------------------------
+           → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁
 
-data Check {n} (Γ : Ctx n) : Behaviour → Set where
-  yes : {b : Behaviour} → Check Γ b
-  no : {b : Behaviour} → Check Γ b
+  --t-par
 
-typecheck_behaviour : {n : ℕ} (Γ : Ctx n) → (b : Behaviour) → Check Γ b
-typecheck_behaviour ctx nil = yes
-typecheck_behaviour ctx (if e b1 b2) =
-  case e of λ
-  {
-    -- If conditional expression is variable
-    (var v) →
-      let ctx1 = typecheck_behaviour ctx b1 in
-      case (type_of_var v) of λ
-      -- 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 ()
-  ; _ → no
-  }
-typecheck_behaviour _ _ = no
+  t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
+        → Γ ⊢ b1 ▹ Γ₁
+        → Γ₁ ⊢ b2 ▹ Γ₂
+        --------------
+        → Γ ⊢ seq b1 b2 ▹ Γ₂
+
+  
-- 
2.50.1