|
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
|
|
7
|
6 -- open import Data.List
|
|
3
|
7 open import Data.Maybe
|
|
0
|
8 open import Data.Bool using ( Bool ; true ; false )
|
|
2
|
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
1
|
10 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
11
|
|
0
|
12
|
|
|
13 data Regex ( Σ : Set ) : Set where
|
|
|
14 _* : Regex Σ → Regex Σ
|
|
|
15 _&_ : Regex Σ → Regex Σ → Regex Σ
|
|
1
|
16 _||_ : Regex Σ → Regex Σ → Regex Σ
|
|
6
|
17 <_> : Σ → Regex Σ
|
|
0
|
18
|
|
|
19
|
|
|
20 -- data In2 : Set where
|
|
|
21 -- a : In2
|
|
|
22 -- b : In2
|
|
|
23
|
|
|
24 open import automaton
|
|
|
25
|
|
1
|
26
|
|
|
27 record RST ( Σ : Set )
|
|
|
28 : Set where
|
|
7
|
29 inductive
|
|
1
|
30 field
|
|
|
31 state : ℕ
|
|
7
|
32 move : Maybe Σ → Tree (RST Σ)
|
|
1
|
33 RSTend : Bool
|
|
|
34
|
|
|
35 open RST
|
|
|
36
|
|
|
37 record RNFA ( Σ : Set )
|
|
|
38 : Set where
|
|
|
39 field
|
|
7
|
40 Rstates : Tree ( RST Σ )
|
|
4
|
41 Rstart : RST Σ
|
|
|
42 Rend : RST Σ
|
|
3
|
43 Rnum : ℕ
|
|
5
|
44
|
|
1
|
45 open RNFA
|
|
|
46
|
|
7
|
47 [_] : { Σ : Set} → RST Σ → Tree (RST Σ )
|
|
|
48 [ x ] = leaf ( state x ) x
|
|
|
49
|
|
|
50 [] : { Σ : Set} → Tree (RST Σ )
|
|
|
51 [] = empty
|
|
|
52
|
|
|
53
|
|
|
54 infixr 5 _++_
|
|
|
55
|
|
|
56 _++_ : { Σ : Set} → Tree (RST Σ ) → Tree (RST Σ ) → Tree (RST Σ )
|
|
|
57 empty ++ t = t
|
|
|
58 leaf n e ++ t = insertT n e t
|
|
|
59 node n e left right ++ t =
|
|
|
60 left ++ ( insertT n e (right ++ t ) )
|
|
4
|
61
|
|
3
|
62 generateRNFA : { Σ : Set } → ( Regex Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) → RNFA Σ
|
|
|
63 generateRNFA {Σ} regex _≟_ = generate regex (
|
|
4
|
64 record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; RSTend = true } ;
|
|
|
65 Rend = record { state = 0 ; move = λ q → [] ; RSTend = true } ; Rnum = 1 } )
|
|
3
|
66 where
|
|
7
|
67 literal : Maybe Σ → Σ → ℕ → Tree (RST Σ)
|
|
|
68 literal nothing q' n = []
|
|
6
|
69 literal (just q) q' n with q ≟ q'
|
|
7
|
70 ... | yes _ = [ record { state = n ; move = λ i → empty ; RSTend = true } ]
|
|
6
|
71 ... | no _ = []
|
|
3
|
72 generate : ( Regex Σ ) → RNFA Σ → RNFA Σ
|
|
4
|
73 generate (x *) R = record R' { Rstart = record (Rstart R') { move = move0 } ;
|
|
|
74 Rend = record (Rend R') { move = move1 } }
|
|
|
75 where
|
|
|
76 R' : RNFA Σ
|
|
|
77 R' = generate x R
|
|
7
|
78 move0 : Maybe Σ → Tree (RST Σ)
|
|
4
|
79 move0 (just x) = move (Rstart R') (just x )
|
|
7
|
80 move0 nothing = move (Rstart R') nothing ++ [ Rend R' ]
|
|
|
81 move1 : Maybe Σ → Tree (RST Σ)
|
|
4
|
82 move1 (just x) = move (Rstart R') (just x )
|
|
7
|
83 move1 nothing = move (Rstart R') nothing ++ [ Rstart R' ] ++ [ Rend R' ]
|
|
5
|
84 generate (x & y) R = record R1 { Rend = Rend R2 ;
|
|
4
|
85 Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
|
|
|
86 where
|
|
|
87 R2 : RNFA Σ
|
|
|
88 R2 = generate y R
|
|
|
89 R1 : RNFA Σ
|
|
6
|
90 R1 = generate x ( record R2 { Rstart = Rstart R2 ; Rend = Rstart R2 } )
|
|
4
|
91 generate (x || y) R = record R1 { Rstart = Rstart R1 ; Rend = Rend R2 ;
|
|
|
92 Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] }
|
|
|
93 where
|
|
6
|
94 R1 : RNFA Σ
|
|
|
95 R1 = generate x ( record R { Rnum = Rnum R + 1 } )
|
|
5
|
96 S1 : RST Σ
|
|
6
|
97 S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move = λ q → [] }
|
|
|
98 R2 : RNFA Σ
|
|
5
|
99 R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1 } )
|
|
7
|
100 move0 : Maybe Σ → Tree (RST Σ)
|
|
5
|
101 move0 (just x) = move (Rstart R1) (just x )
|
|
7
|
102 move0 nothing = move (Rstart R1) nothing ++ [ Rstart R2 ]
|
|
|
103 move1 : Maybe Σ → Tree (RST Σ)
|
|
5
|
104 move1 (just x) = move (Rend R1) (just x )
|
|
7
|
105 move1 nothing = move (Rend R1) nothing ++ [ Rend R2 ]
|
|
3
|
106 generate < x > R = record R {
|
|
|
107 Rnum = Rnum R + 1 ;
|
|
5
|
108 Rstart = record {
|
|
3
|
109 state = Rnum R
|
|
6
|
110 ; move = λ q → literal q x ( state (Rstart R) )
|
|
3
|
111 ; RSTend = false
|
|
6
|
112 } ;
|
|
7
|
113 Rstates = [ Rstart R ] ++ Rstates R
|
|
|
114 }
|
|
1
|
115
|
|
3
|
116 regex2nfa : (regex : Regex In2 ) → εAutomaton (RST In2) In2
|
|
2
|
117 regex2nfa regex = record {
|
|
7
|
118 εδ = move
|
|
3
|
119 ; εid = λ s → state s
|
|
6
|
120 ; allState = Rstates G
|
|
|
121 ; εstart = Rstart G
|
|
3
|
122 ; εend = λ s → RSTend s }
|
|
6
|
123 where
|
|
|
124 G : RNFA In2
|
|
|
125 G = generateRNFA regex ieq
|
|
1
|
126
|
