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.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 

M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
M-Union {Σ} A B = record {
       states =  states A × states B
     ; astart = ( astart A , astart B )
     ; aℕ = {!!}
     ; afin = {!!}
     ; 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)

fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
fin-∨ {A} {B} {c} {b} fa fb = record {
              Q←F = f0
            ; F←Q = f1
            ; finiso→ = f2
            ; finiso← = f3
   } where
        f0 : Fin (c + b) → A ∨ B
        f0 x with <-cmp (toℕ x) c
        f0 x | tri< a ¬b ¬c = case1 ( Q←F fa (fromℕ≤ a ) )
        f0 x | tri≈ ¬a b ¬c = case2 ( Q←F fb (fromℕ≤ {!!} ))
        f0 x | tri> ¬a ¬b c = case2 ( Q←F fb (fromℕ≤ {!!} ))
        f1 : A ∨ B → Fin (c + b)
        f1 (case1 x) = inject+ b (F←Q fa x )
        f1 (case2 x) = raise c (F←Q fb x )
        f2 : (q : A ∨ B) → f0 (f1 q) ≡ q
        f2 = {!!}
        f3 : (f : Fin (c + b)) → f1 (f0 f) ≡ f
        f3 = {!!}

fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
fin→ {A} {a} fa = record {
              Q←F = f0
            ; F←Q = {!!}
            ; finiso→ = {!!}
            ; finiso← = {!!}
      } where
          f0 : Fin (exp 2 a) → A → Bool
          f0 = {!!}
          f1 : (A → Bool) → Fin (exp 2 a)
          f1 = {!!}

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

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 
       
lemma1 : {Σ : Set} →  ( x y : List Σ )
    → (A B : RegularLanguage Σ ) 
    → accept (automaton A) (astart A) x ≡ true
    → accept (automaton B) (astart B) y ≡ true
    → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) (Concat-NFA-start A B) ( x ++ y ) ≡ true
lemma1 {Σ} x y A B aA aB = lemma2 x (astart A) (Concat-NFA-start A B) aA where
    lemma2 : (x : List Σ) → (q : states A) → (qab : states A ∨ states B → Bool)
       → accept (automaton A) q x ≡ true → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) qab ( x ++ y ) ≡ true
    lemma2 [] q qab aA = {!!}
    lemma2 (h ∷ t ) q qab aA  = lemma2 t {!!} {!!} {!!}

-- 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 with  split {!!} {!!} x
-- closed-in-concat A B x | true = {!!}
-- closed-in-concat A B x | false = {!!}