Rename typecheck to typingbehaviour

diff --git a/src/Typecheck.agda b/src/TypingBehaviour.agda
similarity index 86%
rename from src/Typecheck.agda
rename to src/TypingBehaviour.agda
index 48a8ad3e0f4e064b1f082c9be2058f26fb9d8015..1ac75744fd6a585478564c16dcf28e6d97db52b0 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/TypingBehaviour.agda
@@ -1,11 +1,11 @@
-module Typecheck where
+module TypingBehaviour where
 
 open import Data.List.All using (All)
 open import Relation.Nullary using (¬_)
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl; sym; trans)
 open import Data.Nat using (ℕ; _+_; suc; _≟_)
 open import Data.List using (List)
-open import Data.Vec using (_∈_; []; _++_; _∷_)
+open import Data.Vec using (_∈_; []; _++_; _∷_; here; there)
 open import Data.Product using (_,_; _×_)
 open import Function
 open import Expr
@@ -149,8 +149,20 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
          ------------------------
          → Γ ⊢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
+struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → b1 ≡ b2 → Γ ⊢B b2 ▹ Γ₁
+struct-congruence t refl = t
+
+struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (seq nil b) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
+struct-cong-nil (t-seq t-nil t) = t
+
+struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
+struct-cong-par-nil (t-par t t-nil) = {!!}
+
+struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁
+struct-cong-par-sym (t-par t₁ t₂) = {!!}
+
+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) ▹ Γ₁
+struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!}
 
 data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
   updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
@@ -160,4 +172,5 @@ data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
 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 Γ Γ₁)= {!!}
+--preservation t-nil (updated {_} {k} Γ Γₐ) = t-nil {k} {Γₐ}
+preservation = {!!}