Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/derive.agda @ 274:1c8ed1220489

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixes
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Dec 2021 16:27:46 +0900
parents f60c1041ae8e
children 407684f806e4
comparison
equal deleted inserted replaced
273:192263adfc02 274:1c8ed1220489
15 open import automaton 15 open import automaton
16 open import logic 16 open import logic
17 open import regex 17 open import regex
18 open FiniteSet 18 open FiniteSet
19 19
20 -- whether a regex accepts empty input
21 --
20 empty? : Regex Σ → Bool 22 empty? : Regex Σ → Bool
21 empty? ε = true 23 empty? ε = true
22 empty? φ = false 24 empty? φ = false
23 empty? (x *) = true 25 empty? (x *) = true
24 empty? (x & y) = empty? x /\ empty? y 26 empty? (x & y) = empty? x /\ empty? y
158 regex-derive1 x (i ∷ t) r = regex-derive1 x t (insert r (derivative x i)) 160 regex-derive1 x (i ∷ t) r = regex-derive1 x t (insert r (derivative x i))
159 regex-derive0 : List (Regex Σ) → List (Regex Σ) → List (Regex Σ) 161 regex-derive0 : List (Regex Σ) → List (Regex Σ) → List (Regex Σ)
160 regex-derive0 [] t = t 162 regex-derive0 [] t = t
161 regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t) 163 regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t)
162 164
165 --
166 -- if (Derivative r is finite, regex→automaton is finite
167 --
168 drive-is-finite : (r : Regex Σ) → FiniteSet (Derivative r)
169 drive-is-finite ε = {!!}
170 drive-is-finite φ = {!!}
171 drive-is-finite (r *) = {!!} where
172 d1 : FiniteSet (Derivative r )
173 d1 = drive-is-finite r
174 drive-is-finite (r & r₁) = {!!}
175 drive-is-finite (r || r₁) = {!!}
176 drive-is-finite < x > = {!!}
177