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
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  Σ

open import nfa

_‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
x ‖ y = λ s → x s ∨ y s


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

_・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
x ・ y = λ z → split x y z

{-# 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 = ( regular-language x f ) ・ ( regular-language y f )
regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )
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  ∷ [] )

regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } {fin : FiniteSet Σ {n}} → NAutomaton (Regex Σ) Σ
regex2nfa {Σ} r {n} {fin} = record {
          Nδ     = Nδ
      ;   Nstart = Nstart
      ;   Nend   = Nend
  } where
          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
          Nδ = {!!}
          Nstart : (Regex Σ) → Bool
          Nstart = {!!}
          Nend  :  (Regex Σ) → Bool
          Nend  = {!!}