{-# OPTIONS --safe  #-}

open import Level
open import Data.Nat
open import Data.Fin
open import Data.Maybe
open import Data.Sum
open import Data.Bool
open import Data.List
open import Function.Base
open import Data.Product
open import Relation.Binary.PropositionalEquality

module DFA {ℓ : Level} (A : Set ℓ) where

record DFA : Set ℓ where
  field
    states : ℕ

  Q : Set
  Q = Fin states

  field
    q₀ : Q
    δ : Q → A → Q
    accepts : Q → Bool

  δ* : Q → List A → Q
  δ* q [] = q
  δ* q (x ∷ w) = δ* (δ q x) w

  ⟦Q_⟧ : Q → List A → Bool
  ⟦Q q ⟧ [] = accepts q
  ⟦Q q ⟧ (a ∷ w) = ⟦Q δ q a ⟧ w

  ⟦Q⟧-δ* : ∀ q w → ⟦Q q ⟧ w ≡ accepts (δ* q w)
  ⟦Q⟧-δ* q [] = refl
  ⟦Q⟧-δ* q (x ∷ w) = ⟦Q⟧-δ* (δ q x) w

  ⟦DFA⟧₀ : List A → Bool
  ⟦DFA⟧₀ = ⟦Q q₀ ⟧


-- Same semantics of DFAs
_≈_ : DFA → DFA → Set ℓ
_≈_ M1 M2 = ∀ w → ⟦ M1 ⟧ w ≡ ⟦ M2 ⟧ w
  where
    ⟦_⟧ = DFA.⟦DFA⟧₀