module automaton 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 logic

record Automaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
        δ : Q → Σ → Q
        aend : Q → Bool

open Automaton

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

data  In2   : Set  where
   i0 : In2
   i1 : In2

moves : { Q : Set } { Σ : Set  }
    → Automaton Q  Σ
    → Q → List  Σ → Q
moves {Q} { Σ} M q L = move q L
   where
      move : (q : Q ) ( L : List  Σ ) → Q
      move q [] = q
      move q ( H  ∷ T ) = move ( δ M q H)  T

accept : { Q : Set } { Σ : Set  }
    → Automaton Q  Σ
    → (astart : Q)
    → List  Σ → Bool
accept {Q} { Σ} M astart L = move astart L
   where
      move : (q : Q ) ( L : List  Σ ) → Bool
      move q [] = aend M q
      move q ( H  ∷ T ) = move (  (δ M) q H ) T

transition1 : States1  → In2  → States1
transition1 sr i0  = sr
transition1 sr i1  = ss
transition1 ss i0  = sr
transition1 ss i1  = st
transition1 st i0  = sr
transition1 st i1  = st

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

am1  :  Automaton  States1 In2
am1  =  record {  δ = transition1 ; aend = fin1   }


example1-1 = accept am1 sr ( i0  ∷ i1  ∷ i0  ∷ [] )
example1-2 = accept am1 sr ( i1  ∷ i1  ∷ i1  ∷ [] )

reachable : { Q : Set } { Σ : Set  }
    → (M : Automaton Q  Σ  )
    → (astart q : Q )
    → (L : List  Σ ) → Set
reachable M astart q L = moves M astart  L ≡ q

example1-3 = reachable am1 sr st ( i1  ∷ i1  ∷ i1  ∷ [] )

ieq : (i i' : In2 ) → Dec ( i ≡ i' )
ieq i0 i0 = yes refl
ieq i1 i1 = yes refl
ieq i0 i1 = no ( λ () )
ieq i1 i0 = no ( λ () )

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  } → (M : Automaton Q  Σ) →  ¬ accept M ( inputnn {n} x y [] )
-- lemmaNN = ?