module non-regular where

open import Data.Nat
open import Data.Empty
open import Data.List
open import Data.Maybe hiding ( map )
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import logic
open import automaton
open import automaton-ex
open import finiteSetUtil
open import finiteSet
open import Relation.Nullary 
open import regular-language

open FiniteSet

inputnn :  List  In2 → Maybe (List In2)
inputnn [] = just []
inputnn  (i1 ∷ t) = just (i1 ∷ t)
inputnn  (i0 ∷ t) with inputnn t
... | nothing = nothing
... | just [] = nothing
... | just (i0 ∷ t1) = nothing   -- can't happen
... | just (i1 ∷ t1) = just t1   -- remove i1 from later part

inputnn1 :  List  In2 → Bool
inputnn1  s with inputnn  s 
... | nothing = false
... | just [] = true
... | just _ = false

t1 = inputnn1 ( i0 ∷ i1 ∷ [] )
t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
t3 = inputnn1 ( i0 ∷ i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )

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

t4 : inputnn1 ( inputnn0 5 i0 i1 [] ) ≡ true
t4 = refl

--
--  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
--  The function is determinted by inputs,
--

open RegularLanguage
open Automaton

open _∧_

data Trace { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) : (is : List Σ) → ( List Q) → Set where
    tend  : {q : Q} → aend fa q ≡ true → Trace fa [] (q ∷ [])
    tnext : {q : Q} → {i : Σ} { is : List Σ} {qs : List Q} 
        → Trace fa is (δ fa q i  ∷ qs) → Trace fa (i ∷ is) ( q ∷ δ fa q i  ∷ qs ) 

tr-accept→ : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → accept fa q is ≡ true
tr-accept→ {Q} {Σ} fa [] q [] (tend x)  = x
tr-accept→ {Q} {Σ} fa (i ∷ is) q (x ∷ qs) (tnext tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) qs tr

tr-accept← : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is (trace fa q is)
tr-accept← {Q} {Σ} fa [] q ac = tend ac
tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext (tend ac )
tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac) 


tr-append-is : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q )
     →  memberQ finq q qs ≡ true 
     →  Trace fa is (q ∷ qs) → List Σ ∧ List Q
tr-append-is {Q} {Σ} fa finq q [] [] () (tend x)
tr-append-is {Q} {Σ} fa finq q (x ∷ is) [] () tr
tr-append-is {Q} {Σ} fa finq q (x ∷ is) (q0 ∷ qs) mb tr with equal? finq q q0
... | true = ⟪ x ∷ [] , q0 ∷ [] ⟫
tr-append-is {Q} {Σ} fa finq q (x ∷ is) (.(δ fa q x) ∷ qs) mb (tnext tr) | false = tr3 (δ fa q x ∷ qs) tr2 is tr  where
     tr2 : memberQ finq q (δ fa q x ∷ qs) ≡ true
     tr2 = {!!}
     tr3 : (qs : List Q) → memberQ finq q qs ≡ true → (is :  List Σ) → Trace fa is qs → List Σ ∧ List Q
     tr3 (x ∷ []) mb [] (tend x₁) = {!!}
     tr3 (q0 ∷ qs) mb (x₁ ∷ is) (tnext tr) with equal? finq q q0
     ... | true = ⟪ x ∷ [] , {!!} ⟫
     ... | false = ⟪ x ∷ proj1 (tr3 qs mb is tr) , {!!} ⟫

tr-append : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q )
     → (mb :  memberQ finq q qs ≡ true )
     → (tr : Trace fa is ( q ∷ qs ))
     → Trace fa (proj1 (tr-append-is fa finq q is qs mb tr) ++ is) (proj2 (tr-append-is fa finq q is qs mb tr) ++ (q ∷ qs))
tr-append = {!!}

lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r ) 
lemmaNN r Rg = {!!}