{-# OPTIONS --safe  #-}

open import Level hiding (_⊔_)
import DFA as D
open import Data.Bool hiding (_<_; _≤_)
open import Data.Nat as ℕ
open import Data.Sum
open import Data.Fin using (Fin; fromℕ)
import Data.Fin as Fin
open import Data.Empty
open import Data.List
open import Data.Unit
open import Data.Maybe using (Maybe; just)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Unary.Any
open import Relation.Nullary.Decidable
import Data.Vec as V
import Data.Vec.Properties as V
open import Data.Vec using (Vec)
import Data.Nat.Properties as ℕ
open import Data.Product
open import Function.Base
open import Data.Nat.Logarithm
open import Relation.Binary.PropositionalEquality
open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; module CastReasoning)
open import Relation.Nullary.Negation.Core using (contraposition)
open import Utils
open import Auxiliary-Definitions
open import Finite

module DFA-Examples.Password-DFA (k : ℕ) where

private
  A : Set 0ℓ
  A = Fin k


open import DFA A

private
  ⟦DFA_⟧ = DFA.⟦DFA⟧₀

sink : ∀ {n} → Fin ( + n)
sink {n} = (fromℕ (ℕ.suc n))
-- The transition function of a password dfa
--   states:
--   0 is the first state
--   1+n (Fin.suc (fromℕ (ℕ.suc n))) is the sink state
accepting : ∀ {n} → Fin ( + n) → Bool
accepting {ℕ.zero} Fin.zero = true
accepting {ℕ.zero} (Fin.suc Fin.zero) = false
accepting {ℕ.suc n} Fin.zero = false
accepting {ℕ.suc n} (Fin.suc x) = accepting {n} x

password-dfa-δ : ∀ {n} → Vec A n → Fin ( + n) → A → Fin ( + n)
password-dfa-δ {} V.[] _ _ = Fin.zero
password-dfa-δ {ℕ.suc n} (a V.∷ w) (Fin.suc x) i =
  Fin.suc (password-dfa-δ w x i)
password-dfa-δ {ℕ.suc n} (a V.∷ w) Fin.zero i =
  case (a Fin.≟ i) of λ
  { (yes _) → Fin.zero
  ; (no _) → sink -- fromℕ (ℕ.suc n) -- sink state
  }

password-dfa-δ-suc : ∀ {n} → (a : A) → (w : Vec A n) → ∀ q i
                   → password-dfa-δ (a V.∷ w) (Fin.suc q) i ≡ Fin.suc (password-dfa-δ w q i)
password-dfa-δ-suc a V.[] q i = refl
password-dfa-δ-suc a (x V.∷ w) (Fin.suc q) i = refl
password-dfa-δ-suc a (x V.∷ w) Fin.zero i = refl

password-dfa : ∀ {n} → Vec A n → DFA
password-dfa {n} w = record
   --  states = elements of Fin (2 + n):
   -- 0 -> 1 -> ... -> n → 1+n
   { states = ℕ.suc (ℕ.suc n)
   ; q₀ = Fin.zero
   ; δ = λ q a → Fin.suc (password-dfa-δ w q a)
   ; accepts = accepting
   }

open DFA using (δ*; accepts) renaming (⟦Q_⟧ to L[_/_])

password-dfa-∷-δ* : ∀ {n} → (a : A) → (w : Vec A n) → ∀ q v
               → δ* (password-dfa (a V.∷ w)) (Fin.suc q) v ≡ Fin.suc (δ* (password-dfa w) q v)
password-dfa-∷-δ* a w _ [] = refl
password-dfa-∷-δ* a w q (i ∷ v) rewrite (password-dfa-δ-suc a w q i) = password-dfa-∷-δ* a w q' v
  where q' = Fin.suc (password-dfa-δ w q i)

L[password-dfa-∷] : ∀ {n} → (a : A) → (w : Vec A n) → ∀ q
               → L[ password-dfa (a V.∷ w) / (Fin.suc q) ] ≗ L[ password-dfa w / q ]
L[password-dfa-∷] a w q v = begin
  L[ [a∷w] / Fin.suc q ] v ≡⟨ DFA.⟦Q⟧-δ* [a∷w] (Fin.suc q) v ⟩
  accepts [a∷w] (δ* [a∷w] (Fin.suc q) v) ≡⟨ cong (accepts [a∷w]) (password-dfa-∷-δ* a w q v) ⟩
  accepts [a∷w] (Fin.suc (δ* [w] q v)) ≡⟨⟩
  accepts [w] (δ* [w] q v) ≡⟨ DFA.⟦Q⟧-δ* [w] q v ⟨
  L[ password-dfa w / q ] v
  ∎
  where
    [a∷w] = password-dfa (a V.∷ w)
    [w] = password-dfa (w)
    open ≡-Reasoning

password-dfa-sink : ∀ {n} → (w : Vec A n) → ∀ v → L[ password-dfa w / sink ] v ≡ false
password-dfa-sink V.[] [] = refl
password-dfa-sink V.[] (x ∷ v) = password-dfa-sink V.[] v
password-dfa-sink (a V.∷ w) v rewrite (L[password-dfa-∷] a w sink v) = password-dfa-sink w v

password-dfa-accepts-w : ∀ {n} → (w : Vec A n) → ⟦DFA password-dfa w ⟧ (V.toList w) ≡ true
password-dfa-accepts-w V.[] = refl
password-dfa-accepts-w (a V.∷ w) with (a Fin.≟ a)
... | (no a≢a) = ⊥-elim (a≢a refl)
... | (yes refl) =
      subst (_≡ true)
            (sym (L[password-dfa-∷] a w Fin.zero (V.toList w)))
            (password-dfa-accepts-w w)

password-dfa-accepts-only-w : ∀ {n} → (w : Vec A n) → ∀ v → ⟦DFA password-dfa w ⟧ v ≡ true → V.toList w ≡ v
password-dfa-accepts-only-w V.[] [] v∈L = refl
password-dfa-accepts-only-w V.[] (x ∷ v) xv∈L rewrite (password-dfa-sink V.[] v) = case xv∈L of λ ()
password-dfa-accepts-only-w (_ V.∷ w) [] ()
password-dfa-accepts-only-w (a V.∷ w) (i ∷ v) iv∈L with (a Fin.≟ i)
... | (no a≢i) =
      -- then we transition to sink state. so acceptance is a
      -- contradiction
      case subst (_≡ true) (password-dfa-sink (a V.∷ w) v) iv∈L of λ ()
... | (yes refl) = cong (a ∷_) (password-dfa-accepts-only-w w v v∈L)
  where
    v∈L : ⟦DFA password-dfa w ⟧ v ≡ true
    v∈L = subst (_≡ true) (L[password-dfa-∷] a w Fin.zero v) iv∈L

password-dfa-rejects-everything-else : ∀ {n} → (w : Vec A n) → ∀ v → V.toList w ≢ v → ⟦DFA password-dfa w ⟧ v ≡ false
password-dfa-rejects-everything-else w v w≢v with (⟦DFA password-dfa w ⟧ v) in eq
... | false = refl
... | true = ⊥-elim (w≢v (password-dfa-accepts-only-w w v eq))

password-dfa-rejects-other-lengths : ∀ {n} → (w : Vec A n) → ∀ v → length v ≢ n → ⟦DFA password-dfa w ⟧ v ≡ false
password-dfa-rejects-other-lengths {n} w v len[v]≢n with (⟦DFA password-dfa w ⟧ v) in eq
... | false = refl
... | true = ⊥-elim (len[v]≢n (subst (λ - → length - ≡ n) w≡v (V.length-toList w)))
  where
    w≡v : V.toList w ≡ v
    w≡v = password-dfa-accepts-only-w w v eq