{-# OPTIONS --safe  #-}

open import Level
open import Data.Nat
open import Data.Fin
open import Data.Maybe
open import Data.Sum
open import Data.List
open import Function.Base
open import Data.Product

open import Auxiliary-Definitions

module Moore {ℓ : Level} (I O : Set ℓ) where

record Moore-Automaton : Set ℓ where
  field
    states : ℕ

  Q : Set
  Q = Fin states

  field
    initial : Q
    δ : Q → I → Q
    output : Q → O

  ⟦_/_⟧ : Q → List I → O
  ⟦ q / [] ⟧ = output q
  ⟦ q / (x ∷ w) ⟧ =
    ⟦ q / w ⟧

  L[_] : List I → O
  L[_] w = ⟦ initial / w ⟧