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

t5 : ( n : ℕ ) → Set
t5 n = inputnn1 ( inputnn0 n i0 i1 [] ) ≡ true

--
--  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 Σ) → Q → Set where
    tend  : {q : Q} → aend fa q ≡ true → Trace fa [] q
    tnext : (q : Q) → {i : Σ} { is : List Σ} 
        → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q 

tr-len :  { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is ) 
tr-len {Q} {Σ} fa .[] q (tend x) = refl 
tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t)

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

tr-accept← : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is q
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→qs : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → Trace fa is q → List Q
tr→qs fa [] q (tend x) = []
tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr 

tr→qs=is : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡  length (tr→qs fa is q tr)
tr→qs=is fa .[] q (tend x) = refl
tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is  (δ fa q i) tr)

open Data.Maybe

-- head : {a : Set} → List a → Maybe a
-- head [] = nothing
-- head (h ∷ _ ) = just h

tr-append1 : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (i : Σ) → ( q : Q)  
    → (is : List Σ)
    → Trace fa is ( δ fa q i )  →  Trace fa (i ∷ is) q
tr-append1 fa i q is tr = tnext _ tr 

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 

record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (phase : ℕ)  ( q qd : Q )  : Set where
    field
       x y z : List Σ
       trace-z    : phase > 1 → Trace fa z  qd
       trace-yz   : phase > 0 → Trace fa (y ++ z)  qd
       trace-xyz  : phase ≡ 0 → Trace fa (x ++ y ++ z)  q
       trace-xyyz : phase ≡ 0 → Trace fa (x ++ y ++ y ++ z) q

open import nat

make-TA : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
     → (tr : Trace fa is q )
     → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
     → TA fa 0 q qd 
make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
   open TA
   tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase2 finq qd (tr→qs fa is q tr) ≡ true  → TA fa 1 q qd
   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q
   ... | true = {!!} 
   ... | false = {!!}
   tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa 0 q qd 
   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q
   ... | true = record { x = [] ; y = y TA0 ;  z = z TA0 ; trace-z = λ () ; trace-yz = λ _ → trace-yz TA0 a<sa 
           ; trace-xyz  = λ _ → subst (λ k → Trace fa (y TA0 ++ z TA0) k ) {!!}  (trace-yz TA0 a<sa)
           ; trace-xyyz = λ _ → {!!}} where
        TA0 : {!!}
        TA0 = tra-phase2 (δ fa q i ) is tr p
   ... | false = record { x = i ∷ x TA0 ; y = y TA0 ; z = z TA0 ; trace-z = λ () ; trace-yz = λ ()
            ; trace-xyz = λ _ → tnext q (trace-xyz TA0 refl ) ; trace-xyyz = λ _ → tnext q (trace-xyyz TA0 refl )} where
        TA0 : TA fa 0 (δ fa q i ) qd 
        TA0 = tra-phase1 (δ fa q i ) is tr p

open RegularLanguage
open import Data.Nat.Properties
open import nat

lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r ) 
lemmaNN r Rg = {!!} where
    n : ℕ
    n = suc (finite (afin r))
    nn =  inputnn0 n i0 i1 []
    nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
    nn01 zero = refl
    nn01 (suc i) with nn01 i
    ... | t = {!!}
    nn03 : accept (automaton r) (astart r) nn ≡ true
    nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
    count : In2 → List In2 → ℕ
    count _ [] = 0
    count i0 (i0 ∷ s) = suc (count i0 s)
    count i1 (i1 ∷ s) = suc (count i1 s)
    count x (_ ∷ s) = count x s
    nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
    nn10 = {!!}
    nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
    nn11 = {!!}
    nntrace = trace (automaton r) (astart r) nn
    nn04 :  Trace (automaton r) nn (astart r)
    nn04 = tr-accept← (automaton r) nn (astart r) nn03 
    nn07 : (n : ℕ) →  length (inputnn0 n i0 i1 []) ≡ n + n 
    nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where
       nn08 : (n : ℕ) → (s : List In2) → length (inputnn0 n i0 i1 s) ≡ n + n + length s
       nn08 zero s = refl
       nn08 (suc n) s = begin
         length (inputnn0 (suc n) i0 i1 s) ≡⟨ refl ⟩
         suc (length (inputnn0 n i0 i1 (i1 ∷ s))) ≡⟨ cong suc (nn08 n (i1 ∷ s)) ⟩
         suc (n + n + suc (length s)) ≡⟨ +-assoc (suc n) n _  ⟩
         suc n + (n + suc (length s)) ≡⟨ cong (λ k → suc n + k) (sym (+-assoc n  _ _))  ⟩
         suc n + ((n + 1) + length s) ≡⟨ cong (λ k → suc n + (k + length s)) (+-comm n _) ⟩
         suc n + (suc n + length s) ≡⟨ sym (+-assoc (suc n)  _ _) ⟩
         suc n + suc n + length s  ∎  where open ≡-Reasoning
    nn09 : (n m : ℕ) → n ≤ n + m
    nn09 zero m = z≤n
    nn09 (suc n) m = s≤s (nn09 n m)
    nn05 : length nntrace > finite (afin r)
    nn05 = begin
         suc (finite (afin r))  ≤⟨ nn09 _ _ ⟩
         n + n   ≡⟨ sym (nn07 n) ⟩
         length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s  ⟩
         {!!} ≤⟨ {!!} ⟩
         length nntrace ∎  where open ≤-Reasoning
    nn02 : {!!} -- TA (automaton r) {!!} {!!} {!!}
    nn02 = {!!} where -- make-TA (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) ? where
        nn06 : Dup-in-list ( afin r) nntrace
        nn06 = dup-in-list>n (afin r) nntrace nn05
    nn12 : (x y z : List In2)
        → ¬ y ≡ []
        → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true →  ¬ (accept (automaton r) (astart r)  (x ++ y ++ y ++ z) ≡ true)
    nn12 x y z p q = {!!} where
         mono-color : List In2 → Bool
         mono-color [] = true
         mono-color (i0 ∷ s) = mono-color0 s where
              mono-color0 : List In2 → Bool
              mono-color0 [] = true
              mono-color0 (i1 ∷ s) = false
              mono-color0 (i0 ∷ s) = mono-color0 s
         mono-color (i1 ∷ s) = mono-color1 s where
              mono-color1 : List In2 → Bool
              mono-color1 [] = true
              mono-color1 (i0 ∷ s) = false
              mono-color1 (i1 ∷ s) = mono-color1 s
         mono-color (i1 ∷ s) = {!!}
         i1-i0? : List In2 → Bool
         i1-i0? [] = false
         i1-i0? (i1 ∷ []) = false
         i1-i0? (i0 ∷ []) = false
         i1-i0? (i1 ∷ i0 ∷ s) = true
         i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1)  
         nn13 : mono-color y ≡ true → count i0  (x ++ y ++ z) ≡  count i1 (x ++ y ++ z) → 
             ¬ ( count i0   (x ++ y ++ y ++ z) ≡  count i1  (x ++ y ++ y ++ z) )
         nn13 = {!!}
         nn16 :  (s : List In2 ) →  accept  (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
         nn16 = {!!}
         nn15 :  (s : List In2 ) → i1-i0? s ≡ true → accept  (automaton r) (astart r) s ≡ false
         nn15 = {!!}
         nn14 : mono-color y ≡ false → i1-i0? (x ++ y ++ y ++ z) ≡ true
         nn14 = {!!}
         nn17 : accept (automaton r) (astart r) (x ++ y ++ z) ≡ true →  ¬ (accept (automaton r) (astart r)  (x ++ y ++ y ++ z) ≡ true)
         nn17 p q with mono-color y | inspect mono-color y
         ... | true | record { eq = eq } = {!!}
         ... | false | record { eq = eq } = {!!} -- q ( nn15 (x ++ y ++ z) (nn14 eq))