Mercurial > hg > Members > kono > Proof > automaton

comparison agda/regex.agda @ 2:e4d298d26820

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Aug 2018 00:18:38 +0900
parents 3c6de7cf2a95
children 3ac6311293ec
comparison
equal deleted inserted replaced
1:3c6de7cf2a95 2:e4d298d26820
3 open import Level renaming ( suc to succ ; zero to Zero ) 3 open import Level renaming ( suc to succ ; zero to Zero )
4 open import Data.Fin 4 open import Data.Fin
5 open import Data.Nat 5 open import Data.Nat
6 open import Data.List 6 open import Data.List
7 open import Data.Bool using ( Bool ; true ; false ) 7 open import Data.Bool using ( Bool ; true ; false )
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
9 open import Relation.Nullary using (¬_; Dec; yes; no) 9 open import Relation.Nullary using (¬_; Dec; yes; no)
10 10
11 11
12 data Regex ( Σ : Set ) : Set where 12 data Regex ( Σ : Set ) : Set where
13 _* : Regex Σ → Regex Σ 13 _* : Regex Σ → Regex Σ
26 record RST ( Σ : Set ) 26 record RST ( Σ : Set )
27 : Set where 27 : Set where
28 inductive 28 inductive
29 field 29 field
30 state : ℕ 30 state : ℕ
31 move : Σ → List (RST Σ) 31 move : Σ → List ℕ
32 RSTend : Bool 32 RSTend : Bool
33 33
34 open RST 34 open RST
35 35
36 record RNFA ( Σ : Set ) 36 record RNFA ( Σ : Set )
37 : Set where 37 : Set where
38 field 38 field
39 eqRST? : (q q' : RST Σ) → Dec (q ≡ q') 39 states : List ( RST Σ )
40 start : RST Σ 40 map1 : ( List ( RST Σ ) ) → ℕ → RST Σ
41 end : RST Σ → Bool 41 map1 [] _ ()
42 map1 ( h ∷ t ) 0 = h
43 map1 ( h ∷ t ) (suc n) = map1 t n
44 map : ℕ → RST Σ
45 map n = map1 n states
46 start : RST Σ
47 start = map 3
42 48
43 open RNFA 49 open RNFA
44 50
45 generateRNFA : { Σ : Set } → ( Regex Σ ) → RNFA Σ 51 generateRNFA : { Σ : Set } → ( (q q' : Σ) → Dec ( q ≡ q' )) → ( Regex Σ ) → RNFA Σ
46 generateRNFA {Σ} regex = record { 52 generateRNFA {Σ} _≟_ regex = record {
47 eqRST? = eqRST 53 start = generate regex true 2
48 ; start = {!!} 54 [ record { state = 0 ; move = λ q → [] ; RSTend = true } ]
55 [ record { state = 1 ; move = λ q → [] ; RSTend = false } ]
49 ; end = λ s → RSTend s 56 ; end = λ s → RSTend s
50 } where 57 } where
51 eqRST : (q q' : RST Σ) → Dec (q ≡ q') 58 listcase : Σ → List Σ → List ( RST Σ ) → List ( RST Σ ) → List ( RST Σ )
52 eqRST q q' with (state q) ≟ (state q') 59 listcase q [] ok else = else
53 ... | yes eq = {!!} 60 listcase q ( q' ∷ t ) ok else with q ≟ q'
54 ... | no neq = {!!} 61 ... | yes _ = ok
62 ... | no _ = listcase q t ok else
63 generate : ( Regex Σ ) → Bool → ℕ → List ( RST Σ ) → List ( RST Σ ) → ( RST Σ )
64 generate (x *) end n next else = loop
65 where
66 loop : RST Σ
67 repeat : RST Σ
68 loop = generate x end (n + 1) [ repeat ] else
69 repeat = record {
70 state = n
71 ; move = {!!}
72 ; RSTend = end
73 }
74 generate (x & y) end n next else = {!!}
75 generate (x || y) end n next else = {!!}
76 generate < x > end n next else = record {
77 state = n
78 ; move = λ q → listcase q x end else
79 ; RSTend = false
80 }
55 81
56 82
57 regex2nfa : (regex : Regex In2 ) → NAutomaton (RST In2) In2 83 regex2nfa : (regex : Regex In2 ) → NAutomaton (RST In2) In2
58 regex2nfa regex = record { nδ = λ s i → move s i ; n≟ = {!!} ; nstart = {!!} ; nend = {!!} } 84 regex2nfa regex = record {
85 nδ = λ s i → move s i
86 ; sid = λ s → state s
87 ; nstart = start ( generateRNFA ieq regex )
88 ; nend = λ s → RSTend s }
59 89