1 files changed, 73 insertions, 82 deletions

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index 1cd57a7..f37694b 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -1,104 +1,95 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Function
-open import Relation.Binary
-import Relation.Binary.PropositionalEquality as ≡
+open import Relation.Binary using (REL; Setoid)
 
 module Cfe.Expression.Base
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid over renaming (Carrier to C)
+open Setoid over using () renaming (Carrier to C)
 
-open import Cfe.Language over as 𝕃
-open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ₗ_)
-open import Cfe.Language.Construct.Single over
-open import Cfe.Language.Construct.Union over
-open import Cfe.Language.Indexed.Construct.Iterate over
-open import Data.Fin as F hiding (_≤_; cast)
-open import Data.Nat as ℕ hiding (_≤_; _⊔_)
-open import Data.Product
+open import Cfe.Language over renaming (_∙_ to _∙ˡ_; _≈_ to _≈ˡ_)
+open import Data.Fin hiding (_+_; _<_)
+open import Data.Nat hiding (_≟_; _⊔_)
 open import Data.Vec
-open import Level renaming (suc to lsuc) hiding (Lift)
-open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary
+open import Function using (_on_)
+open import Relation.Nullary using (yes; no)
 
-infix 10 _[_/_]
+private
+  variable
+    m n : ℕ
+
+------------------------------------------------------------------------
+-- Definition
+
+infix 8 μ_
 infix 7 _∙_
 infix 6 _∨_
-infix 4 _≋_
 
 data Expression : ℕ → Set c where
-  ⊥ : ∀ {n} → Expression n
-  ε : ∀ {n} → Expression n
-  Char : ∀ {n} → C → Expression n
-  _∨_ : ∀ {n} → Expression n → Expression n → Expression n
-  _∙_ : ∀ {n} → Expression n → Expression n → Expression n
-  Var : ∀ {n} → Fin n → Expression n
-  μ : ∀ {n} → Expression (suc n) → Expression n
-
-cast : ∀ {m n} → .(_ : m ≡ n) → Expression m → Expression n
-cast eq ⊥ = ⊥
-cast eq ε = ε
-cast eq (Char x) = Char x
-cast eq (e₁ ∨ e₂) = cast eq e₁ ∨ cast eq e₂
-cast eq (e₁ ∙ e₂) = cast eq e₁ ∙ cast eq e₂
-cast eq (Var i) = Var (F.cast eq i)
-cast eq (μ e) = μ (cast (cong suc eq) e)
-
-wkn : ∀ {n} → Expression n → Fin (suc n) → Expression (suc n)
-wkn ⊥ i = ⊥
-wkn ε i = ε
-wkn (Char x) i = Char x
+  ⊥    : Expression n
+  ε    : Expression n
+  Char : (c : C) → Expression n
+  _∨_  : Expression n → Expression n → Expression n
+  _∙_  : Expression n → Expression n → Expression n
+  Var  : (j : Fin n) → Expression n
+  μ_   : Expression (suc n) → Expression n
+
+------------------------------------------------------------------------
+-- Semantics
+
+infix 4 _≈_
+
+⟦_⟧ : Expression n → Vec (Language _) n → Language _
+⟦ ⊥ ⟧       _ = ∅
+⟦ ε ⟧       _ = ｛ε｝ {ℓ}
+⟦ Char x ⟧  _ = ｛ x ｝
+⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ
+⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ˡ ⟦ e₂ ⟧ γ
+⟦ Var n ⟧   γ = lookup γ n
+⟦ μ e ⟧     γ = ⋃ (λ X → ⟦ e ⟧ (X ∷ γ))
+
+_≈_ : {n : ℕ} → Expression n → Expression n → Set _
+e₁ ≈ e₂ = ∀ γ → ⟦ e₁ ⟧ γ ≈ˡ ⟦ e₂ ⟧ γ
+
+------------------------------------------------------------------------
+-- Syntax manipulation
+
+infix 10 _[_/_]
+
+wkn : Expression n → Fin (suc n) → Expression (suc n)
+wkn ⊥         i = ⊥
+wkn ε         i = ε
+wkn (Char c)  i = Char c
 wkn (e₁ ∨ e₂) i = wkn e₁ i ∨ wkn e₂ i
 wkn (e₁ ∙ e₂) i = wkn e₁ i ∙ wkn e₂ i
-wkn (Var x) i = Var (punchIn i x)
-wkn (μ e) i = μ (wkn e (suc i))
+wkn (Var j)   i = Var (punchIn i j)
+wkn (μ e)     i = μ wkn e (suc i)
 
-_[_/_] : ∀ {n} → Expression (suc n) → Expression n → Fin (suc n) → Expression n
-⊥ [ e′ / i ] = ⊥
-ε [ e′ / i ] = ε
-Char x [ e′ / i ] = Char x
+_[_/_] : Expression (suc n) → Expression n → Fin (suc n) → Expression n
+⊥         [ e′ / i ] = ⊥
+ε         [ e′ / i ] = ε
+Char x    [ e′ / i ] = Char x
 (e₁ ∨ e₂) [ e′ / i ] = e₁ [ e′ / i ] ∨ e₂ [ e′ / i ]
 (e₁ ∙ e₂) [ e′ / i ] = e₁ [ e′ / i ] ∙ e₂ [ e′ / i ]
-Var j [ e′ / i ] with i F.≟ j
-... | yes i≡j = e′
-... | no i≢j = Var (punchOut i≢j)
-μ e [ e′ / i ] = μ (e [ wkn e′ F.zero / suc i ])
-
-rotate : ∀ {n} → Expression n → (i j : Fin n) → .(_ : i F.≤ j) → Expression n
-rotate ⊥ _ _ _ = ⊥
-rotate ε _ _ _ = ε
-rotate (Char x) _ _ _ = Char x
-rotate (e₁ ∨ e₂) i j i≤j = rotate e₁ i j i≤j ∨ rotate e₂ i j i≤j
-rotate (e₁ ∙ e₂) i j i≤j = rotate e₁ i j i≤j ∙ rotate e₂ i j i≤j
-rotate {suc n} (Var k) i j _ with i F.≟ k
-... | yes i≡k = Var j
-... | no i≢k = Var (punchIn j (punchOut i≢k))
-rotate (μ e) i j i≤j = μ (rotate e (suc i) (suc j) (s≤s i≤j))
-
-⟦_⟧ : ∀ {n : ℕ} → Expression n → Vec (Language (c ⊔ ℓ)) n → Language (c ⊔ ℓ)
-⟦ ⊥ ⟧ _ = Lift (c ⊔ ℓ) ∅
-⟦ ε ⟧ _ = Lift ℓ ｛ε｝
-⟦ Char x ⟧ _ = Lift ℓ ｛ x ｝
-⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ
-⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ₗ ⟦ e₂ ⟧ γ
-⟦ Var n ⟧ γ = lookup γ n
-⟦ μ e ⟧ γ = ⋃ (λ X → ⟦ e ⟧ (X ∷ γ))
-
-_≋_ : {n : ℕ} → Expression n → Expression n → Set (lsuc (c ⊔ ℓ))
-e₁ ≋ e₂ = ∀ γ → ⟦ e₁ ⟧ γ 𝕃.≈ ⟦ e₂ ⟧ γ
-
-rank : {n : ℕ} → Expression n → ℕ
-rank ⊥ = 0
-rank ε = 0
-rank (Char _) = 0
-rank (e₁ ∨ e₂) = suc (rank e₁ ℕ.+ rank e₂)
-rank (e₁ ∙ _) = suc (rank e₁)
-rank (Var _) = 0
-rank (μ e) = suc (rank e)
+Var j     [ e′ / i ] with i ≟ j
+...                     | yes i≡j = e′
+...                     | no  i≢j = Var (punchOut i≢j)
+(μ e)     [ e′ / i ] = μ e [ wkn e′ zero / suc i ]
+
+------------------------------------------------------------------------
+-- Syntax properties
 
 infix 4 _<ᵣₐₙₖ_
 
-_<ᵣₐₙₖ_ : ∀ {n} → Rel (Expression n) _
-_<ᵣₐₙₖ_ = ℕ._<_ on rank
+rank : Expression n → ℕ
+rank ⊥         = 0
+rank ε         = 0
+rank (Char _)  = 0
+rank (e₁ ∨ e₂) = suc (rank e₁ + rank e₂)
+rank (e₁ ∙ _)  = suc (rank e₁)
+rank (Var _)   = 0
+rank (μ e)     = suc (rank e)
+
+_<ᵣₐₙₖ_ : REL (Expression m) (Expression n) _
+e <ᵣₐₙₖ e′ = rank e < rank e′