module sbconst2 where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.List
open import Data.Bool using ( Bool ; true ; false ; _∧_ )

open import automaton
open import nfa
open NAutomaton
open Automaton
open FiniteSet

δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → nδ r i q )

subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
    (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
subset-construction {Q} { Σ} {n} N NFA = record {
        δ = λ q x → δconv N ( Nδ NFA ) q x
     ;  astart = astart1
     ;  aend = aend1
   } where
     astart1 : Q → Bool
     astart1 = Nstart NFA 
     aend1 : (Q → Bool) → Bool
     aend1 f = exists N ( λ q → f q ∧ Nend NFA q )

test4 = subset-construction finState1 am2

test5 = accept test4  ( i0  ∷ i1  ∷ i0  ∷ [] )
test6 = accept test4  ( i1  ∷ i1  ∷ i1  ∷ [] )