From: Eugene Akentyev Date: Tue, 27 Dec 2016 01:19:31 +0000 (+0500) Subject: Update type rules of behaviour layer. X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=6abff2b0672cb9e05f1c82bd925578b0e2df2499;p=jolie.agda.git Update type rules of behaviour layer. --- diff --git a/src/Typecheck.agda b/src/Typecheck.agda index be66298..48a8ad3 100644 --- a/src/Typecheck.agda +++ b/src/Typecheck.agda @@ -5,7 +5,7 @@ open import Relation.Nullary using (¬_) open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl) open import Data.Nat using (ℕ; _+_; suc; _≟_) open import Data.List using (List) -open import Data.Vec using (_∈_) +open import Data.Vec using (_∈_; []; _++_; _∷_) open import Data.Product using (_,_; _×_) open import Function open import Expr @@ -25,26 +25,26 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where → Γ ⊢ₑ s ∶ b data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where - t-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} - --------------------------- - → Γ ⊢B nil ▹ Γ₁ + t-nil : ∀ {n} {Γ : Ctx n} + -------------- + → Γ ⊢B nil ▹ Γ t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool → Γ ⊢B b1 ▹ Γ₁ → Γ ⊢B b2 ▹ Γ₁ - --------------------------- + ---------------------- → Γ ⊢B if e b1 b2 ▹ Γ₁ - t-while : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} {b : Behaviour} {e : Expr} + t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool - → Γ ⊢B b ▹ Γ₁ - -------------------------- - → Γ ⊢B while e b ▹ Γ₁ + → Γ ⊢B b ▹ Γ + --------------------- + → Γ ⊢B while e b ▹ Γ t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)} → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices - ----------------------------------------------- + ------------------------------- → Γ ⊢B inputchoice choices ▹ Γ₁ t-par : ∀ {n m} {Γ : Ctx n} {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour} @@ -52,104 +52,112 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where → Γ₁ ⊢B b1 ▹ Γ₁' → Γ₂ ⊢B b2 ▹ Γ₂' -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions - -------------------- - → Γ ⊢B par b1 b2 ▹ Γ' + ---------------------------------------- + → (Γ₁ ++ Γ₂) ⊢B par b1 b2 ▹ (Γ₁' ++ Γ₂') - t-seq : ∀ {n m} {Γ : Ctx n} {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour} + t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → Γ₁ ⊢B b2 ▹ Γ₂ - -------------------- + --------------------- → Γ ⊢B seq b1 b2 ▹ Γ₂ - t-notification : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type} + t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type} → (outNotify o l T₀) ∈ Γ → Γ ⊢ e ∶ Tₑ → Tₑ ⊆ T₀ - ------------------------------------------- - → Γ ⊢B output (notification o l (var e)) ▹ subst Ctx n≡m Γ + --------------------------------------------- + → Γ ⊢B output (notification o l (var e)) ▹ Γ - t-assign-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ - → (var x Tₑ) ∈ Γ₁ - --------------------- - → Γ ⊢B assign x e ▹ Γ₁ + ----------------------------------- + → Γ ⊢B assign x e ▹ (var x Tₑ ∷ Γ) - t-assign-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ - → (var x Tₓ) ∈ Γ + → var x Tₓ ∈ Γ → Tₑ ≡ Tₓ - --------------------- - → Γ ⊢B assign x e ▹ subst Ctx n≡m Γ - - t-oneway-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} - → (inOneWay o Tᵢ) ∈ Γ - → ¬ ((var x Tₓ) ∈ Γ) - → (var x Tᵢ) ∈ Γ₁ - ------------------------------- - → Γ ⊢B input (oneway o x) ▹ Γ₁ - - t-oneway-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} - → (inOneWay o Tᵢ) ∈ Γ - → ((var x Tₓ) ∈ Γ) + ---------------------- + → Γ ⊢B assign x e ▹ Γ + + t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} + → inOneWay o Tᵢ ∈ Γ + → ¬ (var x Tₓ ∈ Γ) + ------------------------------------------ + → Γ ⊢B input (oneway o x) ▹ (var x Tᵢ ∷ Γ) + + t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} + → inOneWay o Tᵢ ∈ Γ + → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ - -------------------------------- - → Γ ⊢B input (oneway o x) ▹ subst Ctx n≡m Γ + ------------------------------ + → Γ ⊢B input (oneway o x) ▹ Γ - t-solresp-new : ∀ {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-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} + → outSolRes o l Tₒ Tᵢ ∈ Γ → Tₑ ⊆ Tₒ → ¬ (var x Tₓ ∈ Γ) - → (var x Tᵢ) ∈ Γ₁ - ----------------------------------------- - → Γ ⊢B output (solicitres o l e x) ▹ Γ₁ + -------------------------------------------------- + → Γ ⊢B output (solicitres o l e x) ▹ (var x Tᵢ ∷ Γ) - t-solresp-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} - → (outSolRes o l Tₒ Tᵢ) ∈ Γ + t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable} + → outSolRes o l Tₒ Tᵢ ∈ Γ → Tₑ ⊆ Tₒ - → (var x Tₓ) ∈ Γ + → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ - ----------------------------------------- - → Γ ⊢B output (solicitres o l e x) ▹ subst Ctx n≡m Γ + --------------------------------------- + → Γ ⊢B output (solicitres o l e x) ▹ Γ - t-reqresp-new : ∀ {n m} {Γ : Ctx n} {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour} - → (inReqRes o Tᵢ Tₒ) ∈ Γ + t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {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ₐ) ∈ Γ₁ + → (var x Tₓ ∷ Γ) ⊢B b ▹ Γ₁ + → var a Tₐ ∈ Γ₁ → Tₐ ⊆ Tₒ - ----------------------------------- + ---------------------------------- → Γ ⊢B input (reqres 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} → (inReqRes o Tᵢ Tₒ) ∈ Γ - → (var x Tₓ) ∈ Γ + → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ → Γ ⊢B b ▹ Γ₁ - → (var a Tₐ) ∈ Γ₁ + → var a Tₐ ∈ Γ₁ → Tₐ ⊆ Tₒ - ------------------------------------ + ---------------------------------- → Γ ⊢B input (reqres o x a b) ▹ Γ₁ - t-wait-new : ∀ {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ₓ) ∈ Γ) - → (var x Tᵢ) ∈ Γ₁ - ------------------------ - → Γ ⊢B wait r o l x ▹ Γ₁ + 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-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable} - → (outSolRes o l Tₒ Tᵢ) ∈ Γ - → ((var x Tₓ) ∈ Γ) + t-wait-exists : ∀ {n} {Γ : Ctx n} {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} - → (inReqRes o Tᵢ Tₒ) ∈ Γ + → inReqRes o Tᵢ Tₒ ∈ Γ → Γ ⊢B b ▹ Γ₁ - → (var x Tₓ) ∈ Γ + → var x Tₓ ∈ Γ → Tₓ ⊆ Tₒ ------------------------ → Γ ⊢B exec r o x b ▹ Γ₁ + +congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → b1 ≡ b2 → Γ ⊢B b2 ▹ Γ₁ +congruence t refl = 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 t (updated Γ Γ₁)= {!!}