module derive where

open import nfa
open import regex1
open import Data.Nat hiding ( _<_ ; _>_ )
open import Data.Fin hiding ( _<_ )
open import Data.List hiding ( [_] )

open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)

open import finiteSet

finIn2 : FiniteSet In2
finIn2 = record {
        Q←F = Q←F'
      ; F←Q  = F←Q'
      ; finiso→ = finiso→'
      ; finiso← = finiso←'
   } where
       Q←F' : Fin 2 → In2
       Q←F' zero = i0
       Q←F' (suc zero) = i1
       Q←F' (suc (suc ())) 
       F←Q' : In2 → Fin 2
       F←Q' i0 = zero
       F←Q' i1 = suc (zero)
       finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
       finiso→' i0 = refl
       finiso→' i1 = refl
       finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
       finiso←' zero = refl
       finiso←' (suc zero) = refl
       finiso←' (suc (suc ()))


tr1 = < i0 > & < i1 >
tr2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
tr3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
tr4 = (< i0 > * ) & < i1 >
tr5 = ( ((< i0 > * ) & < i1 > ) || ( < i1 > & ( ( < i1 > * ) || ( < i0 > * )) ) ) *

sb : { Σ : Set } → Regex Σ → List ( Regex Σ )
sb (x *) =  map (λ r → ( r & (x *) )) ( sb x ) ++ ( sb x ) 
sb (x & y) = map (λ r → ( r & y )) ( sb x ) ++ ( sb y ) 
sb (x || y) = sb x ++ sb y 
sb < x > = < x >  ∷ []


nth : { S : Set } → (x : List S ) → Fin ( length x ) → S
nth [] ()
nth (s ∷ t) zero = s
nth (_ ∷ t) (suc f) = nth t f