|
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
|
|
0
|
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
|
|
|
29 field
|
|
|
30 state : ℕ
|
|
3
|
31 move : Maybe Σ → List ℕ
|
|
1
|
32 RSTend : Bool
|
|
|
33
|
|
|
34 open RST
|
|
|
35
|
|
|
36 record RNFA ( Σ : Set )
|
|
|
37 : Set where
|
|
|
38 field
|
|
3
|
39 Rstates : List ( RST Σ )
|
|
4
|
40 Rstart : RST Σ
|
|
|
41 Rend : RST Σ
|
|
3
|
42 Rnum : ℕ
|
|
5
|
43
|
|
1
|
44 open RNFA
|
|
|
45
|
|
4
|
46 mergeℕ : List ℕ → List ℕ → List ℕ
|
|
|
47 mergeℕ [] L = L
|
|
|
48 mergeℕ (h ∷ t ) L with member h L
|
|
|
49 ... | true = mergeℕ t L
|
|
|
50 ... | false = h ∷ mergeℕ t L
|
|
|
51
|
|
3
|
52 generateRNFA : { Σ : Set } → ( Regex Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) → RNFA Σ
|
|
|
53 generateRNFA {Σ} regex _≟_ = generate regex (
|
|
4
|
54 record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; RSTend = true } ;
|
|
|
55 Rend = record { state = 0 ; move = λ q → [] ; RSTend = true } ; Rnum = 1 } )
|
|
3
|
56 where
|
|
6
|
57 literal : Maybe Σ → Σ → ℕ → List ℕ
|
|
|
58 literal nothing _ _ = []
|
|
|
59 literal (just q) q' n with q ≟ q'
|
|
3
|
60 ... | yes _ = [ n ]
|
|
6
|
61 ... | no _ = []
|
|
3
|
62 generate : ( Regex Σ ) → RNFA Σ → RNFA Σ
|
|
4
|
63 generate (x *) R = record R' { Rstart = record (Rstart R') { move = move0 } ;
|
|
|
64 Rend = record (Rend R') { move = move1 } }
|
|
|
65 where
|
|
|
66 R' : RNFA Σ
|
|
|
67 R' = generate x R
|
|
|
68 move0 : Maybe Σ → List ℕ
|
|
|
69 move0 nothing = mergeℕ (move (Rstart R') nothing) [ state (Rend R') ]
|
|
|
70 move0 (just x) = move (Rstart R') (just x )
|
|
|
71 move1 : Maybe Σ → List ℕ
|
|
|
72 move1 nothing = mergeℕ (move (Rstart R') nothing) ( state (Rend R') ∷ state (Rend R') ∷ [] )
|
|
|
73 move1 (just x) = move (Rstart R') (just x )
|
|
5
|
74 generate (x & y) R = record R1 { Rend = Rend R2 ;
|
|
4
|
75 Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
|
|
|
76 where
|
|
|
77 R2 : RNFA Σ
|
|
|
78 R2 = generate y R
|
|
|
79 R1 : RNFA Σ
|
|
6
|
80 R1 = generate x ( record R2 { Rstart = Rstart R2 ; Rend = Rstart R2 } )
|
|
4
|
81 generate (x || y) R = record R1 { Rstart = Rstart R1 ; Rend = Rend R2 ;
|
|
|
82 Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] }
|
|
|
83 where
|
|
6
|
84 R1 : RNFA Σ
|
|
|
85 R1 = generate x ( record R { Rnum = Rnum R + 1 } )
|
|
5
|
86 S1 : RST Σ
|
|
6
|
87 S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move = λ q → [] }
|
|
|
88 R2 : RNFA Σ
|
|
5
|
89 R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1 } )
|
|
|
90 move0 : Maybe Σ → List ℕ
|
|
|
91 move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
|
|
|
92 move0 (just x) = move (Rstart R1) (just x )
|
|
|
93 move1 : Maybe Σ → List ℕ
|
|
|
94 move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
|
|
|
95 move1 (just x) = move (Rend R1) (just x )
|
|
3
|
96 generate < x > R = record R {
|
|
|
97 Rnum = Rnum R + 1 ;
|
|
5
|
98 Rstart = record {
|
|
3
|
99 state = Rnum R
|
|
6
|
100 ; move = λ q → literal q x ( state (Rstart R) )
|
|
3
|
101 ; RSTend = false
|
|
6
|
102 } ;
|
|
|
103 Rstates = Rstart R ∷ Rstates R }
|
|
|
104
|
|
|
105 moveRegex : { Σ : Set } → List (RST Σ) → ( RST Σ → ℕ ) → RST Σ → Maybe Σ → List (RST Σ)
|
|
|
106 moveRegex { Σ} L sid s i = toRST ( move s i )
|
|
|
107 where
|
|
|
108 toRST : List ℕ → List ( RST Σ )
|
|
|
109 toRST [] = []
|
|
|
110 toRST (h ∷ t ) with findSbyNum h L sid
|
|
|
111 ... | nothing = toRST t
|
|
|
112 ... | just s = s ∷ toRST t
|
|
|
113
|
|
1
|
114
|
|
3
|
115 regex2nfa : (regex : Regex In2 ) → εAutomaton (RST In2) In2
|
|
2
|
116 regex2nfa regex = record {
|
|
6
|
117 εδ = moveRegex ( Rstates G ) state
|
|
3
|
118 ; εid = λ s → state s
|
|
6
|
119 ; allState = Rstates G
|
|
|
120 ; εstart = Rstart G
|
|
3
|
121 ; εend = λ s → RSTend s }
|
|
6
|
122 where
|
|
|
123 G : RNFA In2
|
|
|
124 G = generateRNFA regex ieq
|
|
1
|
125
|
