------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: smart constructors
-- Computing the Brzozowski derivative of a regular expression may lead
-- to a blow-up in the size of the expression. To keep it tractable it
-- is crucial to use smart constructors.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Bundles using (Preorder)

module Text.Regex.SmartConstructors {a e r} (P : Preorder a e r) where

open import Data.List.Base using ([])
open import Data.List.Relation.Ternary.Appending.Propositional
open import Data.Sum.Base using (inj₁; inj₂; fromInj₁; fromInj₂)

open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality.Core using (refl)

open import Text.Regex.Base P as R hiding (_∣_; _∙_; _⋆)
open import Text.Regex.Properties.Core P

------------------------------------------------------------------------
-- Sum

infixr 5 _∣_

_∣_ : (e f : Exp)  Exp
e  f with is-∅ e | is-∅ f
... | yes _ | _ = f
... | _ | yes _ = e
... | _ | _     = e R.∣ f

∣-sound :  {w} e f  w  (e  f)  w  (e R.∣ f)
∣-sound e f p with is-∅ e | is-∅ f
... | yes _ | _     = sum (inj₂ p)
... | no _  | yes _ = sum (inj₁ p)
... | no _  | no _  = p

∣-complete :  {w} e f  w  (e R.∣ f)  w  (e  f)
∣-complete e f pr@(sum p) with is-∅ e | is-∅ f
... | yes refl | _        = fromInj₂  p  contradiction p ∉∅) p
... | no _     | yes refl = fromInj₁  p  contradiction p ∉∅) p
... | no _     | no _     = pr

------------------------------------------------------------------------
-- Product

infixr 6 _∙_

_∙_ : (e f : Exp)  Exp
e  f with is-∅ e | is-ε e | is-∅ f | is-ε f
... | yes _ | _ | _ | _ = R.∅
... | _ | yes _ | _ | _ = f
... | _ | _ | yes _ | _ = R.∅
... | _ | _ | _ | yes _ = e
... | _ | _ | _ | _ = e R.∙ f

∙-sound :  {w} e f  w  (e  f)  w  (e R.∙ f)
∙-sound e f p with is-∅ e | is-ε e | is-∅ f | is-ε f
... | yes refl | _        | _        | _        = contradiction p ∉∅
... | no _     | yes refl | _        | _        = prod ([] ++ _) ε p
... | no _     | no _     | yes refl | _        = contradiction p ∉∅
... | no _     | no _     | no _     | yes refl = prod (_ ++[]) p ε
... | no _     | no _     | no _     | no _     = p

∙-complete :  {w} e f  w  (e R.∙ f)  w  (e  f)
∙-complete e f pr@(prod eq p q) with is-∅ e | is-ε e | is-∅ f | is-ε f
... | yes refl | _        | _        | _        = contradiction p ∉∅
... | no _     | yes refl | _        | _        = ∈ε∙e-inv pr
... | no _     | no _     | yes refl | _        = contradiction q ∉∅
... | no _     | no _     | no _     | yes refl = ∈e∙ε-inv pr
... | no _     | no _     | no _     | no _     = pr

------------------------------------------------------------------------
-- Kleene star

infix  7 _⋆

_⋆ : Exp  Exp
e  with is-∅ e | is-ε e
... | yes _ | _ = R.ε
... | _ | yes _ = R.ε
... | _ | _ = e R.⋆

⋆-sound :  {w} e  w  (e )  w  (e R.⋆)
⋆-sound e p with is-∅ e | is-ε e
... | yes refl | _        = star (sum (inj₁ p))
... | no _     | yes refl = star (sum (inj₁ p))
... | no _     | no _     = p

⋆-complete :  {w} e  w  (e R.⋆)  w  (e )
⋆-complete e pr with is-∅ e | is-ε e
... | yes refl | no _     = ∈∅⋆-inv pr
... | no _     | yes refl = ∈ε⋆-inv pr
... | no _     | no _     = pr

------------------------------------------------------------------------
-- Derived notions: at least one and maybe one

infixl 7 _+ _⁇
_+ : Exp  Exp
e + = e  e 

_⁇ : Exp  Exp
  = ε
e  = ε  e