Mercurial > hg > Members > kono > Proof > automaton
annotate agda/regex.agda @ 89:e919e82e95a2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Nov 2019 12:21:44 +0900 |
| parents | 02b4ecc9972c |
| children | b3f05cd08d24 |
| rev | line source |
|---|---|
| 0 | 1 module regex where |
| 2 | |
| 3 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 3 | 4 -- open import Data.Fin |
| 1 | 5 open import Data.Nat |
| 8 | 6 open import Data.Product |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
7 -- open import Data.List |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
8 open import Data.Maybe |
| 0 | 9 open import Data.Bool using ( Bool ; true ; false ) |
| 2 | 10 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 1 | 11 open import Relation.Nullary using (¬_; Dec; yes; no) |
| 12 | |
| 0 | 13 |
| 14 data Regex ( Σ : Set ) : Set where | |
| 15 _* : Regex Σ → Regex Σ | |
| 16 _&_ : Regex Σ → Regex Σ → Regex Σ | |
| 1 | 17 _||_ : Regex Σ → Regex Σ → Regex Σ |
| 6 | 18 <_> : Σ → Regex Σ |
| 0 | 19 |
| 20 | |
| 21 -- data In2 : Set where | |
| 22 -- a : In2 | |
| 23 -- b : In2 | |
| 24 | |
| 25 open import automaton | |
| 9 | 26 open import epautomaton |
| 0 | 27 |
| 1 | 28 |
| 29 record RST ( Σ : Set ) | |
| 30 : Set where | |
| 7 | 31 inductive |
| 1 | 32 field |
| 33 state : ℕ | |
| 7 | 34 move : Maybe Σ → Tree (RST Σ) |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
35 cond : Maybe Σ |
| 1 | 36 RSTend : Bool |
| 37 | |
| 38 open RST | |
| 39 | |
| 40 record RNFA ( Σ : Set ) | |
| 41 : Set where | |
| 42 field | |
| 7 | 43 Rstates : Tree ( RST Σ ) |
| 4 | 44 Rstart : RST Σ |
| 45 Rend : RST Σ | |
| 3 | 46 Rnum : ℕ |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
47 |
| 1 | 48 open RNFA |
| 49 | |
| 7 | 50 [_] : { Σ : Set} → RST Σ → Tree (RST Σ ) |
| 51 [ x ] = leaf ( state x ) x | |
| 52 | |
| 53 [] : { Σ : Set} → Tree (RST Σ ) | |
| 54 [] = empty | |
| 55 | |
| 56 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
57 infixr 5 _++_ |
| 7 | 58 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
59 _++_ : { Q : Set} → Tree Q → Tree Q → Tree Q |
| 7 | 60 empty ++ t = t |
| 61 leaf n e ++ t = insertT n e t | |
| 62 node n e left right ++ t = | |
| 63 left ++ ( insertT n e (right ++ t ) ) | |
| 4 | 64 |
| 3 | 65 generateRNFA : { Σ : Set } → ( Regex Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) → RNFA Σ |
| 66 generateRNFA {Σ} regex _≟_ = generate regex ( | |
| 8 | 67 record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; cond = nothing ; RSTend = true } ; |
| 68 Rend = record { state = 0 ; move = λ q → [] ; cond = nothing ; RSTend = true } ; Rnum = 1 } ) | |
| 3 | 69 where |
| 7 | 70 literal : Maybe Σ → Σ → ℕ → Tree (RST Σ) |
| 71 literal nothing q' n = [] | |
| 6 | 72 literal (just q) q' n with q ≟ q' |
| 8 | 73 ... | yes _ = [ record { state = n ; move = λ i → empty ; cond = nothing ; RSTend = true } ] |
| 6 | 74 ... | no _ = [] |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
75 generate : ( Regex Σ ) → RNFA Σ → RNFA Σ |
| 4 | 76 generate (x *) R = record R' { Rstart = record (Rstart R') { move = move0 } ; |
| 77 Rend = record (Rend R') { move = move1 } } | |
| 78 where | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
79 R' : RNFA Σ |
| 4 | 80 R' = generate x R |
| 7 | 81 move0 : Maybe Σ → Tree (RST Σ) |
| 4 | 82 move0 (just x) = move (Rstart R') (just x ) |
| 7 | 83 move0 nothing = move (Rstart R') nothing ++ [ Rend R' ] |
| 84 move1 : Maybe Σ → Tree (RST Σ) | |
| 4 | 85 move1 (just x) = move (Rstart R') (just x ) |
| 7 | 86 move1 nothing = move (Rstart R') nothing ++ [ Rstart R' ] ++ [ Rend R' ] |
| 5 | 87 generate (x & y) R = record R1 { Rend = Rend R2 ; |
| 4 | 88 Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 } |
| 89 where | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
90 R2 : RNFA Σ |
| 4 | 91 R2 = generate y R |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
92 R1 : RNFA Σ |
| 6 | 93 R1 = generate x ( record R2 { Rstart = Rstart R2 ; Rend = Rstart R2 } ) |
| 4 | 94 generate (x || y) R = record R1 { Rstart = Rstart R1 ; Rend = Rend R2 ; |
| 95 Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] } | |
| 96 where | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
97 R1 : RNFA Σ |
| 6 | 98 R1 = generate x ( record R { Rnum = Rnum R + 1 } ) |
| 5 | 99 S1 : RST Σ |
| 8 | 100 S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move = λ q → [] ; cond = nothing } |
| 6 | 101 R2 : RNFA Σ |
| 5 | 102 R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1 } ) |
| 7 | 103 move0 : Maybe Σ → Tree (RST Σ) |
| 5 | 104 move0 (just x) = move (Rstart R1) (just x ) |
| 7 | 105 move0 nothing = move (Rstart R1) nothing ++ [ Rstart R2 ] |
| 106 move1 : Maybe Σ → Tree (RST Σ) | |
| 5 | 107 move1 (just x) = move (Rend R1) (just x ) |
| 7 | 108 move1 nothing = move (Rend R1) nothing ++ [ Rend R2 ] |
| 3 | 109 generate < x > R = record R { |
| 110 Rnum = Rnum R + 1 ; | |
| 5 | 111 Rstart = record { |
| 3 | 112 state = Rnum R |
| 6 | 113 ; move = λ q → literal q x ( state (Rstart R) ) |
| 8 | 114 ; cond = just x |
| 3 | 115 ; RSTend = false |
| 6 | 116 } ; |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
117 Rstates = [ Rstart R ] ++ Rstates R |
| 7 | 118 } |
| 1 | 119 |
| 11 | 120 In2toℕ : In2 → ℕ |
| 121 In2toℕ i1 = zero | |
| 122 In2toℕ i2 = 1 | |
| 123 | |
| 124 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
125 regex2nfa : (regex : Regex In2 ) → εAutomaton (RST In2) In2 |
| 2 | 126 regex2nfa regex = record { |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
127 εδ = move |
| 8 | 128 ; all-εδ = cond1 |
| 3 | 129 ; εid = λ s → state s |
| 11 | 130 ; Σid = λ s → In2toℕ s |
| 6 | 131 ; allState = Rstates G |
| 132 ; εstart = Rstart G | |
| 3 | 133 ; εend = λ s → RSTend s } |
| 6 | 134 where |
| 135 G : RNFA In2 | |
| 136 G = generateRNFA regex ieq | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
137 GTree : Tree ( Tree (RST In2) ) |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
138 GTree = εclosure (Rstates G) move |
| 8 | 139 cond2 : Maybe (Tree (RST In2) ) → Tree (Maybe In2 × Tree (RST In2)) |
| 140 cond2 nothing = empty | |
| 141 cond2 (just empty) = empty | |
| 142 cond2 (just (leaf n r)) = leaf n ( cond r , move r ( cond r ) ) | |
| 143 cond2 (just (node n r left right )) = cond2 (just left ) ++ leaf n ( cond r , move r ( cond r ) ) ++ cond2 (just right ) | |
| 144 cond1 : RST In2 → Tree (Maybe In2 × Tree (RST In2)) | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
145 cond1 s = cond2 ( memberT ( state s ) GTree ) |
| 1 | 146 |
| 8 | 147 |