repos / jolie.agda.git

commit

e5b592a

parent

6abff2b

author

Eugene Akentyev

date

2016-12-27 19:14:26 +0400 +04

Rename typecheck to typingbehaviour

 1@@ -1,11 +1,11 @@
 2-module Typecheck where
 3+module TypingBehaviour where
 4 
 5 open import Data.List.All using (All)
 6 open import Relation.Nullary using (¬_)
 7-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
 8+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl; sym; trans)
 9 open import Data.Nat using (ℕ; _+_; suc; _≟_)
10 open import Data.List using (List)
11-open import Data.Vec using (_∈_; []; _++_; _∷_)
12+open import Data.Vec using (_∈_; []; _++_; _∷_; here; there)
13 open import Data.Product using (_,_; _×_)
14 open import Function
15 open import Expr
16@@ -149,8 +149,20 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
17          ------------------------
18          → Γ ⊢B exec r o x b ▹ Γ₁
19 
20-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → b1 ≡ b2 → Γ ⊢B b2 ▹ Γ₁
21-congruence t refl = t
22+struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → b1 ≡ b2 → Γ ⊢B b2 ▹ Γ₁
23+struct-congruence t refl = t
24+
25+struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (seq nil b) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
26+struct-cong-nil (t-seq t-nil t) = t
27+
28+struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
29+struct-cong-par-nil (t-par t t-nil) = {!!}
30+
31+struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁
32+struct-cong-par-sym (t-par t₁ t₂) = {!!}
33+
34+struct-cong-par-assoc : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 b3 : Behaviour} → Γ ⊢B par (par b1 b2) b3 ▹ Γ₁ → Γ ⊢B par b1 (par b2 b3) ▹ Γ₁
35+struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!}
36 
37 data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
38   updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
39@@ -160,4 +172,5 @@ data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
40 preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁ 
41 preservation t undefined = t
42 preservation t (identity γ) = t
43-preservation t (updated Γ Γ₁)= {!!}
44+--preservation t-nil (updated {_} {k} Γ Γₐ) = t-nil {k} {Γₐ}
45+preservation = {!!}