module automaton where

-- open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.List
open import Data.Maybe
-- open import Data.Bool using ( Bool ; true ; false ; _∧_ )
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import logic
-- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or )

record Automaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
        δ : Q → Σ → Q
        aend : Q → Bool

open Automaton

data  StatesQ   : Set  where
   q1 : StatesQ
   q2 : StatesQ
   q3 : StatesQ

data  In2   : Set  where
   i0 : In2
   i1 : In2

transitionQ : StatesQ  → In2 → StatesQ
transitionQ q1 i0 = q1
transitionQ q1 i1 = q2
transitionQ q2 i0 = q3
transitionQ q2 i1 = q2
transitionQ q3 i0 = q2
transitionQ q3 i1 = q2

aendQ : StatesQ → Bool
aendQ q2 = true
aendQ _ = false

a1 : Automaton StatesQ In2
a1 = record {
       δ = transitionQ
     ; aend = aendQ
   }

accept : { Q : Set } { Σ : Set  }
    → Automaton Q  Σ
    → (astart : Q)
    → List  Σ → Bool
accept {Q} { Σ} M q [] = aend M q
accept {Q} { Σ} M q ( H  ∷ T ) = accept M ( (δ M) q H ) T

test1 : accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ false
test1 = refl
test2 = accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) 

data  States1   : Set  where
   sr : States1
   ss : States1
   st : States1

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

transition1 : States1  → In2  → States1
transition1 sr i0  = sr
transition1 sr i1  = ss
transition1 ss i0  = sr
transition1 ss i1  = st
transition1 st i0  = sr
transition1 st i1  = st

fin1 :  States1  → Bool
fin1 st = true
fin1 ss = false
fin1 sr = false

am1  :  Automaton  States1 In2
am1  =  record {  δ = transition1 ; aend = fin1   }


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

reachable : { Q : Set } { Σ : Set  }
    → (M : Automaton Q  Σ  )
    → (astart q : Q )
    → (L : List  Σ ) → Set
reachable M astart q L = moves M astart  L ≡ q

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

ieq : (i i' : In2 ) → Dec ( i ≡ i' )
ieq i0 i0 = yes refl
ieq i1 i1 = yes refl
ieq i0 i1 = no ( λ () )
ieq i1 i0 = no ( λ () )

inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ 
inputnn {zero} {_} _ _ s = s
inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )

-- lemmaNN :  { Q : Set } { Σ : Set  } → (M : Automaton Q  Σ) →  ¬ accept M ( inputnn {n} x y [] )
-- lemmaNN = ?

lemma4 : {i n : ℕ } → i < n → i < suc n
lemma4 {0} {0} ()
lemma4 {0} {suc n} lt = s≤s z≤n
lemma4 {suc i} {0} ()
lemma4 {suc i} {suc n} (s≤s lt) =  s≤s (lemma4 lt)

lemma5 : {n : ℕ } → n < suc n
lemma5 {zero} = s≤s z≤n
lemma5 {suc n} =  s≤s lemma5

record accept-n { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (astart : Q ) (n : ℕ ) (s : {i : ℕ } → (i < n)  → Σ ) : Set where
   field
      r : (i : ℕ ) → i < suc n  → Q
      accept-1 : r 0 (s≤s z≤n)  ≡ astart
      accept-2 : (i : ℕ ) → (i<n : i < n ) → δ M (r i (lemma4 i<n)) (s i<n) ≡ r (suc i) (s≤s i<n)
      accept-3 : aend M (r n lemma5 ) ≡ true

get : { Σ : Set  } →  (x : List Σ ) → { i : ℕ } → i < length x  → Σ
get [] ()
get (h ∷ t) {0} (s≤s lt) = h
get (h ∷ t) {suc i} (s≤s lt) = get t lt

open import Data.Empty

lemma7 : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (h : Σ) → (t : List Σ ) → accept M q (h ∷ t) ≡ true →  accept M (δ M q h) t ≡ true
lemma7 M q h t eq with accept M (δ M q h) t
lemma7 M q h t refl | true = refl
lemma7 M q h t () | false 

trace : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → accept M q x ≡ true → List Q
trace M q [] _ = [ q ]
trace M q (h ∷ t)  eq = ( q ∷ trace M (δ M q h) t (lemma7 M q h t eq ) )

trace-lemma : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → (eq : accept M q x ≡ true ) → suc (length x) ≡ length (trace M q x eq)
trace-lemma M q [] eq = refl
trace-lemma M q (h ∷ t) eq = cong ( λ k → suc k ) ( trace-lemma M (δ M q h) t (lemma7 M q h t eq ))

open accept-n

lemma :  { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → accept M q x ≡ true → accept-n M q (length x) (get x )
lemma {Q} {Σ} M q [] eq = record { r = λ i lt → get [ q ] {i} lt ; accept-1 = refl ; accept-2 = λ _ () ; accept-3 = eq  } 
lemma {Q} {Σ} M q (h ∷ t) eq with lemma M (δ M q h) t (lemma7 M q h t eq) 
... | an = record { r = λ i lt → get (trace M q (h ∷ t) eq ) {i} (r1 lt) ; accept-1 = {!!} ; accept-2 = {!!} ; accept-3 = lemma8 (accept-3 an) } where
    r1 : {i : ℕ} → i < 2 + length t → i < length (trace M q (h ∷ t) eq)
    r1 lt rewrite trace-lemma M q (h ∷ t) eq = lt
    lemma9 : ( lt : suc (length t) < length (q ∷ trace M q (h ∷ t) eq) ) → r an (length t) lemma5 ≡ get (q ∷ trace M q (h ∷ t) eq ) {suc (length t)} lt 
    lemma9 = {!!}
    lemma8 : aend M (r an (length t) lemma5 ) ≡ true → aend M (get (trace M q (h ∷ t) eq) (r1 lemma5)) ≡ true
    lemma8 eq1 with trace-lemma M q ( h ∷ t ) eq
    ... | eq2 = subst (λ k → aend M k ≡ true ) (lemma9 {!!} ) eq1