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)

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

open Automaton

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

data  In2   : Set  where
   i0 : In2
   i1 : In2


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 ( λ () )

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  Σ
    → List  Σ → Bool
accept {Q} { Σ} M L = move (astart M) 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 _ = false

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


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

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

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

s1id : States1  → ℕ
s1id sr = 0
s1id ss = 1
s1id st = 2

record NAutomaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
          nδ : Q → Σ → List Q
          sid : Q  →  ℕ
          nstart : Q
          nend  : Q → Bool

open NAutomaton

insert : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) →  List Q  → Q  → List Q
insert  M  [] q =  q ∷ []
insert  M  ( q  ∷ T ) q' with  (sid M q ) ≟ (sid M q')
... | yes _ = insert  M  T q'
... | no _ = q  ∷ (insert  M  T q' )

merge : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) → List Q  → List Q  → List Q
merge  M L1 [] = L1
merge  M L1 ( H  ∷ L  ) =  insert M (merge M L1 L ) H

Nmoves : { Q : Set } { Σ : Set  }
    → NAutomaton Q  Σ
    → List Q → List  Σ → List Q
Nmoves {Q} { Σ} M q L = Nmoves1 q L []
   where
      Nmoves1 : (q : List Q ) ( L : List  Σ ) → List Q → List Q
      Nmoves1 q  [] _ = q
      Nmoves1 []  (_  ∷ L) LQ = Nmoves1 LQ L []
      Nmoves1 (q  ∷ T ) (H  ∷ L) LQ = Nmoves1 T  (H  ∷ L) ( merge M  ( nδ M q H ) LQ )


Naccept : { Q : Set } { Σ : Set  }
    → NAutomaton Q  Σ
    →  List  Σ → Bool
Naccept {Q} { Σ} M L =
       checkAccept ( Nmoves M ((nstart M)  ∷ [] )  L )
   where
      checkAccept : (q : List Q ) → Bool
      checkAccept [] = false
      checkAccept ( H ∷ L ) with (nend M) H
      ... | true = true
      ... | false = checkAccept L


transition2 : States1  → In2  → List States1
transition2 sr i0  = (sr ∷ [])
transition2 sr i1  = (ss ∷ sr ∷ [] )
transition2 ss i0  = (sr  ∷ [])
transition2 ss i1  = (st  ∷ [])
transition2 st i0  = (sr  ∷ [])
transition2 st i1  = (st  ∷ [])

am2  :  NAutomaton  States1 In2
am2  =  record { nδ = transition2 ; sid = s1id ; nstart = sr ; nend = fin1}


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