{-# OPTIONS --allow-unsolved-metas #-} 
module nfa where
open import Level renaming ( suc to Suc ; zero to Zero )

open import Relation.Binary.PropositionalEquality 
open import Data.List
open import Relation.Nullary
open import automaton
open import logic

record NAutomaton {n : Level} ( Q : Set n ) ( Σ : Set  )
       : Set (Suc n) where
    field
          Nδ : Q → Σ → Q → Set
          NF : Q → Set

open NAutomaton

naccept : {n  : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set)  → Set) → NAutomaton Q Σ → (Q → Set) → List Σ → Set 
naccept {n} {Q} {Σ} Nexists nfa qs [] = Nexists (λ p → qs p ∧ NF nfa p )
naccept {n} {Q} {Σ} Nexists nfa qs (x ∷ input) = 
    naccept Nexists nfa (λ p' → Nexists (λ p → qs p ∧ Nδ nfa p x p' ))  input

qlist : {n : Level} {Q : Set n} → (P : Q → Set ) → ((q : Q) → Dec ( P q))  → List Q → List Q
qlist P dec [] = []
qlist P dec (q ∷ qs) with dec q
... | yes _ = q ∷ qlist P dec qs
... | no _ = qlist P dec qs

ntrace : {n  : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set)  → Set) → (nfa : NAutomaton Q Σ) → (qs : Q → Set ) → (input : List Σ )
     → naccept Nexists nfa qs input
     → ((q : Q) → Dec (qs q))
     → (next-dec : (qs : Q → Set) → ((q : Q) → Dec (qs q)) → (x : Σ) → (q : Q ) → Dec (Nexists (λ nq → qs nq ∧ Nδ nfa nq x q)))
     → List Q
     → List (List Q)
ntrace {n} {Q} {Σ} Nexists nfa qs [] a dec next-dec L = qlist qs dec L ∷ []
ntrace {n} {Q} {Σ} Nexists nfa qs (x ∷ t) a dec next-dec L = 
      qlist qs dec L ∷ ( ntrace Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a (next-dec qs dec x) next-dec L ) 

data exists-in-Q3 (P : Q3 → Set) :  Set where
    qe1 :  P q₁ → exists-in-Q3 P
    qe2 :  P q₂ → exists-in-Q3 P
    qe3 :  P q₃ → exists-in-Q3 P

record FindQ {n : Level} (Q : Set n) (Nexists : (Q → Set)  → Set) : Set (Suc n) where
    field
       create : {P : Q → Set} (q : Q ) → P q  → Nexists (λ q → P q) 
       found  : {P : Q → Set} → Nexists (λ q → P q) → Q
       exists : {P : Q → Set} → (n : Nexists (λ q → P q)) → P (found n)

FindQ3 : FindQ Q3 exists-in-Q3
FindQ3 = record { create = create ;  found = found ; exists = exists } where
    create :  {P : Q3 → Set} (q : Q3) → P q → exists-in-Q3 P
    create q₁ p = qe1 p
    create q₂ p = qe2 p
    create q₃ p = qe3 p
    found : {P : Q3 → Set} → exists-in-Q3 P → Q3
    found (qe1 x) = q₁
    found (qe2 x) = q₂
    found (qe3 x) = q₃
    exists : {P : Q3 → Set} (n : exists-in-Q3 P) → P (found n)
    exists (qe1 x) = x
    exists (qe2 x) = x
    exists (qe3 x) = x

data transition136 : Q3  → Σ2  → Q3 → Set  where
    d0 : transition136 q₁ s1 q₂ 
    d1 : transition136 q₁ s0 q₁ 
    d2 : transition136 q₂ s0 q₂ 
    d3 : transition136 q₂ s0 q₃ 
    d4 : transition136 q₂ s1 q₃ 
    d5 : transition136 q₃ s0 q₁ 

start136 : Q3 → Set
start136 q = q ≡ q₁

nfa136 :  NAutomaton Q3 Σ2 
nfa136 =  record { Nδ = transition136 ; NF = λ q → q ≡ q₁ }

example136-1 = naccept exists-in-Q3 nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )

example136-0 = naccept exists-in-Q3 nfa136 start136 ( s0 ∷ [] )

example136-2 = naccept exists-in-Q3 nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )

subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → (Nexists : (Q → Set)  → Set) → 
    (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ 
subset-construction {n} {Q} { Σ} Nexists  nfa = record {
        δ = λ qs x q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )
     ;  F = λ qs → Nexists ( λ q → qs q ∧ NF nfa q )
   } 

dfa136 : Automaton (Q3 → Set) Σ2
dfa136 = subset-construction  exists-in-Q3 nfa136

t136 : accept dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ []) → List ( Q3 → Set )
t136 = trace  dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) 

open _∧_

subset-construction-lemma→ : { Q : Set } { Σ : Set  }   →   
    (Nexists : (Q → Set)  → Set) →
    (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
    → (x : List Σ)
    → naccept Nexists NFA ( λ q1 → astart q1) x 
    → accept (  subset-construction Nexists NFA ) ( λ q1 → astart q1) x 
subset-construction-lemma→ {Q} {Σ} Nexists nfa qs [] na = na
subset-construction-lemma→ {Q} {Σ} Nexists nfa qs (x ∷ t) na = 
   subset-construction-lemma→ Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t na 

subset-construction-lemma← : { Q : Set } { Σ : Set  }   → 
    (Nexists : (Q → Set)  → Set) →
    (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
    → (x : List Σ)
    → accept (  subset-construction Nexists NFA ) ( λ q1 → astart q1) x 
    → naccept Nexists NFA ( λ q1 →  astart q1) x 
subset-construction-lemma← {Q} {Σ} Nexists nfa qs [] a = a 
subset-construction-lemma← {Q} {Σ} Nexists nfa qs (x ∷ t) a = 
   subset-construction-lemma← Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a 

open import regular-language 

open RegularLanguage
open Automaton
open import Data.Empty 

Union-Nexists : {n m : Level}  → {A : Set n} → {B : Set m}  → ( (A → Set) → Set )→ ( (B → Set) → Set ) → ( (A ∨ B → Set) → Set )
Union-Nexists {n} {m} {A} {B} PA PB P = PA (λ q → P (case1 q)) ∨ PB (λ q → P (case2 q))

Concat-NFA : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ )  → NAutomaton (states A ∨ states B) Σ 
Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend  }
   module Concat-NFA where
       data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where
         a-case   : {q : states A}  {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i))
         ab-trans : {q : states A}  {i : Σ } → F (automaton A) q  → δnfa ( case1 q) i (case2 (δ (automaton B) (astart B) i))
         b-case   : {q : states B}  {i : Σ } → δnfa ( case2 q) i (case2 (δ (automaton B) q i))
       nend : states A ∨ states B → Set
       nend (case2 q) = F (automaton B) q
       nend (case1 q) = F (automaton A) q ∧ F (automaton B) (astart B) -- empty B case

data state-is {n : Level} {Σ : Set }  (A B : RegularLanguage {n} Σ ) : (q : states A ∨ states B ) → Set where
   this : state-is A B (case1 (astart A))

record Split {Σ : Set} (A : List Σ → Set ) ( B : List Σ → Set ) (x :  List Σ ) : Set where
    field
        sp0 : List Σ
        sp1 : List Σ
        sp-concat : sp0 ++ sp1 ≡ x
        prop0 : A sp0 
        prop1 : B sp1 

open Split
split→AB :  {Σ : Set} → (A B : List Σ → Set ) → ( x : List Σ ) → split A B x → Split A B x
split→AB A B [] sp = record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = proj1 sp ; prop1 = proj2 sp }
split→AB A B (x ∷ t) (case1 sp) = record { sp0 = [] ; sp1 = x ∷ t ; sp-concat = refl ; prop0 = proj1 sp ; prop1 = proj2 sp } 
split→AB A B (x ∷ t) (case2 sp) with split→AB  (λ t1 → A ( x ∷ t1 )) B t sp
... | Sn = record { sp0 = x ∷ sp0 Sn ; sp1 = sp1 Sn ; sp-concat = cong (λ k → x ∷ k) (sp-concat Sn) ; prop0 = prop0 Sn ; prop1 = prop1 Sn } 

closed-in-concat :  {n : Level} {Σ : Set } → (A B : RegularLanguage {n}  Σ ) → ( x : List Σ ) 
   (PA : (states A  → Set)  → Set) (FA : FindQ (states A) PA)
   (PB : (states B  → Set)  → Set) (FB : FindQ (states B) PB)
   → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A B q
         ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
closed-in-concat {n} {Σ} A B x PA FA PB FB =  [ closed-in-concat→ x , closed-in-concat← x ] where
    open FindQ 
    fa : RegularLanguage  Σ
    fa = record {states = states A ∨ states B → Set ; astart = λ q → state-is A B q
         ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
    closed-in-concat→ : (x : List Σ) → Concat {n} {Σ} (contain A) (contain B) x → contain fa x
    closed-in-concat→ [] c = cc1 c where
        cc1 : contain A [] ∧ contain B [] → 
                PA (λ q → astart fa (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fa (case2 q) ∧ NF (Concat-NFA A B) (case2 q))
        cc1 ctab = case1 (create FA (astart A) [ this , [ proj1 ctab , proj2 ctab ] ] )
    -- fina : (F (automaton A) (astart A) ∧ accept (automaton B) (δ (automaton B) (astart B) x) t) 
    closed-in-concat→ (x ∷ t) (case1 fina ) = {!!}
    -- sp :  split (λ t1 → accept (automaton A) (δ (automaton A) (astart A) x) t1) (λ x₁ → accept (automaton B) (astart B) x₁) t
    closed-in-concat→ (x ∷ t) (case2 sp ) = {!!}
    closed-in-concat← : (x : List Σ) → contain fa x → Concat {n} {Σ} (contain A) (contain B) x
    closed-in-concat← [] cn = cc2 cn where
        cc2 : PA (λ q → astart fa (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fa (case2 q) ∧ NF (Concat-NFA A B) (case2 q))
            →   contain A [] ∧ contain B [] 
        -- ca : PA (λ q → state-is A B (case1 q) ∧ F (automaton A) q ∧ F (automaton B) (astart B))
        cc2 (case1 ca) = [ subst (λ k → accept (automaton A) k [] ) (cc5 _ (proj1 (exists FA ca))) cc3 , proj2 (proj2 (exists FA ca)) ] where
           cc5 : (q : states A) → state-is A B (case1 q) → q ≡ astart A
           cc5 q this = refl
           cc3 : accept (automaton A) (found FA ca ) []
           cc3 = proj1 (proj2 (exists FA  ca)) 
        cc2 (case2 cb) with proj1 (exists FB  cb)
        ... | ()
    closed-in-concat← (x ∷ t) cn = {!!}