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
→ Γ ⊢ₑ 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}
→ Γ₁ ⊢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 Γ Γ₁)= {!!}
projects / jolie.agda.git / commitdiff