init

diff --git a/.gitignore b/.gitignore
index 171a38976c10152af35e1ad8cf931f3488b894ed..dfe49af29164ac756efd16ea104583c7b32aa7fe 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 *.agdai
+*~

diff --git a/src/Behaviour.agda b/src/Behaviour.agda
new file mode 100644 (file)
index 0000000..5f2a893
--- /dev/null
+++ b/src/Behaviour.agda
@@ -0,0 +1,34 @@
+module Behaviour where
+
+open import Data.Maybe using (Maybe)
+open import Data.String using (String)
+open import Data.List using (List)
+open import Data.Product using (_×_)
+open import Variable
+open import Expr
+open import Type
+
+
+data Output_ex : Set where
+  notification : Operation → Location → Expr → Output_ex
+  solicitRes : Operation → Location → Expr → Variable → Output_ex
+
+data Behaviour : Set
+
+data Input_ex : Set where
+  oneway : Operation → Variable → Input_ex
+  reqRes : Operation → Variable → Variable → Behaviour → Input_ex
+
+data Behaviour where
+  input : Input_ex → Behaviour
+  output : Output_ex → Behaviour
+  if : Expr → Behaviour → Maybe Behaviour → Behaviour
+  while : Expr → Behaviour → Behaviour
+  seq : Behaviour → Behaviour → Behaviour
+  par : Behaviour → Behaviour → Behaviour
+  assign : Variable → Expr → Behaviour
+  nil : Behaviour
+  inputchoice : List (Input_ex × Behaviour) → Behaviour
+  wait : Channel → Operation → Location → Variable → Behaviour
+  exec : Channel → Operation → Variable → Behaviour → Behaviour
+

diff --git a/src/Expr.agda b/src/Expr.agda
new file mode 100644 (file)
index 0000000..ed60c25
--- /dev/null
+++ b/src/Expr.agda
@@ -0,0 +1,16 @@
+module Expr where
+
+open import Variable
+
+
+data BinOp : Set where
+  plus : BinOp
+  minus : BinOp
+  mult : BinOp
+  div : BinOp
+  power : BinOp
+
+data Expr : Set where
+  var : Variable → Expr
+  binary : BinOp → Variable → Variable → Expr
+  constant : Variable.Value → Expr

diff --git a/src/Type.agda b/src/Type.agda
new file mode 100644 (file)
index 0000000..a2ac4d4
--- /dev/null
+++ b/src/Type.agda
@@ -0,0 +1,52 @@
+module Type where
+
+open import Data.String using (String)
+open import Data.List using (List)
+open import Expr
+open import Variable
+
+
+Operation : Set
+Operation = String
+
+Location : Set
+Location = String
+
+Channel : Set
+Channel = String
+
+data Cardinality : Set where
+  oo : Cardinality
+  oi : Cardinality
+  ii : Cardinality
+
+data BasicType : Set where
+  bool : BasicType
+  int : BasicType
+  double : BasicType
+  long : BasicType
+  string : BasicType
+  raw : BasicType
+  void : BasicType
+
+data TypeTree : Set
+
+data ChildType : Set where
+  child : String → Cardinality → TypeTree → ChildType
+
+data TypeTree where
+  leaf : BasicType → TypeTree
+  node : BasicType → List ChildType → TypeTree
+
+data TypeDecl : Set where
+  outNotify : Operation → Location → TypeTree → TypeDecl
+  outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl
+  inOneWay : Operation → TypeTree → TypeDecl
+  inReqRes : Operation → TypeTree → TypeTree → TypeDecl
+  var : Variable → TypeTree → TypeDecl
+  empty : TypeDecl
+  pair : TypeDecl → TypeDecl → TypeDecl
+
+Γ : Set
+Γ = List TypeDecl
+

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
new file mode 100644 (file)
index 0000000..e776604
--- /dev/null
+++ b/src/Typecheck.agda
@@ -0,0 +1,22 @@
+module Typecheck where
+
+open import Data.Maybe using (Maybe; just; nothing)
+open import Function
+open import Expr
+open import Type
+open import Behaviour
+open import Variable
+
+
+typecheck_behaviour : Γ → Behaviour → Maybe Γ
+typecheck_behaviour env nil = just env
+typecheck_behaviour env (if e b1 maybe_b2) =
+  case e of λ
+  {
+    -- If conditional expression is variable
+    (var v) →
+      let ctx1 = typecheck_behaviour env b1 in
+      {!!}
+  ; _ → nothing
+  }
+typecheck_behaviour _ _ = nothing

diff --git a/src/Variable.agda b/src/Variable.agda
new file mode 100644 (file)
index 0000000..2f92269
--- /dev/null
+++ b/src/Variable.agda
@@ -0,0 +1,24 @@
+module Variable where
+
+open import Data.Integer using (ℤ)
+open import Data.String using (String)
+open import Data.Product using (_×_)
+open import Data.Maybe using (Maybe)
+open import Data.List using (List)
+open import Data.Bool using (Bool)
+
+
+Name : Set
+Name = String
+
+data Value : Set where
+  string : String → Value
+  int : ℤ → Value
+  bool : Bool → Value
+  double : ℤ × ℤ → Value
+  long : ℤ → Value
+
+data Variable : Set where
+  leaf : Name → Value → Variable
+  node : Name → Maybe Value → List Variable → Variable
+