{-# OPTIONS --allow-unsolved-metas #-}

open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.List hiding ( [_] )
open import finiteSet

module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where

-- open import nfa
open import Data.Nat
-- open import Data.Nat hiding ( _<_ ; _>_ )
-- open import Data.Fin hiding ( _<_ )
open import finiteSetUtil
open import automaton
open import logic
open import regex
open FiniteSet

empty? : Regex  Σ → Bool
empty?  ε       = true
empty?  φ       = false
empty? (x *)    = true
empty? (x & y)  = empty? x /\ empty? y
empty? (x || y) = empty? x \/ empty? y
empty? < x >    = false

derivative :  Regex  Σ → Σ → Regex  Σ
derivative ε s = φ
derivative φ s = φ
derivative (x *) s with derivative x s
... | ε = x *
... | φ = φ
... | t = t & (x *)
derivative (x & y) s with empty? x
... | true with derivative x s | derivative y s
... | ε | φ = φ
... | ε | t = y || t
... | φ | t = t
... | x1 | φ = x1 & y
... | x1 | y1 = (x1 & y) || y1
derivative (x & y) s | false with derivative x s 
... | ε = y
... | φ = φ
... | t = t & y
derivative (x || y) s with derivative x s | derivative y s
... | φ | y1 = y1
... | x1 | φ = x1
... | x1 | y1 = x1 || y1
derivative < x > s with eq? x s
... | yes _ = ε
... | no  _ = φ

data regex-states (x : Regex  Σ ) : Regex  Σ → Set where
    unit   : regex-states x x
    derive : { y : Regex  Σ } → regex-states x y → (s : Σ)  → regex-states x ( derivative y s )

record Derivative (x : Regex  Σ ) : Set where
    field
       state : Regex  Σ
       is-derived : regex-states x state

open Derivative

open import Data.Fin hiding (_<_)

-- derivative generates   (x & y) || ... form. y and x part is a substerm of original regex
-- since subterm is finite, only finite number of state is generated for each operator 
-- this does not work, becuase it depends on input sequences
-- finite-derivative : (r : Regex  Σ) → FiniteSet Σ  → FiniteSet (Derivative r) 
-- order : Regex  Σ → ℕ
-- decline-derive : (x : Regex Σ ) (i : Σ ) → 0 < order x → order (derivative x i) < order x 
--    is not so easy
-- in case of automaton, number of derivative is limited by iteration of input length, so it is finite.
-- so we cannot say derived automaton is finite i.e. regex-match is regular language now

regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step d s} ; aend = λ d → empty? (state d) }  where
    derive-step : (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s)
    derive-step d0 s = derive (is-derived d0) s

regex-match : (r : Regex   Σ) →  (List Σ) → Bool
regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 

open import Relation.Binary.Definitions


data _r<_  : (x y : Regex Σ)  → Set  where
   ε<φ : ε r< φ  
   ε<* : {y : Regex Σ} → ε r< (y *) 
   ε<|| : {y y₁ : Regex Σ} → ε r< (y || y₁) 
   ε<& : {y y₁ : Regex Σ} → ε r< (y & y₁) 
   ε<<> : {x : Σ} → ε r< < x > 
   φ<* : {y : Regex Σ} → φ r< (y *) 
   φ<|| : {y y₁ : Regex Σ} → φ r< (y || y₁) 
   φ<& : {y y₁ : Regex Σ} → φ r< (y & y₁) 
   φ<<> : {x : Σ} → φ r< < x > 
   *<* : {x y : Regex Σ} → x r< y → (x *) r< (y *) 
   *<& : {x y y₁ : Regex Σ} → (x *) r< (y & y₁) 
   *<|| : {x y y₁ : Regex Σ} → (x *) r< (y || y₁) 
   <><* : {x₁ : Σ} {x : Regex Σ} → < x₁ > r< (x *)  
   &<&0 : {x x₁ y y₁ : Regex Σ} → x r<  y  → (x & x₁) r< (y & y₁) 
   &<&1 : {x x₁ y₁ : Regex Σ} → x₁ r< y₁  → (x & x₁) r< (x & y₁) 
   &<|| : (x x₁ y y₁ : Regex Σ) → (x & x₁) r< (y || y₁) 
   ||<||0 : {x x₁ y y₁ : Regex Σ} → x r< y  → (x || x₁) r< (y || y₁) 
   ||<||1 : {x x₁ y₁ : Regex Σ} → x₁ r< y₁  → (x || x₁) r< (x || y₁) 
   <><<> : {x x₁ : Σ} → F←Q fin x Data.Fin.< F←Q fin x₁  → < x > r< < x₁ > 

cmp-regex : Trichotomous  _≡_  _r<_  
cmp-regex ε ε = tri≈ (λ ()) refl (λ ())
cmp-regex ε φ = tri< ε<φ (λ ()) (λ ())
cmp-regex ε (y *) = tri< ε<* (λ ()) (λ ())
cmp-regex ε (y & y₁) = tri< ε<& (λ ()) (λ ())
cmp-regex ε (y || y₁) = tri< ε<|| (λ ()) (λ ())
cmp-regex ε < x > = tri< ε<<> (λ ()) (λ ())
cmp-regex φ ε = tri> (λ ()) (λ ()) ε<φ 
cmp-regex φ φ = tri≈ (λ ()) refl (λ ())
cmp-regex φ (y *) = tri< φ<*   (λ ()) (λ ())
cmp-regex φ (y & y₁) = tri< φ<&   (λ ()) (λ ())
cmp-regex φ (y || y₁) = tri< φ<||   (λ ()) (λ ())
cmp-regex φ < x > = tri< φ<<>   (λ ()) (λ ())
cmp-regex (x *) ε =  tri> (λ ()) (λ ()) ε<*
cmp-regex (x *) φ = tri> (λ ()) (λ ()) φ<*
cmp-regex (x *) (y *) with cmp-regex x y
... | tri< a ¬b ¬c = tri< ( *<* a ) {!!} {!!}
... | tri≈ ¬a refl ¬c = tri≈ {!!} refl {!!}
... | tri> ¬a ¬b c = {!!}
cmp-regex (x *) (y & y₁) = tri< *<& (λ ()) (λ ()) 
cmp-regex (x *) (y || y₁) = tri< *<|| (λ ()) (λ ()) 
cmp-regex (x *) < x₁ > =  tri> (λ ()) (λ ()) <><*
cmp-regex (x & x₁) y = {!!}
cmp-regex (x || x₁) y = {!!}
cmp-regex < x > y = {!!}

data Tree ( Key : Set ) : Set where
    leaf : Tree Key 
    node : Key → Tree Key → Tree Key → Tree Key 

insert : Tree (Regex Σ) → (Regex Σ) → Tree (Regex Σ) 
insert leaf k = node k leaf leaf
insert (node x t t₁) k with cmp-regex k x
... | tri< a ¬b ¬c = node x (insert t k) t₁
... | tri≈ ¬a b ¬c = node x t t₁
... | tri> ¬a ¬b c = node x t (insert t₁ k) 

regex-derive : Tree (Regex Σ) → Tree (Regex Σ)
regex-derive t = regex-derive0 t t where
   regex-derive1 : Regex Σ → List Σ → Tree (Regex Σ) → Tree (Regex Σ)
   regex-derive1 x [] t = t
   regex-derive1 x (i ∷ t) r =  regex-derive1 x t (insert r (derivative x i))
   regex-derive0 :  Tree (Regex Σ)  → Tree (Regex Σ) → Tree (Regex Σ)
   regex-derive0 leaf t = t
   regex-derive0 (node x r r₁) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true))  (regex-derive0 r₁ t))