blob: 74854df0178f7df8a2bfd6b335688176cead0b45 (
plain)
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary as B using (Setoid)
module Cfe.Language.Base
{c ℓ} (over : Setoid c ℓ)
where
open Setoid over using () renaming (Carrier to C)
open import Algebra
open import Data.Empty
open import Data.List hiding (null)
open import Data.Product
open import Data.Unit using (⊤; tt)
open import Function hiding (Injection; Surjection; Inverse)
import Function.Equality as Equality using (setoid)
open import Level as L hiding (Lift)
open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Relation.Binary.Indexed.Heterogeneous
infix 4 _∈_
infix 4 _∉_
Language : ∀ a aℓ → Set (suc c ⊔ suc a ⊔ suc aℓ)
Language a aℓ = IndexedSetoid (List C) a aℓ
∅ : Language 0ℓ 0ℓ
∅ = Trivial.indexedSetoid (≡.setoid ⊥)
｛ε｝ : Language c 0ℓ
｛ε｝ = record
{ Carrier = [] ≡_
; _≈_ = λ _ _ → ⊤
; isEquivalence = record
{ refl = tt
; sym = λ _ → tt
; trans = λ _ _ → tt
}
}
Lift : ∀ {a aℓ} → (b bℓ : Level) → Language a aℓ → Language (a ⊔ b) (aℓ ⊔ bℓ)
Lift b bℓ A = record
{ Carrier = L.Lift b ∘ A.Carrier
; _≈_ = λ (lift x) (lift y) → L.Lift bℓ (x A.≈ y)
; isEquivalence = record
{ refl = lift A.refl
; sym = λ (lift x) → lift (A.sym x)
; trans = λ (lift x) (lift y) → lift (A.trans x y)
}
}
where
module A = IndexedSetoid A
𝕃 : ∀ {a aℓ} → Language a aℓ → List C → Set a
𝕃 = IndexedSetoid.Carrier
_∈_ : ∀ {a aℓ} → List C → Language a aℓ → Set a
_∈_ = flip 𝕃
_∉_ : ∀ {a aℓ} → List C → Language a aℓ → Set a
l ∉ A = l ∈ A → ⊥
∈-cong : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → l₁ ≡ l₂ → l₁ ∈ A → l₂ ∈ A
∈-cong A ≡.refl l∈A = l∈A
≈ᴸ : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → 𝕃 A l₁ → 𝕃 A l₂ → Set aℓ
≈ᴸ = IndexedSetoid._≈_
≈ᴸ-refl : ∀ {a aℓ} → (A : Language a aℓ) → Reflexive (𝕃 A) (≈ᴸ A)
≈ᴸ-refl = IsIndexedEquivalence.refl ∘ IndexedSetoid.isEquivalence
≈ᴸ-sym : ∀ {a aℓ} → (A : Language a aℓ) → Symmetric (𝕃 A) (≈ᴸ A)
≈ᴸ-sym = IsIndexedEquivalence.sym ∘ IndexedSetoid.isEquivalence
≈ᴸ-trans : ∀ {a aℓ} → (A : Language a aℓ) → Transitive (𝕃 A) (≈ᴸ A)
≈ᴸ-trans = IsIndexedEquivalence.trans ∘ IndexedSetoid.isEquivalence
≈ᴸ-cong : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂ l₃ l₄} →
(l₁≡l₂ : l₁ ≡ l₂) → (l₃≡l₄ : l₃ ≡ l₄) →
(l₁∈A : l₁ ∈ A) → (l₃∈A : l₃ ∈ A) →
≈ᴸ A l₁∈A l₃∈A →
≈ᴸ A (∈-cong A l₁≡l₂ l₁∈A) (∈-cong A l₃≡l₄ l₃∈A)
≈ᴸ-cong A ≡.refl ≡.refl l₁∈A l₃∈A eq = eq
record _≤_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where
field
f : ∀ {l} → l ∈ A → l ∈ B
cong : ∀ {l₁ l₂ l₁∈A l₂∈A} → ≈ᴸ A {l₁} {l₂} l₁∈A l₂∈A → ≈ᴸ B (f l₁∈A) (f l₂∈A)
record _≈_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (c ⊔ ℓ ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where
field
f : ∀ {l} → l ∈ A → l ∈ B
f⁻¹ : ∀ {l} → l ∈ B → l ∈ A
cong₁ : ∀ {l₁ l₂ l₁∈A l₂∈A} → ≈ᴸ A {l₁} {l₂} l₁∈A l₂∈A → ≈ᴸ B (f l₁∈A) (f l₂∈A)
cong₂ : ∀ {l₁ l₂ l₁∈B l₂∈B} → ≈ᴸ B {l₁} {l₂} l₁∈B l₂∈B → ≈ᴸ A (f⁻¹ l₁∈B) (f⁻¹ l₂∈B)
null : ∀ {a} {aℓ} → Language a aℓ → Set a
null A = [] ∈ A
first : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a)
first A x = ∃[ l ] x ∷ l ∈ A
flast : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a)
flast A x = ∃[ l ] (l ≡.≢ [] × ∃[ l′ ] l ++ x ∷ l′ ∈ A)
|
