|
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 ( _≟_ )
|
|
|
6 open import Data.List
|
|
|
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
|
|
34
|
18 open import nfa
|
|
1
|
19
|
|
34
|
20 _‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
|
|
|
21 x ‖ y = λ s → x s ∨ y s
|
|
7
|
22
|
|
|
23
|
|
34
|
24 split : {Σ : Set} → (List Σ → Bool)
|
|
|
25 → ( List Σ → Bool) → List Σ → Bool
|
|
|
26 split x y [] = x [] ∧ y []
|
|
|
27 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
|
28 split (λ t1 → x ( ( h ∷ [] ) ++ t1 )) (λ t2 → y t2 ) t
|
|
|
29
|
|
|
30 _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
|
|
|
31 x ・ y = λ z → split x y z
|
|
7
|
32
|
|
34
|
33 {-# TERMINATING #-}
|
|
|
34 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
|
|
|
35 repeat x [] = true
|
|
|
36 repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t )
|
|
|
37
|
|
|
38 open FiniteSet
|
|
|
39
|
|
|
40 cmpi : {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡ F←Q fin y)
|
|
|
41 cmpi fin x y = F←Q fin x ≟ F←Q fin y
|
|
4
|
42
|
|
34
|
43 regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → List Σ → Bool
|
|
|
44 regular-language (x *) f = repeat ( regular-language x f )
|
|
|
45 regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
|
|
|
46 regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )
|
|
|
47 regular-language < h > f [] = false
|
|
|
48 regular-language < h > f (h1 ∷ [] ) with cmpi f h h1
|
|
|
49 ... | yes _ = true
|
|
|
50 ... | no _ = false
|
|
|
51 regular-language < h > f _ = false
|
|
1
|
52
|
|
34
|
53 finIn2 : FiniteSet In2
|
|
|
54 finIn2 = record {
|
|
|
55 Q←F = Q←F'
|
|
|
56 ; F←Q = F←Q'
|
|
|
57 ; finiso→ = finiso→'
|
|
|
58 ; finiso← = finiso←'
|
|
|
59 } where
|
|
|
60 Q←F' : Fin 2 → In2
|
|
|
61 Q←F' zero = i0
|
|
|
62 Q←F' (suc zero) = i1
|
|
|
63 Q←F' (suc (suc ()))
|
|
|
64 F←Q' : In2 → Fin 2
|
|
|
65 F←Q' i0 = zero
|
|
|
66 F←Q' i1 = suc (zero)
|
|
|
67 finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
|
|
|
68 finiso→' i0 = refl
|
|
|
69 finiso→' i1 = refl
|
|
|
70 finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
|
|
|
71 finiso←' zero = refl
|
|
|
72 finiso←' (suc zero) = refl
|
|
|
73 finiso←' (suc (suc ()))
|
|
11
|
74
|
|
|
75
|
|
34
|
76 test-r1 = < i0 > & < i1 >
|
|
|
77 test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i1 ∷ [] )
|
|
|
78 test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i0 ∷ [] )
|
|
1
|
79
|
|
34
|
80 regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } {fin : FiniteSet Σ {n}} → NAutomaton (Regex Σ) Σ
|
|
|
81 regex2nfa {Σ} r {n} {fin} = record {
|
|
|
82 Nδ = Nδ
|
|
|
83 ; Nstart = Nstart
|
|
|
84 ; Nend = Nend
|
|
|
85 } where
|
|
|
86 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
|
|
|
87 Nδ = {!!}
|
|
|
88 Nstart : (Regex Σ) → Bool
|
|
|
89 Nstart = {!!}
|
|
|
90 Nend : (Regex Σ) → Bool
|
|
|
91 Nend = {!!}
|
|
8
|
92
|
