|
141
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
36
|
2
|
|
44
|
3 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
4 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
141
|
5 open import Data.List hiding ( [_] )
|
|
366
|
6 open import Data.Empty
|
|
271
|
7 open import finiteSet
|
|
405
|
8 open import finiteFunc
|
|
366
|
9 open import fin
|
|
141
|
10
|
|
271
|
11 module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
|
|
141
|
12
|
|
138
|
13 open import automaton
|
|
141
|
14 open import logic
|
|
|
15 open import regex
|
|
401
|
16 open import regular-language
|
|
141
|
17
|
|
274
|
18 -- whether a regex accepts empty input
|
|
|
19 --
|
|
141
|
20 empty? : Regex Σ → Bool
|
|
|
21 empty? ε = true
|
|
|
22 empty? φ = false
|
|
|
23 empty? (x *) = true
|
|
|
24 empty? (x & y) = empty? x /\ empty? y
|
|
|
25 empty? (x || y) = empty? x \/ empty? y
|
|
|
26 empty? < x > = false
|
|
|
27
|
|
|
28 derivative : Regex Σ → Σ → Regex Σ
|
|
|
29 derivative ε s = φ
|
|
|
30 derivative φ s = φ
|
|
|
31 derivative (x *) s with derivative x s
|
|
|
32 ... | ε = x *
|
|
|
33 ... | φ = φ
|
|
|
34 ... | t = t & (x *)
|
|
|
35 derivative (x & y) s with empty? x
|
|
|
36 ... | true with derivative x s | derivative y s
|
|
|
37 ... | ε | φ = φ
|
|
335
|
38 ... | ε | t = t || y
|
|
141
|
39 ... | φ | t = t
|
|
|
40 ... | x1 | φ = x1 & y
|
|
|
41 ... | x1 | y1 = (x1 & y) || y1
|
|
|
42 derivative (x & y) s | false with derivative x s
|
|
|
43 ... | ε = y
|
|
|
44 ... | φ = φ
|
|
|
45 ... | t = t & y
|
|
|
46 derivative (x || y) s with derivative x s | derivative y s
|
|
|
47 ... | φ | y1 = y1
|
|
|
48 ... | x1 | φ = x1
|
|
|
49 ... | x1 | y1 = x1 || y1
|
|
|
50 derivative < x > s with eq? x s
|
|
|
51 ... | yes _ = ε
|
|
|
52 ... | no _ = φ
|
|
138
|
53
|
|
141
|
54 data regex-states (x : Regex Σ ) : Regex Σ → Set where
|
|
371
|
55 unit : { z : Regex Σ} → z ≡ x → regex-states x z
|
|
|
56 derive : { y z : Regex Σ } → regex-states x y → (s : Σ) → z ≡ derivative y s → regex-states x z
|
|
44
|
57
|
|
141
|
58 record Derivative (x : Regex Σ ) : Set where
|
|
|
59 field
|
|
|
60 state : Regex Σ
|
|
|
61 is-derived : regex-states x state
|
|
|
62
|
|
|
63 open Derivative
|
|
|
64
|
|
335
|
65 derive-step : (r : Regex Σ) (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s)
|
|
371
|
66 derive-step r d0 s = derive (is-derived d0) s refl
|
|
335
|
67
|
|
|
68 regex→automaton : (r : Regex Σ) → Automaton (Derivative r) Σ
|
|
371
|
69 regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive (is-derived d) s refl }
|
|
335
|
70 ; aend = λ d → empty? (state d) }
|
|
|
71
|
|
|
72 regex-match : (r : Regex Σ) → (List Σ) → Bool
|
|
371
|
73 regex-match ex is = accept ( regex→automaton ex ) record { state = ex ; is-derived = unit refl } is
|
|
335
|
74
|
|
370
|
75 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
|
|
366
|
76
|
|
335
|
77 -- open import nfa
|
|
405
|
78 open import Data.Nat hiding (eq?)
|
|
373
|
79 open import Data.Nat.Properties hiding ( eq? )
|
|
336
|
80 open import nat
|
|
335
|
81 open import finiteSetUtil
|
|
|
82 open FiniteSet
|
|
366
|
83 open import Data.Fin hiding (_<_ ; _≤_ ; pred )
|
|
141
|
84
|
|
336
|
85 -- finiteness of derivative
|
|
|
86 -- term generate x & y for each * and & only once
|
|
|
87 -- rank : Regex → ℕ
|
|
|
88 -- r₀ & r₁ ... r
|
|
337
|
89 -- generated state is a subset of the term set
|
|
141
|
90
|
|
271
|
91 open import Relation.Binary.Definitions
|
|
|
92
|
|
374
|
93 open _∧_
|
|
|
94
|
|
|
95 fb20 : {r s r₁ s₁ : Regex Σ} → r & r₁ ≡ s & s₁ → (r ≡ s ) ∧ (r₁ ≡ s₁ )
|
|
|
96 fb20 refl = ⟪ refl , refl ⟫
|
|
|
97
|
|
|
98 fb21 : {r s r₁ s₁ : Regex Σ} → r || r₁ ≡ s || s₁ → (r ≡ s ) ∧ (r₁ ≡ s₁ )
|
|
|
99 fb21 refl = ⟪ refl , refl ⟫
|
|
|
100
|
|
|
101 rg-eq? : (r s : Regex Σ) → Dec ( r ≡ s )
|
|
|
102 rg-eq? ε ε = yes refl
|
|
|
103 rg-eq? ε φ = no (λ ())
|
|
|
104 rg-eq? ε (s *) = no (λ ())
|
|
|
105 rg-eq? ε (s & s₁) = no (λ ())
|
|
|
106 rg-eq? ε (s || s₁) = no (λ ())
|
|
|
107 rg-eq? ε < x > = no (λ ())
|
|
|
108 rg-eq? φ ε = no (λ ())
|
|
|
109 rg-eq? φ φ = yes refl
|
|
|
110 rg-eq? φ (s *) = no (λ ())
|
|
|
111 rg-eq? φ (s & s₁) = no (λ ())
|
|
|
112 rg-eq? φ (s || s₁) = no (λ ())
|
|
|
113 rg-eq? φ < x > = no (λ ())
|
|
|
114 rg-eq? (r *) ε = no (λ ())
|
|
|
115 rg-eq? (r *) φ = no (λ ())
|
|
|
116 rg-eq? (r *) (s *) with rg-eq? r s
|
|
|
117 ... | yes eq = yes ( cong (_*) eq)
|
|
|
118 ... | no ne = no (λ eq → ne (fb10 eq) ) where
|
|
|
119 fb10 : {r s : Regex Σ} → (r *) ≡ (s *) → r ≡ s
|
|
|
120 fb10 refl = refl
|
|
|
121 rg-eq? (r *) (s & s₁) = no (λ ())
|
|
|
122 rg-eq? (r *) (s || s₁) = no (λ ())
|
|
|
123 rg-eq? (r *) < x > = no (λ ())
|
|
|
124 rg-eq? (r & r₁) ε = no (λ ())
|
|
|
125 rg-eq? (r & r₁) φ = no (λ ())
|
|
|
126 rg-eq? (r & r₁) (s *) = no (λ ())
|
|
|
127 rg-eq? (r & r₁) (s & s₁) with rg-eq? r s | rg-eq? r₁ s₁
|
|
|
128 ... | yes y | yes y₁ = yes ( cong₂ _&_ y y₁)
|
|
|
129 ... | yes y | no n = no (λ eq → n (proj2 (fb20 eq) ))
|
|
|
130 ... | no n | yes y = no (λ eq → n (proj1 (fb20 eq) ))
|
|
|
131 ... | no n | no n₁ = no (λ eq → n (proj1 (fb20 eq) ))
|
|
|
132 rg-eq? (r & r₁) (s || s₁) = no (λ ())
|
|
|
133 rg-eq? (r & r₁) < x > = no (λ ())
|
|
|
134 rg-eq? (r || r₁) ε = no (λ ())
|
|
|
135 rg-eq? (r || r₁) φ = no (λ ())
|
|
|
136 rg-eq? (r || r₁) (s *) = no (λ ())
|
|
|
137 rg-eq? (r || r₁) (s & s₁) = no (λ ())
|
|
|
138 rg-eq? (r || r₁) (s || s₁) with rg-eq? r s | rg-eq? r₁ s₁
|
|
|
139 ... | yes y | yes y₁ = yes ( cong₂ _||_ y y₁)
|
|
|
140 ... | yes y | no n = no (λ eq → n (proj2 (fb21 eq) ))
|
|
|
141 ... | no n | yes y = no (λ eq → n (proj1 (fb21 eq) ))
|
|
|
142 ... | no n | no n₁ = no (λ eq → n (proj1 (fb21 eq) ))
|
|
|
143 rg-eq? (r || r₁) < x > = no (λ ())
|
|
|
144 rg-eq? < x > ε = no (λ ())
|
|
|
145 rg-eq? < x > φ = no (λ ())
|
|
|
146 rg-eq? < x > (s *) = no (λ ())
|
|
|
147 rg-eq? < x > (s & s₁) = no (λ ())
|
|
|
148 rg-eq? < x > (s || s₁) = no (λ ())
|
|
|
149 rg-eq? < x > < x₁ > with eq? x x₁
|
|
|
150 ... | yes y = yes (cong <_> y)
|
|
|
151 ... | no n = no (λ eq → n (fb11 eq)) where
|
|
|
152 fb11 : < x > ≡ < x₁ > → x ≡ x₁
|
|
|
153 fb11 refl = refl
|
|
|
154
|
|
336
|
155 rank : (r : Regex Σ) → ℕ
|
|
|
156 rank ε = 0
|
|
|
157 rank φ = 0
|
|
|
158 rank (r *) = suc (rank r)
|
|
|
159 rank (r & r₁) = suc (max (rank r) (rank r₁))
|
|
|
160 rank (r || r₁) = max (rank r) (rank r₁)
|
|
|
161 rank < x > = 0
|
|
|
162
|
|
398
|
163 --
|
|
|
164 -- s is subterm of r
|
|
|
165 --
|
|
374
|
166 data SB : (r s : Regex Σ) → Set where
|
|
397
|
167 sε : SB ε ε
|
|
|
168 sφ : SB φ φ
|
|
|
169 s<> : {s : Σ} → SB < s > < s >
|
|
374
|
170 sub|1 : {x y z : Regex Σ} → SB x z → SB (x || y) z
|
|
|
171 sub|2 : {x y z : Regex Σ} → SB y z → SB (x || y) z
|
|
|
172 sub* : {x y : Regex Σ} → SB x y → SB (x *) y
|
|
|
173 sub&1 : (x y z : Regex Σ) → SB x z → SB (x & y) z
|
|
|
174 sub&2 : (x y z : Regex Σ) → SB y z → SB (x & y) z
|
|
398
|
175 sub*& : (x y : Regex Σ) → rank x < rank y → SB y x → SB (y *) (x & (y *))
|
|
|
176 sub&& : (x y z : Regex Σ) → rank z < rank x → SB (x & y) z → SB (x & y) (z & y)
|
|
374
|
177
|
|
398
|
178 --
|
|
|
179 -- set of subterm of s
|
|
|
180 --
|
|
374
|
181 record ISB (r : Regex Σ) : Set where
|
|
|
182 field
|
|
|
183 s : Regex Σ
|
|
|
184 is-sub : SB r s
|
|
341
|
185
|
|
338
|
186 open import bijection using ( InjectiveF ; Is )
|
|
336
|
187
|
|
378
|
188 finISB : (r : Regex Σ) → FiniteSet (ISB r)
|
|
397
|
189 finISB ε = record { finite = 1 ; Q←F = λ _ → record { s = ε ; is-sub = sε } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
|
|
|
190 fb00 : (q : ISB ε) → record { s = ε ; is-sub = sε } ≡ q
|
|
|
191 fb00 record { s = .ε ; is-sub = sε } = refl
|
|
|
192 fb01 : (q : ISB ε) → record { s = ε ; is-sub = sε } ≡ q
|
|
|
193 fb01 record { s = .ε ; is-sub = sε } = refl
|
|
|
194 finISB φ = record { finite = 1 ; Q←F = λ _ → record { s = φ ; is-sub = sφ } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
|
|
|
195 fb00 : (q : ISB φ) → record { s = φ ; is-sub = sφ } ≡ q
|
|
|
196 fb00 record { s = .φ ; is-sub = sφ } = refl
|
|
|
197 fb01 : (q : ISB φ) → record { s = φ ; is-sub = sφ } ≡ q
|
|
|
198 fb01 record { s = .φ ; is-sub = sφ } = refl
|
|
|
199 finISB < s > = record { finite = 1 ; Q←F = λ _ → record { s = < s > ; is-sub = s<> } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
|
|
|
200 fb00 : (q : ISB < s >) → record { s = < s > ; is-sub = s<> } ≡ q
|
|
|
201 fb00 record { s = < s > ; is-sub = s<> } = refl
|
|
|
202 fb01 : (q : ISB < s >) → record { s = < s > ; is-sub = s<> } ≡ q
|
|
|
203 fb01 record { s = < s > ; is-sub = s<> } = refl
|
|
|
204 finISB (x || y) = iso-fin (fin-∨ (finISB x) (finISB y)) record { fun← = fb00 ; fun→ = fb01 ; fiso← = {!!} ; fiso→ = {!!} } where
|
|
|
205 fb00 : ISB (x || y) → ISB x ∨ ISB y
|
|
|
206 fb00 record { s = s ; is-sub = (sub|1 is-sub) } = case1 record { s = s ; is-sub = is-sub }
|
|
|
207 fb00 record { s = s ; is-sub = (sub|2 is-sub) } = case2 record { s = s ; is-sub = is-sub }
|
|
|
208 fb01 : ISB x ∨ ISB y → ISB (x || y)
|
|
|
209 fb01 (case1 record { s = s ; is-sub = is-sub }) = record { s = s ; is-sub = sub|1 is-sub }
|
|
|
210 fb01 (case2 record { s = s ; is-sub = is-sub }) = record { s = s ; is-sub = sub|2 is-sub }
|
|
|
211 fb02 : (x : ISB x ∨ ISB y) → fb00 (fb01 x) ≡ x
|
|
|
212 fb02 (case1 record { s = s ; is-sub = is-sub }) = refl
|
|
|
213 fb02 (case2 record { s = s ; is-sub = is-sub }) = refl
|
|
382
|
214 finISB (x & y) = iso-fin (fin-∨ (inject-fin (fin-∧ (finISB x) (finISB y)) fi {!!}) (fin-∨1 (fin-∨ (finISB x) (finISB y)))) {!!} where
|
|
|
215 record Z : Set where
|
|
|
216 field
|
|
|
217 x1 y1 z : Regex Σ
|
|
|
218 lt : rank z < suc (max (rank x1) (rank z))
|
|
|
219 is-sub : SB x1 z
|
|
|
220 fb00 : ISB (x & y) → {!!}
|
|
|
221 fb00 record { s = s ; is-sub = (sub&1 .x .y .s is-sub) } = {!!}
|
|
|
222 fb00 record { s = s ; is-sub = (sub&2 .x .y .s is-sub) } = {!!}
|
|
|
223 fb00 record { s = (z & y) ; is-sub = (sub&& x y z lt is-sub) } = {!!}
|
|
|
224 fi : InjectiveF Z (ISB x ∧ ISB y)
|
|
|
225 fi = record { f = f ; inject = {!!} } where
|
|
|
226 f : Z → ISB x ∧ ISB y
|
|
|
227 f z = ⟪ record { s = Z.x1 z ; is-sub = {!!} } , {!!} ⟫
|
|
|
228 finISB (x *) = iso-fin (fin-∨ (inject-fin (finISB x) fi {!!} ) (fin-∨1 (finISB x) )) record { fun← = fb00 } where
|
|
380
|
229 record Z : Set where
|
|
|
230 field
|
|
|
231 z : Regex Σ
|
|
|
232 lt : rank z < rank x
|
|
|
233 is-sub : SB x z
|
|
|
234 fi : InjectiveF Z (ISB x)
|
|
382
|
235 fi = record { f = f ; inject = {!!} } where
|
|
380
|
236 f : Z → ISB x
|
|
|
237 f z = record { s = Z.z z ; is-sub = Z.is-sub z }
|
|
382
|
238 fb00 : ISB (x *) → {!!}
|
|
|
239 fb00 record { s = s ; is-sub = (sub* is-sub) } = {!!}
|
|
380
|
240 fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt }
|
|
370
|
241
|
|
403
|
242 d-ISB : (r : Regex Σ) → ISB r → (s : Σ) → ISB r → Bool
|
|
|
243 d-ISB r x s y = ?
|
|
|
244
|
|
378
|
245 toSB : (r : Regex Σ) → ISB r → Bool
|
|
381
|
246 toSB r record { s = s ; is-sub = is-sub } with rg-eq? r s
|
|
|
247 ... | yes _ = true
|
|
|
248 ... | no _ = false
|
|
374
|
249
|
|
398
|
250 -- whether one of subset of subterm accepts empty input
|
|
|
251 -- in case of empty set, return true
|
|
|
252 --
|
|
378
|
253 sbempty? : (r : Regex Σ) → (ISB r → Bool) → Bool
|
|
397
|
254 sbempty? ε f with f record { s = ε ; is-sub = sε }
|
|
381
|
255 ... | true = true
|
|
398
|
256 ... | false = true
|
|
|
257 sbempty? φ f with f record { s = φ ; is-sub = sφ }
|
|
|
258 ... | true = false
|
|
|
259 ... | false = true
|
|
|
260 sbempty? (r *) f = true
|
|
|
261 sbempty? (r & r₁) f = ? where
|
|
|
262 sb01 : (isb : ISB (r & r₁)) → ( ISB.is-sub isb ≡ sub&1 _ _ _ ? )
|
|
|
263 ∨ ( ISB.is-sub isb ≡ sub&2 _ _ _ ? )
|
|
|
264 ∨ ( ISB.is-sub isb ≡ subst (λ k → SB ? ?) ? (sub&& _ _ _ ? ? ))
|
|
405
|
265 sb01 isb with ISB.is-sub isb in eq
|
|
|
266 ... | sub&1 .r .r₁ .(ISB.s isb) t = case1 ?
|
|
|
267 ... | sub&2 .r .r₁ .(ISB.s isb) t = case2 (case1 ?)
|
|
|
268 ... | sub&& .r .r₁ z x t = case2 (case2 ?)
|
|
398
|
269 sb00 : ISB r → Bool
|
|
|
270 sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub&1 _ _ _ is-sub }
|
|
|
271 sbempty? (r || r₁) f with f record { s = r ; is-sub = sub|1 ? } | f record { s = r₁ ; is-sub = sub|2 ? }
|
|
|
272 ... | false | t = true
|
|
|
273 ... | true | t = empty? r \/ empty? r₁
|
|
|
274 sbempty? < x > f with f record { s = < x > ; is-sub = s<> }
|
|
|
275 ... | false = true
|
|
|
276 ... | true = false
|
|
364
|
277
|
|
382
|
278 sbderive : (r : Regex Σ) → (ISB r → Bool) → Σ → ISB r → Bool
|
|
397
|
279 sbderive ε f s record { s = .ε ; is-sub = sε } = false
|
|
|
280 sbderive φ f s record { s = t ; is-sub = sφ } = false
|
|
403
|
281 sbderive (r *) f s record { s = t ; is-sub = sub* is-sub } = ?
|
|
|
282 sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = sub*& x .r x₁ is-sub } = ?
|
|
398
|
283 sbderive (r & r₁) f s record { s = t ; is-sub = sub&1 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&1 r r₁ t is-sub }
|
|
|
284 ... | false = true
|
|
|
285 ... | true = false
|
|
399
|
286 sbderive (r & r₁) f s record { s = t ; is-sub = sub&2 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&2 r r₁ t is-sub }
|
|
398
|
287 ... | false = true
|
|
|
288 ... | true with derivative r s | derivative r₁ s
|
|
|
289 ... | ε | φ = false
|
|
399
|
290 ... | ε | y = true
|
|
|
291 ... | φ | y = false
|
|
398
|
292 ... | x1 | φ = false
|
|
|
293 ... | x1 | y1 = false
|
|
399
|
294 sbderive (r & r₁) f s record { s = .(z & r₁) ; is-sub = (sub&& .r .r₁ z x is-sub) } with f record { s = z & r₁ ; is-sub = sub&& r r₁ z x is-sub }
|
|
|
295 ... | false = true
|
|
|
296 ... | true with derivative r s | derivative r₁ s
|
|
|
297 ... | ε | φ = false
|
|
|
298 ... | ε | y = true
|
|
|
299 ... | φ | y = false
|
|
|
300 ... | x1 | φ = false
|
|
|
301 ... | x1 | y1 = false
|
|
398
|
302 sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|1 is-sub) } = sbderive r sb00 s₁ record { s = s ; is-sub = is-sub } where
|
|
|
303 sb00 : ISB r → Bool
|
|
|
304 sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub|1 is-sub }
|
|
|
305 sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|2 is-sub) } = sbderive r₁ sb00 s₁ record { s = s ; is-sub = is-sub } where
|
|
|
306 sb00 : ISB r₁ → Bool
|
|
|
307 sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub|2 is-sub }
|
|
|
308 sbderive < x > f s record { s = .(< x >) ; is-sub = s<> } with eq? x s
|
|
400
|
309 ... | yes _ = false -- because there is no next state
|
|
|
310 ... | no _ = true -- because this term set is empty
|
|
382
|
311
|
|
374
|
312 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
|
|
|
313 -- this is not correct because it contains s || s || s || .....
|
|
372
|
314
|
|
378
|
315 finSBTA : (r : Regex Σ) → FiniteSet (ISB r → Bool)
|
|
|
316 finSBTA r = fin→ ( finISB r )
|
|
364
|
317
|
|
378
|
318 regex→automaton1 : (r : Regex Σ) → Automaton (ISB r → Bool) Σ
|
|
374
|
319 regex→automaton1 r = record { δ = sbderive r ; aend = sbempty? r }
|
|
371
|
320
|
|
|
321 regex-match1 : (r : Regex Σ) → (List Σ) → Bool
|
|
372
|
322 regex-match1 r is = accept ( regex→automaton1 r ) (λ sb → toSB r sb) is
|
|
335
|
323
|
|
401
|
324 rg00 : (x : Σ) (y : List Σ) → {r : Regex Σ} → (d : Derivative r) → state d ≡ φ → accept (regex→automaton r) d y ≡ false
|
|
|
325 rg00 x [] d refl = refl
|
|
|
326 rg00 x (z ∷ y) record { state = φ ; is-derived = isd } refl = rg00 z y record { state = φ ; is-derived = derive isd z refl } refl
|
|
|
327
|
|
|
328 derive-ε : (r : Regex Σ) → (s : Σ) → r ≡ ε → derivative r s ≡ φ
|
|
|
329 derive-ε r s refl = refl
|
|
|
330
|
|
402
|
331 rg03-or : (x s : Σ) → {r r₁ : Regex Σ} → (derivative (r || r₁) s ≡ derivative r s ) ∨ (derivative (r || r₁) s ≡ derivative r₁ s )
|
|
|
332 ∨ (derivative (r || r₁) s ≡ derivative r s || derivative r₁ s )
|
|
|
333 rg03-or x s {r} {r₁} with derivative r s | derivative r₁ s
|
|
|
334 ... | φ | rr = case2 (case1 refl)
|
|
|
335 ... | ε | φ = case1 refl
|
|
|
336 ... | rr * | φ = case1 refl
|
|
|
337 ... | rr & rr₁ | φ = case1 refl
|
|
|
338 ... | rr || rr₁ | φ = case1 refl
|
|
|
339 ... | < x₁ > | φ = case1 refl
|
|
|
340 ... | ε | ε = case2 (case2 refl)
|
|
|
341 ... | rr * | ε = case2 (case2 refl)
|
|
|
342 ... | rr & rr₁ | ε = case2 (case2 refl)
|
|
|
343 ... | rr || rr₁ | ε = case2 (case2 refl)
|
|
|
344 ... | < x₁ > | ε = case2 (case2 refl)
|
|
|
345 ... | ε | rr₁ * = case2 (case2 refl)
|
|
|
346 ... | rr * | rr₁ * = case2 (case2 refl)
|
|
|
347 ... | rr & rr₂ | rr₁ * = case2 (case2 refl)
|
|
|
348 ... | rr || rr₂ | rr₁ * = case2 (case2 refl)
|
|
|
349 ... | < x₁ > | rr₁ * = case2 (case2 refl)
|
|
|
350 ... | rr | rr₁ & rr₂ = case2 (case2 ?)
|
|
|
351 ... | rr | rr₁ || rr₂ = case2 (case2 ?)
|
|
|
352 ... | rr | < x₁ > = case2 (case2 ?)
|
|
|
353
|
|
384
|
354 derive-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match r x
|
|
|
355 derive-is-regex-language ε [] = refl
|
|
401
|
356 derive-is-regex-language ε (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl)
|
|
384
|
357 derive-is-regex-language φ [] = refl
|
|
401
|
358 derive-is-regex-language φ (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl)
|
|
|
359 derive-is-regex-language (r *) [] with empty? (r *)
|
|
|
360 ... | true = refl
|
|
|
361 ... | false = refl
|
|
|
362 derive-is-regex-language (r *) (h ∷ x) = ? where
|
|
|
363 rg03 : (x s : Σ) → ?
|
|
|
364 rg03 = ?
|
|
384
|
365 derive-is-regex-language (r & r₁) x = ?
|
|
401
|
366 derive-is-regex-language (r || r₁) [] = cong₂ (λ j k → j \/ k ) (derive-is-regex-language r []) (derive-is-regex-language r₁ [])
|
|
402
|
367 derive-is-regex-language (r || r₁) (x ∷ x₁) = ?
|
|
384
|
368 derive-is-regex-language < x₁ > [] = refl
|
|
|
369 derive-is-regex-language < x₁ > (x ∷ []) with eq? x₁ x
|
|
|
370 ... | yes _ = refl
|
|
|
371 ... | no _ = refl
|
|
401
|
372 derive-is-regex-language < x₁ > (x ∷ x₂ ∷ x₃) = sym rg02 where
|
|
384
|
373 rg03 : (x s : Σ) → (derivative < x > s ≡ ε ) ∨ (derivative < x > s ≡ φ )
|
|
|
374 rg03 x s with eq? x s
|
|
|
375 ... | yes _ = case1 refl
|
|
|
376 ... | no _ = case2 refl
|
|
|
377 rg02 : regex-match < x₁ > (x ∷ x₂ ∷ x₃ ) ≡ false
|
|
|
378 rg02 with rg03 x₁ x
|
|
401
|
379 ... | case2 eq = rg00 x (x₂ ∷ x₃) record { state = _ ; is-derived = derive (unit refl) _ refl} eq
|
|
|
380 ... | case1 eq = rg00 x₂ x₃ record { state = _ ; is-derived = derive (derive (unit refl) _ refl) _ refl } (derive-ε _ _ eq )
|
|
384
|
381 -- immediate with eq? x₁ x generates an error w != eq? a b of type Dec (a ≡ b)
|
|
|
382
|
|
402
|
383 derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match1 r x
|
|
384
|
384 derive=ISB ε [] = refl
|
|
|
385 derive=ISB ε (x ∷ x₁) = ?
|
|
|
386 derive=ISB φ [] = refl
|
|
|
387 derive=ISB φ (x ∷ x₁) = ?
|
|
|
388 derive=ISB (r *) x = ?
|
|
|
389 derive=ISB (r & r₁) x = ?
|
|
|
390 derive=ISB (r || r₁) x = ?
|
|
398
|
391 derive=ISB < x₁ > [] = ?
|
|
384
|
392 derive=ISB < x₁ > (x ∷ []) with eq? x₁ x
|
|
400
|
393 ... | yes _ = refl
|
|
|
394 ... | no _ = refl
|
|
384
|
395 derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ?
|
|
|
396
|
|
335
|
397
|
|
|
398
|
|
338
|
399
|
