{-# OPTIONS --allow-unsolved-metas #-}
module dfa2regex where

open import Level renaming ( suc to Suc ; zero to Zero )
open import Data.List hiding ( any ;  [_] ; concat )
open import  Relation.Binary.PropositionalEquality hiding ( [_] ) 
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Empty
open import Data.Unit
open import Data.Maybe
open import logic
open import automaton
open import regex

open Automaton 

initail : {n  : Level} {Q : Set n} {Σ : Set } → (atm : Automaton Q Σ) → ((q : Q ) → Dec (F atm q))  → (Q → Regex Σ)
initail atm decF q with decF q
... | yes _ = ε
... | no _ = φ

add1 : {n  : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → List Σ → (Q → Regex Σ) → (Q → Regex Σ)
add1 atm [] qs q = qs q
add1 atm (x ∷ L) qs q with add1 atm L qs q | δ atm q x
... | rx | nq = ( < x > & qs nq ) || rx

{-# TERMINATING #-}
sumup : {n  : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → ((s t : Σ) → Dec (s ≡ t))  → List Σ → (Q → Regex Σ) → Q → Regex Σ
sumup atm dec L f q with RE-dec dec (f q) (add1 atm L f q) 
... | yes _ = f q
... | no _ = sumup atm dec L (add1 atm L f) q

L2 : List Σ2
L2 = s0 ∷  s1 ∷ []

dec2 : (s t : Σ2) → Dec (s ≡ t)
dec2 s0 s0 = yes refl
dec2 s0 s1 = no (λ ())
dec2 s1 s0 = no (λ ())
dec2 s1 s1 = yes refl

a16Fdec : (q : Q3) → Dec (F a16 q)
a16Fdec q₁ = no (λ ())
a16Fdec q₂ = yes a16q2
a16Fdec q₃ = no (λ ())

sm1 : Regex Σ2 
sm1 = sumup a16 dec2 L2 (initail a16 a16Fdec) q₁