module nfa where

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


data  States1   : Set  where
   sr : States1
   ss : States1
   st : States1

data  In2   : Set  where
   i0 : In2
   i1 : In2


record NAutomaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
          Nδ : Q → Σ → Q → Bool
          Nstart : Q → Bool
          Nend  :  Q → Bool

open NAutomaton

record FiniteSet ( Q : Set ) { n : ℕ }
        : Set  where
     field
        Q←F : Fin n → Q
        F←Q : Q → Fin n 
        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
     lt0 : (n : ℕ) →  n Data.Nat.≤ n
     lt0 zero = z≤n
     lt0 (suc n) = s≤s (lt0 n)
     lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
     lt2 {zero} lt = z≤n
     lt2 {suc m} {zero} ()
     lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
     exists : ( Q → Bool ) → Bool
     exists p = exists1 n (lt0 n) p where
         exists1 : (m : ℕ ) → m Data.Nat.≤ n  → ( Q → Bool ) → Bool
         exists1  zero  _ _ = false
         exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) ∨ exists1 m (lt2 m<n) p

fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
fless zero = s≤s z≤n
fless (suc f) = s≤s ( fless f )

finState1 : FiniteSet States1 
finState1 = record {
        Q←F = Q←F
      ; F←Q  = F←Q
      ; finiso→ = finiso→
      ; finiso← = finiso←
   } where
       Q←F : Fin 3 → States1
       Q←F zero = sr
       Q←F (suc zero) = ss
       Q←F (suc (suc zero)) = st
       Q←F (suc (suc (suc ()))) 
       F←Q : States1 → Fin 3
       F←Q sr = zero
       F←Q ss = suc (zero)
       F←Q st = suc ( suc zero )
       finiso→ : (q : States1) → Q←F (F←Q q) ≡ q
       finiso→ sr = refl
       finiso→ ss = refl
       finiso→ st = refl
       finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
       finiso← zero = refl
       finiso← (suc zero) = refl
       finiso← (suc (suc zero)) = refl
       finiso← (suc (suc (suc ()))) 


open FiniteSet

Nmoves : { Q : Set } { Σ : Set  }
    → NAutomaton Q  Σ
    → {n : ℕ } → FiniteSet Q  {n}
    →  ( Q → Bool )  → Σ → Q → Bool
Nmoves {Q} { Σ} M fin  Qs  s q  =
      exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))


Naccept : { Q : Set } { Σ : Set  } 
    → NAutomaton Q  Σ
    → {n : ℕ } → FiniteSet Q {n}
    → List  Σ  → Bool
Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input
   where
      Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  →  Bool
      Naccept1 M sb []  = exists fin ( λ q → sb q ∧ Nend M q )
      Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb i ) t


transition3 : States1  → In2  → States1 → Bool
transition3 sr i0 sr = true
transition3 sr i1 ss = true
transition3 sr i1 sr = true
transition3 ss i0 sr = true
transition3 ss i1 st = true
transition3 st i0 sr = true
transition3 st i1 st = true
transition3 _ _ _ = false

fin1 :  States1  → Bool
fin1 st = true
fin1 ss = false
fin1 sr = false

start1 : States1 → Bool
start1 sr = true
start1 _ = false

am2  :  NAutomaton  States1 In2
am2  =  record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1}

example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 

fin0 :  States1  → Bool
fin0 st = false
fin0 ss = false
fin0 sr = false

test0 : Bool
test0 = exists finState1 fin0

test1 : Bool
test1 = exists finState1 fin1

test2 = Nmoves am2 finState1 start1 

-- test4 : Fin 2 → Bool
-- test4 zero = {!!}
-- test4 (suc zero) = {!!}
-- test4 (suc (suc ()))

--  0011
--  00000111111
inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
inputnn {zero} {_} _ _ s = s
inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )                                                                                                         
-- lemmaNN :  { Q : Set } { Σ : Set  } → ( x y : Σ ) → (M : NAutomaton Q  Σ)
--     → ( n :  ℕ )  → (fin :  FiniteSet Q  {n} ) 
--     →  Naccept M fin ( inputnn {n} x y [] )  ≡ true  
--     →  Naccept M fin ( inputnn {suc n} x y [] )  ≡ false  
-- lemmaNN {Q} {Σ} x y M n fin nac = {!!}