Mercurial > hg > Members > kono > Proof > automaton
changeset 3:3ac6311293ec
εAutomaton
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 15 Aug 2018 03:37:57 +0900 |
| parents | e4d298d26820 |
| children | 843f155846fb |
| files | agda/automaton.agda agda/regex.agda |
| diffstat | 2 files changed, 107 insertions(+), 48 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/automaton.agda Wed Aug 15 00:18:38 2018 +0900 +++ b/agda/automaton.agda Wed Aug 15 03:37:57 2018 +0900 @@ -3,8 +3,9 @@ open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Nat open import Data.List +open import Data.Maybe open import Data.Bool using ( Bool ; true ; false ) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality hiding ( [_] ) record Automaton ( Q : Set ) ( Σ : Set ) : Set where @@ -141,4 +142,74 @@ example2-1 = Naccept am2 ( i0 ∷ i1 ∷ i0 ∷ [] ) example2-2 = Naccept am2 ( i1 ∷ i1 ∷ i1 ∷ [] ) +nth : {S : Set } → ℕ → List S → Maybe S +nth _ [] = nothing +nth 0 ( x ∷ _ ) = just x +nth (suc n) ( _ ∷ t ) = nth n t +member : ℕ → List ℕ → Bool +member _ [] = false +member n ( x ∷ t ) with n ≟ x +... | yes _ = true +... | no _ = member n t + +record εAutomaton ( Q : Set ) ( Σ : Set ) + : Set where + field + εδ : Q → Maybe Σ → List Q + εid : Q → ℕ + allState : List Q + εstart : Q + εend : Q → Bool + +open εAutomaton + +εclosure : { Q : Set } { Σ : Set } + → εAutomaton Q Σ + → List ( List ℕ ) +εclosure {Q} { Σ} M = closure ( ℕList ( allState M) ) + where + ℕList : List Q → List ℕ + ℕList [] = [] + ℕList ( q ∷ t ) = (εid M q ) ∷ ℕList t + closure2 : List Q → List ℕ → List ℕ + closure2 [] C = C + closure2 ( n1 ∷ t ) C with member (εid M n1) C + ... | false = closure2 t ( (εid M n1) ∷ C ) + ... | true = closure2 t C + closure1 : ℕ → List ℕ + closure1 n with nth n (allState M) + ... | nothing = [] + ... | just q = closure2 (εδ M q nothing) [ n ] + closure : List ℕ → List ( List ℕ ) + closure [] = [] + closure (n ∷ t ) = ( closure1 n ∷ closure t ) + +εAutomaton2U : { Q : Set } { Σ : Set } + → εAutomaton Q Σ → NAutomaton Q Σ +εAutomaton2U {Q} { Σ} M = record { + nδ = nδ' ; + sid = εid M ; + nstart = εstart M ; + nend = εend M + } where + MList : List ( List ℕ ) + MList = εclosure M + DummyUA : NAutomaton Q Σ + DummyUA = record { nδ = λ n i → [] ; sid = εid M ; nstart = εstart M ; nend = εend M } + nδ1 : List ℕ → Σ → List Q + nδ1 [] _ = [] + nδ1 (h ∷ t ) i with nth h ( allState M) + ... | nothing = nδ1 t i + ... | just q = merge DummyUA ( εδ M q ( just i )) ( nδ1 t i ) + nδ' : Q → Σ → List Q + nδ' q i with nth ( εid M q ) MList + ... | nothing = [] + ... | just x = nδ1 x i + + + + + + +
--- a/agda/regex.agda Wed Aug 15 00:18:38 2018 +0900 +++ b/agda/regex.agda Wed Aug 15 03:37:57 2018 +0900 @@ -1,9 +1,10 @@ module regex where open import Level renaming ( suc to succ ; zero to Zero ) -open import Data.Fin +-- open import Data.Fin open import Data.Nat open import Data.List +open import Data.Maybe open import Data.Bool using ( Bool ; true ; false ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no) @@ -25,10 +26,9 @@ record RST ( Σ : Set ) : Set where - inductive field state : ℕ - move : Σ → List ℕ + move : Maybe Σ → List ℕ RSTend : Bool open RST @@ -36,54 +36,42 @@ record RNFA ( Σ : Set ) : Set where field - states : List ( RST Σ ) - map1 : ( List ( RST Σ ) ) → ℕ → RST Σ - map1 [] _ () - map1 ( h ∷ t ) 0 = h - map1 ( h ∷ t ) (suc n) = map1 t n - map : ℕ → RST Σ - map n = map1 n states - start : RST Σ - start = map 3 + Rstates : List ( RST Σ ) + Rstart : ℕ + Rend : ℕ + Rnum : ℕ open RNFA -generateRNFA : { Σ : Set } → ( (q q' : Σ) → Dec ( q ≡ q' )) → ( Regex Σ ) → RNFA Σ -generateRNFA {Σ} _≟_ regex = record { - start = generate regex true 2 - [ record { state = 0 ; move = λ q → [] ; RSTend = true } ] - [ record { state = 1 ; move = λ q → [] ; RSTend = false } ] - ; end = λ s → RSTend s - } where - listcase : Σ → List Σ → List ( RST Σ ) → List ( RST Σ ) → List ( RST Σ ) - listcase q [] ok else = else - listcase q ( q' ∷ t ) ok else with q ≟ q' - ... | yes _ = ok - ... | no _ = listcase q t ok else - generate : ( Regex Σ ) → Bool → ℕ → List ( RST Σ ) → List ( RST Σ ) → ( RST Σ ) - generate (x *) end n next else = loop - where - loop : RST Σ - repeat : RST Σ - loop = generate x end (n + 1) [ repeat ] else - repeat = record { - state = n - ; move = {!!} - ; RSTend = end - } - generate (x & y) end n next else = {!!} - generate (x || y) end n next else = {!!} - generate < x > end n next else = record { - state = n - ; move = λ q → listcase q x end else - ; RSTend = false - } +generateRNFA : { Σ : Set } → ( Regex Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) → RNFA Σ +generateRNFA {Σ} regex _≟_ = generate regex ( + record { Rstates = [ record { state = 0 ; move = λ q → [] ; RSTend = true } ] ; Rstart = 0 ; Rend = 0 ; Rnum = 1 } ) + where + listcase : Maybe Σ → List Σ → ℕ → List ℕ + listcase nothing _ _ = [] + listcase (just q) [] n = [] + listcase (just q) ( q' ∷ t ) n with q ≟ q' + ... | yes _ = [ n ] + ... | no _ = listcase (just q) t n + generate : ( Regex Σ ) → RNFA Σ → RNFA Σ + generate (x *) R = record R { Rstart = {!!} ; Rstates = Rstates R ++ ( {!!} ∷ {!!} ∷ [] ) } + generate (x & y) R = {!!} + generate (x || y) R = {!!} + generate < x > R = record R { + Rnum = Rnum R + 1 ; + Rstates = Rstates R ++ ( + record { + state = Rnum R + ; move = λ q → listcase q x (Rstart R) + ; RSTend = false + } ∷ [] ) } -regex2nfa : (regex : Regex In2 ) → NAutomaton (RST In2) In2 +regex2nfa : (regex : Regex In2 ) → εAutomaton (RST In2) In2 regex2nfa regex = record { - nδ = λ s i → move s i - ; sid = λ s → state s - ; nstart = start ( generateRNFA ieq regex ) - ; nend = λ s → RSTend s } + εδ = λ s i → {!!} -- move s i + ; εid = λ s → state s + ; allState = Rstates ( generateRNFA regex ieq ) + ; εstart = {!!} -- Rstart ( generateRNFA regex ieq ) + ; εend = λ s → RSTend s }