------------------------------------------------------------------------
-- 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  _∣_

_∣_ : (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  _∙_

_∙_ : (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   _⋆

_⋆ : 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  _+ _⁇
_+ : Exp → Exp
e + = e ∙ e ⋆

_⁇ : Exp → Exp
∅ ⁇ = ε
e ⁇ = ε ∣ e