{-# OPTIONS --allow-unsolved-metas #-} 
module regular-language where

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

language :  { Σ : Set } → Set (Suc Zero)
language {Σ} = List Σ → Set

open Automaton

record RegularLanguage {n : Level} ( Σ : Set ) : Set (Level.suc n )  where
   field
      states : Set n
      astart : states 
      automaton : Automaton states Σ
   contain : List Σ → Set 
   contain x = accept automaton astart x

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

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

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

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

data In2 : Set where
  i0 : In2
  i1 : In2

test-AB→split : {Σ : Set} → {A B : List In2 → Set} → 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-AB→split {_} {A} {B} = refl

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

M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ
M-Union {n} {Σ} A B = record {
       states =  states A × states B
     ; astart = ( astart A , astart B )
     ; automaton = record {
             δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
           ; F = λ q → ( F (automaton A) (proj₁ q) ∨ F (automaton B) (proj₂ q) )
        }
   }  

open _∧_

closed-in-union :  {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
closed-in-union A B [] = lemma where
   lemma : (F (automaton A) (astart A) ∨ F (automaton B) (astart B)) ⇔
           (F (automaton A) (astart A) ∨ F (automaton B) (astart B))
   lemma = [ id , id ]
closed-in-union {n} {Σ} A B ( h ∷ t ) = lemma4 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
   lemma4 : (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
   lemma4 [] qa qb = [ id , id ]
   lemma4 (h ∷ t ) qa qb = lemma4 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))

-- closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x {!!}
-- closed-in-concat = {!!}