{-# 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  Σ → 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 ∷ [] )
   empty : regular-expr φ [] 
   none : ⊥ → regular-expr φ [] 
   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.Empty 
open import  Relation.Nullary

regex-language : {Σ : Set} → (r : Regex Σ) →  ((i j : Σ) → Dec ( i ≡ j)) →  (t : List Σ ) → Set
regex-language φ dec  _ = ⊥
regex-language ε dec [] = ⊤
regex-language ε dec (_ ∷ _) = ⊥
regex-language (x *) dec f = Star ( regex-language x dec )  f
regex-language (x & y) dec f = split ( regex-language x dec ) ( regex-language y dec ) f
regex-language (x || y) dec f = ( regex-language x dec f )  ∨  ( regex-language y dec f )
regex-language < h > dec [] = ⊥
regex-language < h > dec (h1  ∷ [] ) with dec h h1
... | yes _ = ⊤
... | no _  = ⊥
regex-language < h > 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 ∷ []

test-regex2 : ¬ (regex-language r1 char-dec ( a ∷ [] ) )
test-regex2 (case1 ())
test-regex2 (case2 ())

test-regex3 : regex-language r1 char-dec  ( a ∷ b ∷ c ∷ [] ) 
test-regex3 = case2 (case1 [ tt , case2 (case1 [ tt , tt ]) ] )

splitb : {Σ : Set} → (List Σ → Bool)
      → ( List Σ → Bool) → List Σ → Bool
splitb x y  [] = x [] /\ y []
splitb x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
  splitb (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

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

regular-language : {Σ : Set} → Regex Σ → ((i j : Σ) → Dec ( i ≡ j)) →  List Σ → Bool
regular-language ε dec _ = false
regular-language φ dec [] = true
regular-language φ dec (_ ∷ _ ) = false
regular-language (x *) dec = repeatb ( regular-language x dec )
regular-language (x & y) dec = splitb ( regular-language x dec ) ( regular-language y dec )
regular-language (x || y) dec = λ s → ( regular-language x dec s )  \/ ( regular-language y dec s)
regular-language < h > dec [] = false
regular-language < h > dec (h1  ∷ [] ) with dec h h1
... | yes _ = true
... | no _  = false
regular-language < h > dec _ = false

test-regex4 : Bool
test-regex4 = regular-language  r1 char-dec ( a ∷ [] ) 

test-regex5 : Bool
test-regex5 = regular-language  r1 char-dec  ( a ∷ b ∷ c ∷ [] )

-- 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? φ = false
empty? ε = true
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 φ x dec  = fail
derivative ε x dec  = fail
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 _ = ⊥

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 = {!!} 



RE-dec : {Σ : Set} → ((s t : Σ) → Dec (s ≡ t))  → (x y : Regex Σ) →  Dec (x ≡ y)
RE-dec dec (x *) (y *) with RE-dec dec x y
... | yes refl = yes refl
... | no n = no (contra-position relem1 n ) where
   relem1 : (x *) ≡ (y *) → x ≡ y
   relem1 refl = refl
RE-dec dec (x *) (_ & _) = no (λ ())
RE-dec dec (x *) (_ || _) = no (λ ())
RE-dec dec (x *) < _ > = no (λ ())
RE-dec dec (x & x1) (y & y1) with RE-dec dec x y | RE-dec dec x1 y1
... | yes refl | yes refl = yes refl
... | no n | _ = no (contra-position relem2 n ) where
   relem2 : x & x1 ≡ y & y1 → x ≡ y
   relem2 refl = refl
... |  _ | no n = no (contra-position relem3 n ) where
   relem3 :  x & x1 ≡ y & y1 → x1 ≡ y1
   relem3 refl = refl
RE-dec dec (x & x1) (y *) = no (λ ())
RE-dec dec (x & x1) (_ || _) = no (λ ())
RE-dec dec (x & x1) < _ > = no (λ ())
RE-dec dec (x || x1) φ = no (λ ())
RE-dec dec (x || x1) ε = no (λ ())
RE-dec dec (x || x1) (y *) = no (λ ())
RE-dec dec (x || x1) (y & y₁) = no (λ ())
RE-dec dec (x || x1) (y || y1) with RE-dec dec x y | RE-dec dec x1 y1
... | yes refl | yes refl = yes refl
... | no n | _ = no (contra-position relem4 n ) where
   relem4 :   x || x1 ≡ y || y1 → x ≡ y
   relem4 refl = refl
... |  _ | no n = no (contra-position relem5 n ) where
   relem5 :  x || x1 ≡ y || y1 → x1 ≡ y1
   relem5 refl = refl
RE-dec dec (x || x1) < x₁ > = no (λ ())
RE-dec dec < x > φ = no (λ ()) 
RE-dec dec < x > ε =  no (λ ())
RE-dec dec < x > (y *) =  no (λ ())
RE-dec dec < x > (y & y₁) =  no (λ ())
RE-dec dec < x > (y || y₁) =  no (λ ())
RE-dec dec < x > < x₁ > with dec x x₁
... | yes refl = yes refl
... | no n = no (contra-position relem6 n ) where
   relem6 :  < x > ≡ < x₁ > → x ≡ x₁
   relem6 refl = refl
RE-dec dec φ φ = yes refl
RE-dec dec φ ε = no (λ ())
RE-dec dec φ (y *) = no (λ ())
RE-dec dec φ (y & y₁) = no (λ ())
RE-dec dec φ (y || y₁) = no (λ ())
RE-dec dec φ < x > = no (λ ())
RE-dec dec ε φ = no (λ ())
RE-dec dec ε ε = yes refl
RE-dec dec ε (y *) = no (λ ())
RE-dec dec ε (y & y₁) = no (λ ())
RE-dec dec ε (y || y₁) = no (λ ())
RE-dec dec ε < x > = no (λ ())
RE-dec dec (x *) φ = no (λ ())
RE-dec dec (x *) ε = no (λ ())
RE-dec dec (x & x1) φ = no (λ ())
RE-dec dec (x & x1) ε = no (λ ())