repos / jolie.agda.git

commit

7b68f9a

parent

e5b592a

author

Eugene Akentyev

date

2016-12-28 23:08:19 +0400 +04

Add typing service.

1@@ -1,8 +0,0 @@
2-module Queue where
3-
4-open import Data.List using (List)
5-
6-
7-data Queue (A : Set) : Set where
8-  nil : Queue A
9-  cons : List A → List A → Queue A

 1@@ -6,9 +6,10 @@ open import Data.String using (String)
 2 open import Data.Product using (_×_)
 3 open import Type
 4 open import Behaviour
 5-open import Queue
 6 open import Variable
 7 
 8+Queue : (A : Set) → Set
 9+Queue A = List A
10 
11 Message : Set
12 Message = Channel × Operation × String
13@@ -19,12 +20,12 @@ MessageQueue = Queue Message
14 data Process : Set where
15   _∙_∙_ : Behaviour → List Variable → MessageQueue → Process
16   nil : Process
17-  _||_ : Process → Process → Process
18+  par : Process → Process → Process
19 
20 data AliasingFunction : Set where
21 
22-Deployment : {m : ℕ} → Set
23-Deployment {m} = AliasingFunction × Ctx m
24+Deployment : (m : ℕ) → Set
25+Deployment m = AliasingFunction × Ctx m
26 
27 data Service : Set where
28-  service : {m : ℕ} → Behaviour → Deployment {m} → Process → Service
29+  _▹_-_ : {m : ℕ} → Behaviour → Deployment m → Process → Service

 1@@ -155,22 +155,22 @@ struct-congruence t refl = t
 2 struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (seq nil b) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
 3 struct-cong-nil (t-seq t-nil t) = t
 4 
 5-struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
 6-struct-cong-par-nil (t-par t t-nil) = {!!}
 7+--struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
 8+--struct-cong-par-nil (t-par t t-nil) = {!!}
 9 
10-struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁
11-struct-cong-par-sym (t-par t₁ t₂) = {!!}
12+--struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁
13+--struct-cong-par-sym (t-par t₁ t₂) = {!!}
14 
15-struct-cong-par-assoc : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 b3 : Behaviour} → Γ ⊢B par (par b1 b2) b3 ▹ Γ₁ → Γ ⊢B par b1 (par b2 b3) ▹ Γ₁
16-struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!}
17+--struct-cong-par-assoc : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 b3 : Behaviour} → Γ ⊢B par (par b1 b2) b3 ▹ Γ₁ → Γ ⊢B par b1 (par b2 b3) ▹ Γ₁
18+--struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!}
19 
20 data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
21   updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
22   identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
23   undefined : SideEffect [] []
24 
25-preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁ 
26-preservation t undefined = t
27-preservation t (identity γ) = t
28+--preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁
29+--preservation t undefined = t
30+--preservation t (identity γ) = t
31 --preservation t-nil (updated {_} {k} Γ Γₐ) = t-nil {k} {Γₐ}
32-preservation = {!!}
33+--preservation = {!!}

 1@@ -0,0 +1,35 @@
 2+module TypingService where
 3+
 4+open import Data.List.All using (All)
 5+open import Data.List using (List)
 6+open import Data.Product using (_×_; _,_)
 7+open import TypingBehaviour using (_⊢B_▹_)
 8+open import Type
 9+open import Service
10+open import Behaviour
11+
12+data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
13+  t-bsl-nil : ∀ {n} {Γ : Ctx n}
14+            ----------------
15+            → Γ ⊢BSL nil ▹ Γ
16+
17+-- TODO: finish
18+--  t-bsl-choice : ∀ {n} {Γ : Ctx n} {Γ₁ : Ctx n} {choices : List (Input_ex × Behaviour)}
19+--               → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
20+--               → Γ ⊢BSL 
21+
22+data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
23+  t-process-nil : ∀ {n} {Γ : Ctx n}
24+                ----------
25+                → Γ ⊢P nil
26+
27+  t-process-par : ∀ {n} {Γ : Ctx n} {p₁ p₂ : Process}
28+                → Γ ⊢P p₁
29+                → Γ ⊢P p₂
30+                ----------------
31+                → Γ ⊢P par p₁ p₂
32+
33+data _⊢S_ : ∀ {n} → Ctx n → Service → Set where
34+  t-service : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {d : Deployment m} {p : Process}
35+            ------------------
36+            → Γ ⊢S (b ▹ d - p)