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