module DFA where

-- A pair type 
record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

-- A list type
infixr  _∷_
data List (a : Set) : Set where
  [] : List a
  _∷_ : a → List a → List a

-- Elements of type x ∈ xs is a proof that x is somewhere in xs
data _∈_ {A : Set}(x : A) : (xs : List A) → Set where
  here : ∀ {xs} → x ∈ (x ∷ xs)
  there : ∀ {y xs} → x ∈ xs → x ∈ (y ∷ xs)

-- Elements of type a ≡ b is a proof that a and b are the same
data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

-- The empty type. There are no members of this type, so it is the same as false
data ⊥ : Set where

-- Negation is defined by a function that takes a proof and returns ⊥, which is impossible. In agda an inhabited type means a proof, and an uninhabited means no proof.
¬_ : Set → Set
¬ A = A → ⊥

-- A DFA is a five tuple of Q Σ q₀ δ F
record DFA (Q : Set) (Σ : Set) (q₀ : Q) (δ : Q × Σ → Q) (F : List Q) : Set where

-- The DFArun data type keeps track of a running dfa.
data DFArun {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (q : Q) → (w : List Σ) → Set where
  empty : {q : Q} → q ∈ F → DFArun dfa q []
  acceptOne : {ws : List Σ} →
              (w : Σ) →
              (q : Q) →
              DFArun dfa (δ (q , w)) ws →
              DFArun dfa q (w ∷ ws)

-- Accepts dfa w is a proof that running the dfa with input w is possible form the start state q₀
data Accepts {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (w : List Σ) → Set where
  accepts : ∀{w} → DFArun dfa q₀ w → Accepts dfa w

-- CantAccept dfa q w is a proof that running the dfa on imput w is impossible if we want to start at state q₀. It has to start in q instead.
data CantAccept {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (q : Q) → (w : List Σ) → Set where
  cantAccept : ∀ {w q} → DFArun dfa q w → ¬(q ≡ q₀) → CantAccept dfa q w


-- w ∈Lang dfa gives either a proof that w is in the language of the dfa, or that it isn't.
data _∈Lang_ {Q Σ q₀ δ F}(w : List Σ)(dfa : DFA Q Σ q₀ δ F) : Set where
  inLang : Accepts dfa w → w ∈Lang dfa
  notInLang : ∀{q} → CantAccept dfa q w → w ∈Lang dfa




-- Test stuff. Create a DFA which only accepts an input with an even number of a's

data TestQ : Set where
  evenNumberOfAs : TestQ
  oddNumberOfAs : TestQ

data TestΣ : Set where
  a : TestΣ
  b : TestΣ

Testδ : TestQ × TestΣ → TestQ
Testδ (evenNumberOfAs , a) = oddNumberOfAs
Testδ (evenNumberOfAs , b) = evenNumberOfAs
Testδ (oddNumberOfAs , a) = evenNumberOfAs
Testδ (oddNumberOfAs , b) = oddNumberOfAs

TestF : List TestQ
TestF = evenNumberOfAs ∷ []

TestDFA : DFA TestQ TestΣ evenNumberOfAs Testδ TestF
TestDFA = _ -- Since a DFA is a record with no fields, agda can infer it

-- Try to construct proofs for different input strings

input₁ input₂ input₃ : List TestΣ
input₁ = [] -- Empty string
input₂ = a ∷ b ∷ a ∷ a ∷ b ∷ [] -- Three a's
input₃ = b ∷ b ∷ a ∷ b ∷ a ∷ [] -- Two a's


-- The proofs are found automatically by agda, and no other proofs would type check
proof₁ : input₁ ∈Lang TestDFA -- Proof that input₁ is in the language
proof₁ = inLang (accepts (empty here))

proof₂ : input₂ ∈Lang TestDFA -- Proof that input₂ is not in the language
proof₂ = notInLang
           (cantAccept
            (acceptOne a oddNumberOfAs
             (acceptOne b evenNumberOfAs
              (acceptOne a evenNumberOfAs
               (acceptOne a oddNumberOfAs
                (acceptOne b evenNumberOfAs (empty here))))))
            (λ ()))

proof₃ : input₃ ∈Lang TestDFA -- Proof that input₃ is in the language
proof₃ = inLang
           (accepts
            (acceptOne b evenNumberOfAs
             (acceptOne b evenNumberOfAs
              (acceptOne a evenNumberOfAs
               (acceptOne b oddNumberOfAs
                (acceptOne a oddNumberOfAs (empty here)))))))