|
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
|
|
7
|
7 -- open import Data.List
|
|
3
|
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 Σ)
|
|
8
|
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 : ℕ
|
|
5
|
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
|
|
|
57 infixr 5 _++_
|
|
|
58
|
|
8
|
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 _ = []
|
|
3
|
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
|
|
|
79 R' : RNFA Σ
|
|
|
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
|
|
|
90 R2 : RNFA Σ
|
|
|
91 R2 = generate y R
|
|
|
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
|
|
6
|
97 R1 : RNFA Σ
|
|
|
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 } ;
|
|
7
|
117 Rstates = [ Rstart R ] ++ Rstates R
|
|
|
118 }
|
|
1
|
119
|
|
3
|
120 regex2nfa : (regex : Regex In2 ) → εAutomaton (RST In2) In2
|
|
2
|
121 regex2nfa regex = record {
|
|
7
|
122 εδ = move
|
|
8
|
123 ; all-εδ = cond1
|
|
3
|
124 ; εid = λ s → state s
|
|
6
|
125 ; allState = Rstates G
|
|
|
126 ; εstart = Rstart G
|
|
3
|
127 ; εend = λ s → RSTend s }
|
|
6
|
128 where
|
|
|
129 G : RNFA In2
|
|
|
130 G = generateRNFA regex ieq
|
|
8
|
131 GTree : Tree ( Tree (RST In2) )
|
|
|
132 GTree = εclosure (Rstates G) move
|
|
|
133 cond2 : Maybe (Tree (RST In2) ) → Tree (Maybe In2 × Tree (RST In2))
|
|
|
134 cond2 nothing = empty
|
|
|
135 cond2 (just empty) = empty
|
|
|
136 cond2 (just (leaf n r)) = leaf n ( cond r , move r ( cond r ) )
|
|
|
137 cond2 (just (node n r left right )) = cond2 (just left ) ++ leaf n ( cond r , move r ( cond r ) ) ++ cond2 (just right )
|
|
|
138 cond1 : RST In2 → Tree (Maybe In2 × Tree (RST In2))
|
|
|
139 cond1 s = cond2 ( memberT ( state s ) GTree )
|
|
1
|
140
|
|
8
|
141
|
