module regex1 where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Fin
open import Data.Nat hiding ( _≟_ )
open import Data.List hiding ( any )
import Data.Bool using ( Bool ; true ; false ; _∧_ )
open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
open import Relation.Nullary using (¬_; Dec; yes; no)


data Regex   ( Σ : Set  ) : Set  where
   _*    : Regex  Σ → Regex  Σ
   _&_   : Regex  Σ → Regex  Σ → Regex Σ
   _||_  : Regex  Σ → Regex  Σ → Regex Σ
   <_>   : Σ → Regex  Σ

-- postulate a b c d : Set

data hoge : Set where
   a : hoge
   b : hoge
   c : hoge
   d : hoge

infixr 40 _&_ _||_

r1' =    (< a > & < b >) & < c >
r1 =    < a > & < b > & < c >
any = < a > || < b >  || < c >
r2 =    ( any * ) & ( < a > & < b > & < c > )
r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )

open import nfa

split : {Σ : Set} → (List Σ → Bool)
      → ( List Σ → Bool) → List Σ → Bool
split x y  [] = x [] ∧ y []
split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

{-# TERMINATING #-}
repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
repeat x [] = true
repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )

open FiniteSet

cmpi :  {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡  F←Q fin y) 
cmpi fin x y = F←Q fin x ≟  F←Q fin y 

regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) →  List Σ → Bool
regular-language (x *) f = repeat ( regular-language x f )
regular-language (x & y) f = split ( regular-language x f ) ( regular-language y f )
regular-language (x || y) f = λ s → ( regular-language x f s )  ∨  ( regular-language y f s)
regular-language < h > f [] = false
regular-language < h > f (h1  ∷ [] ) with cmpi f h h1
... | yes _ = true
... | no _  = false
regular-language < h > f _ = false

finIn2 : FiniteSet In2
finIn2 = record {
        Q←F = Q←F'
      ; F←Q  = F←Q'
      ; finiso→ = finiso→'
      ; finiso← = finiso←'
   } where
       Q←F' : Fin 2 → In2
       Q←F' zero = i0
       Q←F' (suc zero) = i1
       Q←F' (suc (suc ())) 
       F←Q' : In2 → Fin 2
       F←Q' i0 = zero
       F←Q' i1 = suc (zero)
       finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
       finiso→' i0 = refl
       finiso→' i1 = refl
       finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
       finiso←' zero = refl
       finiso←' (suc zero) = refl
       finiso←' (suc (suc ()))


test-r1 = < i0 > & < i1 >
test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )

issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool
issub (r *) s f = issub r s f
issub (r & r₁) s f = issub r s f ∨ issub r₁ s f
issub (r || r₁) s f =  issub r s f ∨ issub r₁ s f
issub < x > < s > f with cmpi f x s 
issub < x > < s > f | yes p = true
issub < x > < s > f | no ¬p = false
issub < x > s f  = false

record RegexSub {Σ : Set} (R :  Regex Σ) {n : ℕ }  (fin :  FiniteSet Σ {n} ): Set where
    field
       Subterm : Regex Σ
       sub     : issub R Subterm fin ≡ true

open import Data.Product


regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ × ( List (Regex Σ) ) 
regex2nfa {Σ} (r *) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!}  where
          nr0 =  proj₁ (regex2nfa r fin)
          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1)
          Nstart : (Regex Σ) → Bool
          Nstart s0 = NAutomaton.Nstart nr0 s0
          Nend : (Regex Σ) → Bool
          Nend s0 =  NAutomaton.Nend nr0 s0
regex2nfa {Σ} (r0 & r1) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
          nr0 =  proj₁ (regex2nfa r0 fin)
          nr1 =  proj₁ (regex2nfa r1 fin)
          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧  NAutomaton.Nδ nr1 s0 i s1 )
          Nstart : (Regex Σ) → Bool
          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 )
          Nend : (Regex Σ) → Bool
          Nend s0 = NAutomaton.Nend nr0 s0  ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 )
regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
          nr0 =  proj₁ (regex2nfa r0 fin)
          nr1 =  proj₁ (regex2nfa r1 fin)
          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1
          Nstart : (Regex Σ) → Bool
          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ NAutomaton.Nstart nr1 s0 
          Nend : (Regex Σ) → Bool
          Nend s0 = NAutomaton.Nend nr0 s0  ∨ NAutomaton.Nend nr1 s0 
regex2nfa {Σ} < x > fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
          Nδ r1 s r2 with cmpi fin s x
          Nδ r1 s r2 | yes _ = true
          Nδ r1 s r2 | no _ = false
          Nstart : (Regex Σ) → Bool
          Nstart < s > with cmpi fin s x
          ... | yes _ = true
          ... | no  _ = false
          Nstart _ = false
          Nend  :  (Regex Σ) → Bool
          Nend  _ = false

test-r4 = regex2nfa  (< i0 > & < i1 >) finIn2 

-- testr5 = Naccept test-r4 {!!} ( i0  ∷ i1  ∷ [] )

rfin : {Σ : Set} → (s : List ( Regex Σ)) → FiniteSet (Regex Σ ) {length s } 
rfin {Σ} s = record {
        Q←F = Q←F'
      ; F←Q  = F←Q'
      ; finiso→ = finiso→'
      ; finiso← = finiso←'
  } where
        Q←F' : Fin (length s) → Regex Σ
        Q←F' = {!!}
        F←Q'  : Regex Σ → Fin (length s)
        F←Q'  = {!!}
        finiso→' : (q : Regex Σ) → Q←F' (F←Q' q) ≡ q
        finiso→' = {!!}
        finiso←' : (f : Fin (length s)) → F←Q' (Q←F' f) ≡ f
        finiso←' = {!!}

reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n}) 
     → ( regex : Regex Σ )
     → ( In : List Σ )
     → regular-language regex fin  In  ≡ Naccept {Regex Σ} {_} (  proj₁ ( regex2nfa {Σ} regex  fin  ))
         (rfin (proj₂  ( regex2nfa {Σ} regex  fin  ) )) In
reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) In = {!!}
reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) In = {!!}
reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) In = {!!}
reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > In = {!!}