repos / jolie.agda.git

commit

0fd4be2

parent

a867bc4

author

Eugene Akentyev

date

2016-12-08 00:40:25 +0400 +04

Inline substCtx

 1@@ -13,9 +13,6 @@ open import Behaviour
 2 open import Variable
 3 
 4 
 5-substCtx : {n m : ℕ} → n ≡ m → Ctx n → Ctx m
 6-substCtx n≡m Γ = subst (λ x → Vec TypeDecl x) n≡m Γ
 7-
 8 data _⊢_∶_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
 9   var-t : {s : Variable} {b : Type}
10         → (var s b) ∈ Γ
11@@ -29,7 +26,7 @@ data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
12 data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
13   t-nil : {n≡m : n ≡ m}
14         ---------------------------
15-        → Γ ⊢B nil ▹ substCtx n≡m Γ
16+        → Γ ⊢B nil ▹ subst Ctx n≡m Γ
17           
18   t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
19        → Γ ⊢ e ∶ bool -- Γ ⊢ e : bool
20@@ -42,7 +39,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
21           → Γ ⊢ e ∶ bool
22           → Γ ⊢B b ▹ Γ
23           --------------------------
24-          → Γ ⊢B while (var e) b ▹ substCtx n≡m Γ
25+          → Γ ⊢B while (var e) b ▹ subst Ctx n≡m Γ
26           
27   t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
28              {b : Behaviour} {behaviours : Vec Behaviour n}
29@@ -71,7 +68,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
30                  → Γ ⊢ e ∶ Tₑ
31                  → Tₑ ⊆ T₀
32                  -------------------------------------------
33-                 → Γ ⊢B output (notification o l (var e)) ▹ substCtx n≡m Γ
34+                 → Γ ⊢B output (notification o l (var e)) ▹ subst Ctx n≡m Γ
35 
36   t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
37                → Γ ⊢ₑ e of Tₑ -- Γ ⊢ e : bool
38@@ -85,7 +82,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
39                   → (var x Tₓ) ∈ Γ
40                   → Tₑ ≡ Tₓ
41                   ---------------------
42-                  → Γ ⊢B assign x e ▹ substCtx n≡m Γ
43+                  → Γ ⊢B assign x e ▹ subst Ctx n≡m Γ
44 
45   t-oneway-new : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
46                → (inOneWay o Tᵢ) ∈ Γ
47@@ -99,7 +96,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
48                   → ((var x Tₓ) ∈ Γ)
49                   → Tᵢ ⊆ Tₓ
50                   --------------------------------
51-                  → Γ ⊢B (input (oneway o x)) ▹ substCtx n≡m Γ
52+                  → Γ ⊢B (input (oneway o x)) ▹ subst Ctx n≡m Γ
53 
54   t-solresp-new : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
55                 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
56@@ -115,7 +112,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
57                    → (var x Tₓ) ∈ Γ
58                    → Tᵢ ⊆ Tₓ
59                    -----------------------------------------
60-                   → Γ ⊢B (output (solicitres o l e x)) ▹ substCtx n≡m Γ
61+                   → Γ ⊢B (output (solicitres o l e x)) ▹ subst Ctx n≡m Γ
62 
63   t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
64                 → (inReqRes o Tᵢ Tₒ) ∈ Γ