Mercurial > hg > Members > kono > Proof > automaton
diff agda/regex.agda @ 2:e4d298d26820
fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 15 Aug 2018 00:18:38 +0900 (2018-08-14) |
parents | 3c6de7cf2a95 |
children | 3ac6311293ec |
line wrap: on
line diff
--- a/agda/regex.agda Tue Aug 14 21:44:12 2018 +0900 +++ b/agda/regex.agda Wed Aug 15 00:18:38 2018 +0900 @@ -5,7 +5,7 @@ open import Data.Nat open import Data.List open import Data.Bool using ( Bool ; true ; false ) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no) @@ -28,7 +28,7 @@ inductive field state : ℕ - move : Σ → List (RST Σ) + move : Σ → List ℕ RSTend : Bool open RST @@ -36,24 +36,54 @@ record RNFA ( Σ : Set ) : Set where field - eqRST? : (q q' : RST Σ) → Dec (q ≡ q') - start : RST Σ - end : RST Σ → Bool + 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 open RNFA -generateRNFA : { Σ : Set } → ( Regex Σ ) → RNFA Σ -generateRNFA {Σ} regex = record { - eqRST? = eqRST - ; start = {!!} +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 - eqRST : (q q' : RST Σ) → Dec (q ≡ q') - eqRST q q' with (state q) ≟ (state q') - ... | yes eq = {!!} - ... | no neq = {!!} + 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 + } regex2nfa : (regex : Regex In2 ) → NAutomaton (RST In2) In2 -regex2nfa regex = record { nδ = λ s i → move s i ; n≟ = {!!} ; nstart = {!!} ; nend = {!!} } +regex2nfa regex = record { + nδ = λ s i → move s i + ; sid = λ s → state s + ; nstart = start ( generateRNFA ieq regex ) + ; nend = λ s → RSTend s }