From a9f1698353219d88e3357ba5329c8a4921a4b016 Mon Sep 17 00:00:00 2001 From: Eugene Akentyev Date: Wed, 18 Jan 2017 08:06:25 +0300 Subject: [PATCH] Expand behaviour's typing rules. Add network and service typing rules. --- src/Network.agda | 7 ++ src/Type.agda | 31 ++++++--- src/TypingBehaviour.agda | 142 +++++++++++++++++---------------------- src/TypingNetwork.agda | 33 +++++++-- src/TypingService.agda | 6 +- 5 files changed, 119 insertions(+), 100 deletions(-) diff --git a/src/Network.agda b/src/Network.agda index b413c91..34631bb 100644 --- a/src/Network.agda +++ b/src/Network.agda @@ -1,5 +1,6 @@ module Network where +open import Data.List using (List; []; [_]; _++_) open import Type open import Service @@ -9,3 +10,9 @@ data Network : Set where νr : Network → Network _∥_ : Network → Network → Network nil : Network + +locs : Network → List Location +locs (νr n) = locs n +locs (n₁ ∥ n₂) = locs n₁ ++ locs n₂ +locs nil = [] +locs ([ s ] l) = [ l ] diff --git a/src/Type.agda b/src/Type.agda index a275abe..f5c3130 100644 --- a/src/Type.agda +++ b/src/Type.agda @@ -2,18 +2,13 @@ module Type where open import Data.Nat using (ℕ) open import Data.String using (String) -open import Data.Vec using (Vec) +open import Data.Vec using (Vec) renaming (_∷_ to _∷-Vec_) open import Variable -Operation : Set -Operation = String - -Location : Set -Location = String - -Channel : Set -Channel = String +data Operation : Set where +data Location : Set where +data Channel : Set where data Type : Set where bool int double long string raw void : Type @@ -30,3 +25,21 @@ data _⊆_ : Type → Type → Set where Ctx : ℕ → Set Ctx = Vec TypeDecl + +data Context : Set where + ◆ : ∀ {n} → Ctx n → Context + ■ : ∀ {n m} → Ctx n → Ctx m → Context + +infix 4 _∈_ + +data _∈_ : TypeDecl → Context → Set where + here-◆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ◆ (x ∷-Vec xs) + there-◆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ◆ xs) → x ∈ ◆ (y ∷-Vec xs) + here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (x ∷-Vec xs) ys + here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ xs (x ∷-Vec ys) + there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ (x ∷-Vec xs) ys + there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ xs (x ∷-Vec ys) + +_∷_ : TypeDecl → Context → Context +t ∷ ◆ xs = ◆ (t ∷-Vec xs) +x ∷ ■ xs ys = ■ (x ∷-Vec xs) ys diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda index 642c23f..7d82a79 100644 --- a/src/TypingBehaviour.agda +++ b/src/TypingBehaviour.agda @@ -5,7 +5,7 @@ open import Relation.Nullary using (¬_) open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Data.Nat using (ℕ) open import Data.List using (List) -open import Data.Vec using (_∈_; []; _++_; _∷_; here; there) +open import Data.Vec using ([]; _++_) open import Data.Product using (_,_; _×_) open import Function open import Expr @@ -22,143 +22,132 @@ data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour -- Identity idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b -data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where +data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where expr-t : {s : Expr} {b : Type} → Γ ⊢ₑ s ∶ b -data Context : Set where - ◆ : ∀ {n} → Ctx n → Context - ■ : ∀ {n m} → Ctx n → Ctx m → Context - data _⊢B_▹_ : Context → Behaviour → Context → Set where - t-nil : ∀ {n} {Γ : Ctx n} + t-nil : {Γ : Context} ------------------ - → ◆ Γ ⊢B nil ▹ ◆ Γ + → Γ ⊢B nil ▹ Γ - t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} {e : Expr} + t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool - → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁ - → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁ + → Γ ⊢B b₁ ▹ Γ₁ + → Γ ⊢B b₂ ▹ Γ₁ -------------------------- - → ◆ Γ ⊢B if e then b₁ else b₂ ▹ ◆ Γ₁ + → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁ - t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr} + t-while : {Γ : Context} {b : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool - → ◆ Γ ⊢B b ▹ ◆ Γ + → Γ ⊢B b ▹ Γ ------------------------ - → ◆ Γ ⊢B while[ e ] b ▹ ◆ Γ + → Γ ⊢B while[ e ] b ▹ Γ - t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (η × Behaviour)} - → All (λ { (η , b) → ◆ Γ ⊢B (input η) ∶ b ▹ ◆ Γ₁ }) choices + t-choice : {Γ Γ₁ : Context} {choices : List (η × Behaviour)} + → All (λ { (η , b) → Γ ⊢B (input η) ∶ b ▹ Γ₁ }) choices ----------------------------------- - → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁ + → Γ ⊢B inputchoice choices ▹ Γ₁ t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁' → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂' - -------------------------------------- + ------------------------------------ → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂') - t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b₁ b₂ : Behaviour} - → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁ - → ◆ Γ₁ ⊢B b₂ ▹ ◆ Γ₂ - ------------------------- - → ◆ Γ ⊢B b₁ ∶ b₂ ▹ ◆ Γ₂ + t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour} + → Γ ⊢B b₁ ▹ Γ₁ + → Γ₁ ⊢B b₂ ▹ Γ₂ + ----------------------- + → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂ - t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type} + t-notification : {Γ : Context} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type} → (outNotify o l T₀) ∈ Γ → var e Tₑ ∈ Γ → Tₑ ⊆ T₀ ------------------------------------------------ - → ◆ Γ ⊢B output (o at l [ var e ]) ▹ ◆ Γ + → Γ ⊢B output (o at l [ var e ]) ▹ Γ - t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + t-assign-new : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ -------------------------------------- - → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ) + → Γ ⊢B x ≃ e ▹ (var x Tₑ ∷ Γ) - t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ → var x Tₓ ∈ Γ → Tₑ ≡ Tₓ ------------------------- - → ◆ Γ ⊢B x ≃ e ▹ ◆ Γ + → Γ ⊢B x ≃ e ▹ Γ - t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} + t-oneway-new : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} → inOneWay o Tᵢ ∈ Γ → ¬ (var x Tₓ ∈ Γ) - ---------------------------------------------- - → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ) + --------------------------------------- + → Γ ⊢B input (o [ x ]) ▹ (var x Tᵢ ∷ Γ) - t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} + t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} → inOneWay o Tᵢ ∈ Γ → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ - --------------------------------- - → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ Γ + -------------------------- + → Γ ⊢B input (o [ x ]) ▹ Γ - t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} + t-solresp-new : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → Tₑ ⊆ Tₒ → ¬ (var x Tₓ ∈ Γ) - ------------------------------------------------------- - → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ) + -------------------------------------------------- + → Γ ⊢B output (o at l [ e ][ x ]) ▹ (var x Tᵢ ∷ Γ) - t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} + t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → Tₑ ⊆ Tₒ → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ - ------------------------------------------ - → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ Γ + ------------------------------------- + → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ - t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour} + t-reqresp-new : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour} → inReqRes o Tᵢ Tₒ ∈ Γ → ¬ (var x Tₓ ∈ Γ) - → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁ + → (var x Tₓ ∷ Γ) ⊢B b ▹ Γ₁ → var a Tₐ ∈ Γ₁ → Tₐ ⊆ Tₒ - -------------------------------------- - → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁ + ---------------------------------- + → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁ - t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable} + t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable} → (inReqRes o Tᵢ Tₒ) ∈ Γ → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ - → ◆ Γ ⊢B b ▹ ◆ Γ₁ + → Γ ⊢B b ▹ Γ₁ → var a Tₐ ∈ Γ₁ → Tₐ ⊆ Tₒ - -------------------------------------- - → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁ + ---------------------------------- + → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁ - t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable} + t-wait-new : {Γ : Context} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → ¬ (var x Tₓ ∈ Γ) - ---------------------------------------- - → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ) + ------------------------------------ + → Γ ⊢B wait r o l x ▹ (var x Tᵢ ∷ Γ) - t-wait-exists : ∀ {n} {Γ : Ctx n} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable} + t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ - --------------------------- - → ◆ Γ ⊢B wait r o l x ▹ ◆ Γ + ----------------------- + → Γ ⊢B wait r o l x ▹ Γ - t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable} + t-exec : {Γ Γ₁ : Context} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable} → inReqRes o Tᵢ Tₒ ∈ Γ - → ◆ Γ ⊢B b ▹ ◆ Γ₁ + → Γ ⊢B b ▹ Γ₁ → var x Tₓ ∈ Γ → Tₓ ⊆ Tₒ - ---------------------------- - → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁ - - t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b₁ b₂ : Behaviour} - → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂ - → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁ - ------------------ - → ◆ Γₐ ⊢B b₂ ▹ ◆ Γ₁ - + ------------------------ + → Γ ⊢B exec r o x b ▹ Γ₁ struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁ @@ -171,18 +160,7 @@ struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁ → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁' struct-cong-par-nil (t-par x _) = x -struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b₁ b₂ : Behaviour} - → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂' - → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁' -struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁ - -struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} - → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁ - → ◆ Γ ⊢B b ▹ ◆ Γ₁ -struct-cong-nil = t-mutate upd - -preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} - → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁ - → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂ - → ◆ Γₐ ⊢B b₂ ▹ ◆ Γ₁ -preservation x s = t-mutate s x +--struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b₁ b₂ : Behaviour} +-- → Γ₁ ++ Γ₂ ⊢B (b₁ ∥ b₂) ▹ Γ₁' ++ Γ₂' +-- → Γ₂ ++ Γ₁ ⊢B (b₂ ∥ b₁) ▹ Γ₂' ++ Γ₁' +--struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁ diff --git a/src/TypingNetwork.agda b/src/TypingNetwork.agda index 3816edd..be79b1a 100644 --- a/src/TypingNetwork.agda +++ b/src/TypingNetwork.agda @@ -1,16 +1,35 @@ module TypingNetwork where +open import Relation.Nullary using (¬_) +open import Data.Vec using (_∈_; fromList) +open import Data.Product using (_,_) +open import TypingService +open import Service open import Network open import Type +open import Behaviour -data _⊢N_ : ∀ {n} → Ctx n → Network → Set where + +data _⊢N_ : Context → Network → Set where t-network-nil : ∀ {n} {Γ : Ctx n} - ---------- - → Γ ⊢N nil + ------------ + → ◆ Γ ⊢N nil + + t-deployment : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {l : Location} {o : Operation} {p : Process} {d : Deployment m} {Tₒ : Type} + → Γ ⊢S (b ▹ d - p) + → ¬ (outNotify o l Tₒ ∈ Γ) + -------------------------- + → ◆ Γ ⊢N ([ b ▹ d - p ] l) - -- TODO: implement t-network and t-deployment + t-network : ∀ {n} {m} {Γ₁ : Ctx n} {Γ₂ : Ctx m} {N₁ N₂ : Network} {l : Location} + → ◆ Γ₁ ⊢N N₁ + → ◆ Γ₂ ⊢N N₂ +-- → , ¬ (l ∈ fromList (locs N₁)) + → ¬ (l ∈ fromList (locs N₂)) + ---------------------- + → ■ Γ₁ Γ₂ ⊢N (N₁ ∥ N₂) t-restriction : ∀ {n} {Γ : Ctx n} {n : Network} - → Γ ⊢N n - ----------- - → Γ ⊢N νr n + → ◆ Γ ⊢N n + ------------- + → ◆ Γ ⊢N νr n diff --git a/src/TypingService.agda b/src/TypingService.agda index 7e2dc36..eeefc58 100644 --- a/src/TypingService.agda +++ b/src/TypingService.agda @@ -6,7 +6,7 @@ open import Data.List.All using (All) open import Data.Vec using (Vec; toList; concat; _∈_) open import Data.List using (List; zip) open import Data.Product using (_×_; _,_) -open import TypingBehaviour using (_⊢B_▹_; ◆) +open import TypingBehaviour using (_⊢B_▹_) open import Type open import Service open import Behaviour @@ -41,6 +41,8 @@ data _⊢P_ : ∀ {n} → Ctx n → Process → Set where data _⊢S_ : ∀ {n} → Ctx n → Service → Set where - t-service : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {d : Deployment m} {p : Process} + t-service : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {b : Behaviour} {d : Deployment m} {p : Process} + → Γ ⊢BSL b ▹ Γ₁ + → Γ ⊢P p ------------------ → Γ ⊢S (b ▹ d - p) -- 2.50.1