-
Notifications
You must be signed in to change notification settings - Fork 0
/
Transition.agda
53 lines (44 loc) · 3.35 KB
/
Transition.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
module Transition where
open import ProofRelevantPiCommon
open import Action as ᴬ using (Action; Actionᵇ; Actionᶜ; _ᵇ; _ᶜ; inc); open ᴬ.Actionᵇ; open ᴬ.Actionᶜ
import Action.Ren
open import Name as ᴺ using (Name; _+_; suc; zero; toℕ)
open import Proc as ᴾ using (Proc); open ᴾ.Proc
import Proc.Ren
open import Ren as ᴿ using (push; pop; swap; Renameable); open ᴿ.Renameable ⦃...⦄
-- Transitions carry an explicit size index so we can define residuals to be size-preserving. Symmetric
-- variants of _│•_ and _│ᵥ_ are omitted.
data _—[_-_]→_ {Γ} : Proc Γ → (a : Action Γ) → Size → Proc (Γ + inc a) → Set where
_•∙_ : ∀ {ι} (x : Name Γ) (P : Proc (Γ + 1)) → x •∙ P —[ x • ᵇ - ↑ ι ]→ P
•_〈_〉∙_ : ∀ {ι} (x y : Name Γ) (P : Proc Γ) → • x 〈 y 〉∙ P —[ • x 〈 y 〉 ᶜ - ↑ ι ]→ P
_➕₁_ : ∀ {ι P} {a : Action Γ} {R} → P —[ a - ι ]→ R → (Q : Proc Γ) → P ➕ Q —[ a - ↑ ι ]→ R
_ᵇ│_ : ∀ {ι P} {a : Actionᵇ Γ} {R} → P —[ a ᵇ - ι ]→ R → (Q : Proc Γ) → P │ Q —[ a ᵇ - ↑ ι ]→ R │ (push *) Q
_ᶜ│_ : ∀ {ι P} {a : Actionᶜ Γ} {R} → P —[ a ᶜ - ι ]→ R → (Q : Proc Γ) → P │ Q —[ a ᶜ - ↑ ι ]→ R │ Q
_│ᵇ_ : ∀ {ι Q} {a : Actionᵇ Γ} {S} → (P : Proc Γ) → Q —[ a ᵇ - ι ]→ S → P │ Q —[ a ᵇ - ↑ ι ]→ (push *) P │ S
_│ᶜ_ : ∀ {ι Q} {a : Actionᶜ Γ} {S} → (P : Proc Γ) → Q —[ a ᶜ - ι ]→ S → P │ Q —[ a ᶜ - ↑ ι ]→ P │ S
_│•_ : ∀ {ι P R Q S} {x y : Name Γ} →
P —[ x • ᵇ - ι ]→ R → Q —[ • x 〈 y 〉 ᶜ - ι ]→ S → P │ Q —[ τ ᶜ - ↑ ι ]→ (pop y *) R │ S
-- Being explicit about the substitution 0 ↦ 0 makes life _way_ easier when defining slicing.
_│ᵥ_ : ∀ {ι P R Q S} {x : Name Γ} → P —[ x • ᵇ - ι ]→ R → Q —[ (• x) ᵇ - ι ]→ S →
P │ Q —[ τ ᶜ - ↑ ι ]→ ν ((id *) R │ S)
ν•_ : ∀ {ι P R} {x : Name Γ} → P —[ • suc x 〈 zero 〉 ᶜ - ι ]→ R → ν P —[ (• x) ᵇ - ↑ ι ]→ R
νᵇ_ : ∀ {ι P R} {a : Actionᵇ Γ} → P —[ (push *) a ᵇ - ι ]→ R → ν P —[ a ᵇ - ↑ ι ]→ ν (swap *) R
νᶜ_ : ∀ {ι P R} {a : Actionᶜ Γ} → P —[ (push *) a ᶜ - ι ]→ R → ν P —[ a ᶜ - ↑ ι ]→ ν R
!_ : ∀ {ι P} {a : Action Γ} {R} → P │ ! P —[ a - ι ]→ R → ! P —[ a - ↑ ι ]→ R
infixl 0 _—[_-_]→_
infixl 6 _➕₁_ _ᵇ│_ _ᶜ│_ _│ᵇ_ _│ᶜ_ _│•_ _│ᵥ_
infixr 7 _•∙_ •_〈_〉∙_
src : ∀ {ι Γ P} {a : Action Γ} {R} → P —[ a - ι ]→ R → Proc Γ
src {P = P} _ = P
out : ∀ {ι Γ P} {a : Action Γ} {R} → P —[ a - ι ]→ R → Σ[ a′ ∈ Action Γ ] Proc (Γ + inc a′)
out {a = a} {R} _ = a , R
action : ∀ {ι Γ P} {a : Action Γ} {R} → P —[ a - ι ]→ R → Action Γ
action = π₁ ∘ out
tgt : ∀ {ι Γ P} {a : Action Γ} {R} → P —[ a - ι ]→ R → Proc (Γ + inc a)
tgt = π₂ ∘ out
-- Existentially quantified version.
record TransitionFrom {Γ} (P : Proc Γ) : Set where
field
a : Action _
R : Proc _
E : P —[ a - _ ]→ R