------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: basic types and semantics
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles using (Preorder)

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

open import Level using (_⊔_)

open import Data.Bool.Base using (Bool)
open import Data.List.Base as L using (List; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any)
open import Data.List.Relation.Unary.All using (All)
open import Data.Sum.Base using (_⊎_)

open import Relation.Nullary.Negation.Core using (¬_)

open Preorder P using (_≈_) renaming (Carrier to A; _∼_ to _≤_)
open import Data.List.Relation.Ternary.Appending.Propositional {A = A}

------------------------------------------------------------------------
-- Regular expressions on the alphabet A

infix  [_] _─_
data Range : Set a where
  [_] : (a : A)     → Range
  _─_ : (lb ub : A) → Range

infixr  _∣_
infixr  _∙_
infixl  _⋆
infix  [^_]

data Exp : Set a where
  ε    : Exp
  [_]  : (rs : List Range) → Exp
  [^_] : (rs : List Range) → Exp
  _∣_  : (e f : Exp) → Exp
  _∙_  : (e f : Exp) → Exp
  _⋆   : (e : Exp) → Exp

-- A regular expression has additional parameters:
-- * should the match begin at the very start of the input?
-- * should it span until the very end?

record Regex : Set a where
  field
    fromStart  : Bool
    tillEnd    : Bool
    expression : Exp

updateExp : (Exp → Exp) → Regex → Regex
updateExp f r = record r { expression = f (Regex.expression r) }

------------------------------------------------------------------------
-- Derived notions: nothing, anything, and singleton

pattern ∅ = [ List.[] ]
pattern · = [^ List.[] ]

pattern singleton a = [ Range.[ a ] ∷ [] ]

------------------------------------------------------------------------
-- Semantics: matching words

infix  _∈ᴿ_ _∉ᴿ_
data _∈ᴿ_ (c : A) : Range → Set (a ⊔ r ⊔ e) where
  [_] : ∀ {val}   → c ≈ val         → c ∈ᴿ [ val ]
  _─_ : ∀ {lb ub} → lb ≤ c → c ≤ ub → c ∈ᴿ (lb ─ ub)

_∉ᴿ_ : A → Range → Set (a ⊔ r ⊔ e)
a ∉ᴿ r = ¬ (a ∈ᴿ r)

infix  _∈_ _∉_
data _∈_ : List A → Exp → Set (a ⊔ r ⊔ e) where
  ε      :                                                     []      ∈ ε
  [_]    : ∀ {a rs} → Any (a ∈ᴿ_) rs →                         L.[ a ] ∈ [ rs ]
  [^_]   : ∀ {a rs} → All (a ∉ᴿ_) rs →                         L.[ a ] ∈ [^ rs ]
  sum    : ∀ {w e f} → (w ∈ e) ⊎ (w ∈ f) →                     w       ∈ (e ∣ f)
  prod   : ∀ {v w vw e f} → Appending v w vw → v ∈ e → w ∈ f → vw      ∈ (e ∙ f)
  star   : ∀ {v e} → v ∈ (ε ∣ e ∙ (e ⋆)) →                     v       ∈ (e ⋆)

_∉_ : List A → Exp → Set (a ⊔ r ⊔ e)
w ∉ e = ¬ (w ∈ e)