module regular-language where

open import Level renaming ( suc to Suc ; zero to Zero )
open import Data.List 
open import Data.Nat hiding ( _≟_ )
open import Data.Fin hiding ( _+_ )
open import Data.Empty 
open import Data.Product
-- open import Data.Maybe
open import  Relation.Nullary
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import logic
open import nat
open import automaton
open import finiteSet

language : { Σ : Set } → Set
language {Σ} = List Σ → Bool

language-L : { Σ : Set } → Set
language-L {Σ} = List (List Σ)

open Automaton

record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
   field
      states : Set 
      astart : states 
      aℕ : ℕ
      afin : FiniteSet states {aℕ}
      automaton : Automaton states Σ
   contain : List Σ → Bool
   contain x = accept automaton astart x

Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Union {Σ} A B x = (A x ) \/ (B x)

split : {Σ : Set} → (List Σ → Bool)
      → ( List Σ → Bool) → List Σ → Bool
split x y  [] = x [] /\ y []
split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Concat {Σ} A B = split A B

{-# TERMINATING #-}
Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
Star {Σ} A = split A ( Star {Σ} A )

test-split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
       ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ 
       ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ 
       ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
       ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  ) 
   )
test-split {_} {A} {B} = refl

open RegularLanguage 
isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
isRegular A x r = A x ≡ contain r x 

postulate 
   fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}

M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
M-Union {Σ} A B = record {
       states =  states A × states B
     ; astart = ( astart A , astart B )
     ; aℕ = aℕ A * aℕ B
     ; afin = fin-× (afin A) (afin B)
     ; automaton = record {
             δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
           ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
        }
   } 

closed-in-union :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
closed-in-union A B [] = lemma where
   lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
           aend (automaton A) (astart A) \/ aend (automaton B) (astart B)
   lemma = refl
closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
   lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) → 
     accept (automaton A) qa t \/ accept (automaton B) qb  t
       ≡ accept (automaton (M-Union A B)) (qa , qb) t
   lemma1 [] qa qb = refl
   lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))

-- M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
-- M-Concat {Σ} A B = record {
--        states =  states A ∨ states B
--      ; astart = case1 (astart A )
--      ; automaton = record {
--              δ = {!!}
--            ; aend = {!!}
--         }
--    } 
-- 
-- closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
-- closed-in-concat = {!!}

open import nfa
open import sbconst2
open FiniteSet
open import Data.Nat.Properties
open import Relation.Binary as B hiding (Decidable)

postulate 
   fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
   fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}

Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ 
Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } where
       δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
       δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
       δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\ (equal? (afin B) qb (astart B) )
       δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁
       δnfa _ i _ = false
       nend : states A ∨ states B → Bool
       nend (case2 q) = aend (automaton B) q
       nend _ = false

-- Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
-- Concat-NFA-start A B (case1 q) = equal? (afin A) q (astart A)
-- Concat-NFA-start _ _ _ = false

Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q

M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
M-Concat {Σ} A B = record {
       states = states A ∨ states B → Bool
     ; astart = Concat-NFA-start A B
     ; aℕ = finℕ finf
     ; afin = finf
     ; automaton = subset-construction fin (Concat-NFA A B) (case1 (astart A))
   } where
       fin : FiniteSet (states A ∨ states B ) {aℕ A + aℕ B}
       fin = fin-∨ (afin A) (afin B)
       finf : FiniteSet (states A ∨ states B → Bool ) 
       finf = fin→ fin 
       
record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
    field
        sp0 : List Σ
        sp1 : List Σ
        sp-concat : sp0 ++ sp1 ≡ x
        prop0 : A sp0 ≡ true
        prop1 : B sp1 ≡ true

open Split

list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
list-empty++ [] (x ∷ y) ()
list-empty++ (x ∷ x₁) y ()

open _∧_

open import Relation.Binary.PropositionalEquality hiding ( [_] )

c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
   → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
   → split (λ t1 → A (h ∷ t1)) B t ≡ true
c-split-lemma {Σ} A B h t eq (case1 ¬p ) = sym ( begin
      true
  ≡⟨  sym eq  ⟩
      split A B (h ∷ t ) 
  ≡⟨⟩
      A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
  ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-1 (¬-bool-t ¬p)) ⟩
      false \/ split (λ t1 → A (h ∷ t1)) B t
  ≡⟨ bool-or-1 refl ⟩
      split (λ t1 → A (h ∷ t1)) B t
  ∎ ) where open ≡-Reasoning
c-split-lemma {Σ} A B h t eq (case2 ¬p ) = sym ( begin
      true
  ≡⟨  sym eq  ⟩
      split A B (h ∷ t ) 
  ≡⟨⟩
      A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
  ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-2 (¬-bool-t ¬p)) ⟩
      false \/ split (λ t1 → A (h ∷ t1)) B t
  ≡⟨ bool-or-1 refl ⟩
      split (λ t1 → A (h ∷ t1)) B t
  ∎ ) where open ≡-Reasoning

c-split :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
c-split {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true 
c-split {Σ} A B [] eq | yes eqa | yes eqb = 
    record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
c-split {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
c-split {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
c-split {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
... | no px | _ with c-split (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
c-split {Σ} A B (h ∷ t ) eq  | _ | no px with c-split (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }

split++ :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
split++ {Σ} A B [] [] eqa eqb = begin
       split A B [] 
     ≡⟨⟩
       A [] /\ B []
     ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
      true
     ∎  where open ≡-Reasoning
split++ {Σ} A B [] (h ∷ y ) eqa eqb = begin
      split A B (h ∷ y )
     ≡⟨⟩
      A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
     ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
      true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
     ≡⟨⟩
      true \/ split (λ t1 → A (h ∷ t1)) B y
     ≡⟨⟩
      true
     ∎  where open ≡-Reasoning
split++ {Σ} A B (h ∷ t) y eqa eqb = begin
       split A B ((h ∷ t) ++ y)  
     ≡⟨⟩
       A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
     ≡⟨ cong ( λ k →  A [] /\ B (h ∷ t ++ y) \/ k ) ( begin
          split (λ t1 → A (h ∷ t1)) B (t ++ y) 
        ≡⟨ split++ {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ⟩
          true 
        ∎ ) ⟩
       A [] /\ B (h ∷ t ++ y) \/ true
     ≡⟨ bool-or-3 ⟩
      true
     ∎  where open ≡-Reasoning

postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)

open NAutomaton

closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
closed-in-concat {Σ} A B x = ≡-Bool-func lemma3 lemma4 where
    finav = (fin-∨ (afin A) (afin B))
    NFA = (Concat-NFA A B)
    abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B
    abmove (case1 q) h = case1 (δ (automaton A) q h)
    abmove (case2 q) h = case2 (δ (automaton B) q h)
    nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
       exists finav (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
    nmove = {!!}
    lemma6 : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) 
        → Naccept NFA finav nq z  ≡ true
    lemma6 [] q nq _ fb = lemma8 where
        lemma8 : exists finav ( λ q → nq q /\ Nend NFA q ) ≡ true
        lemma8 = {!!}
    lemma6 (h ∷ t ) q nq nq=q fb = lemma6 t (δ (automaton B) q h) (Nmoves NFA finav nq h) (nmove (case2 q) nq nq=q h) fb 
    lemma7 : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
        → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true ) 
        → Naccept NFA finav nq (y ++ z)  ≡ true
    lemma7 [] z q nq nq=q fa fb = lemma6 z (astart B) nq {!!} fb
    lemma7 (h ∷ t) z q nq nq=q fa fb = lemma7 t z (δ (automaton A) q h) (Nmoves NFA finav nq h) (nmove (case1 q) nq nq=q h)  fa fb where
    lemma9 : equal? finav (case1 (astart A)) (case1 (astart A)) ≡ true
    lemma9 with Data.Fin._≟_ (F←Q finav (case1 (astart A))) ( F←Q finav (case1 (astart A)) )
    lemma9 | yes refl = refl
    lemma9 | no ¬p = ⊥-elim ( ¬p refl )
    lemma5 : Split (contain A) (contain B) x
        → Naccept NFA finav (equal? finav (case1 (astart A))) x  ≡ true
    lemma5 S = subst ( λ k → Naccept NFA finav (equal? finav (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
        (lemma7 (sp0 S) (sp1 S)  (astart A) (equal? finav (case1 (astart A))) lemma9 (prop0 S) (prop1 S) )
    lemma3 : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
    lemma3 concat with c-split (contain A) (contain B) x concat
    ... | S = begin
          accept (subset-construction finav NFA (case1 (astart A))) (Concat-NFA-start A B ) x 
       ≡⟨ ≡-Bool-func (subset-construction-lemma← finav NFA (case1 (astart A)) x ) 
          (subset-construction-lemma→ finav NFA (case1 (astart A)) x ) ⟩
          Naccept NFA finav (equal? finav (case1 (astart A))) x
       ≡⟨ lemma5 S ⟩
         true
       ∎  where open ≡-Reasoning
    lemma4 : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
    lemma4 C = {!!} -- split++ (contain A) (contain B) x y (accept ?) (accept ?)