Mercurial > hg > Members > kono > Proof > automaton
annotate agda/regex1.agda @ 43:31e4bd173951
using Fin id
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Dec 2018 03:08:21 +0900 |
| parents | ae69102153a9 |
| children | aa15eff1aeb3 |
| rev | line source |
|---|---|
| 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 ) |
| 37 | 7 import Data.Bool using ( Bool ; true ; false ; _∧_ ) |
| 34 | 8 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ ) |
| 9 open import Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) | |
| 1 | 10 open import Relation.Nullary using (¬_; Dec; yes; no) |
| 11 | |
| 0 | 12 |
| 13 data Regex ( Σ : Set ) : Set where | |
| 14 _* : Regex Σ → Regex Σ | |
| 15 _&_ : Regex Σ → Regex Σ → Regex Σ | |
| 34 | 16 _||_ : Regex Σ → Regex Σ → Regex Σ |
| 17 <_> : Σ → Regex Σ | |
| 1 | 18 |
| 36 | 19 -- postulate a b c d : Set |
| 20 | |
| 21 data hoge : Set where | |
| 22 a : hoge | |
| 23 b : hoge | |
| 24 c : hoge | |
| 25 d : hoge | |
| 26 | |
| 27 infixr 40 _&_ _||_ | |
| 28 | |
| 29 r1' = (< a > & < b >) & < c > | |
| 30 r1 = < a > & < b > & < c > | |
| 31 any = < a > || < b > || < c > | |
| 32 r2 = ( any * ) & ( < a > & < b > & < c > ) | |
| 33 r3 = ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > ) | |
| 34 r4 = ( < a > & < b > & < c > ) || ( < b > & < c > & < d > ) | |
| 35 r5 = ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > ) | |
| 36 | |
| 34 | 37 open import nfa |
| 1 | 38 |
| 34 | 39 split : {Σ : Set} → (List Σ → Bool) |
| 40 → ( List Σ → Bool) → List Σ → Bool | |
| 41 split x y [] = x [] ∧ y [] | |
| 42 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ | |
| 41 | 43 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t |
| 34 | 44 |
| 45 {-# TERMINATING #-} | |
| 46 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool | |
| 47 repeat x [] = true | |
| 48 repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t ) | |
| 49 | |
| 50 open FiniteSet | |
| 51 | |
| 52 cmpi : {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡ F←Q fin y) | |
| 53 cmpi fin x y = F←Q fin x ≟ F←Q fin y | |
| 4 | 54 |
| 34 | 55 regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → List Σ → Bool |
| 56 regular-language (x *) f = repeat ( regular-language x f ) | |
| 39 | 57 regular-language (x & y) f = split ( regular-language x f ) ( regular-language y f ) |
| 58 regular-language (x || y) f = λ s → ( regular-language x f s ) ∨ ( regular-language y f s) | |
| 34 | 59 regular-language < h > f [] = false |
| 60 regular-language < h > f (h1 ∷ [] ) with cmpi f h h1 | |
| 61 ... | yes _ = true | |
| 62 ... | no _ = false | |
| 63 regular-language < h > f _ = false | |
| 1 | 64 |
| 34 | 65 finIn2 : FiniteSet In2 |
| 66 finIn2 = record { | |
| 67 Q←F = Q←F' | |
| 68 ; F←Q = F←Q' | |
| 69 ; finiso→ = finiso→' | |
| 70 ; finiso← = finiso←' | |
| 71 } where | |
| 72 Q←F' : Fin 2 → In2 | |
| 73 Q←F' zero = i0 | |
| 74 Q←F' (suc zero) = i1 | |
| 75 Q←F' (suc (suc ())) | |
| 76 F←Q' : In2 → Fin 2 | |
| 77 F←Q' i0 = zero | |
| 78 F←Q' i1 = suc (zero) | |
| 79 finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q | |
| 80 finiso→' i0 = refl | |
| 81 finiso→' i1 = refl | |
| 82 finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f | |
| 83 finiso←' zero = refl | |
| 84 finiso←' (suc zero) = refl | |
| 85 finiso←' (suc (suc ())) | |
| 11 | 86 |
| 87 | |
| 34 | 88 test-r1 = < i0 > & < i1 > |
| 89 test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i1 ∷ [] ) | |
| 90 test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i0 ∷ [] ) | |
| 1 | 91 |
| 36 | 92 issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool |
| 93 issub (r *) s f = issub r s f | |
| 94 issub (r & r₁) s f = issub r s f ∨ issub r₁ s f | |
| 95 issub (r || r₁) s f = issub r s f ∨ issub r₁ s f | |
| 96 issub < x > < s > f with cmpi f x s | |
| 97 issub < x > < s > f | yes p = true | |
| 98 issub < x > < s > f | no ¬p = false | |
| 99 issub < x > s f = false | |
| 100 | |
| 101 record RegexSub {Σ : Set} (R : Regex Σ) {n : ℕ } (fin : FiniteSet Σ {n} ): Set where | |
| 102 field | |
| 103 Subterm : Regex Σ | |
| 104 sub : issub R Subterm fin ≡ true | |
| 105 | |
| 37 | 106 open import Data.Product |
| 107 | |
| 108 | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
109 regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ × ( List (Regex Σ) ) |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
110 regex2nfa {Σ} (r *) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } , {!!} where |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
111 nr0 = proj₁ (regex2nfa r fin) |
| 35 | 112 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool |
| 113 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1) | |
| 114 Nstart : (Regex Σ) → Bool | |
| 115 Nstart s0 = NAutomaton.Nstart nr0 s0 | |
| 116 Nend : (Regex Σ) → Bool | |
| 117 Nend s0 = NAutomaton.Nend nr0 s0 | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
118 regex2nfa {Σ} (r0 & r1) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } , {!!} where |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
119 nr0 = proj₁ (regex2nfa r0 fin) |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
120 nr1 = proj₁ (regex2nfa r1 fin) |
| 35 | 121 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool |
| 122 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr1 s0 i s1 ) | |
| 123 Nstart : (Regex Σ) → Bool | |
| 124 Nstart s0 = NAutomaton.Nstart nr0 s0 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 ) | |
| 125 Nend : (Regex Σ) → Bool | |
| 126 Nend s0 = NAutomaton.Nend nr0 s0 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 ) | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
127 regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } , {!!} where |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
128 nr0 = proj₁ (regex2nfa r0 fin) |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
129 nr1 = proj₁ (regex2nfa r1 fin) |
| 34 | 130 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool |
| 35 | 131 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1 |
| 132 Nstart : (Regex Σ) → Bool | |
| 133 Nstart s0 = NAutomaton.Nstart nr0 s0 ∨ NAutomaton.Nstart nr1 s0 | |
| 134 Nend : (Regex Σ) → Bool | |
| 135 Nend s0 = NAutomaton.Nend nr0 s0 ∨ NAutomaton.Nend nr1 s0 | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
136 regex2nfa {Σ} < x > fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } , {!!} where |
| 35 | 137 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool |
| 138 Nδ r1 s r2 with cmpi fin s x | |
| 139 Nδ r1 s r2 | yes _ = true | |
| 140 Nδ r1 s r2 | no _ = false | |
| 34 | 141 Nstart : (Regex Σ) → Bool |
| 35 | 142 Nstart < s > with cmpi fin s x |
| 143 ... | yes _ = true | |
| 144 ... | no _ = false | |
| 145 Nstart _ = false | |
| 34 | 146 Nend : (Regex Σ) → Bool |
| 35 | 147 Nend _ = false |
| 148 | |
| 149 test-r4 = regex2nfa (< i0 > & < i1 >) finIn2 | |
| 8 | 150 |
| 36 | 151 -- testr5 = Naccept test-r4 {!!} ( i0 ∷ i1 ∷ [] ) |
| 35 | 152 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
153 rfin : {Σ : Set} → (s : List ( Regex Σ)) → FiniteSet (Regex Σ ) {length s } |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
154 rfin {Σ} s = record { |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
155 Q←F = Q←F' |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
156 ; F←Q = F←Q' |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
157 ; finiso→ = finiso→' |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
158 ; finiso← = finiso←' |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
159 } where |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
160 Q←F' : Fin (length s) → Regex Σ |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
161 Q←F' = {!!} |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
162 F←Q' : Regex Σ → Fin (length s) |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
163 F←Q' = {!!} |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
164 finiso→' : (q : Regex Σ) → Q←F' (F←Q' q) ≡ q |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
165 finiso→' = {!!} |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
166 finiso←' : (f : Fin (length s)) → F←Q' (Q←F' f) ≡ f |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
167 finiso←' = {!!} |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
168 |
| 37 | 169 reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n}) |
| 170 → ( regex : Regex Σ ) | |
| 171 → ( In : List Σ ) | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
172 → regular-language regex fin In ≡ Naccept {Regex Σ} {_} ( proj₁ ( regex2nfa {Σ} regex fin )) |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
173 (rfin (proj₂ ( regex2nfa {Σ} regex fin ) )) In |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
174 reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) In = {!!} |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
175 reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) In = {!!} |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
176 reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) In = {!!} |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
177 reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > In = {!!} |
| 35 | 178 |
| 179 | |
| 180 | |
| 37 | 181 |
| 182 | |
| 183 | |
| 184 | |
| 185 | |
| 186 | |
| 187 |