module automaton where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Fin
open import Data.List 
open import Data.Bool using ( Bool ; true ; false )
open import  Relation.Binary.PropositionalEquality

record Automaton ( Q : Set ) ( Σ : Set  ) 
          ( δ : Q → Σ → Q ) ( q0 : Q ) ( F : Q → Bool )
       : Set  where

data  States1   : Set  where
   r : States1
   s : States1
   t : States1

data  In2   : Set  where
   i0 : In2
   i1 : In2

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

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

transition1 : States1  → In2  → States1 
transition1 r i0  = r
transition1 r i1  = s
transition1 s i0  = r
transition1 s i1  = t
transition1 t i0  = r
transition1 t i1  = t

fin1 :  States1  → Bool 
fin1 t = true
fin1 _ = false

am1  :  Automaton  States1 In2 transition1 r fin1
am1  =  record {}


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

reachable : { Q : Set } { Σ : Set  } { δ : Q → Σ → Q } { q0 : Q } { F : Q → Bool }
    → (M : Automaton Q  Σ  δ  q0  F )
    → (q : Q )
    → (L : List  Σ ) → Set 
reachable {_} {_} {_} {q0} {_} M q L = moves M q0 L ≡ q

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

open import Relation.Nullary using (¬_; Dec; yes; no)

state≟ : (s s' : States1 ) → Dec  ( s ≡ s' )
state≟ r r = yes refl
state≟ s s = yes refl
state≟ t t = yes refl
state≟ r t = no  λ()
state≟ r s = no  λ()
state≟ s t = no  λ()
state≟ s r = no  λ()
state≟ t s = no  λ()
state≟ t r = no  λ()

record NAutomaton ( Q : Set ) ( Σ : Set  ) 
          ( δ : Q → Σ → List Q ) ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) ) ( q0 : Q ) ( F : Q → Bool )
       : Set  where

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

merge : { Q : Set } →  ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) )  → List Q  → List Q  → List Q  
merge  _≟_ L1 [] = L1
merge  _≟_ L1 ( H  ∷ L  ) =  insert _≟_ (merge _≟_ L1 L ) H 

Nmoves : { Q : Set } { Σ : Set  } { δ : Q → Σ → List Q }  { _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) } { q0 : Q } { F : Q → Bool }
    → NAutomaton Q  Σ  δ  _≟_  q0  F
    → List Q → List  Σ → List Q
Nmoves {Q} { Σ} { δ } {_≟_} { q0 } { F } _ 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 _≟_  ( δ q H ) LQ )


Naccept : { Q : Set } { Σ : Set  } { δ : Q → Σ → List Q }  { _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) } { q0 : Q } { F : Q → Bool }
    → NAutomaton Q  Σ  δ  _≟_  q0  F
    →  List  Σ → Bool
Naccept {Q} { Σ} { δ } {_≟_} { q0 } { F } M L =
       checkAccept ( Nmoves M (q0  ∷ [] )  [] )
   where
      checkAccept : (q : List Q ) → Bool
      checkAccept [] = false
      checkAccept ( H ∷ L ) with F H
      ... | true = true
      ... | false = checkAccept L


transition2 : States1  → In2  → List States1 
transition2 r i0  = (r ∷ [])
transition2 r i1  = (s ∷ r ∷ [] )
transition2 s i0  = (r  ∷ [])
transition2 s i1  = (t  ∷ [])
transition2 t i0  = (r  ∷ [])
transition2 t i1  = (t  ∷ [])

am2  :  NAutomaton  States1 In2 transition2 state≟ r fin1
am2  =  record {}


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