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

open import Relation.Binary.PropositionalEquality 
open import Data.List hiding ([_])
open import Relation.Nullary
open import logic

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

open NAutomaton

record Automaton {n m : Level} (Q : Set n) (Σ : Set ) : Set (n ⊔ Suc m) where
    field
          δ : Q → Σ → Q
          F : Q → Set m

open Automaton

accept : {n m : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set m
accept {n} {Q} {Σ} atm q [] = F atm q
accept {n} {Q} {Σ} atm q (x ∷ input) = 
    accept atm (δ atm q x ) input

trace : {n m : Level} {Q : Set n} {Σ : Set } → (A : Automaton {n} {m} Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q
trace {n} {Q} {Σ} A q [] a = q ∷ []
trace {n} {Q} {Σ} A q (x ∷ t) a = q ∷ ( trace A (δ A q x) t a )

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

naccept : {n m : Level} {Q : Set n} {Σ : Set } → NAutomaton {n} {m} Q Σ → (Q → Set (Suc n ⊔ m)) → List Σ → Set (Suc n ⊔ m)
naccept {n} {m} {Q} {Σ} nfa qs [] = (q : Q) → qs q ∧ NF nfa q
naccept {n} {m} {Q} {Σ} nfa qs (x ∷ input) = 
    naccept nfa (λ q → (( q' : 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

naccept? : {n m : Level} {Q : Set n} {Σ : Set } → (nfa : NAutomaton {n} {m} Q Σ ) → Set (Suc (Suc n) ⊔ Suc m) 
naccept? {n} {m} {Q} {Σ} nfa = (qs : Dec (Q → Set (Suc n ⊔ m))) → (i : List Σ ) → Dec ((qs : Q → Set (Suc n ⊔ m)) → naccept nfa qs i)

ntrace : {n m : Level} {Q : Set n} {Σ : Set } → (nfa : NAutomaton {n} {m} Q Σ) → (qs : Dec (Q → Set (Suc n ⊔ m))) → (input : List Σ )
     → (a : naccept? {n} {m}{Q} {Σ} nfa  )
     → List (List Q)
ntrace {n} {m} {Q} {Σ} nfa qs [] a with a qs []
... | yes t = {!!}
... | no t = {!!}
ntrace {n} {m} {Q} {Σ} nfa qs (x ∷ t) a =
      {!!} ∷ ntrace nfa {!!} t a

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)

data Q3 : Set where
  q₁ : Q3
  q₂ : Q3
  q₃ : Q3

data Σ2 : Set where
  s0 : Σ2
  s1 : Σ2

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 (Suc Zero)
start136 q = Lift (Suc Zero) (q ≡ q₁)

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

accept-136 : naccept? {_} {_} {Q3} nfa136
accept-136 qs1 [] = {!!}
accept-136 qs1 (x ∷ i) = {!!}

example136-1 = naccept nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )
e1 : naccept nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )
e1 = {!!}

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

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

dfa136 : Automaton (Q3 → Set (Suc Zero)) Σ2
dfa136 = subset-construction nfa136

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

open _∧_
-- 
-- 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→ {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 
--