diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-04-24 15:30:30 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-04-24 15:30:30 +0100 |
| commit | 0708355c7988345c98961cad087dc56eeb16ea7f (patch) | |
| tree | 76f4e4ef3f7a0eb0cf3f40d3d58e3563287044c4 /src/Cfe/Derivation/Base.agda | |
| parent | c58866bea6ee251868d98a3da11f64030bb00aa7 (diff) | |
Cleanup Derivation.cleanup
Diffstat (limited to 'src/Cfe/Derivation/Base.agda')
| -rw-r--r-- | src/Cfe/Derivation/Base.agda | 54 |
1 files changed, 29 insertions, 25 deletions
diff --git a/src/Cfe/Derivation/Base.agda b/src/Cfe/Derivation/Base.agda index ce368d0..0432c3d 100644 --- a/src/Cfe/Derivation/Base.agda +++ b/src/Cfe/Derivation/Base.agda @@ -8,37 +8,41 @@ module Cfe.Derivation.Base open Setoid over renaming (Carrier to C; _≈_ to _∼_) -open import Cfe.Expression over hiding (_≋_) -open import Data.Fin -open import Data.List -open import Data.List.Relation.Binary.Equality.Setoid over +open import Cfe.Expression over hiding (_≈_) +open import Data.Fin using (zero) +open import Data.List using (List; []; [_]; _++_) +open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_) open import Level using (_⊔_) infix 5 _⤇_ infix 4 _≈_ data _⤇_ : Expression 0 → List C → Set (c ⊔ ℓ) where - Eps : ε ⤇ [] + Eps : ε ⤇ [] Char : ∀ {c y} → (c∼y : c ∼ y) → Char c ⤇ [ y ] - Cat : ∀ {e₁ e₂ l₁ l₂ l} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → l₁ ++ l₂ ≋ l → e₁ ∙ e₂ ⤇ l - Veeˡ : ∀ {e₁ e₂ l} → e₁ ⤇ l → e₁ ∨ e₂ ⤇ l - Veeʳ : ∀ {e₁ e₂ l} → e₂ ⤇ l → e₁ ∨ e₂ ⤇ l - Fix : ∀ {e l} → e [ μ e / zero ] ⤇ l → μ e ⤇ l + Cat : ∀ {e₁ e₂ w₁ w₂ w} → e₁ ⤇ w₁ → e₂ ⤇ w₂ → w₁ ++ w₂ ≋ w → e₁ ∙ e₂ ⤇ w + Veeˡ : ∀ {e₁ e₂ w} → e₁ ⤇ w → e₁ ∨ e₂ ⤇ w + Veeʳ : ∀ {e₁ e₂ w} → e₂ ⤇ w → e₁ ∨ e₂ ⤇ w + Fix : ∀ {e w} → e [ μ e / zero ] ⤇ w → μ e ⤇ w -data _≈_ : ∀ {e l l′} → REL (e ⤇ l) (e ⤇ l′) (c ⊔ ℓ) where - Eps : Eps ≈ Eps +data _≈_ : ∀ {e w w′} → REL (e ⤇ w) (e ⤇ w′) (c ⊔ ℓ) where + Eps : Eps ≈ Eps Char : ∀ {c y y′} → (c∼y : c ∼ y) → (c∼y′ : c ∼ y′) → Char c∼y ≈ Char c∼y′ - Cat : ∀ {e₁ e₂ l l₁ l₂ l₁′ l₂′ e₁⤇l₁ e₁⤇l₁′ e₂⤇l₂ e₂⤇l₂′} → - (e₁⤇l₁≈e₁⤇l′ : _≈_ {e₁} {l₁} {l₁′} e₁⤇l₁ e₁⤇l₁′) → - (e₂⤇l₂≈e₂⤇l′ : _≈_ {e₂} {l₂} {l₂′} e₂⤇l₂ e₂⤇l₂′) → - (eq : l₁ ++ l₂ ≋ l) → (eq′ : l₁′ ++ l₂′ ≋ l) → - Cat e₁⤇l₁ e₂⤇l₂ eq ≈ Cat e₁⤇l₁′ e₂⤇l₂′ eq′ - Veeˡ : ∀ {e₁ e₂ l l′ e₁⤇l e₁⤇l′} → - (e₁⤇l≈e₁⤇l′ : _≈_ {e₁} {l} {l′} e₁⤇l e₁⤇l′) → - Veeˡ {e₂ = e₂} e₁⤇l ≈ Veeˡ e₁⤇l′ - Veeʳ : ∀ {e₁ e₂ l l′ e₂⤇l e₂⤇l′} → - (e₂⤇l≈e₂⤇l′ : _≈_ {e₂} {l} {l′} e₂⤇l e₂⤇l′) → - Veeʳ {e₁} e₂⤇l ≈ Veeʳ e₂⤇l′ - Fix : ∀ {e l l′ e[μe/0]⤇l e[μe/0]⤇l′} → - (e[μe/0]⤇l≈e[μe/0]⤇l′ : _≈_ {e [ μ e / zero ]} {l} {l′} e[μe/0]⤇l e[μe/0]⤇l′) → - Fix {e} e[μe/0]⤇l ≈ Fix e[μe/0]⤇l′ + Cat : + ∀ {e₁ e₂ w w₁ w₂ w₁′ w₂′ e₁⤇w₁ e₁⤇w₁′ e₂⤇w₂ e₂⤇w₂′} → + (e₁⤇w₁≈e₁⤇w′ : _≈_ {e₁} {w₁} {w₁′} e₁⤇w₁ e₁⤇w₁′) → + (e₂⤇w₂≈e₂⤇w′ : _≈_ {e₂} {w₂} {w₂′} e₂⤇w₂ e₂⤇w₂′) → + (eq : w₁ ++ w₂ ≋ w) → (eq′ : w₁′ ++ w₂′ ≋ w) → + Cat e₁⤇w₁ e₂⤇w₂ eq ≈ Cat e₁⤇w₁′ e₂⤇w₂′ eq′ + Veeˡ : + ∀ {e₁ e₂ w w′ e₁⤇w e₁⤇w′} → + (e₁⤇w≈e₁⤇w′ : _≈_ {e₁} {w} {w′} e₁⤇w e₁⤇w′) → + Veeˡ {e₂ = e₂} e₁⤇w ≈ Veeˡ e₁⤇w′ + Veeʳ : + ∀ {e₁ e₂ w w′ e₂⤇w e₂⤇w′} → + (e₂⤇w≈e₂⤇w′ : _≈_ {e₂} {w} {w′} e₂⤇w e₂⤇w′) → + Veeʳ {e₁} e₂⤇w ≈ Veeʳ e₂⤇w′ + Fix : + ∀ {e w w′ e[μe/0]⤇w e[μe/0]⤇w′} → + (e[μe/0]⤇w≈e[μe/0]⤇w′ : _≈_ {e [ μ e / zero ]} {w} {w′} e[μe/0]⤇w e[μe/0]⤇w′) → + Fix {e} e[μe/0]⤇w ≈ Fix e[μe/0]⤇w′ |