Eugene Akentyev
·
2017-02-22
Type.agda
1module Type where
2
3open import Data.Nat using (ℕ)
4open import Data.String using (String)
5open import Data.Vec using (Vec; _∷_)
6open import Variable
7
8
9data Operation : Set where
10data Location : Set where
11data Channel : Set where
12
13data Type : Set where
14 bool int double long string raw void : Type
15
16data TypeDecl : Set where
17 outNotify : Operation → Location → Type → TypeDecl
18 outSolRes : Operation → Location → Type → Type → TypeDecl
19 inOneWay : Operation → Type → TypeDecl
20 inReqRes : Operation → Type → Type → TypeDecl
21 var : Variable → Type → TypeDecl
22
23data _⊆_ : Type → Type → Set where
24 sub : {T₁ T₂ : Type} → T₁ ⊆ T₂
25
26Ctx : ℕ → Set
27Ctx = Vec TypeDecl
28
29data Context : Set where
30 ⋆ : ∀ {n} → Ctx n → Context
31 & : Context → Context → Context
32-- sideEffect : {Γ Γ′ : Context}
33
34infix 4 _∈_
35
36data _∈_ : TypeDecl → Context → Set where
37 here-⋆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ⋆ (x ∷ xs)
38 there-⋆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ⋆ xs) → x ∈ ⋆ (y ∷ xs)
39 here-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
40 here-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
41 there-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
42 there-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
43
44appendContext : TypeDecl → Context → Context
45appendContext t (⋆ Γ) = ⋆ (t ∷ Γ)
46appendContext t (& Γ₁ Γ₂) = & (appendContext t Γ₁) Γ₂