|
34
|
1 module regex1 where
|
|
0
|
2
|
|
|
3 open import Level renaming ( suc to succ ; zero to Zero )
|
|
34
|
4 open import Data.Fin
|
|
|
5 open import Data.Nat hiding ( _≟_ )
|
|
36
|
6 open import Data.List hiding ( any )
|
|
34
|
7 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
|
|
|
8 open import Relation.Binary.PropositionalEquality as RBF hiding ( [_] )
|
|
1
|
9 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
10
|
|
0
|
11
|
|
|
12 data Regex ( Σ : Set ) : Set where
|
|
|
13 _* : Regex Σ → Regex Σ
|
|
|
14 _&_ : Regex Σ → Regex Σ → Regex Σ
|
|
34
|
15 _||_ : Regex Σ → Regex Σ → Regex Σ
|
|
|
16 <_> : Σ → Regex Σ
|
|
1
|
17
|
|
36
|
18 -- postulate a b c d : Set
|
|
|
19
|
|
|
20 data hoge : Set where
|
|
|
21 a : hoge
|
|
|
22 b : hoge
|
|
|
23 c : hoge
|
|
|
24 d : hoge
|
|
|
25
|
|
|
26 infixr 40 _&_ _||_
|
|
|
27
|
|
|
28 r1' = (< a > & < b >) & < c >
|
|
|
29 r1 = < a > & < b > & < c >
|
|
|
30 any = < a > || < b > || < c >
|
|
|
31 r2 = ( any * ) & ( < a > & < b > & < c > )
|
|
|
32 r3 = ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
|
|
|
33 r4 = ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
|
|
|
34 r5 = ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
|
|
|
35
|
|
34
|
36 open import nfa
|
|
1
|
37
|
|
34
|
38 _‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
|
|
|
39 x ‖ y = λ s → x s ∨ y s
|
|
7
|
40
|
|
|
41
|
|
34
|
42 split : {Σ : Set} → (List Σ → Bool)
|
|
|
43 → ( List Σ → Bool) → List Σ → Bool
|
|
|
44 split x y [] = x [] ∧ y []
|
|
|
45 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
|
46 split (λ t1 → x ( ( h ∷ [] ) ++ t1 )) (λ t2 → y t2 ) t
|
|
|
47
|
|
|
48 _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
|
|
|
49 x ・ y = λ z → split x y z
|
|
7
|
50
|
|
34
|
51 {-# TERMINATING #-}
|
|
|
52 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
|
|
|
53 repeat x [] = true
|
|
|
54 repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t )
|
|
|
55
|
|
|
56 open FiniteSet
|
|
|
57
|
|
|
58 cmpi : {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡ F←Q fin y)
|
|
|
59 cmpi fin x y = F←Q fin x ≟ F←Q fin y
|
|
4
|
60
|
|
34
|
61 regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → List Σ → Bool
|
|
|
62 regular-language (x *) f = repeat ( regular-language x f )
|
|
|
63 regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
|
|
|
64 regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )
|
|
|
65 regular-language < h > f [] = false
|
|
|
66 regular-language < h > f (h1 ∷ [] ) with cmpi f h h1
|
|
|
67 ... | yes _ = true
|
|
|
68 ... | no _ = false
|
|
|
69 regular-language < h > f _ = false
|
|
1
|
70
|
|
34
|
71 finIn2 : FiniteSet In2
|
|
|
72 finIn2 = record {
|
|
|
73 Q←F = Q←F'
|
|
|
74 ; F←Q = F←Q'
|
|
|
75 ; finiso→ = finiso→'
|
|
|
76 ; finiso← = finiso←'
|
|
|
77 } where
|
|
|
78 Q←F' : Fin 2 → In2
|
|
|
79 Q←F' zero = i0
|
|
|
80 Q←F' (suc zero) = i1
|
|
|
81 Q←F' (suc (suc ()))
|
|
|
82 F←Q' : In2 → Fin 2
|
|
|
83 F←Q' i0 = zero
|
|
|
84 F←Q' i1 = suc (zero)
|
|
|
85 finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
|
|
|
86 finiso→' i0 = refl
|
|
|
87 finiso→' i1 = refl
|
|
|
88 finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
|
|
|
89 finiso←' zero = refl
|
|
|
90 finiso←' (suc zero) = refl
|
|
|
91 finiso←' (suc (suc ()))
|
|
11
|
92
|
|
|
93
|
|
34
|
94 test-r1 = < i0 > & < i1 >
|
|
|
95 test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i1 ∷ [] )
|
|
|
96 test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i0 ∷ [] )
|
|
1
|
97
|
|
36
|
98 issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool
|
|
|
99 issub (r *) s f = issub r s f
|
|
|
100 issub (r & r₁) s f = issub r s f ∨ issub r₁ s f
|
|
|
101 issub (r || r₁) s f = issub r s f ∨ issub r₁ s f
|
|
|
102 issub < x > < s > f with cmpi f x s
|
|
|
103 issub < x > < s > f | yes p = true
|
|
|
104 issub < x > < s > f | no ¬p = false
|
|
|
105 issub < x > s f = false
|
|
|
106
|
|
|
107 record RegexSub {Σ : Set} (R : Regex Σ) {n : ℕ } (fin : FiniteSet Σ {n} ): Set where
|
|
|
108 field
|
|
|
109 Subterm : Regex Σ
|
|
|
110 sub : issub R Subterm fin ≡ true
|
|
|
111
|
|
35
|
112 regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ
|
|
|
113 regex2nfa {Σ} (r *) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } where
|
|
|
114 nr0 = regex2nfa r fin
|
|
|
115 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
|
|
|
116 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1)
|
|
|
117 Nstart : (Regex Σ) → Bool
|
|
|
118 Nstart s0 = NAutomaton.Nstart nr0 s0
|
|
|
119 Nend : (Regex Σ) → Bool
|
|
|
120 Nend s0 = NAutomaton.Nend nr0 s0
|
|
|
121 regex2nfa {Σ} (r0 & r1) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } where
|
|
|
122 nr0 = regex2nfa r0 fin
|
|
|
123 nr1 = regex2nfa r1 fin
|
|
|
124 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
|
|
|
125 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr1 s0 i s1 )
|
|
|
126 Nstart : (Regex Σ) → Bool
|
|
|
127 Nstart s0 = NAutomaton.Nstart nr0 s0 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 )
|
|
|
128 Nend : (Regex Σ) → Bool
|
|
|
129 Nend s0 = NAutomaton.Nend nr0 s0 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 )
|
|
|
130 regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } where
|
|
|
131 nr0 = regex2nfa r0 fin
|
|
|
132 nr1 = regex2nfa r1 fin
|
|
34
|
133 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
|
|
35
|
134 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1
|
|
|
135 Nstart : (Regex Σ) → Bool
|
|
|
136 Nstart s0 = NAutomaton.Nstart nr0 s0 ∨ NAutomaton.Nstart nr1 s0
|
|
|
137 Nend : (Regex Σ) → Bool
|
|
|
138 Nend s0 = NAutomaton.Nend nr0 s0 ∨ NAutomaton.Nend nr1 s0
|
|
|
139 regex2nfa {Σ} < x > fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } where
|
|
|
140 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
|
|
|
141 Nδ r1 s r2 with cmpi fin s x
|
|
|
142 Nδ r1 s r2 | yes _ = true
|
|
|
143 Nδ r1 s r2 | no _ = false
|
|
34
|
144 Nstart : (Regex Σ) → Bool
|
|
35
|
145 Nstart < s > with cmpi fin s x
|
|
|
146 ... | yes _ = true
|
|
|
147 ... | no _ = false
|
|
|
148 Nstart _ = false
|
|
34
|
149 Nend : (Regex Σ) → Bool
|
|
35
|
150 Nend _ = false
|
|
|
151
|
|
|
152 test-r4 = regex2nfa (< i0 > & < i1 >) finIn2
|
|
8
|
153
|
|
36
|
154 -- testr5 = Naccept test-r4 {!!} ( i0 ∷ i1 ∷ [] )
|
|
35
|
155
|
|
|
156
|
|
|
157
|
|
|
158
|
