From: Eugene Akentyev Date: Fri, 21 Oct 2016 20:02:59 +0000 (+0300) Subject: init X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=21e6ab0251d622a2a0ad03c5eb1fd76b48ea8a2e;p=jolie.agda.git init --- diff --git a/.gitignore b/.gitignore index 171a389..dfe49af 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ *.agdai +*~ diff --git a/src/Behaviour.agda b/src/Behaviour.agda new file mode 100644 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 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 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 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 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 +