|
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)
|
|
141
|
12 open import regex
|
|
1
|
13
|
|
36
|
14 -- postulate a b c d : Set
|
|
|
15
|
|
141
|
16 data In : Set where
|
|
|
17 a : In
|
|
|
18 b : In
|
|
|
19 c : In
|
|
|
20 d : In
|
|
36
|
21
|
|
141
|
22 cmpi : (x y : In ) → Dec (x ≡ y)
|
|
|
23 cmpi a a = yes refl
|
|
|
24 cmpi b b = yes refl
|
|
|
25 cmpi c c = yes refl
|
|
|
26 cmpi d d = yes refl
|
|
|
27 cmpi a b = no (λ ())
|
|
|
28 cmpi a c = no (λ ())
|
|
|
29 cmpi a d = no (λ ())
|
|
|
30 cmpi b a = no (λ ())
|
|
|
31 cmpi b c = no (λ ())
|
|
|
32 cmpi b d = no (λ ())
|
|
|
33 cmpi c a = no (λ ())
|
|
|
34 cmpi c b = no (λ ())
|
|
|
35 cmpi c d = no (λ ())
|
|
|
36 cmpi d a = no (λ ())
|
|
|
37 cmpi d b = no (λ ())
|
|
|
38 cmpi d c = no (λ ())
|
|
36
|
39
|
|
141
|
40 -- infixr 40 _&_ _||_
|
|
|
41
|
|
|
42 r1' = (< a > & < b >) & < c > --- abc
|
|
|
43 r1 = < a > & < b > & < c > --- abc
|
|
|
44 any = < a > || < b > || < c > --- a|b|c
|
|
|
45 r2 = ( any * ) & ( < a > & < b > & < c > ) -- .*abc
|
|
36
|
46 r3 = ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
|
|
|
47 r4 = ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
|
|
|
48 r5 = ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
|
|
|
49
|
|
34
|
50 open import nfa
|
|
1
|
51
|
|
141
|
52 -- former ++ later ≡ x
|
|
|
53 split : {Σ : Set} → ((former : List Σ) → Bool) → ((later : List Σ) → Bool) → (x : List Σ ) → Bool
|
|
34
|
54 split x y [] = x [] ∧ y []
|
|
|
55 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
41
|
56 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
34
|
57
|
|
141
|
58 -- tt1 : {Σ : Set} → ( P Q : List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] )
|
|
|
59 -- tt1 P Q = ?
|
|
|
60
|
|
34
|
61 {-# TERMINATING #-}
|
|
|
62 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
|
|
|
63 repeat x [] = true
|
|
|
64 repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t )
|
|
|
65
|
|
141
|
66 regular-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y)) → List Σ → Bool
|
|
|
67 regular-language φ cmp _ = false
|
|
|
68 regular-language ε cmp [] = true
|
|
|
69 regular-language ε cmp (_ ∷ _) = false
|
|
|
70 regular-language (x *) cmp = repeat ( regular-language x cmp )
|
|
|
71 regular-language (x & y) cmp = split ( λ z → (regular-language x cmp) z ) (λ z → regular-language y cmp z )
|
|
|
72 regular-language (x || y) cmp = λ s → ( regular-language x cmp s ) ∨ ( regular-language y cmp s)
|
|
|
73 regular-language < h > cmp [] = false
|
|
|
74 regular-language < h > cmp (h1 ∷ [] ) with cmp h h1
|
|
34
|
75 ... | yes _ = true
|
|
|
76 ... | no _ = false
|
|
141
|
77 regular-language < h > _ (_ ∷ _ ∷ _) = false
|
|
1
|
78
|
|
141
|
79 test-regex : regular-language r1' cmpi ( a ∷ [] ) ≡ false
|
|
138
|
80 test-regex = refl
|
|
|
81
|
|
141
|
82 test-regex1 : regular-language r2 cmpi ( a ∷ a ∷ b ∷ c ∷ [] ) ≡ true
|
|
138
|
83 test-regex1 = refl
|
|
|
84
|
|
141
|
85
|
|
|
86 test-AB→split : {Σ : Set} → {A B : List In → Bool} → split A B ( a ∷ b ∷ a ∷ [] ) ≡ (
|
|
|
87 ( A [] ∧ B ( a ∷ b ∷ a ∷ [] ) ) ∨
|
|
|
88 ( A ( a ∷ [] ) ∧ B ( b ∷ a ∷ [] ) ) ∨
|
|
|
89 ( A ( a ∷ b ∷ [] ) ∧ B ( a ∷ [] ) ) ∨
|
|
|
90 ( A ( a ∷ b ∷ a ∷ [] ) ∧ B [] )
|
|
|
91 )
|
|
|
92 test-AB→split {_} {A} {B} = refl
|
|
138
|
93
|
|
141
|
94 -- from example 1.53 1
|
|
|
95
|
|
|
96 ex53-1 : Set
|
|
|
97 ex53-1 = (s : List In ) → regular-language ( (< a > *) & < b > & (< a > *) ) cmpi s ≡ true → {!!} -- contains exact one b
|
|
|
98
|
|
|
99 ex53-2 : Set
|
|
|
100 ex53-2 = (s : List In ) → regular-language ( (any * ) & < b > & (any *) ) cmpi s ≡ true → {!!} -- contains at lease one b
|
|
|
101
|
|
|
102 evenp : {Σ : Set} → List Σ → Bool
|
|
|
103 oddp : {Σ : Set} → List Σ → Bool
|
|
|
104 oddp [] = false
|
|
|
105 oddp (_ ∷ t) = evenp t
|
|
138
|
106
|
|
141
|
107 evenp [] = true
|
|
|
108 evenp (_ ∷ t) = oddp t
|
|
|
109
|
|
|
110 -- from example 1.53 5
|
|
|
111 egex-even : Set
|
|
|
112 egex-even = (s : List In ) → regular-language ( ( any & any ) * ) cmpi s ≡ true → evenp s ≡ true
|
|
|
113
|
|
|
114 test11 = regular-language ( ( any & any ) * ) cmpi (a ∷ [])
|
|
|
115 test12 = regular-language ( ( any & any ) * ) cmpi (a ∷ b ∷ [])
|
|
|
116
|
|
|
117 -- proof-egex-even : egex-even
|
|
|
118 -- proof-egex-even [] _ = refl
|
|
|
119 -- proof-egex-even (a ∷ []) ()
|
|
|
120 -- proof-egex-even (b ∷ []) ()
|
|
|
121 -- proof-egex-even (c ∷ []) ()
|
|
|
122 -- proof-egex-even (x ∷ x₁ ∷ s) y = proof-egex-even s {!!}
|
|
|
123
|
|
|
124 open import derive In cmpi
|
|
|
125 open import automaton
|
|
|
126
|
|
|
127 ra-ex = trace (regex→automaton r2) (record { state = r2 ; is-derived = unit }) ( a ∷ b ∷ c ∷ [])
|
|
|
128
|
