{-# 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

-- 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 Σ → Bool
empty? (r *) = true
empty? (r & s) with empty? r
... | false = false
... | true  = empty? s
empty? (r || s) with empty? r | empty? s
... | false | false = false
... | true | _ = true
... | _ | true = true
empty? < x > = false

data RexResult {Σ : Set}  : Set where
   fail     : RexResult
   finish   : RexResult
   continue : (Regex Σ) → RexResult

derivative : {Σ : Set} →  Regex Σ → Σ → ((i j : Σ ) → Dec ( i ≡ j )) → RexResult
derivative (r *) x dec  with derivative r x dec 
... | continue r1 = continue (r1 & (r *))
... | finish = continue (r *)
... | fail = fail
derivative (r & s) x dec  with derivative r x dec | derivative s x dec | empty? r
... | fail        | _            | _     = fail
... | finish      | continue s1  | true  = continue (s1 || s)
... | finish      | _            | _     = continue s
... | continue r1 | continue s1  | true  = continue (s1 || (r1 & s))
... | continue r1 | _            | _     = continue (r1 & s)
derivative (r || s) x dec  with derivative r x dec  | derivative s x dec 
... | continue r1 | continue s1 = continue ( r1 || s1 ) 
... | fail        | p           = p
... | p           | fail        = p
... | finish      | _           = finish
... | _           | finish      = finish
derivative < i > x dec  with dec i x
... | yes y = finish
... | no _  = fail

open import automaton

regex→automaton :  {Σ : Set} →  Regex Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Automaton RexResult Σ
regex→automaton {Σ} r dec = record {
      δ = δ
    ; F = F
   } where
      δ : RexResult → Σ → RexResult
      δ fail i = fail
      δ finish i = fail
      δ (continue r) i = derivative r i dec 
      F : RexResult  → Set
      F (continue r) with empty? r
      ... | true  = ⊤
      ... | false = ⊥
      F finish = ⊤
      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 ∷ []

open Automaton 

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

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

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


regex→accept :  {Σ : Set} →  (r : Regex Σ ) → (x : List Σ)  → (dec : (i j : Σ ) → Dec ( i ≡ j ))
   → accept (regex→automaton r dec) (continue 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) (continue r) x 
regex←accept r x dec re = {!!} 



-- charRE-dec : (x y : Regex char) → Dec (x ≡ y)
-- charRE-dec (x *) (y *) with charRE-dec x y
-- ... | yes refl = yes refl
-- ... | no n = no {!!}
-- charRE-dec (x *) (_ & _) = no (λ ())
-- charRE-dec (x *) (_ || _) = no (λ ())
-- charRE-dec (x *) < _ > = no (λ ())
-- charRE-dec (x & x1) (y & y1) with charRE-dec x y | charRE-dec x1 y1
-- ... | yes refl | yes refl = yes refl
-- ... | no n | _ = no {!!}
-- ... |  _ | no n = no {!!}
-- charRE-dec (x & x1) (y *) = no (λ ())
-- charRE-dec (x & x1) (_ || _) = no (λ ())
-- charRE-dec (x & x1) < _ > = no (λ ())
-- charRE-dec (x || x₁) y = {!!}
-- charRE-dec < x > y = {!!}