|
36
|
1 module derive where
|
|
|
2
|
|
|
3 open import nfa
|
|
|
4 open import regex1
|
|
44
|
5 open import Data.Nat hiding ( _<_ ; _>_ )
|
|
|
6 open import Data.Fin hiding ( _<_ )
|
|
|
7 open import Data.List hiding ( [_] )
|
|
36
|
8
|
|
|
9 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
|
|
44
|
10 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
11 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
12
|
|
|
13 open import finiteSet
|
|
|
14
|
|
|
15 finIn2 : FiniteSet In2
|
|
|
16 finIn2 = record {
|
|
|
17 Q←F = Q←F'
|
|
|
18 ; F←Q = F←Q'
|
|
|
19 ; finiso→ = finiso→'
|
|
|
20 ; finiso← = finiso←'
|
|
|
21 } where
|
|
|
22 Q←F' : Fin 2 → In2
|
|
|
23 Q←F' zero = i0
|
|
|
24 Q←F' (suc zero) = i1
|
|
|
25 Q←F' (suc (suc ()))
|
|
|
26 F←Q' : In2 → Fin 2
|
|
|
27 F←Q' i0 = zero
|
|
|
28 F←Q' i1 = suc (zero)
|
|
|
29 finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
|
|
|
30 finiso→' i0 = refl
|
|
|
31 finiso→' i1 = refl
|
|
|
32 finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
|
|
|
33 finiso←' zero = refl
|
|
|
34 finiso←' (suc zero) = refl
|
|
|
35 finiso←' (suc (suc ()))
|
|
|
36
|
|
|
37
|
|
45
|
38 tr1 = < i0 > & < i1 >
|
|
|
39 tr2 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i1 ∷ [] )
|
|
|
40 tr3 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i0 ∷ [] )
|
|
|
41 tr4 = (< i0 > * ) & < i1 >
|
|
|
42 tr5 = ( ((< i0 > * ) & < i1 > ) || ( < i1 > & ( ( < i1 > * ) || ( < i0 > * )) ) ) *
|
|
44
|
43
|
|
45
|
44 sb : { Σ : Set } → Regex Σ → List ( Regex Σ )
|
|
|
45 sb (x *) = map (λ r → ( r & (x *) )) ( sb x ) ++ ( sb x )
|
|
|
46 sb (x & y) = map (λ r → ( r & y )) ( sb x ) ++ ( sb y )
|
|
|
47 sb (x || y) = sb x ++ sb y
|
|
|
48 sb < x > = < x > ∷ []
|
|
44
|
49
|
|
|
50
|
|
45
|
51 nth : { S : Set } → (x : List S ) → Fin ( length x ) → S
|
|
|
52 nth [] ()
|
|
|
53 nth (s ∷ t) zero = s
|
|
|
54 nth (_ ∷ t) (suc f) = nth t f
|
