------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions
--
-- The content of this module (and others in the Regex subdirectory) is
-- based on Alexandre Agular and Bassel Mannaa's 2009 technical report:
-- Regular Expressions in Agda
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles using (DecPoset)

module Text.Regex {a e r} (decPoset : DecPoset a e r) where


private
  preorder = DecPoset.preorder decPoset

import Text.Regex.Base                  preorder as Regex
import Text.Regex.SmartConstructors     preorder as Smart
import Text.Regex.Derivative.Brzozowski decPoset as Eat
import Text.Regex.Search                decPoset as Search

------------------------------------------------------------------------
-- Re-exporting basic definition and semantics

open Regex public
  using ( Range; module Range
        ; [_]; _─_
        ; Regex; module Regex; Exp; module Exp
        ; ε; [^_]; ∅; ·; singleton
        ; _∈ᴿ_; _∉ᴿ_
        ; _∈_; _∉_; sum; prod; star
        )

------------------------------------------------------------------------
-- Re-exporting smart constructors

open Smart public
  using (_∣_; _∙_; _⋆; _+; _⁇)

------------------------------------------------------------------------
-- Re-exporting semantics decidability

open Eat public
  using (_∈?_; _∉?_)

------------------------------------------------------------------------
-- Re-exporting search algorithms

open Search public
  using (Span; toInfix; Match; mkMatch; search)