Add typing service.

diff --git a/src/Queue.agda b/src/Queue.agda
deleted file mode 100644 (file)
index a1c2e32..0000000
--- a/src/Queue.agda
+++ /dev/null
@@ -1,8 +0,0 @@
-module Queue where
-
-open import Data.List using (List)
-
-
-data Queue (A : Set) : Set where
-  nil : Queue A
-  cons : List A → List A → Queue A

diff --git a/src/Service.agda b/src/Service.agda
index aaee86e06b71b783ea07621badaa00a6f2d6a0f0..45bce0c2ad41120630f24aee3924f3147c59df04 100644 (file)
--- a/src/Service.agda
+++ b/src/Service.agda
@@ -6,9 +6,10 @@ open import Data.String using (String)
 open import Data.Product using (_×_)
 open import Type
 open import Behaviour
-open import Queue
 open import Variable
 
+Queue : (A : Set) → Set
+Queue A = List A
 
 Message : Set
 Message = Channel × Operation × String
@@ -19,12 +20,12 @@ MessageQueue = Queue Message
 data Process : Set where
   _∙_∙_ : Behaviour → List Variable → MessageQueue → Process
   nil : Process
-  _||_ : Process → Process → Process
+  par : Process → Process → Process
 
 data AliasingFunction : Set where
 
-Deployment : {m : ℕ} → Set
-Deployment {m} = AliasingFunction × Ctx m
+Deployment : (m : ℕ) → Set
+Deployment m = AliasingFunction × Ctx m
 
 data Service : Set where
-  service : {m : ℕ} → Behaviour → Deployment {m} → Process → Service
+  _▹_-_ : {m : ℕ} → Behaviour → Deployment m → Process → Service

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 1ac75744fd6a585478564c16dcf28e6d97db52b0..efef10ef3ff108003b362d434e820f60e732256a 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -155,22 +155,22 @@ struct-congruence t refl = t
 struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (seq nil b) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
 struct-cong-nil (t-seq t-nil t) = t
 
-struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
-struct-cong-par-nil (t-par t t-nil) = {!!}
+--struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
+--struct-cong-par-nil (t-par t t-nil) = {!!}
 
-struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁
-struct-cong-par-sym (t-par t₁ t₂) = {!!}
+--struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁
+--struct-cong-par-sym (t-par t₁ t₂) = {!!}
 
-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) ▹ Γ₁
-struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!}
+--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) ▹ Γ₁
+--struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!}
 
 data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
   updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
   identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
   undefined : SideEffect [] []
 
-preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁ 
-preservation t undefined = t
-preservation t (identity γ) = t
+--preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁
+--preservation t undefined = t
+--preservation t (identity γ) = t
 --preservation t-nil (updated {_} {k} Γ Γₐ) = t-nil {k} {Γₐ}
-preservation = {!!}
+--preservation = {!!}

diff --git a/src/TypingService.agda b/src/TypingService.agda
new file mode 100644 (file)
index 0000000..1eb1d4e
--- /dev/null
+++ b/src/TypingService.agda
@@ -0,0 +1,35 @@
+module TypingService where
+
+open import Data.List.All using (All)
+open import Data.List using (List)
+open import Data.Product using (_×_; _,_)
+open import TypingBehaviour using (_⊢B_▹_)
+open import Type
+open import Service
+open import Behaviour
+
+data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
+  t-bsl-nil : ∀ {n} {Γ : Ctx n}
+            ----------------
+            → Γ ⊢BSL nil ▹ Γ
+
+-- TODO: finish
+--  t-bsl-choice : ∀ {n} {Γ : Ctx n} {Γ₁ : Ctx n} {choices : List (Input_ex × Behaviour)}
+--               → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
+--               → Γ ⊢BSL 
+
+data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
+  t-process-nil : ∀ {n} {Γ : Ctx n}
+                ----------
+                → Γ ⊢P nil
+
+  t-process-par : ∀ {n} {Γ : Ctx n} {p₁ p₂ : Process}
+                → Γ ⊢P p₁
+                → Γ ⊢P p₂
+                ----------------
+                → Γ ⊢P par p₁ p₂
+
+data _⊢S_ : ∀ {n} → Ctx n → Service → Set where
+  t-service : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {d : Deployment m} {p : Process}
+            ------------------
+            → Γ ⊢S (b ▹ d - p)