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
     → ((qs : Q → Set) (q : Q) → Dec (qs q ∧ NF nfa q))
     → ((qs : Q → Set) (x : Σ) (t : List Σ) (q : Q) → Dec (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q') t))
     → List Q
     → List (List Q)
ntrace {n} {Q} {Σ} Nexists nfa qs [] a decNF decNδ L = qlist (λ q → qs q ∧ NF nfa q) (decNF qs) L ∷ []
ntrace {n} {Q} {Σ} Nexists nfa qs (x ∷ t) a decNF decNδ L = 
      qlist (λ q → (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q' ) t )) (decNδ qs x t) L
      ∷ ( ntrace Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a decNF decNδ L )

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

nfa136-FN : (q : Q3 ) → Dec ( NF nfa136 q )
nfa136-FN q₁ = yes refl
nfa136-FN q₂ = no (λ ())
nfa136-FN q₃ = no (λ ())

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

decFN136 : (qs qs' : Q3 → Set)  → (x : List Σ2) → naccept exists-in-Q3 nfa136 qs x → (q : Q3) → Dec (qs' q ∧ NF nfa136 q)
decFN136 qs qs' (_ ∷ _)  _ _ = {!!}
decFN136 qs qs' [] (qe1 x) q₁ = yes [ {!!} , refl ]
decFN136 qs qs' []  _ q₂ = no (λ ())
decFN136 qs qs' []  _ q₃ = no (λ ())

decF̨δ136 :  (qs qs' : Q3 → Set) (s : Σ2) (t x : List Σ2) → naccept exists-in-Q3 nfa136 qs x → (q : Q3) →
    Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q s q') t)
decF̨δ136 qs qs' s t x a q₁ = {!!}
decF̨δ136 qs qs' s t x a q₂ = {!!}
decF̨δ136 qs qs' s t x a q₃ = {!!}

nfa136trace : (qs : Q3 → Set) → (input : List Σ2 ) → naccept exists-in-Q3 nfa136 qs input → List (List Q3)
nfa136trace qs x a = ntrace exists-in-Q3 nfa136 qs x a (λ qs' q → decFN136 qs qs' x a q ) (λ qs' s t q →  decF̨δ136 qs qs' s t x a q ) Q3List

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

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→ = {!!}

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← = {!!}

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 {Σ} A B x = {!!}