{-# OPTIONS --allow-unsolved-metas #-}
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 import finiteSet

fin : FiniteSet hoge
fin = record {
        Q←F = Q←F
      ; F←Q  = F←Q
      ; finiso→ = finiso→
      ; finiso← = finiso←
   } where
       Q←F : Fin 4 → hoge
       Q←F zero = a
       Q←F (suc zero) = b
       Q←F (suc (suc zero)) = c
       Q←F (suc (suc (suc zero))) = d
       F←Q : hoge → Fin 4
       F←Q a = zero
       F←Q b = suc zero
       F←Q c = suc (suc zero)
       F←Q d = suc (suc (suc zero))
       finiso→ : (q : hoge) → Q←F (F←Q q) ≡ q
       finiso→ a = refl
       finiso→ b = refl
       finiso→ c = refl
       finiso→ d = refl
       finiso← : (f : Fin 4) → F←Q (Q←F f) ≡ f
       finiso← zero = refl
       finiso← (suc zero) = refl
       finiso← (suc (suc zero)) = refl
       finiso← (suc (suc (suc zero))) = refl
       finiso← (suc (suc (suc (suc ()))))

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

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

test-regex : regular-language 1r1' fin ( a ∷ [] ) ≡ false
test-regex = refl

test-regex1 : regular-language 1r1' fin ( a ∷ b ∷ c ∷ [] ) ≡ true
test-regex1 = refl


open import Data.Nat.DivMod

test-regex-even : Set
test-regex-even = (s : List hoge ) → regular-language ( ( 1any || 1any ) * )  fin s  ≡ true → (length s) mod 2 ≡ zero