From: Eugene Akentyev Date: Wed, 18 Jan 2017 13:28:00 +0000 (+0300) Subject: Add typing rules for cases with disjoint union X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=e4f03b5d89e4b2483b8a893c890ab1a298c6d145;p=jolie.agda.git Add typing rules for cases with disjoint union --- diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda index 80afd96..0d2aa3e 100644 --- a/src/TypingBehaviour.agda +++ b/src/TypingBehaviour.agda @@ -28,25 +28,25 @@ data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where data _⊢B_▹_ : Context → Behaviour → Context → Set where t-nil : {Γ : Context} - ------------------ + -------------- → Γ ⊢B nil ▹ Γ t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool → Γ ⊢B b₁ ▹ Γ₁ → Γ ⊢B b₂ ▹ Γ₁ - -------------------------- + -------------------------------- → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁ t-while : {Γ : Context} {b : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool → Γ ⊢B b ▹ Γ - ------------------------ + ----------------------- → Γ ⊢B while[ e ] b ▹ Γ t-choice : {Γ Γ₁ : Context} {choices : List (η × Behaviour)} → All (λ { (η , b) → Γ ⊢B (input η) ∶ b ▹ Γ₁ }) choices - ----------------------------------- + ------------------------------- → Γ ⊢B inputchoice choices ▹ Γ₁ t-par : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b1 b2 : Behaviour} @@ -58,35 +58,59 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour} → Γ ⊢B b₁ ▹ Γ₁ → Γ₁ ⊢B b₂ ▹ Γ₂ - ----------------------- + ------------------- → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂ 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 ]) ▹ Γ t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → ◆ Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool → ¬ (var x Tₓ ∈ ◆ Γ) -- x ∉ Γ - -------------------------------------- + --------------------------------- → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ) + t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool + → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ + ------------------------------------------------------- + → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ (var x Tₑ ∷ Γ)) (◆ Γ₁) + + t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool + → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ + ------------------------------------------------------ + → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ Γ) (◆ (var x Tₑ ∷ Γ₁)) + t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ → var x Tₓ ∈ Γ → Tₑ ≡ Tₓ - ------------------------- + ---------------- → Γ ⊢B x ≃ e ▹ Γ t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} → inOneWay o Tᵢ ∈ ◆ Γ → ¬ (var x Tₓ ∈ ◆ Γ) - --------------------------------------- + ------------------------------------------- → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ) + t-oneway-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} + → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁) + → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) + ----------------------------------------------------------------- + → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁) + + t-oneway-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} + → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁) + → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) + ----------------------------------------------------------------- + → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁)) + t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} → inOneWay o Tᵢ ∈ Γ → var x Tₓ ∈ Γ @@ -98,9 +122,23 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ → Tₑ ⊆ Tₒ → ¬ (var x Tₓ ∈ ◆ Γ) - -------------------------------------------------- + ------------------------------------------------------ → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ) + t-solresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {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ᵢ ∷ Γ)) (◆ Γ₁) + + t-solresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {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ᵢ ∷ Γ₁)) + t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → Tₑ ⊆ Tₒ @@ -115,9 +153,27 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁ → var a Tₐ ∈ ◆ Γ₁ → Tₐ ⊆ Tₒ - ---------------------------------- + -------------------------------------- → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁ + t-reqresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : 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 a Tₐ ∈ Γ₂ + → Tₐ ⊆ Tₒ + ------------------------------------ + → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂ + + t-reqresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : 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 a Tₐ ∈ Γ₂ + → Tₐ ⊆ Tₒ + ------------------------------------ + → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂ + t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable} → (inReqRes o Tᵢ Tₒ) ∈ Γ → var x Tₓ ∈ Γ @@ -131,9 +187,21 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where t-wait-new : ∀ {n} {Γ : Ctx n} {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ᵢ ∷ Γ) + t-wait-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {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ᵢ ∷ Γ)) (◆ Γ₁) + + t-wait-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {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ᵢ ∷ Γ₁)) + t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable} → outSolRes o l Tₒ Tᵢ ∈ Γ → var x Tₓ ∈ Γ