|
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 Σ
|
|
0
|
17 <_> : List Σ → Regex Σ
|
|
|
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
|
|
|
57 listcase : Maybe Σ → List Σ → ℕ → List ℕ
|
|
|
58 listcase nothing _ _ = []
|
|
|
59 listcase (just q) [] n = []
|
|
|
60 listcase (just q) ( q' ∷ t ) n with q ≟ q'
|
|
|
61 ... | yes _ = [ n ]
|
|
|
62 ... | no _ = listcase (just q) t n
|
|
|
63 generate : ( Regex Σ ) → RNFA Σ → RNFA Σ
|
|
4
|
64 generate (x *) R = record R' { Rstart = record (Rstart R') { move = move0 } ;
|
|
|
65 Rend = record (Rend R') { move = move1 } }
|
|
|
66 where
|
|
|
67 R' : RNFA Σ
|
|
|
68 R' = generate x R
|
|
|
69 move0 : Maybe Σ → List ℕ
|
|
|
70 move0 nothing = mergeℕ (move (Rstart R') nothing) [ state (Rend R') ]
|
|
|
71 move0 (just x) = move (Rstart R') (just x )
|
|
|
72 move1 : Maybe Σ → List ℕ
|
|
|
73 move1 nothing = mergeℕ (move (Rstart R') nothing) ( state (Rend R') ∷ state (Rend R') ∷ [] )
|
|
|
74 move1 (just x) = move (Rstart R') (just x )
|
|
5
|
75 generate (x & y) R = record R1 { Rend = Rend R2 ;
|
|
4
|
76 Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
|
|
|
77 where
|
|
|
78 R2 : RNFA Σ
|
|
|
79 R2 = generate y R
|
|
|
80 R1 : RNFA Σ
|
|
5
|
81 R1 = generate x ( record R2 { Rstart = record (Rstart R1) { move = move0 } ; Rend = record (Rend R1) { move = move1 } } )
|
|
4
|
82 move0 : Maybe Σ → List ℕ
|
|
5
|
83 move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
|
|
|
84 move0 (just x) = move (Rstart R1) (just x )
|
|
|
85 move1 : Maybe Σ → List ℕ
|
|
|
86 move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
|
|
|
87 move1 (just x) = move (Rend R1) (just x )
|
|
4
|
88 generate (x || y) R = record R1 { Rstart = Rstart R1 ; Rend = Rend R2 ;
|
|
|
89 Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] }
|
|
|
90 where
|
|
5
|
91 S1 : RST Σ
|
|
|
92 S1 = record { state = Rnum R ; RSTend = RSTend R ; move = λ q → [] }
|
|
|
93 R1 = generate x ( record R { Rnum = Rnum R +1 } )
|
|
|
94 R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1 } )
|
|
|
95 move0 : Maybe Σ → List ℕ
|
|
|
96 move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
|
|
|
97 move0 (just x) = move (Rstart R1) (just x )
|
|
|
98 move1 : Maybe Σ → List ℕ
|
|
|
99 move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
|
|
|
100 move1 (just x) = move (Rend R1) (just x )
|
|
3
|
101 generate < x > R = record R {
|
|
|
102 Rnum = Rnum R + 1 ;
|
|
5
|
103 Rstart = record {
|
|
3
|
104 state = Rnum R
|
|
4
|
105 ; move = λ q → listcase q x ( state (Rstart R) )
|
|
3
|
106 ; RSTend = false
|
|
5
|
107 }
|
|
|
108 Rstates = Rstart R ∷ Rstate R }
|
|
1
|
109
|
|
3
|
110 regex2nfa : (regex : Regex In2 ) → εAutomaton (RST In2) In2
|
|
2
|
111 regex2nfa regex = record {
|
|
3
|
112 εδ = λ s i → {!!} -- move s i
|
|
|
113 ; εid = λ s → state s
|
|
|
114 ; allState = Rstates ( generateRNFA regex ieq )
|
|
|
115 ; εstart = {!!} -- Rstart ( generateRNFA regex ieq )
|
|
|
116 ; εend = λ s → RSTend s }
|
|
1
|
117
|
