module nfa where
open import Level renaming ( suc to Suc ; zero to Zero )

open import Relation.Binary.PropositionalEquality 
open import Data.List
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
          Nexists  : (Q → Set)  → Set

open NAutomaton

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

ntrace : {n  : Level} {Q : Set n} {Σ : Set } → (NFA : NAutomaton Q Σ) → (start : Q → Set ) → (input : List Σ ) → naccept NFA start input
     → ((Q → Set) → List Q)
     → List (List Q)
ntrace {n} {Q} {Σ} A q [] a list = list q ∷ []
ntrace {n} {Q} {Σ} A q (x ∷ t) a list = list q ∷ ( ntrace A {!!} t {!!} list )

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₁ ; Nexists = exists-in-Q3 }

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

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

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

--
-- ((Q → Set)  → Set) → ((Q → Set) → Set) → Set
--

data Nexists→exits  {n : Level} { Q : Set n }  {Σ : Set} ( NFA : NAutomaton Q  Σ ) : ((Q → Set) → Set) → Set where
   one-of : Nexists→exits NFA  (Nexists NFA)

subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → 
    (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ 
subset-construction {n} {Q} { Σ}  NFA = record {
        δ = λ qs x qs → Nexists NFA (λ q → Nδ NFA q x qs )
     ;  F = λ qs → Nexists NFA ( λ q → NF NFA q )
     ;  exists = Nexists→exits NFA   -- what this means?
   } 

subset-construction-lemma→ : { Q : Set } { Σ : Set  }   →   
    (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
    → (x : List Σ)
    → naccept NFA ( λ q1 → astart q1) x 
    → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
subset-construction-lemma→ = {!!}

subset-construction-lemma← : { Q : Set } { Σ : Set  }   → 
    (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
    → (x : List Σ)
    → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
    → naccept NFA ( λ q1 →  astart q1) x 
subset-construction-lemma← = {!!}

open import regular-language 

open RegularLanguage
open Automaton
open import Data.Empty 

Concat-exists : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) →  (states A ∨ states B → Set) → Set
Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ 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  ; Nexists = Concat-exists A B } 
   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 Σ ) 
   → 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 ( Concat-NFA A B )}
closed-in-concat {Σ} A B x = {!!}