repos / jolie.agda.git

commit

cc67ec1

parent

912e12b

author

Eugene Akentyev

date

2016-12-17 19:58:21 +0400 +04

Add t-choice case.

 1@@ -1,8 +1,7 @@
 2 module Behaviour where
 3 
 4-open import Data.Nat using (ℕ)
 5 open import Data.String using (String)
 6-open import Data.Vec using (Vec)
 7+open import Data.List using (List)
 8 open import Data.Product using (_×_)
 9 open import Variable
10 open import Expr
11@@ -28,7 +27,7 @@ data Behaviour where
12   par : Behaviour → Behaviour → Behaviour
13   assign : Variable → Expr → Behaviour
14   nil : Behaviour
15-  inputchoice : {n : ℕ} → Vec (Input_ex × Behaviour) n → Behaviour
16+  inputchoice : List (Input_ex × Behaviour) → Behaviour
17   wait : Channel → Operation → Location → Variable → Behaviour
18   exec : Channel → Operation → Variable → Behaviour → Behaviour
19 

 1@@ -1,12 +1,14 @@
 2 module Typecheck where
 3 
 4-import Data.List as List
 5+open import Data.List.All using (All; all) renaming ([] to []-All; _∷_ to _∷-All_)
 6 import Data.Vec.Equality as VecEq
 7 open import Relation.Nullary using (¬_)
 8 open import Relation.Nullary
 9 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
10 open import Data.Nat using (ℕ; _+_; suc; _≟_)
11-open import Data.Vec using (Vec; _∈_; zip; _∷_; here)
12+open import Data.List using (List; []; _∷_; foldl)
13+open import Data.Vec using (Vec; _∈_; zip; _∷_; here; fromList; toList) renaming ([] to []-Vec)
14+open import Data.Product using (_,_; _×_)
15 open import Function
16 open import Expr
17 open import Type
18@@ -42,13 +44,10 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
19           --------------------------
20           → Γ ⊢B while e b ▹ Γ₁
21           
22-  t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
23-             {b : Behaviour} {behaviours : Vec Behaviour n}
24-           → η ∈ inputs
25-           → b ∈ behaviours
26-           → Γ ⊢B seq (input η) b ▹ Γ₁
27-           ----------------------------------------------
28-           → Γ ⊢B inputchoice (zip inputs behaviours) ▹ Γ₁
29+  t-choice : {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
30+           → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
31+           -----------------------------------------------
32+           → Γ ⊢B inputchoice choices ▹ Γ₁
33 
34   t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
35           {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
36@@ -135,10 +134,12 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
37                    ------------------------------------
38                    → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
39 
40+
41+{-# NON_TERMINATING #-}
42 check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (_⊢B_▹_ {n} {m} Γ b Γ₁)
43 check-B {n} {m} {Γ₁} Γ nil with Γ CtxEq.≟ Γ₁
44 ... | yes Γ≡Γ₁ = yes (t-nil {n} {m} {Γ} {Γ₁} {Γ≡Γ₁})
45-... | no ¬p = no (λ {(t-nil {Γ₁} {Γ≡Γ₁}) → ¬p Γ≡Γ₁})
46+... | no ¬p = no (λ {(t-nil {_} {Γ≡Γ₁}) → ¬p Γ≡Γ₁})
47 check-B {n} {m} {Γ₁} Γ (if e b1 b2) with check-B Γ b1 | check-B Γ b2
48 ... | yes ctx₁ | yes ctx₂ = yes (t-if expr-t ctx₁ ctx₂)
49 ... | yes _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
50@@ -149,5 +150,8 @@ check-B {n} {m} {Γ₁} Γ (while e b) with Γ CtxEq.≟ Γ₁
51   { (yes ctx) → yes (t-while {n} {m} {Γ} {Γ₁} {Γ≡Γ₁} expr-t ctx)
52   ; (no ¬p) → no (λ {(t-while _ ctx) → ¬p ctx})
53   }
54-... | no ¬p = no {!!}
55+... | no ¬p = no (λ {(t-while {_} {Γ≡Γ₁} _ _) → ¬p Γ≡Γ₁})
56+check-B {n} {m} {Γ₁} Γ (inputchoice pairs) with all (λ { (η , b) → check-B {n} {m} {Γ₁} Γ (seq (input η) b) }) pairs
57+... | yes checked = yes (t-choice checked)
58+... | no ¬p = no (λ { (t-choice checked) → ¬p checked })
59 check-B Γ b = {!!}