module deriveUtil where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.Fin
open import Data.List

open import regex
open import automaton
open import nfa
open import logic
open NAutomaton
open Automaton
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary


open Bool

data alpha2 : Set where
   a : alpha2
   b : alpha2

a-eq? : (x y : alpha2) → Dec (x ≡ y)
a-eq? a a = yes refl
a-eq? b b = yes refl
a-eq? a b = no (λ ())
a-eq? b a = no (λ ())

open Regex

open import derive alpha2 a-eq?
test11 = regex→automaton ( < a > & < b > )

test12 = accept test11 record { state =  < a > & < b > ; is-derived = unit } ( a ∷ b ∷ [] )
test13 = accept test11 record { state =  < a > & < b > ; is-derived = unit } ( a ∷ a ∷ [] )

test14 = regex-match ( (  < a > & < b > ) * ) ( a ∷ b ∷ a ∷ a ∷ [] )