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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
{-# OPTIONS --safe #-}
module Problem19 where
open import Data.List hiding ([_])
open import Data.Product
open import Data.Empty
open import Data.List.Properties
open import Data.Sum
open import Data.Unit hiding (_≟_)
open import Data.Char
open import Data.Maybe
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality hiding ([_])
data Regex : Set where
∅ : Regex
ε : Regex
[_] : Char → Regex
_∘_ : Regex → Regex → Regex
_∪_ : Regex → Regex → Regex
_⋆ : Regex → Regex
variable c : Char
variable R S : Regex
variable s t : List Char
data Matches : Regex → List Char → Set where
empty : Matches ε []
char : Matches [ c ] (c ∷ [])
comp : Matches R s → Matches S t → Matches (R ∘ S) (s ++ t)
un₁ : Matches R s → Matches (R ∪ S) s
un₂ : Matches S s → Matches (R ∪ S) s
starₑ : Matches (R ⋆) []
starₛ : Matches R s → Matches (R ⋆) t → Matches (R ⋆) (s ++ t)
comp⁻¹ : Matches (R ∘ S) s → ∃₂ λ t₁ t₂ → t₁ ++ t₂ ≡ s × Matches R t₁ × Matches S t₂
comp⁻¹ (comp prf prf₁) = _ , _ , refl , prf , prf₁
star⁻¹′ : Matches (R ⋆) s → s ≡ [] ⊎ ∃[ c ] ∃[ t₁ ] ∃[ t₂ ] c ∷ t₁ ++ t₂ ≡ s × Matches R (c ∷ t₁) × Matches (R ⋆) t₂
star⁻¹′ starₑ = inj₁ refl
star⁻¹′ (starₛ {s = []} prf prf₁) = star⁻¹′ prf₁
star⁻¹′ (starₛ {s = x ∷ s} prf prf₁) = inj₂ (x , s , _ , refl , prf , prf₁)
Nullable : Regex → Set
Nullable ∅ = ⊥
Nullable ε = ⊤
Nullable [ x ] = ⊥
Nullable (r ∘ r₁) = Nullable r × Nullable r₁
Nullable (r ∪ r₁) = Nullable r ⊎ Nullable r₁
Nullable (r ⋆) = ⊤
nullable? : (r : Regex) → Dec (Nullable r)
nullable? ∅ = no (λ x → x)
nullable? ε = yes tt
nullable? [ x ] = no (λ x → x)
nullable? (r ∘ r₁) with nullable? r | nullable? r₁
... | no p | _ = no λ (a , b) → p a
... | _ | no p = no λ (a , b) → p b
... | yes p | yes q = yes (p , q)
nullable? (r ∪ r₁) with nullable? r | nullable? r₁
... | yes p | _ = yes (inj₁ p)
... | _ | yes p = yes (inj₂ p)
... | no p | no q = no λ { (inj₁ a) → p a ; (inj₂ b) → q b }
nullable? (r ⋆) = yes tt
nullable-correct₁ : ∀ R → Nullable R → Matches R []
nullable-correct₁ ε _ = empty
nullable-correct₁ (r ∘ r₁) (null₁ , null₂) = comp (nullable-correct₁ r null₁) (nullable-correct₁ r₁ null₂)
nullable-correct₁ (r ∪ r₁) (inj₁ null) = un₁ (nullable-correct₁ r null)
nullable-correct₁ (r ∪ r₁) (inj₂ null) = un₂ (nullable-correct₁ r₁ null)
nullable-correct₁ (r ⋆) _ = starₑ
st≡[]⇒s≡[] : s ++ t ≡ [] → s ≡ []
st≡[]⇒s≡[] {[]} {t} prf = refl
st≡[]⇒t≡[] : s ++ t ≡ [] → t ≡ []
st≡[]⇒t≡[] {[]} {t} prf = prf
nullable-correct₂′ : ∀ {R} → Matches R s → s ≡ [] → Nullable R
nullable-correct₂′ empty s≡[] = _
nullable-correct₂′ (comp s∈r t∈r₁) st≡[] = nullable-correct₂′ s∈r (st≡[]⇒s≡[] st≡[]) , nullable-correct₂′ t∈r₁ (st≡[]⇒t≡[] st≡[])
nullable-correct₂′ (un₁ s∈r) s≡[] = inj₁ (nullable-correct₂′ s∈r s≡[])
nullable-correct₂′ (un₂ s∈r) s≡[] = inj₂ (nullable-correct₂′ s∈r s≡[])
nullable-correct₂′ starₑ s≡[] = _
nullable-correct₂′ (starₛ s∈r s∈r₁) s≡[] = _
nullable-correct₂ : ∀ R → Matches R [] → Nullable R
nullable-correct₂ r []∈r = nullable-correct₂′ []∈r refl
step : Regex → Char → Regex
step ∅ c = ∅
step ε c = ∅
step [ x ] c with c ≟ x
... | yes p = ε
... | no p = ∅
step (r ∘ r₁) c with nullable? r
... | yes p = (step r c ∘ r₁) ∪ step r₁ c
... | no p = step r c ∘ r₁
step (r ∪ r₁) c = step r c ∪ step r₁ c
step (r ⋆) c = step r c ∘ (r ⋆)
steps : Regex → List Char → Regex
steps R (x ∷ xs) = steps (step R x) xs
steps R [] = R
step-correct₁ : ∀ R c s → Matches (step R c) s → Matches R (c ∷ s)
step-correct₁ [ x ] c s prf with c ≟ x
step-correct₁ [ x ] c s empty | yes refl = char
step-correct₁ [ x ] c s () | no p
step-correct₁ (R ∘ R₁) c s prf with nullable? R
step-correct₁ (R ∘ R₁) c s (un₁ (comp prf prf₁)) | yes p = comp (step-correct₁ R c _ prf) prf₁
step-correct₁ (R ∘ R₁) c s (un₂ prf) | yes p = comp (nullable-correct₁ R p) (step-correct₁ R₁ c _ prf)
step-correct₁ (R ∘ R₁) c s (comp prf prf₁) | no p = comp (step-correct₁ R c _ prf) prf₁
step-correct₁ (R ∪ R₁) c s (un₁ prf) = un₁ (step-correct₁ R c s prf)
step-correct₁ (R ∪ R₁) c s (un₂ prf) = un₂ (step-correct₁ R₁ c s prf)
step-correct₁ (R ⋆) c s (comp prf prf₁) = starₛ (step-correct₁ R c _ prf) prf₁
step-correct₂ : ∀ R c s → Matches R (c ∷ s) → Matches (step R c) s
step-correct₂ [ x ] c s char with x ≟ x
... | yes p = empty
... | no p = ⊥-elim (p refl)
step-correct₂ (R ∘ R₁) c s prf with nullable? R | comp⁻¹ prf
... | yes p | [] , t₂ , refl , prf , prf₁ = un₂ (step-correct₂ R₁ c s prf₁)
... | yes p | x ∷ t₁ , t₂ , eq , prf , prf₁ =
un₁ (subst₂ Matches (cong (λ - → step R - ∘ R₁) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
(comp (step-correct₂ R x t₁ prf) prf₁))
... | no p | [] , t₂ , eq , prf , prf₁ = ⊥-elim (p (nullable-correct₂ R prf))
... | no p | x ∷ t₁ , t₂ , eq , prf , prf₁ =
subst₂ Matches (cong (λ - → step R - ∘ R₁) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
(comp (step-correct₂ R x t₁ prf) prf₁)
step-correct₂ (R ∪ R₁) c s (un₁ prf) = un₁ (step-correct₂ R c s prf)
step-correct₂ (R ∪ R₁) c s (un₂ prf) = un₂ (step-correct₂ R₁ c s prf)
step-correct₂ (R ⋆) c s prf with star⁻¹′ prf
... | inj₂ (x , t₁ , t₂ , eq , prf , prf₁) =
subst₂ Matches (cong (λ - → step R - ∘ (R ⋆)) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
(comp (step-correct₂ R x t₁ prf) prf₁)
steps-correct₁ : ∀ R s → Matches (steps R s) [] → Matches R s
steps-correct₁ R [] prf = prf
steps-correct₁ R (x ∷ s) prf = step-correct₁ R x s (steps-correct₁ (step R x) s prf)
steps-correct₂ : ∀ R s → Matches R s → Matches (steps R s) []
steps-correct₂ R [] prf = prf
steps-correct₂ R (x ∷ s) prf = steps-correct₂ (step R x) s (step-correct₂ R x s prf)
check-lemma₁ : ∀ R s → Nullable (steps R s) → Matches R s
check-lemma₁ R s null = steps-correct₁ R s (nullable-correct₁ (steps R s) null)
check-lemma₂ : ∀ R s → Matches R s → Nullable (steps R s)
check-lemma₂ R s prf = nullable-correct₂ (steps R s) (steps-correct₂ R s prf)
check : (R : Regex) (s : List Char) → Dec (Matches R s)
check R s with nullable? (steps R s)
... | yes p = yes (check-lemma₁ R s p)
... | no p = no λ m → p (check-lemma₂ R s m)
|
