summaryrefslogtreecommitdiff
path: root/src/Cfe/Expression
diff options
context:
space:
mode:
Diffstat (limited to 'src/Cfe/Expression')
-rw-r--r--src/Cfe/Expression/Base.agda19
-rw-r--r--src/Cfe/Expression/Properties.agda70
2 files changed, 40 insertions, 49 deletions
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index f4a8dc0..2023a71 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -66,10 +66,21 @@ 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 ])
-⟦_⟧ : ∀ {n : ℕ} → Expression n → Vec (Language (c ⊔ ℓ) (c ⊔ ℓ)) n → Language (c ⊔ ℓ) (c ⊔ ℓ)
-⟦ ⊥ ⟧ _ = Lift (c ⊔ ℓ) (c ⊔ ℓ) ∅
-⟦ ε ⟧ _ = Lift ℓ (c ⊔ ℓ) ｛ε｝
-⟦ Char x ⟧ _ = Lift ℓ (c ⊔ ℓ) ｛ x ｝
+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
+... | 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))
+
+⟦_⟧ : ∀ {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
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index 1e41f42..0b1ae2c 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -70,14 +70,6 @@ isSemiring n = record
{ (inj₁ (l₁ , l₁∈⟦x⟧ , l₂ , l₂∈⟦y⟧ , l₁++l₂≡l)) → -, l₁∈⟦x⟧ , -, inj₁ l₂∈⟦y⟧ , l₁++l₂≡l
; (inj₂ (l₁ , l₁∈⟦x⟧ , l₂ , l₂∈⟦z⟧ , l₁++l₂≡l)) → -, l₁∈⟦x⟧ , -, inj₂ l₂∈⟦z⟧ , l₁++l₂≡l
}
- ; cong₁ = λ
- { (l₁≈l₁′ , ∪.A≈A l₂≈l₂′) → ∪.A≈A (l₁≈l₁′ , l₂≈l₂′)
- ; (l₁≈l₁′ , ∪.B≈B l₂≈l₂′) → ∪.B≈B (l₁≈l₁′ , l₂≈l₂′)
- }
- ; cong₂ = λ
- { (∪.A≈A (l₁≈l₁′ , l₂≈l₂′)) → l₁≈l₁′ , ∪.A≈A l₂≈l₂′
- ; (∪.B≈B (l₁≈l₁′ , l₂≈l₂′)) → l₁≈l₁′ , ∪.B≈B l₂≈l₂′
- }
}) , (λ x y z γ → record
{ f = λ
{ (l₁ , inj₁ l₁∈⟦y⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l) → inj₁ (-, l₁∈⟦y⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l)
@@ -87,34 +79,22 @@ isSemiring n = record
{ (inj₁ (l₁ , l₁∈⟦y⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l)) → -, inj₁ l₁∈⟦y⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l
; (inj₂ (l₁ , l₁∈⟦z⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l)) → -, inj₂ l₁∈⟦z⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l
}
- ; cong₁ = λ
- { (∪.A≈A l₁≈l₁′ , l₂≈l₂′) → ∪.A≈A (l₁≈l₁′ , l₂≈l₂′)
- ; (∪.B≈B l₁≈l₁′ , l₂≈l₂′) → ∪.B≈B (l₁≈l₁′ , l₂≈l₂′)
- }
- ; cong₂ = λ
- { (∪.A≈A (l₁≈l₁′ , l₂≈l₂′)) → ∪.A≈A l₁≈l₁′ , l₂≈l₂′
- ; (∪.B≈B (l₁≈l₁′ , l₂≈l₂′)) → ∪.B≈B l₁≈l₁′ , l₂≈l₂′
- }
})
}
; zero = (λ x γ → record
{ f = λ ()
; f⁻¹ = λ ()
- ; cong₁ = λ {_} {_} {l₁∈⟦⊥∙x⟧} → case l₁∈⟦⊥∙x⟧ of (λ ())
- ; cong₂ = λ {_} {_} {l₁∈⟦⊥⟧} → case l₁∈⟦⊥⟧ of (λ ())
}) , (λ x γ → record
{ f = λ ()
; f⁻¹ = λ ()
- ; cong₁ = λ {_} {_} {l₁∈⟦x∙⊥⟧} → case l₁∈⟦x∙⊥⟧ of (λ ())
- ; cong₂ = λ {_} {_} {l₁∈⟦⊥⟧} → case l₁∈⟦⊥⟧ of (λ ())
})
}
where
- module ∪-comm = IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ})
- module ∙-mon = IsMonoid (∙.isMonoid {ℓ} {c ⊔ ℓ})
+ module ∪-comm = IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ})
+ module ∙-mon = IsMonoid (∙.isMonoid {ℓ})
module _ where
- open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+ open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ)) as VE
open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
cong-env : ∀ {n} → (e : Expression n) → ∀ {γ γ′} → γ VE.≋ γ′ → ⟦ e ⟧ γ ≈ ⟦ e ⟧ γ′
@@ -123,10 +103,10 @@ module _ where
cong-env (Char x) γ≈γ′ = ≈-refl
cong-env (e₁ ∨ e₂) γ≈γ′ = ∪-cong (cong-env e₁ γ≈γ′) (cong-env e₂ γ≈γ′)
where
- open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+ open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
cong-env (e₁ ∙ e₂) γ≈γ′ = ∙-cong (cong-env e₁ γ≈γ′) (cong-env e₂ γ≈γ′)
where
- open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+ open IsMonoid (∙.isMonoid {c ⊔ ℓ})
cong-env (Var j) γ≈γ′ = PW.lookup γ≈γ′ j
cong-env (μ e) γ≈γ′ = ⋃.⋃-cong (λ x → cong-env e (x PW.∷ γ≈γ′))
@@ -136,16 +116,16 @@ wkn-no-use ε i γ = ≈-refl
wkn-no-use (Char x) i γ = ≈-refl
wkn-no-use (e₁ ∨ e₂) i γ = ∪-cong (wkn-no-use e₁ i γ) (wkn-no-use e₂ i γ)
where
- open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+ open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
wkn-no-use (e₁ ∙ e₂) i γ = ∙-cong (wkn-no-use e₁ i γ) (wkn-no-use e₂ i γ)
where
- open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+ open IsMonoid (∙.isMonoid {c ⊔ ℓ})
wkn-no-use (Var j) i γ = reflexive (begin
lookup γ (punchIn i j) ≡˘⟨ ≡.cong (λ x → lookup x (punchIn i j)) (insert-remove γ i) ⟩
lookup (insert (remove γ i) i (lookup γ i)) (punchIn i j) ≡⟨ insert-punchIn (remove γ i) i (lookup γ i) j ⟩
lookup (remove γ i) j ∎)
where
- open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+ open IsEquivalence (≈-isEquivalence {c ⊔ ℓ})
open ≡.≡-Reasoning
wkn-no-use (μ e) i (z ∷ γ) = ⋃.⋃-cong (λ {x} {y} x≈y → begin
⟦ wkn e (suc i) ⟧ (x ∷ z ∷ γ) ≈⟨ cong-env (wkn e (suc i)) (x≈y ∷ ≋-refl) ⟩
@@ -153,8 +133,8 @@ wkn-no-use (μ e) i (z ∷ γ) = ⋃.⋃-cong (λ {x} {y} x≈y → begin
⟦ e ⟧ (remove (y ∷ z ∷ γ) (suc i)) ≡⟨⟩
⟦ e ⟧ (y ∷ remove (z ∷ γ) i) ∎)
where
- open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ))
- open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+ open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ))
+ open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ)) as VE
subst-fun : ∀ {n} → (e : Expression (suc n)) → ∀ e′ i γ → ⟦ e [ e′ / i ] ⟧ γ ≈ ⟦ e ⟧ (insert γ i (⟦ e′ ⟧ γ))
subst-fun ⊥ e′ i γ = ≈-refl
@@ -162,42 +142,42 @@ subst-fun ε e′ i γ = ≈-refl
subst-fun (Char x) e′ i γ = ≈-refl
subst-fun {n} (e₁ ∨ e₂) e′ i γ = ∪-cong (subst-fun e₁ e′ i γ) (subst-fun e₂ e′ i γ)
where
- open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+ open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
subst-fun (e₁ ∙ e₂) e′ i γ = ∙-cong (subst-fun e₁ e′ i γ) (subst-fun e₂ e′ i γ)
where
- open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+ open IsMonoid (∙.isMonoid {c ⊔ ℓ})
subst-fun (Var j) e′ i γ with i F.≟ j
... | yes _≡_.refl = sym (reflexive (insert-lookup γ i (⟦ e′ ⟧ γ)))
where
- open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+ open IsEquivalence (≈-isEquivalence {c ⊔ ℓ})
... | no i≢j = reflexive (begin
lookup γ (punchOut i≢j) ≡˘⟨ ≡.cong (λ x → lookup x (punchOut i≢j)) (remove-insert γ i (⟦ e′ ⟧ γ)) ⟩
lookup (remove (insert γ i (⟦ e′ ⟧ γ)) i) (punchOut i≢j) ≡⟨ remove-punchOut (insert γ i (⟦ e′ ⟧ γ)) i≢j ⟩
lookup (insert γ i (⟦ e′ ⟧ γ)) j ∎)
where
open ≡.≡-Reasoning
- open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+ open IsEquivalence (≈-isEquivalence {c ⊔ ℓ})
subst-fun (μ e) e′ i γ = ⋃.⋃-cong λ {x} {y} x≈y → begin
⟦ e [ wkn e′ F.zero / suc i ] ⟧ (x ∷ γ) ≈⟨ cong-env (e [ wkn e′ F.zero / suc i ]) (x≈y ∷ ≋-refl) ⟩
⟦ e [ wkn e′ F.zero / suc i ] ⟧ (y ∷ γ) ≈⟨ subst-fun e (wkn e′ F.zero) (suc i) (y ∷ γ) ⟩
⟦ e ⟧ (y ∷ insert γ i (⟦ wkn e′ F.zero ⟧ (y ∷ γ))) ≈⟨ cong-env e (≈-refl ∷ insert′ (wkn-no-use e′ F.zero (y ∷ γ)) ≋-refl i) ⟩
⟦ e ⟧ (y ∷ insert γ i (⟦ e′ ⟧ γ)) ∎
where
- open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ))
- open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+ open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ))
+ open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ)) as VE
- insert′ : ∀ {n x y} {xs ys : Vec (Language (c ⊔ ℓ) (c ⊔ ℓ)) n} → x ≈ y → xs VE.≋ ys → (i : Fin (suc n)) → insert xs i x VE.≋ insert ys i y
+ insert′ : ∀ {n x y} {xs ys : Vec (Language (c ⊔ ℓ)) n} → x ≈ y → xs VE.≋ ys → (i : Fin (suc n)) → insert xs i x VE.≋ insert ys i y
insert′ x≈y xs≋ys F.zero = x≈y ∷ xs≋ys
insert′ x≈y (z≈w ∷ xs≋ys) (suc i) = z≈w ∷ insert′ x≈y xs≋ys i
-monotone : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
-monotone ⊥ γ≤γ′ = L.≤-refl
-monotone ε γ≤γ′ = L.≤-refl
-monotone (Char x) γ≤γ′ = L.≤-refl
-monotone (e₁ ∨ e₂) γ≤γ′ = ∪.∪-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
-monotone (e₁ ∙ e₂) γ≤γ′ = ∙.∙-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
-monotone (Var i) γ≤γ′ = PW.lookup γ≤γ′ i
-monotone (μ e) γ≤γ′ = ⋃.⋃-monotone (λ x≤y → monotone e (x≤y PW.∷ γ≤γ′))
+mono : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
+mono ⊥ γ≤γ′ = L.≤-refl
+mono ε γ≤γ′ = L.≤-refl
+mono (Char x) γ≤γ′ = L.≤-refl
+mono (e₁ ∨ e₂) γ≤γ′ = ∪.∪-mono (mono e₁ γ≤γ′) (mono e₂ γ≤γ′)
+mono (e₁ ∙ e₂) γ≤γ′ = ∙.∙-mono (mono e₁ γ≤γ′) (mono e₂ γ≤γ′)
+mono (Var i) γ≤γ′ = PW.lookup γ≤γ′ i
+mono (μ e) γ≤γ′ = ⋃.⋃-mono (λ x≤y → mono e (x≤y PW.∷ γ≤γ′))
cast-inverse : ∀ {m n} e → .(m≡n : m ≡ n) → .(n≡m : n ≡ m) → E.cast m≡n (E.cast n≡m e) ≡ e
cast-inverse ⊥ m≡n n≡m = ≡.refl
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 13:41:04 +0000