Mercurial > hg > Members > kono > Proof > automaton
changeset 2:e4d298d26820
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 15 Aug 2018 00:18:38 +0900 |
| parents | 3c6de7cf2a95 |
| children | 3ac6311293ec |
| files | agda/automaton.agda agda/regex.agda |
| diffstat | 2 files changed, 68 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/automaton.agda Tue Aug 14 21:44:12 2018 +0900 +++ b/agda/automaton.agda Wed Aug 15 00:18:38 2018 +0900 @@ -1,7 +1,7 @@ module automaton where open import Level renaming ( suc to succ ; zero to Zero ) -open import Data.Fin +open import Data.Nat open import Data.List open import Data.Bool using ( Bool ; true ; false ) open import Relation.Binary.PropositionalEquality @@ -24,6 +24,14 @@ i0 : In2 i1 : In2 +open import Relation.Nullary using (¬_; Dec; yes; no) + +ieq : (i i' : In2 ) → Dec ( i ≡ i' ) +ieq i0 i0 = yes refl +ieq i1 i1 = yes refl +ieq i0 i1 = no ( λ () ) +ieq i1 i0 = no ( λ () ) + moves : { Q : Set } { Σ : Set } → Automaton Q Σ → Q → List Σ → Q @@ -69,38 +77,30 @@ example1-3 = reachable am1 st ( i1 ∷ i1 ∷ i1 ∷ [] ) -open import Relation.Nullary using (¬_; Dec; yes; no) - -state≟ : (s s' : States1 ) → Dec ( s ≡ s' ) -state≟ sr sr = yes refl -state≟ ss ss = yes refl -state≟ st st = yes refl -state≟ sr st = no λ() -state≟ sr ss = no λ() -state≟ ss st = no λ() -state≟ ss sr = no λ() -state≟ st ss = no λ() -state≟ st sr = no λ() +s1id : States1 → ℕ +s1id sr = 0 +s1id ss = 1 +s1id st = 2 record NAutomaton ( Q : Set ) ( Σ : Set ) : Set where field nδ : Q → Σ → List Q - n≟ : (q q' : Q ) → Dec ( q ≡ q' ) + sid : Q → ℕ nstart : Q nend : Q → Bool open NAutomaton -insert : { Q : Set } → ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) ) → List Q → Q → List Q -insert _≟_ [] q = q ∷ [] -insert _≟_ ( q ∷ T ) q' with q ≟ q' -... | yes _ = insert _≟_ T q' -... | no _ = q ∷ (insert _≟_ T q' ) +insert : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → Q → List Q +insert M [] q = q ∷ [] +insert M ( q ∷ T ) q' with (sid M q ) ≟ (sid M q') +... | yes _ = insert M T q' +... | no _ = q ∷ (insert M T q' ) -merge : { Q : Set } → ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) ) → List Q → List Q → List Q -merge _≟_ L1 [] = L1 -merge _≟_ L1 ( H ∷ L ) = insert _≟_ (merge _≟_ L1 L ) H +merge : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → List Q → List Q +merge M L1 [] = L1 +merge M L1 ( H ∷ L ) = insert M (merge M L1 L ) H Nmoves : { Q : Set } { Σ : Set } → NAutomaton Q Σ @@ -110,7 +110,7 @@ Nmoves1 : (q : List Q ) ( L : List Σ ) → List Q → List Q Nmoves1 q [] _ = q Nmoves1 [] (_ ∷ L) LQ = Nmoves1 LQ L [] - Nmoves1 (q ∷ T ) (H ∷ L) LQ = Nmoves1 T (H ∷ L) ( merge (n≟ M) ( nδ M q H ) LQ ) + Nmoves1 (q ∷ T ) (H ∷ L) LQ = Nmoves1 T (H ∷ L) ( merge M ( nδ M q H ) LQ ) Naccept : { Q : Set } { Σ : Set } @@ -135,7 +135,7 @@ transition2 st i1 = (st ∷ []) am2 : NAutomaton States1 In2 -am2 = record { nδ = transition2 ; n≟ = state≟ ; nstart = sr ; nend = fin1} +am2 = record { nδ = transition2 ; sid = s1id ; nstart = sr ; nend = fin1} example2-1 = Naccept am2 ( i0 ∷ i1 ∷ i0 ∷ [] )
--- 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 }