From: Eugene Akentyev Date: Sat, 7 Jan 2017 19:18:07 +0000 (+0500) Subject: Clean up X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=25ab3d57143ef9c26f1fa9922282b6754438a02c;p=jolie.agda.git Clean up --- diff --git a/src/Expr.agda b/src/Expr.agda index ff1f59f..1cdf67c 100644 --- a/src/Expr.agda +++ b/src/Expr.agda @@ -1,14 +1,15 @@ module Expr where -open import Data.Maybe using (Maybe; just; nothing) open import Variable --- TODO: add logic operations and, or data BinOp : Set where + -- Arithmetics plus minus mult div power : BinOp + -- Logical operations + and or : BinOp data Expr : Set where var : Variable → Expr binary : BinOp → Expr → Expr → Expr - constant : Variable.Value → Expr + constant : Value → Expr diff --git a/src/Service.agda b/src/Service.agda index 45bce0c..e2745af 100644 --- a/src/Service.agda +++ b/src/Service.agda @@ -8,6 +8,7 @@ open import Type open import Behaviour open import Variable + Queue : (A : Set) → Set Queue A = List A diff --git a/src/Type.agda b/src/Type.agda index 421eba6..a275abe 100644 --- a/src/Type.agda +++ b/src/Type.agda @@ -1,18 +1,8 @@ module Type where -import Data.Vec.Equality as VecEq -open import Level -open import Relation.Nullary -open import Relation.Binary -open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂) -open import Relation.Nullary.Decidable using (⌊_⌋) -open import Function -open import Data.Nat using (ℕ) renaming (_≟_ to _≟-Nat_) -open import Data.Empty -open import Data.String using (String) renaming (_≟_ to _≟-String_) -open import Data.List using (List; filter) -open import Data.Vec using (Vec; toList) -open import Expr +open import Data.Nat using (ℕ) +open import Data.String using (String) +open import Data.Vec using (Vec) open import Variable @@ -28,157 +18,15 @@ Channel = String data Type : Set where bool int double long string raw void : Type -module TypeEq where - _≟_ : Decidable {A = Type} _≡_ - bool ≟ bool = yes refl - int ≟ int = yes refl - double ≟ double = yes refl - long ≟ long = yes refl - string ≟ string = yes refl - raw ≟ raw = yes refl - void ≟ void = yes refl - bool ≟ int = no λ() - bool ≟ double = no λ() - bool ≟ long = no λ() - bool ≟ string = no λ() - bool ≟ raw = no λ() - bool ≟ void = no λ() - int ≟ bool = no λ() - int ≟ double = no λ() - int ≟ long = no λ() - int ≟ string = no λ() - int ≟ raw = no λ() - int ≟ void = no λ() - double ≟ bool = no λ() - double ≟ int = no λ() - double ≟ long = no λ() - double ≟ string = no λ() - double ≟ raw = no λ() - double ≟ void = no λ() - long ≟ bool = no λ() - long ≟ int = no λ() - long ≟ double = no λ() - long ≟ string = no λ() - long ≟ raw = no λ() - long ≟ void = no λ() - string ≟ bool = no λ() - string ≟ int = no λ() - string ≟ double = no λ() - string ≟ long = no λ() - string ≟ raw = no λ() - string ≟ void = no λ() - raw ≟ bool = no λ() - raw ≟ int = no λ() - raw ≟ double = no λ() - raw ≟ long = no λ() - raw ≟ string = no λ() - raw ≟ void = no λ() - void ≟ bool = no λ() - void ≟ int = no λ() - void ≟ double = no λ() - void ≟ long = no λ() - void ≟ string = no λ() - void ≟ raw = no λ() - data TypeDecl : Set where outNotify : Operation → Location → Type → TypeDecl outSolRes : Operation → Location → Type → Type → TypeDecl inOneWay : Operation → Type → TypeDecl inReqRes : Operation → Type → Type → TypeDecl var : Variable → Type → TypeDecl - empty : TypeDecl - pair : TypeDecl → TypeDecl → TypeDecl - -cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} - (f : A → B → C → D) {x y u v m n} → x ≡ y → u ≡ v → m ≡ n → f x u m ≡ f y v n -cong₃ f refl refl refl = refl - -cong₄ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e} - (f : A → B → C → D → E) {x y u v m n k l} → x ≡ y → u ≡ v → m ≡ n → k ≡ l → f x u m k ≡ f y v n l -cong₄ f refl refl refl refl = refl - -module TypeDeclEq where - _≟_ : Decidable {A = TypeDecl} _≡_ - (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) with o1 ≟-String o2 | l1 ≟-String l2 | t1 TypeEq.≟ t2 - ... | yes o | yes l | yes t = yes (cong₃ outNotify o l t) - ... | no ¬p | _ | _ = no (λ { refl → ¬p refl}) - ... | _ | no ¬p | _ = no (λ { refl → ¬p refl}) - ... | _ | _ | no ¬p = no (λ { refl → ¬p refl}) - (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') with o1 ≟-String o2 | l1 ≟-String l2 | t1 TypeEq.≟ t2 | t1' TypeEq.≟ t2' - ... | yes o | yes l | yes t | yes t' = yes (cong₄ outSolRes o l t t') - ... | no ¬p | _ | _ | _ = no (λ { refl → ¬p refl}) - ... | _ | no ¬p | _ | _ = no (λ { refl → ¬p refl}) - ... | _ | _ | no ¬p | _ = no (λ { refl → ¬p refl}) - ... | _ | _ | _ | no ¬p = no (λ { refl → ¬p refl}) - (inOneWay o1 t1) ≟ (inOneWay o2 t2) with o1 ≟-String o2 | t1 TypeEq.≟ t2 - ... | yes o | yes t = yes (cong₂ inOneWay o t) - ... | no ¬p | _ = no (λ { refl → ¬p refl}) - ... | _ | no ¬p = no (λ { refl → ¬p refl}) - (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') with o1 ≟-String o2 | t1 TypeEq.≟ t2 | t1' TypeEq.≟ t2' - ... | yes o | yes l | yes t = yes (cong₃ inReqRes o l t) - ... | no ¬p | _ | _ = no (λ { refl → ¬p refl}) - ... | _ | no ¬p | _ = no (λ { refl → ¬p refl}) - ... | _ | _ | no ¬p = no (λ { refl → ¬p refl}) - (var v1 t1) ≟ (var v2 t2) with v1 ≟-Nat v2 | t1 TypeEq.≟ t2 - ... | yes v | yes t = yes (cong₂ var v t) - ... | no ¬p | _ = no (λ { refl → ¬p refl}) - ... | _ | no ¬p = no (λ { refl → ¬p refl}) - (pair t1 t1') ≟ (pair t2 t2') with t1 ≟ t2 | t1' ≟ t2' - ... | yes t | yes t' = yes (cong₂ pair t t') - ... | no ¬p | _ = no (λ { refl → ¬p refl}) - ... | _ | no ¬p = no (λ { refl → ¬p refl}) - empty ≟ empty = yes refl - empty ≟ (outNotify _ _ _) = no λ() - empty ≟ (outSolRes _ _ _ _) = no λ() - empty ≟ (inOneWay _ _) = no λ() - empty ≟ (inReqRes _ _ _) = no λ() - empty ≟ (var _ _) = no λ() - empty ≟ (pair _ _) = no λ() - (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ() - (outNotify _ _ _) ≟ (inOneWay _ _) = no λ() - (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ() - (outNotify _ _ _) ≟ (var _ _) = no λ() - (outNotify _ _ _) ≟ empty = no λ() - (outNotify _ _ _) ≟ (pair _ _) = no λ() - (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ() - (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ() - (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ() - (outSolRes _ _ _ _) ≟ (var _ _) = no λ() - (outSolRes _ _ _ _) ≟ empty = no λ() - (outSolRes _ _ _ _) ≟ (pair _ _) = no λ() - (inOneWay _ _) ≟ (outNotify _ _ _) = no λ() - (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ() - (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ() - (inOneWay _ _) ≟ (var _ _) = no λ() - (inOneWay _ _) ≟ empty = no λ() - (inOneWay _ _) ≟ (pair _ _) = no λ() - (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ() - (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ() - (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ() - (inReqRes _ _ _) ≟ (var _ _) = no λ() - (inReqRes _ _ _) ≟ empty = no λ() - (inReqRes _ _ _) ≟ (pair _ _) = no λ() - (var _ _) ≟ (outNotify _ _ _) = no λ() - (var _ _) ≟ (outSolRes _ _ _ _) = no λ() - (var _ _) ≟ (inOneWay _ _) = no λ() - (var _ _) ≟ (inReqRes _ _ _) = no λ() - (var _ _) ≟ empty = no λ() - (var _ _) ≟ (pair _ _) = no λ() - (pair _ _) ≟ (outNotify _ _ _) = no λ() - (pair _ _) ≟ (outSolRes _ _ _ _) = no λ() - (pair _ _) ≟ (inOneWay _ _) = no λ() - (pair _ _) ≟ (inReqRes _ _ _) = no λ() - (pair _ _) ≟ (var _ _) = no λ() - (pair _ _) ≟ empty = no λ() - - decSetoid : DecSetoid _ _ - decSetoid = PropEq.decSetoid _≟_ data _⊆_ : Type → Type → Set where sub : {T₁ T₂ : Type} → T₁ ⊆ T₂ Ctx : ℕ → Set Ctx = Vec TypeDecl - -module CtxEq = VecEq.DecidableEquality TypeDeclEq.decSetoid -module CtxPropEq = VecEq.PropositionalEquality diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda index 73fea36..38f9d2f 100644 --- a/src/TypingBehaviour.agda +++ b/src/TypingBehaviour.agda @@ -30,25 +30,25 @@ data Context : Set where data _⊢B_▹_ : Context → Behaviour → Context → Set where 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} {Γ : Ctx n} {b : Behaviour} {e : Expr} → Γ ⊢ₑ e ∶ bool → ◆ Γ ⊢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 : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} @@ -61,47 +61,47 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where 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} {Γ : 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)) ▹ ◆ Γ t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ - ----------------------------------- + -------------------------------------- → ◆ Γ ⊢B assign x e ▹ ◆ (var x Tₑ ∷ Γ) t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} → Γ ⊢ₑ e ∶ Tₑ → var x Tₓ ∈ Γ → Tₑ ≡ 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) ▹ ◆ Γ 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ₓ ∈ Γ) - -------------------------------------------------- + ------------------------------------------------------- → ◆ Γ ⊢B output (solicitres o 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} @@ -109,7 +109,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where → Tₑ ⊆ Tₒ → var x Tₓ ∈ Γ → Tᵢ ⊆ Tₓ - --------------------------------------- + ------------------------------------------ → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ Γ t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour} @@ -118,7 +118,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where → ◆ (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} @@ -128,20 +128,20 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where → ◆ Γ ⊢B b ▹ ◆ Γ₁ → var a Tₐ ∈ Γ₁ → Tₐ ⊆ Tₒ - ---------------------------------- + -------------------------------------- → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁ 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} {Γ : 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 ▹ ◆ Γ t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable} @@ -149,7 +149,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where → ◆ Γ ⊢B b ▹ ◆ Γ₁ → var x Tₓ ∈ Γ → Tₓ ⊆ Tₒ - ------------------------ + ---------------------------- → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁ struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁ @@ -164,13 +164,16 @@ struct-cong-par-nil (t-par t t-nil) = t struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b1 b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (par b2 b1) ▹ ■ Γ₂' Γ₁' struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁ +data Label : Set where + x=e readt νr r:o r,o r,ol : Label + 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} Γ Γₐ) = {!!} -preservation = {!!} +--preservation = {!!} diff --git a/src/TypingService.agda b/src/TypingService.agda index 0006a18..9da969e 100644 --- a/src/TypingService.agda +++ b/src/TypingService.agda @@ -8,6 +8,7 @@ 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} ---------------- diff --git a/src/Variable.agda b/src/Variable.agda index 33b0f60..f3b08cc 100644 --- a/src/Variable.agda +++ b/src/Variable.agda @@ -3,8 +3,6 @@ module Variable where open import Data.Integer using (ℤ) open import Data.String using (String) open import Data.Product using (_×_) -open import Data.Maybe using (Maybe) -open import Data.List using (List) open import Data.Bool using (Bool) open import Data.Nat using (ℕ)