From 80305d19e403d49ff8d6d95414dacbf980204ccd Mon Sep 17 00:00:00 2001 From: Eugene Akentyev Date: Sat, 3 Dec 2016 20:37:13 +0500 Subject: [PATCH] Simplified variables and finished typing rules for behaviour. --- src/Behaviour.agda | 4 +- src/Type.agda | 71 +++++-------------------- src/Typecheck.agda | 126 ++++++++++++++++++++++++++++++++++----------- src/Variable.agda | 14 ++--- 4 files changed, 114 insertions(+), 101 deletions(-) diff --git a/src/Behaviour.agda b/src/Behaviour.agda index 4748617..8c78720 100644 --- a/src/Behaviour.agda +++ b/src/Behaviour.agda @@ -11,13 +11,13 @@ open import Type data Output_ex : Set where notification : Operation → Location → Expr → Output_ex - solicitRes : Operation → Location → Expr → Variable → Output_ex + solicitres : Operation → Location → Expr → Variable → Output_ex data Behaviour : Set data Input_ex : Set where oneway : Operation → Variable → Input_ex - reqRes : Operation → Variable → Variable → Behaviour → Input_ex + reqres : Operation → Variable → Variable → Behaviour → Input_ex data Behaviour where input : Input_ex → Behaviour diff --git a/src/Type.agda b/src/Type.agda index 0b2b9a5..a6fba82 100644 --- a/src/Type.agda +++ b/src/Type.agda @@ -4,12 +4,13 @@ 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 (ℕ) open import Data.Empty open import Data.String using (String) -open import Data.List using (List) -open import Data.Vec using (Vec) +open import Data.List using (List; filter) +open import Data.Vec using (Vec; toList) open import Expr open import Variable @@ -23,68 +24,20 @@ Location = String Channel : Set Channel = String -data Cardinality : Set where - oo oi ii : Cardinality - -data BasicType : Set where - bool int double long string raw void : BasicType - -data TypeTree : Set - -data ChildType : Set where - child : String → Cardinality → TypeTree → ChildType - -data TypeTree where - leaf : BasicType → TypeTree - node : BasicType → List ChildType → TypeTree - -get-basic : TypeTree → BasicType -get-basic (leaf b) = b -get-basic (node b _) = b +data Type : Set where + bool int double long string raw void : Type data TypeDecl : Set where - outNotify : Operation → Location → TypeTree → TypeDecl - outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl - inOneWay : Operation → TypeTree → TypeDecl - inReqRes : Operation → TypeTree → TypeTree → TypeDecl - var : Variable → TypeTree → TypeDecl + 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 -data _⊆_ : TypeTree → TypeTree → Set where - sub : {T₁ T₂ : TypeTree} → T₁ ⊆ T₂ +data _⊆_ : Type → Type → Set where + sub : {T₁ T₂ : Type} → T₁ ⊆ T₂ Ctx : ℕ → Set Ctx = Vec TypeDecl - -roots : {n : ℕ} → Ctx n → List Name -roots xs = go xs - where - open import Data.List using ([]; _∷_) - - go : {n : ℕ} → Ctx n → List Name - go Vec.[] = [] - go (Vec._∷_ x xs) = - case x of λ - { (var v t) → (root v) ∷ (roots xs) - ; _ → roots xs - } - -intersect-roots : List Name → List Name → List Name -intersect-roots xs ys = intersect xs ys - where - open import Data.List using ([]; _∷_) - open import Data.String using (_≟_) - - intersect : List Name → List Name → List Name - intersect [] _ = [] - intersect _ [] = [] - intersect (x ∷ xs) (y ∷ ys) with x ≟ y - ... | yes x≡y = x ∷ intersect xs ys - ... | no _ = intersect xs ys - - -upd : {n m : ℕ} → Ctx n → Variable → TypeTree → Ctx m -upd Γ x Tₓ = - let r = root x in - {!!} diff --git a/src/Typecheck.agda b/src/Typecheck.agda index ad70c02..97d9173 100644 --- a/src/Typecheck.agda +++ b/src/Typecheck.agda @@ -1,77 +1,143 @@ + module Typecheck where import Data.List as List import Data.Vec.Equality as VecEq open import Relation.Nullary using (¬_) +open import Relation.Nullary open import Relation.Binary.PropositionalEquality as PropEq using (_≡_) -open import Data.Nat using (ℕ; _+_) -open import Data.Vec using (Vec; _∈_; zip) +open import Data.Nat using (ℕ; _+_; suc) +open import Data.Vec using (Vec; _∈_; zip; _∷_) open import Expr open import Type open import Behaviour open import Variable -data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → TypeTree → Set where - var-t : {s : Variable} {b : TypeTree} +data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where + var-t : {s : Variable} {b : Type} → Γ ⊢ s of b -data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → TypeTree → Set where - expr-t : {s : Expr} {b : TypeTree} +data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where + expr-t : {s : Expr} {b : Type} → Γ ⊢ₑ s of b -data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where +data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where t-nil : {Γ₁ : Ctx m} → n ≡ m -------------- - → Γ ⊢ nil ▹ Γ₁ + → Γ ⊢B nil ▹ Γ₁ t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable} - → Γ ⊢ e of (leaf bool) -- Γ ⊢ e : bool - → Γ ⊢ b1 ▹ Γ₁ - → Γ ⊢ b2 ▹ Γ₁ + → Γ ⊢ e of bool -- Γ ⊢ e : bool + → Γ ⊢B b1 ▹ Γ₁ + → Γ ⊢B b2 ▹ Γ₁ --------------------------- - → Γ ⊢ if (var e) b1 b2 ▹ Γ₁ + → Γ ⊢B if (var e) b1 b2 ▹ Γ₁ t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable} - → Γ ⊢ e of (leaf bool) - → Γ ⊢ b ▹ Γ₁ + → Γ ⊢ e of bool + → Γ ⊢B b ▹ Γ₁ -------------------------- - → Γ ⊢ while (var e) b ▹ Γ₁ + → Γ ⊢B while (var e) b ▹ Γ₁ t-choice : {Γ₁ : Ctx m} {k n : ℕ} {η : Input_ex} {inputs : Vec Input_ex n} {b : Behaviour} {behaviours : Vec Behaviour n} → η ∈ inputs → b ∈ behaviours - → Γ ⊢ seq (input η) b ▹ Γ₁ + → Γ ⊢B seq (input η) b ▹ Γ₁ ---------------------------------------------- - → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁ + → Γ ⊢B inputchoice (zip inputs behaviours) ▹ Γ₁ t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour} {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m} - → Γ₁ ⊢ b1 ▹ Γ₁' - → Γ₂ ⊢ b2 ▹ Γ₂' - → intersect-roots (roots Γ₁') (roots Γ₂') ≡ List.[] + → Γ₁ ⊢B b1 ▹ Γ₁' + → Γ₂ ⊢B b2 ▹ Γ₂' -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions -------------------- - → Γ ⊢ par b1 b2 ▹ Γ' + → Γ ⊢B par b1 b2 ▹ Γ' t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour} - → Γ ⊢ b1 ▹ Γ₁ - → Γ₁ ⊢ b2 ▹ Γ₂ + → Γ ⊢B b1 ▹ Γ₁ + → Γ₁ ⊢B b2 ▹ Γ₂ -------------------- - → Γ ⊢ seq b1 b2 ▹ Γ₂ + → Γ ⊢B seq b1 b2 ▹ Γ₂ - t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : TypeTree} + t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type} → (outNotify o l T₀) ∈ Γ → Γ ⊢ e of Tₑ → Tₑ ⊆ T₀ - ------------------------------------------- → n ≡ m - → Γ ⊢ output (notification o l (var e)) ▹ Γ₁ + ------------------------------------------- + → Γ ⊢B output (notification o l (var e)) ▹ Γ₁ - t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {T₀ : TypeTree} {Tₓ : TypeTree} - → Γ ⊢ₑ e of T₀ -- Γ ⊢ e : bool + t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + → Γ ⊢ₑ e of Tₑ -- Γ ⊢ e : bool → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ + → (var x Tₑ) ∈ Γ₁ --------------------- - → Γ ⊢ assign x e ▹ upd Γ x (bt Tₑ) + → Γ ⊢B assign x e ▹ Γ₁ + + t-assign-exists : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + → Γ ⊢ₑ e of Tₑ + → (var x Tₓ) ∈ Γ + → Tₑ ≡ Tₓ + → n ≡ m -- TODO Γ ≡ Γ₁ + --------------------- + → Γ ⊢B assign x e ▹ Γ₁ + + t-oneway-new : {Γ₁ : 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 : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable} + → (inOneWay o Tᵢ) ∈ Γ + → ((var x Tₓ) ∈ Γ) + → Tᵢ ⊆ Tₓ + → n ≡ m -- TODO Γ ≡ Γ₁ + -------------------------------- + → Γ ⊢B (input (oneway o x)) ▹ Γ₁ + + t-solresp-new : {Γ₁ : 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ₓ ∈ Γ) + → (var x Tᵢ) ∈ Γ₁ + ----------------------------------------- + → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁ + + t-solresp-exists : {Γ₁ : 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ₓ) ∈ Γ + → Tᵢ ⊆ Tₓ + → n ≡ m -- TODO Γ ≡ Γ₁ + ----------------------------------------- + → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁ + + t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : 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ₐ) ∈ Γ₁ + → Tₐ ⊆ Tₒ + ----------------------------------- + → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁ + + t-reqresp-exists : {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable} + → (inReqRes o Tᵢ Tₒ) ∈ Γ + → (var x Tₓ) ∈ Γ + → Tᵢ ⊆ Tₓ + → Γ ⊢B b ▹ Γ₁ + → (var a Tₐ) ∈ Γ₁ + → Tₐ ⊆ Tₒ + ------------------------------------ + → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁ + + +check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (B : Behaviour) → Dec (Γ ⊢B B ▹ Γ₁) +check-B = {!!} diff --git a/src/Variable.agda b/src/Variable.agda index 71aa474..33b0f60 100644 --- a/src/Variable.agda +++ b/src/Variable.agda @@ -6,10 +6,11 @@ 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 (ℕ) -Name : Set -Name = String +Variable : Set +Variable = ℕ data Value : Set where string : String → Value @@ -17,11 +18,4 @@ data Value : Set where bool : Bool → Value double : ℤ × ℤ → Value long : ℤ → Value - -data Variable : Set where - leaf : Name → Value → Variable - node : Name → Maybe Value → List Variable → Variable - -root : Variable → Name -root (leaf n _) = n -root (node n _ _) = n + void : Value -- 2.50.1