|
271
|
1 module deriveUtil where
|
|
|
2
|
|
|
3 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
4 open import Data.Nat
|
|
|
5 open import Data.Fin
|
|
|
6 open import Data.List
|
|
|
7
|
|
|
8 open import regex
|
|
|
9 open import automaton
|
|
|
10 open import nfa
|
|
|
11 open import logic
|
|
|
12 open NAutomaton
|
|
|
13 open Automaton
|
|
|
14 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
15 open import Relation.Nullary
|
|
|
16
|
|
|
17
|
|
|
18 open Bool
|
|
|
19
|
|
|
20 data alpha2 : Set where
|
|
|
21 a : alpha2
|
|
|
22 b : alpha2
|
|
|
23
|
|
|
24 a-eq? : (x y : alpha2) → Dec (x ≡ y)
|
|
|
25 a-eq? a a = yes refl
|
|
|
26 a-eq? b b = yes refl
|
|
|
27 a-eq? a b = no (λ ())
|
|
|
28 a-eq? b a = no (λ ())
|
|
|
29
|
|
|
30 open Regex
|
|
|
31
|
|
272
|
32 open import finiteSet
|
|
|
33
|
|
|
34 fin-a : FiniteSet alpha2
|
|
|
35 fin-a = record {
|
|
|
36 finite = finite0
|
|
|
37 ; Q←F = Q←F0
|
|
|
38 ; F←Q = F←Q0
|
|
|
39 ; finiso→ = finiso→0
|
|
|
40 ; finiso← = finiso←0
|
|
|
41 } where
|
|
|
42 finite0 : ℕ
|
|
|
43 finite0 = 2
|
|
|
44 Q←F0 : Fin finite0 → alpha2
|
|
|
45 Q←F0 zero = a
|
|
|
46 Q←F0 (suc zero) = b
|
|
|
47 F←Q0 : alpha2 → Fin finite0
|
|
|
48 F←Q0 a = # 0
|
|
|
49 F←Q0 b = # 1
|
|
|
50 finiso→0 : (q : alpha2) → Q←F0 ( F←Q0 q ) ≡ q
|
|
|
51 finiso→0 a = refl
|
|
|
52 finiso→0 b = refl
|
|
|
53 finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f
|
|
|
54 finiso←0 zero = refl
|
|
|
55 finiso←0 (suc zero) = refl
|
|
|
56
|
|
|
57
|
|
|
58 open import derive alpha2 fin-a a-eq?
|
|
271
|
59 test11 = regex→automaton ( < a > & < b > )
|
|
|
60
|
|
|
61 test12 = accept test11 record { state = < a > & < b > ; is-derived = unit } ( a ∷ b ∷ [] )
|
|
|
62 test13 = accept test11 record { state = < a > & < b > ; is-derived = unit } ( a ∷ a ∷ [] )
|
|
|
63
|
|
|
64 test14 = regex-match ( ( < a > & < b > ) * ) ( a ∷ b ∷ a ∷ a ∷ [] )
|
|
272
|
65
|
|
|
66 test15 = regex-derive ( ( < a > & < b > ) * ∷ [] )
|
|
|
67 test16 = regex-derive test15
|
|
|
68 test17 : regex-derive test16 ≡ test16
|
|
|
69 test17 = refl
|
