{-# OPTIONS --allow-unsolved-metas #-}
module regex 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


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

-- postulate a b c d : Set

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

infixr 40 _&_ _||_

r1' =    (< a > & < b >) & < c >
r1 =    < a > & < b > & < c >
any = < a > || < b >  || < c > || < d >
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 > )

data regular-expr  {Σ : Set} : Regex Σ → List Σ → Set where
   atom : (x :  Σ ) →  regular-expr < x > ( x ∷ [] )
   concat : {x y : Regex Σ} {t s : List Σ} →  regular-expr x t →  regular-expr y s →  regular-expr (x & y) (t ++ s )
   select : {x y : Regex Σ} {t : List Σ} →  regular-expr x t ∨  regular-expr y t →  regular-expr (x || y) t
   star-nil : {x : Regex Σ}  →  regular-expr (x *) []
   star : {x : Regex Σ}  → {lx next : List Σ} →  regular-expr x lx → regular-expr (x *) next →  regular-expr (x *) (lx ++ next)

test-regex : Set
test-regex = ¬ (regular-expr r1 ( a ∷ [] ) )

test-regex1 : regular-expr r1 ( a ∷ b ∷ c ∷ [] ) 
test-regex1 = concat (atom a) (concat (atom b) (atom c)) 

open import regular-language

-- match : {Σ : Set} → (r : Regex Σ ) → Automaton (Regex Σ) Σ

-- open import Data.Nat.DivMod

-- test-regex-even : Set
-- test-regex-even = (s : List char ) → regular-expr ( ( any & any ) * )  s  → (length s) mod 2 ≡ zero

empty? : {Σ : Set} →  Regex Σ → Maybe (Regex Σ)
empty? (r *) = just (r *)
empty? (r & s) with empty? r
... | nothing = nothing
... | just _ = empty? s
empty? (r || s) with empty? r | empty? s
... | nothing | nothing = nothing
... | just r1 | _ = just r1
... | _ | just s1 = just s1
empty? < x > = nothing

derivative : {Σ : Set} →  Regex Σ → Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Maybe (Maybe (Regex Σ))
derivative (r *) x dec  with derivative r x dec 
... | just (just r1) = just (just (r1 & (r *)))
... | just nothing = just (just (r *))
... | nothing = nothing
derivative (r & s) x dec  with derivative r x dec | derivative s x dec | empty? r
... | nothing | _ | _ = nothing
... | just nothing | nothing | _ = just (just s)
... | just nothing | just nothing  | _ = just (just s)
... | just nothing | just (just s1)  | nothing = just (just s)
... | just nothing | just (just s1)  | just _ = just (just (s1 || s))
... | just (just r1) | _ | nothing = just (just (r1 & s))
... | just (just r1) | just (just s1)  | just _  = just (just (s1 || (r1 & s)))
... | just (just r1) | _ | just _  = just (just (r1 & s))
derivative (r || s) x dec  with derivative r x dec  | derivative s x dec 
... | just (just r1) | just (just s1) = just (just ( r1 || s1 ) )
... | just nothing | _ = just nothing
... | _ | just nothing = just nothing
... | just (just r1) | _ = just (just r1)
... | _ | just (just s1) = just (just s1)
... | nothing | nothing = nothing
derivative < i > x dec  with dec i x
... | yes y = just nothing
... | no _ = nothing

open import automaton

regex→automaton :  {Σ : Set} →  Regex Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Automaton (Maybe (Maybe (Regex Σ))) Σ
regex→automaton {Σ} r dec = record {
      δ = δ
    ; F = F
   } where
      δ : Maybe (Maybe (Regex Σ)) → Σ → Maybe (Maybe (Regex Σ))
      δ nothing i = nothing
      δ (just nothing) i = nothing
      δ (just (just r)) i = derivative r i dec 
      F : Maybe (Maybe (Regex Σ)) → Set
      F (just (just (r *))) = ⊤
      F (just nothing) = ⊤
      F _ = ⊥

char-dec : (i j : char) → Dec (i ≡ j)
char-dec a a = yes refl
char-dec b b = yes refl
char-dec c c = yes refl
char-dec d d = yes refl
char-dec a b = no (λ ())
char-dec a c = no (λ ())
char-dec a d = no (λ ())
char-dec b a = no (λ ())
char-dec b c = no (λ ())
char-dec b d = no (λ ())
char-dec c a = no (λ ())
char-dec c b = no (λ ())
char-dec c d = no (λ ())
char-dec d a = no (λ ())
char-dec d b = no (λ ())
char-dec d c = no (λ ())

char-list : List char
char-list = a ∷ b ∷ c ∷ d ∷ []

a2 : accept (regex→automaton r2 char-dec ) (just (just r2)) ( a ∷ a ∷ b ∷ c ∷ [] )
a2 = tt
tr2 = trace (regex→automaton r2 char-dec ) (just (just r2)) ( a ∷ a ∷ b ∷ c ∷ [] ) a2

a1  : accept (regex→automaton < a > char-dec ) (just (just < a > )) ( a ∷ [] )
a1  = tt
tr1 = trace (regex→automaton < a > char-dec ) (just (just < a > )) ( a ∷ [] ) a1

a3  = accept (regex→automaton < a > char-dec ) (just (just (< a > & < b > ))) ( a ∷ b ∷ [] )
tr3  = trace (regex→automaton < a > char-dec ) (just (just (< a > & < b > ))) ( a ∷ b ∷ [] )


regex→accept :  {Σ : Set} →  (r : Regex Σ ) → (x : List Σ)  → (dec : (i j : Σ ) → Dec ( i ≡ j ))
   → accept (regex→automaton r dec) (just (just r)) x → regular-expr r x
regex→accept r x dec ac = {!!}

regex←accept :  {Σ : Set} →  (r : Regex Σ ) → (x : List Σ)  → (dec : (i j : Σ ) → Dec ( i ≡ j ))
   → regular-expr r x → accept (regex→automaton r dec) (just (just r)) x 
regex←accept r x dec re = {!!}