diff options
Diffstat (limited to 'src/Cfe/Expression/Base.agda')
| -rw-r--r-- | src/Cfe/Expression/Base.agda | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda index 2023a71..c3367c2 100644 --- a/src/Cfe/Expression/Base.agda +++ b/src/Cfe/Expression/Base.agda @@ -66,16 +66,16 @@ Var j [ e′ / i ] with i F.≟ j ... | no i≢j = Var (punchOut i≢j) μ e [ e′ / i ] = μ (e [ wkn e′ F.zero / suc i ]) -shift : ∀ {n} → Expression n → (i j : Fin n) → .(_ : i F.≤ j) → Expression n -shift ⊥ _ _ _ = ⊥ -shift ε _ _ _ = ε -shift (Char x) _ _ _ = Char x -shift (e₁ ∨ e₂) i j i≤j = shift e₁ i j i≤j ∨ shift e₂ i j i≤j -shift (e₁ ∙ e₂) i j i≤j = shift e₁ i j i≤j ∙ shift e₂ i j i≤j -shift {suc n} (Var k) i j _ with i F.≟ k +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)) -shift (μ e) i j i≤j = μ (shift e (suc i) (suc j) (s≤s i≤j)) +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 ⊔ ℓ) ∅ |