    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Examples of regular expressions and matching
    ------------------------------------------------------------------------

    {-# OPTIONS --with-K #-}

    module README.Text.Regex where

    open import Data.Bool using (true; false)
    open import Data.List.Base using (_∷_; [])
    open import Data.String
    open import Function.Base using () renaming (_$′_ to _$_)
    open import Relation.Nullary.Decidable using (yes)
    open import Relation.Nullary.Decidable using (True; False; from-yes)

    -- Our library available via the Text.Regex module is safe but it works on
    -- lists of characters.

    -- To use it on strings we have to rely on unsafe theorems about the
    -- conversions between strings and lists of characters being inverses.
    -- For convenience we use the following unsafe module for this README.
    open import Text.Regex.String.Unsafe

    ------------------------------------------------------------------------
    -- Defining regular expressions

    -- The type of regular expressions is Exp.

    -- Some examples of regular expressions using:

    -- [_]        for the union of ranges it contains
    -- _─_        for a range
    -- singleton  for an exact character
    -- _∙_        for the concatenation of two regular expressions
    -- _∣_        for the sum of two regular expressions
    -- _⋆         for the Kleene star (zero or more matches of the regular expression)
    -- _⁇         for an optional regular expression

    ℕ* : Exp
    ℕ* = [ '1' ─ '9' ∷ [] ]   -- a non-zero digit
       ∙ [ '0' ─ '9' ∷ [] ] ⋆ -- followed by zero or more digits

    ℕ : Exp
    ℕ = ℕ* ∣ singleton '0' -- ℕ* or exactly 0

    ℤ : Exp
    ℤ = ((singleton '-') ⁇ ∙ ℕ*) -- an optional minus sign followed by a ℕ*
      ∣ singleton '0'            -- or exactly 0

    ------------------------------------------------------------------------
    -- An expression's semantics

    -- The semantics of these regular expression is defined in terms of the
    -- lists of characters they match. The type (str ∈ e) states that the
    -- string str matches the expression e.

    -- It is decidable, and the proof is called _∈?_.
    -- We can run it on a few examples to check that it matches our intuition:

    -- Valid: starts with a non-zero digit, followed by 3 digits
    _ : True ("1848" ∈? ℕ*)
    _ = _

    -- Valid: exactly 0
    _ : True ("0" ∈? ℕ)
    _ = _

    -- Invalid: starts with a leading 0
    _ : False ("007" ∈? ℕ)
    _ = _

    -- Invalid: no negative ℕ number
    _ : False ("-666" ∈? ℕ)
    _ = _

    -- Valid: a negative integer
    _ : True ("-666" ∈? ℤ)
    _ = _

    -- Invalid: no negative 0
    _ : False ("-0" ∈? ℤ)
    _ = _

    ------------------------------------------------------------------------
    -- Matching algorithms

    -- The proof that _∈_ is decidable gives us the ability to check whether
    -- a whole string matches a regular expression. But we may want to use
    -- other matching algorithms detecting a prefix, infix, or suffix of the
    -- input string that matches the regular expression.

    -- This is what the Regex type gives us.

    -- For instance, the following value corresponds to finding an infix
    -- substring matching the string "agda" or "agdai"

    agda : Exp
    agda = singleton 'a'
         ∙ singleton 'g'
         ∙ singleton 'd'
         ∙ singleton 'a'
         ∙ (singleton 'i' ⁇)

    infixAgda : Regex
    infixAgda = record
      { fromStart  = false
      ; tillEnd    = false
      ; expression = agda
      }

    -- The search function gives us the ability to look for matches

    -- Valid: agda in the middle
    _ : True (search "Maria Magdalena" infixAgda)
    _ = _

    -- By changing the value of fromStart and tillEnd we can control where the
    -- substring should be. We can insist on the match being at the end of the
    -- input for instance:

    suffixAgda : Regex
    suffixAgda = record
      { fromStart  = false
      ; tillEnd    = true
      ; expression = agda
      }

    -- Invalid: agda is in the middle
    _ : False (search "Maria Magdalena" suffixAgda)
    _ = _

    -- Valid: agda as a suffix
    _ : True (search "README.agda" suffixAgda)
    _ = _

    -- Valid: agdai as a suffix
    _ : True (search "README.agdai" suffixAgda)
    _ = _

    ------------------------------------------------------------------------
    -- Advanced uses

    -- Search does not just return a boolean, it returns an informative answer.
    -- Infix matches are for instance represented using the `Infix` relation on
    -- list. Such a proof pinpoints the exact position of the match:

    open import Data.List.Relation.Binary.Infix.Heterogeneous
    open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties
    open import Data.List.Relation.Binary.Pointwise using (≡⇒Pointwise-≡)
    open import Relation.Binary.PropositionalEquality

    -- Here is an example of a match: it gives back the substring, the inductive
    -- proof that it is accepted by the regular expression and its precise location
    -- inside the input string
    mariamAGDAlena : Match "Maria Magdalena" infixAgda
    mariamAGDAlena = record
      { string  = "agda"                     -- we have found "agda"
      ; match   = from-yes ("agda" ∈? agda)  -- a proof of the match
      ; related = proof                      -- and its location
      }

      where

        proof : Infix _≡_ (toList "agda") (toList "Maria Magdalena")
        proof = toList "Maria M"
            ++ⁱ fromPointwise (≡⇒Pointwise-≡ refl)
            ⁱ++ toList "lena"

    -- And here is the proof that search returns such an object
    _ : search "Maria Magdalena" infixAgda ≡ yes mariamAGDAlena
    _ = refl