module sbconst1 where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
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 Data.Nat.DivMod
-- open import Data.Fin  using ( toℕ )


open import automaton
open Automaton
open NAutomaton

record FiniteSet ( Q : Set ) ( max1 : ℕ  )
        : Set  where
     field
        not-zero : max1 > 0
        ←ℕ : ℕ → Q
        ←Q : Q → ℕ 
        finite : (q : Q) → ←Q q < max1
        finiso→ :(q : Q) → ←ℕ ( ←Q q ) ≡ q
        finiso← :(n : ℕ) → ←Q ( ←ℕ n ) ≡ n
     max : ℕ
     max = max1

open FiniteSet

exists : { Q : Set} {n  : ℕ } → FiniteSet Q n → ( Q → Bool ) → Bool
exists {Q} {n} N f = exists1 (max N)
  where
     exists1 :  ℕ → Bool
     exists1 zero = false
     exists1 (suc i) with f (←ℕ N (suc i) ) 
     ... | true = true
     ... | false = exists1 i

list2sbst : {Q : Set} { n :  ℕ } → FiniteSet Q n → List Q → Q → Bool
list2sbst N [] _ = false
list2sbst N ( h ∷ t ) q with  ←Q N q  ≟ ←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 → 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

-- _div_ : ℕ → ℕ → Maybe ℕ
-- _div_ x zero = {!!}
-- _div_ x (suc y) = {!!}
-- 
-- _mod_ : ℕ → ℕ → Maybe ℕ
-- _mod_ = {!!}
-- 
-- lemma1 : { Q R : Set} {n m : ℕ } → FiniteSet Q n → FiniteSet R m → FiniteSet (Q × R) ( n * m )
-- lemma1 {Q} {R} {zero} {_} N M  = {!!}
-- lemma1 {Q} {R} {n} {zero} N M  = {!!}
-- lemma1 {Q} {R} {n} {m} N M = record {
--         not-zero = {!!}
--      ;  ←ℕ = λ i → ( ←ℕ N {!!} ,  ←ℕ M {!!})
--      ;  ←Q =  λ q → ( ←Q N ( proj₁ q ) * ( ←Q M (proj₂ q )))
--      ;  finite = {!!}
--      ;  finiso→ = {!!}
--      ;  finiso← = {!!}
--    }
-- 
-- _exp_ : ℕ → ℕ → ℕ
-- _exp_ = {!!}
-- 
-- sbstFin : { Q : Set} {n  : ℕ } → FiniteSet Q n → FiniteSet (Q → Bool) ( 2 exp n )
-- sbstFin = {!!}
--