Mercurial > hg > Members > kono > Proof > automaton
view automaton-in-agda/src/derive.agda @ 365:c46f04f7c99a
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 21 Jul 2023 12:01:16 +0900 (2023-07-21) |
parents | 00f5076ef2de |
children | 19410aadd636 |
line wrap: on
line source
{-# OPTIONS --allow-unsolved-metas #-} open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.List hiding ( [_] ) open import finiteSet module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where open import automaton open import logic open import regex -- whether a regex accepts empty input -- empty? : Regex Σ → Bool empty? ε = true empty? φ = false empty? (x *) = true empty? (x & y) = empty? x /\ empty? y empty? (x || y) = empty? x \/ empty? y empty? < x > = false derivative : Regex Σ → Σ → Regex Σ derivative ε s = φ derivative φ s = φ derivative (x *) s with derivative x s ... | ε = x * ... | φ = φ ... | t = t & (x *) derivative (x & y) s with empty? x ... | true with derivative x s | derivative y s ... | ε | φ = φ ... | ε | t = t || y ... | φ | t = t ... | x1 | φ = x1 & y ... | x1 | y1 = (x1 & y) || y1 derivative (x & y) s | false with derivative x s ... | ε = y ... | φ = φ ... | t = t & y derivative (x || y) s with derivative x s | derivative y s ... | φ | y1 = y1 ... | x1 | φ = x1 ... | x1 | y1 = x1 || y1 derivative < x > s with eq? x s ... | yes _ = ε ... | no _ = φ data regex-states (x : Regex Σ ) : Regex Σ → Set where unit : regex-states x x derive : { y : Regex Σ } → regex-states x y → (s : Σ) → regex-states x ( derivative y s ) record Derivative (x : Regex Σ ) : Set where field state : Regex Σ is-derived : regex-states x state open Derivative derive-step : (r : Regex Σ) (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s) derive-step r d0 s = derive (is-derived d0) s regex→automaton : (r : Regex Σ) → Automaton (Derivative r) Σ regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step r d s} ; aend = λ d → empty? (state d) } regex-match : (r : Regex Σ) → (List Σ) → Bool regex-match ex is = accept ( regex→automaton ex ) record { state = ex ; is-derived = unit } is -- open import nfa open import Data.Nat -- open import Data.Nat hiding ( _<_ ; _>_ ) -- open import Data.Fin hiding ( _<_ ) open import nat open import finiteSetUtil open FiniteSet open import Data.Fin hiding (_<_) -- finiteness of derivative -- term generate x & y for each * and & only once -- rank : Regex → ℕ -- r₀ & r₁ ... r -- generated state is a subset of the term set open import Relation.Binary.Definitions rank : (r : Regex Σ) → ℕ rank ε = 0 rank φ = 0 rank (r *) = suc (rank r) rank (r & r₁) = suc (max (rank r) (rank r₁)) rank (r || r₁) = max (rank r) (rank r₁) rank < x > = 0 data SB : (r : Regex Σ) → (rn : ℕ) → Set where sbε : SB ε 0 sbφ : SB φ 0 sb<> : (s : Σ) → SB < s > 0 sb| : (x y : Regex Σ) → (xn yn xy : ℕ) → SB x xn → SB y yn → xy ≡ max xn yn → SB (x || y) xy sb* : (x : Regex Σ) → (xn : ℕ) → SB x xn → SB (x *) (suc xn) sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn → ( sx : SB x xn ) (sy : SB y yn ) → SB (x & y) (suc yn) sb-id : (r : Regex Σ) → SB r (rank r) → Bool sb-id r sb with rank r | inspect rank r sb-id ε sbε | zero | _ = true sb-id φ sbφ | zero | _ = true sb-id < t > (sb<> s) | zero | _ with eq? t s ... | yes _ = true ... | no _ = false sb-id (x0 || y0) (sb| x y xn yn .zero sb sb₁ x₁) | zero | record { eq = eq1 } = sb-id x0 ? /\ sb-id y0 ? sb-id _ (sb| x y xn yn .(suc k) sb sb₁ x₁) | suc k | record { eq = eq1 } = sb-id x ? /\ sb-id y ? sb-id (y *) (sb* x t u) | suc k | record{ eq = eq1 } = sb-id y ? sb-id (x0 & y0) (sb& .x0 .y0 xn .k x z z₁) | suc k | record { eq = eq1 } = sb-id x0 ? /\ sb-id y0 ? open import bijection using ( InjectiveF ; Is ) finSBTA : (r : Regex Σ) → FiniteSet (SB r (rank r) → Bool) finSBTA r = fin→ ( fb00 (rank r) r refl ) where fb00 : (n : ℕ ) → (r : Regex Σ) → rank r ≡ n → FiniteSet (SB r (rank r)) fb00 zero ε eq = record { finite = 1 ; Q←F = λ _ → sbε ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = ? } fb00 zero φ eq = record { finite = 1 ; Q←F = λ _ → sbφ ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = ? } fb00 zero (r || r₁) eq = iso-fin (fin-∨ (fb00 zero r ?) (fb00 zero r₁ ?)) ? fb00 zero < x > eq = iso-fin fin ? fb00 (suc n) (r *) eq = iso-fin (fb00 n r ?) ? fb00 (suc n) (r & r₁) eq = iso-fin (fin-∧ (fb00 n r ?) (fb00 n r₁ ?)) ? fb00 (suc n) (r || r₁) eq = iso-fin (fin-∧ (fb00 (suc n) r ?) (fb00 (suc n) r₁ ?)) ? record SBf (r : Regex Σ) (n : ℕ) : Set where field rank=n : rank r ≡ n f : Derivative r → SB r n → Bool sb-inject : {x y : Derivative r} → f x ≡ f y → x ≡ y dec : (a : SB r n → Bool ) → Dec (Is (Derivative r) (SB r n → Bool) f a ) SBN : (r : Regex Σ) → SBf r (rank r) SBN ε = record { rank=n = refl ; f = fb02 ; sb-inject = fl05 ; dec = fl03 } where fb02 : Derivative ε → SB ε 0 → Bool fb02 d sbε = true fl03 : (a : SB ε 0 → Bool) → Dec (Is (Derivative ε) (SB ε 0 → Bool) fb02 a) fl03 a with a sbε | inspect a sbε ... | true | record { eq = eq1 } = yes record { a = record { state = ε ; is-derived = unit } ; fa=c = f-extensionality fl04 } where fl04 : (x : SB ε 0) → fb02 (record { state = ε ; is-derived = unit }) x ≡ a x fl04 sbε = sym eq1 ... | false | record { eq = eq1} = no (λ n → ¬-bool {a sbε} eq1 (fl04 n)) where fl04 : Is (Derivative ε) (SB ε 0 → Bool) fb02 a → a sbε ≡ true fl04 n = sym (cong (λ k → k sbε) (Is.fa=c n)) fl05 : {x y : Derivative ε} → fb02 x ≡ fb02 y → x ≡ y fl05 {x} {y} eq = ? SBN φ = ? SBN (r *) = ? SBN (r & r₁) = record { rank=n = ? ; f = ? ; sb-inject = ? ; dec = ? } SBN (r || r₁) = ? SBN < x > = record { rank=n = refl ; f = ? ; sb-inject = ? ; dec = ? } finite-derivative : (r : Regex Σ) → FiniteSet (Derivative r) finite-derivative r = inject-fin (finSBTA r) record { f = SBf.f (SBN r) ; inject = SBf.sb-inject (SBN r) } (SBf.dec (SBN r))