repos / jolie.agda.git

commit

21e6ab0

parent

77cd022

author

Eugene Akentyev

date

2016-10-22 00:02:59 +0400 +04

init

1@@ -1 +1,2 @@
2 *.agdai
3+*~

 1@@ -0,0 +1,34 @@
 2+module Behaviour where
 3+
 4+open import Data.Maybe using (Maybe)
 5+open import Data.String using (String)
 6+open import Data.List using (List)
 7+open import Data.Product using (_×_)
 8+open import Variable
 9+open import Expr
10+open import Type
11+
12+
13+data Output_ex : Set where
14+  notification : Operation → Location → Expr → Output_ex
15+  solicitRes : Operation → Location → Expr → Variable → Output_ex
16+
17+data Behaviour : Set
18+
19+data Input_ex : Set where
20+  oneway : Operation → Variable → Input_ex
21+  reqRes : Operation → Variable → Variable → Behaviour → Input_ex
22+
23+data Behaviour where
24+  input : Input_ex → Behaviour
25+  output : Output_ex → Behaviour
26+  if : Expr → Behaviour → Maybe Behaviour → Behaviour
27+  while : Expr → Behaviour → Behaviour
28+  seq : Behaviour → Behaviour → Behaviour
29+  par : Behaviour → Behaviour → Behaviour
30+  assign : Variable → Expr → Behaviour
31+  nil : Behaviour
32+  inputchoice : List (Input_ex × Behaviour) → Behaviour
33+  wait : Channel → Operation → Location → Variable → Behaviour
34+  exec : Channel → Operation → Variable → Behaviour → Behaviour
35+

 1@@ -0,0 +1,16 @@
 2+module Expr where
 3+
 4+open import Variable
 5+
 6+
 7+data BinOp : Set where
 8+  plus : BinOp
 9+  minus : BinOp
10+  mult : BinOp
11+  div : BinOp
12+  power : BinOp
13+
14+data Expr : Set where
15+  var : Variable → Expr
16+  binary : BinOp → Variable → Variable → Expr
17+  constant : Variable.Value → Expr

 1@@ -0,0 +1,52 @@
 2+module Type where
 3+
 4+open import Data.String using (String)
 5+open import Data.List using (List)
 6+open import Expr
 7+open import Variable
 8+
 9+
10+Operation : Set
11+Operation = String
12+
13+Location : Set
14+Location = String
15+
16+Channel : Set
17+Channel = String
18+
19+data Cardinality : Set where
20+  oo : Cardinality
21+  oi : Cardinality
22+  ii : Cardinality
23+
24+data BasicType : Set where
25+  bool : BasicType
26+  int : BasicType
27+  double : BasicType
28+  long : BasicType
29+  string : BasicType
30+  raw : BasicType
31+  void : BasicType
32+
33+data TypeTree : Set
34+
35+data ChildType : Set where
36+  child : String → Cardinality → TypeTree → ChildType
37+
38+data TypeTree where
39+  leaf : BasicType → TypeTree
40+  node : BasicType → List ChildType → TypeTree
41+
42+data TypeDecl : Set where
43+  outNotify : Operation → Location → TypeTree → TypeDecl
44+  outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl
45+  inOneWay : Operation → TypeTree → TypeDecl
46+  inReqRes : Operation → TypeTree → TypeTree → TypeDecl
47+  var : Variable → TypeTree → TypeDecl
48+  empty : TypeDecl
49+  pair : TypeDecl → TypeDecl → TypeDecl
50+
51+Γ : Set
52+Γ = List TypeDecl
53+

 1@@ -0,0 +1,22 @@
 2+module Typecheck where
 3+
 4+open import Data.Maybe using (Maybe; just; nothing)
 5+open import Function
 6+open import Expr
 7+open import Type
 8+open import Behaviour
 9+open import Variable
10+
11+
12+typecheck_behaviour : Γ → Behaviour → Maybe Γ
13+typecheck_behaviour env nil = just env
14+typecheck_behaviour env (if e b1 maybe_b2) =
15+  case e of λ
16+  {
17+    -- If conditional expression is variable
18+    (var v) →
19+      let ctx1 = typecheck_behaviour env b1 in
20+      {!!}
21+  ; _ → nothing
22+  }
23+typecheck_behaviour _ _ = nothing

 1@@ -0,0 +1,24 @@
 2+module Variable where
 3+
 4+open import Data.Integer using (ℤ)
 5+open import Data.String using (String)
 6+open import Data.Product using (_×_)
 7+open import Data.Maybe using (Maybe)
 8+open import Data.List using (List)
 9+open import Data.Bool using (Bool)
10+
11+
12+Name : Set
13+Name = String
14+
15+data Value : Set where
16+  string : String → Value
17+  int : ℤ → Value
18+  bool : Bool → Value
19+  double : ℤ × ℤ → Value
20+  long : ℤ → Value
21+
22+data Variable : Set where
23+  leaf : Name → Value → Variable
24+  node : Name → Maybe Value → List Variable → Variable
25+