|
44
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
34
|
2 module regex1 where
|
|
0
|
3
|
|
|
4 open import Level renaming ( suc to succ ; zero to Zero )
|
|
34
|
5 open import Data.Fin
|
|
|
6 open import Data.Nat hiding ( _≟_ )
|
|
44
|
7 open import Data.List hiding ( any ; [_] )
|
|
37
|
8 import Data.Bool using ( Bool ; true ; false ; _∧_ )
|
|
34
|
9 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
|
|
|
10 open import Relation.Binary.PropositionalEquality as RBF hiding ( [_] )
|
|
1
|
11 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
12
|
|
0
|
13
|
|
|
14 data Regex ( Σ : Set ) : Set where
|
|
|
15 _* : Regex Σ → Regex Σ
|
|
|
16 _&_ : Regex Σ → Regex Σ → Regex Σ
|
|
34
|
17 _||_ : Regex Σ → Regex Σ → Regex Σ
|
|
|
18 <_> : Σ → Regex Σ
|
|
1
|
19
|
|
36
|
20 -- postulate a b c d : Set
|
|
|
21
|
|
|
22 data hoge : Set where
|
|
|
23 a : hoge
|
|
|
24 b : hoge
|
|
|
25 c : hoge
|
|
|
26 d : hoge
|
|
|
27
|
|
|
28 infixr 40 _&_ _||_
|
|
|
29
|
|
|
30 r1' = (< a > & < b >) & < c >
|
|
|
31 r1 = < a > & < b > & < c >
|
|
|
32 any = < a > || < b > || < c >
|
|
|
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
|
|
34
|
38 open import nfa
|
|
1
|
39
|
|
34
|
40 split : {Σ : Set} → (List Σ → Bool)
|
|
|
41 → ( List Σ → Bool) → List Σ → Bool
|
|
|
42 split x y [] = x [] ∧ y []
|
|
|
43 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
41
|
44 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
34
|
45
|
|
|
46 {-# TERMINATING #-}
|
|
|
47 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
|
|
|
48 repeat x [] = true
|
|
|
49 repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t )
|
|
|
50
|
|
44
|
51 open import finiteSet
|
|
34
|
52 open FiniteSet
|
|
|
53
|
|
|
54 cmpi : {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡ F←Q fin y)
|
|
|
55 cmpi fin x y = F←Q fin x ≟ F←Q fin y
|
|
4
|
56
|
|
34
|
57 regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → List Σ → Bool
|
|
|
58 regular-language (x *) f = repeat ( regular-language x f )
|
|
39
|
59 regular-language (x & y) f = split ( regular-language x f ) ( regular-language y f )
|
|
|
60 regular-language (x || y) f = λ s → ( regular-language x f s ) ∨ ( regular-language y f s)
|
|
34
|
61 regular-language < h > f [] = false
|
|
|
62 regular-language < h > f (h1 ∷ [] ) with cmpi f h h1
|
|
|
63 ... | yes _ = true
|
|
|
64 ... | no _ = false
|
|
|
65 regular-language < h > f _ = false
|
|
1
|
66
|
