|
12
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 module regex where
|
|
|
3
|
|
|
4 open import Level renaming ( suc to Suc ; zero to Zero )
|
|
|
5 open import Data.List hiding ( any ; [_] ; concat )
|
|
|
6 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
7 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
8 open import Data.Empty
|
|
|
9 open import Data.Unit
|
|
|
10 open import Data.Maybe
|
|
|
11 open import logic
|
|
|
12
|
|
|
13
|
|
|
14 data Regex ( Σ : Set ) : Set where
|
|
|
15 _* : Regex Σ → Regex Σ
|
|
|
16 _&_ : Regex Σ → Regex Σ → Regex Σ
|
|
|
17 _||_ : Regex Σ → Regex Σ → Regex Σ
|
|
|
18 <_> : Σ → Regex Σ
|
|
|
19
|
|
|
20 -- postulate a b c d : Set
|
|
|
21
|
|
|
22 data char : Set where
|
|
|
23 a : char
|
|
|
24 b : char
|
|
|
25 c : char
|
|
|
26 d : char
|
|
|
27
|
|
|
28 infixr 40 _&_ _||_
|
|
|
29
|
|
|
30 r1' = (< a > & < b >) & < c >
|
|
|
31 r1 = < a > & < b > & < c >
|
|
|
32 any = < a > || < b > || < c > || < d >
|
|
|
33 r2 = ( any * ) & ( < a > & < b > & < c > )
|
|
|
34 r3 = ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
|
|
|
35 r4 = ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
|
|
|
36 r5 = ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
|
|
|
37
|
|
|
38 data regular-expr {Σ : Set} : Regex Σ → List Σ → Set where
|
|
|
39 atom : (x : Σ ) → regular-expr < x > ( x ∷ [] )
|
|
|
40 concat : {x y : Regex Σ} {t s : List Σ} → regular-expr x t → regular-expr y s → regular-expr (x & y) (t ++ s )
|
|
|
41 select : {x y : Regex Σ} {t : List Σ} → regular-expr x t ∨ regular-expr y t → regular-expr (x || y) t
|
|
|
42 star-nil : {x : Regex Σ} → regular-expr (x *) []
|
|
|
43 star : {x : Regex Σ} → {lx next : List Σ} → regular-expr x lx → regular-expr (x *) next → regular-expr (x *) next
|
|
|
44
|
|
|
45 test-regex : Set
|
|
|
46 test-regex = ¬ (regular-expr r1 ( a ∷ [] ) )
|
|
|
47
|
|
|
48 test-regex1 : regular-expr r1 ( a ∷ b ∷ c ∷ [] )
|
|
|
49 test-regex1 = concat (atom a) (concat (atom b) (atom c))
|
|
|
50
|
|
|
51 open import regular-language
|
|
|
52
|
|
|
53 -- match : {Σ : Set} → (r : Regex Σ ) → Automaton (Regex Σ) Σ
|
|
|
54
|
|
|
55 -- open import Data.Nat.DivMod
|
|
|
56
|
|
|
57 -- test-regex-even : Set
|
|
|
58 -- test-regex-even = (s : List char ) → regular-expr ( ( any & any ) * ) s → (length s) mod 2 ≡ zero
|
|
|
59
|
|
|
60 empty? : {Σ : Set} → Regex Σ → Maybe (Regex Σ)
|
|
|
61 empty? (r *) = just (r *)
|
|
|
62 empty? (r & s) with empty? r
|
|
|
63 ... | nothing = nothing
|
|
|
64 ... | just _ = empty? s
|
|
|
65 empty? (r || s) with empty? r | empty? s
|
|
|
66 ... | nothing | nothing = nothing
|
|
|
67 ... | just r1 | _ = just r1
|
|
|
68 ... | _ | just s1 = just s1
|
|
|
69 empty? < x > = nothing
|
|
|
70
|
|
|
71 derivative : {Σ : Set} → Regex Σ → Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Maybe (Maybe (Regex Σ))
|
|
|
72 derivative (r *) x dec with derivative r x dec
|
|
|
73 ... | just (just r1) = just (just (r1 & (r *)))
|
|
|
74 ... | just (nothing) = just (just (r *))
|
|
|
75 ... | nothing = nothing
|
|
|
76 derivative (r & s) x dec with derivative r x dec | derivative s x dec | empty? r
|
|
|
77 ... | nothing | _ | _ = nothing
|
|
|
78 ... | just nothing | nothing | _ = nothing
|
|
|
79 ... | just nothing | just nothing | _ = just nothing
|
|
|
80 ... | just nothing | just (just s1) | _ = just (just s1)
|
|
|
81 ... | just (just r1) | just (just s1) | nothing = just (just (r1 & s))
|
|
|
82 ... | just (just r1) | just (just s1) | just _ = just (just (s1 || (r1 & s)))
|
|
|
83 ... | just (just r1) | _ | _ = just (just (r1 & s))
|
|
|
84 derivative (r || s) x dec with derivative r x dec | derivative s x dec
|
|
|
85 ... | just (just r1) | just (just s1) = just (just ( r1 || s1 ) )
|
|
|
86 ... | just nothing | _ = just nothing
|
|
|
87 ... | _ | just nothing = just nothing
|
|
|
88 ... | just (just r1) | _ = just (just r1)
|
|
|
89 ... | _ | just (just s1) = just (just s1)
|
|
|
90 ... | nothing | nothing = nothing
|
|
|
91 derivative < i > x dec with dec i x
|
|
|
92 ... | yes y = just nothing
|
|
|
93 ... | no _ = nothing
|
|
|
94
|
|
|
95 open import automaton
|
|
|
96
|
|
|
97 regex→automaton : {Σ : Set} → Regex Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Automaton (Maybe (Maybe (Regex Σ))) Σ
|
|
|
98 regex→automaton {Σ} r dec = record {
|
|
|
99 δ = δ
|
|
|
100 ; F = F
|
|
|
101 } where
|
|
|
102 δ : Maybe (Maybe (Regex Σ)) → Σ → Maybe (Maybe (Regex Σ))
|
|
|
103 δ nothing i = nothing
|
|
|
104 δ (just nothing) i = nothing
|
|
|
105 δ (just (just r)) i = derivative r i dec
|
|
|
106 F : Maybe (Maybe (Regex Σ)) → Set
|
|
|
107 F (just (just (r *))) = ⊤
|
|
|
108 F (just nothing) = ⊤
|
|
|
109 F _ = ⊥
|
|
|
110
|
|
|
111 char-dec : (i j : char) → Dec (i ≡ j)
|
|
|
112 char-dec a a = yes refl
|
|
|
113 char-dec b b = yes refl
|
|
|
114 char-dec c c = yes refl
|
|
|
115 char-dec d d = yes refl
|
|
|
116 char-dec a b = no (λ ())
|
|
|
117 char-dec a c = no (λ ())
|
|
|
118 char-dec a d = no (λ ())
|
|
|
119 char-dec b a = no (λ ())
|
|
|
120 char-dec b c = no (λ ())
|
|
|
121 char-dec b d = no (λ ())
|
|
|
122 char-dec c a = no (λ ())
|
|
|
123 char-dec c b = no (λ ())
|
|
|
124 char-dec c d = no (λ ())
|
|
|
125 char-dec d a = no (λ ())
|
|
|
126 char-dec d b = no (λ ())
|
|
|
127 char-dec d c = no (λ ())
|
|
|
128
|
|
|
129 char-list : List char
|
|
|
130 char-list = a ∷ b ∷ c ∷ d ∷ []
|
|
|
131
|
|
|
132 a2 = accept (regex→automaton r2 char-dec ) (just (just r2)) ( a ∷ a ∷ b ∷ c ∷ [] )
|
|
|
133
|
|
|
134 tr2 = trace (regex→automaton r2 char-dec ) (just (just r2)) char-list
|
|
|
135
|
|
|
136 a1 : accept (regex→automaton < a > char-dec ) (just (just < a > )) ( a ∷ [] )
|
|
|
137 a1 = tt
|
|
|
138 tr1 = trace (regex→automaton < a > char-dec ) (just (just < a > )) ( a ∷ [] ) a1
|
|
|
139
|
|
|
140 a3 = accept (regex→automaton < a > char-dec ) (just (just (< a > & < b > ))) ( a ∷ b ∷ [] )
|
|
|
141 t3 = trace (regex→automaton < a > char-dec ) (just (just (< a > & < b > ))) ( a ∷ b ∷ [] )
|
|
|
142
|
|
|
143
|
|
|
144
|
|
|
145
|
|
|
146
|
|
|
147
|
|
|
148
|
|
|
149
|
|
|
150
|
