{-# 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 (λ q → qs q ∧ NF nfa q )
naccept {n} {Q} {Σ} Nexists nfa qs (x ∷ input) = 
    naccept Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' ))  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

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 ∷ [] )

Q3List : List Q3
Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []

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 : RegularLanguage {n} Σ ) : (a : states A ) → Set where
   this : (a : states A)  → state-is A a

closed-in-concat :  {n : Level} {Σ : Set } → (A B : RegularLanguage {n}  Σ ) → ( x : List Σ ) 
   (PA : (states A  → Set)  → Set) 
   (PB : (states B  → Set)  → Set) 
   → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A)
         ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
closed-in-concat {n} {Σ} A B x PA PB =  [ closed-in-concat→ x , closed-in-concat← x ] where
    fa : RegularLanguage  Σ
    fa = record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A)
         ; 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 {!!}
    closed-in-concat→ (x ∷ t) = {!!}
    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 [] 
        cc2 (case1 ca) = {!!}
        cc2 (case2 cb) = {!!}
    closed-in-concat← (x ∷ t) = {!!}