module sbconst1 where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat hiding ( _≟_ )
open import Data.Fin
open import Data.List
open import Data.Maybe
open import Data.Bool using ( Bool ; true ; false ; _∧_ )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product
open import finiteSet

open import automaton
open import nfa-list
open Automaton
open NAutomaton

open FiniteSet

list2sbst : {Q : Set} { n :  ℕ } → FiniteSet Q {n} → List Q → Q → Bool
list2sbst N [] _ = false
list2sbst N ( h ∷ t ) q with  F←Q N q  ≟ F←Q N h 
... | yes _ = true
... | no _ = list2sbst N t q


δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → List Q ) → (Q → Bool) → Σ → (Q → Bool)
δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r ∧ list2sbst N (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 = list2sbst N [ nstart NFA ]
     aend1 : (Q → Bool) → Bool
     aend1 f = exists N f