------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions acting on strings, using unsafe features
------------------------------------------------------------------------
{-# OPTIONS --with-K #-}
module Text.Regex.String.Unsafe where
open import Data.String.Base using (String; toList; fromList)
import Data.String.Unsafe as Stringₚ
open import Function.Base using (_on_; id)
open import Level using (0ℓ)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; sym; subst)
open import Relation.Nullary.Decidable using (map′)
------------------------------------------------------------------------
-- Re-exporting safe definitions
open import Text.Regex.String as Regex public
hiding (_∈_; _∉_; _∈?_; _∉?_; Span; Match; search)
------------------------------------------------------------------------
-- Specialised definitions
infix 4 _∈_ _∉_ _∈?_ _∉?_
_∈_ : String → Exp → Set
str ∈ e = toList str Regex.∈ e
_∉_ : String → Exp → Set
str ∉ e = toList str Regex.∉ e
_∈?_ : Decidable _∈_
str ∈? e = toList str Regex.∈? e
_∉?_ : Decidable _∉_
str ∉? e = toList str Regex.∉? e
Span : Regex → Rel String 0ℓ
Span e = Regex.Span e _≡_ on toList
-- A match is a string, a proof it matches the regular expression,
-- and a proof it appears as the right sort of substring.
record Match (str : String) (e : Regex) : Set where
constructor mkMatch
field
string : String
match : string ∈ Regex.expression e
related : Span e string str
open Match public
search : Decidable Match
search str e = map′ from to (Regex.search input e) where
input = toList str
exp = Regex.expression e
from : Regex.Match (Regex.Span e _≡_) input exp → Match str e
from (Regex.mkMatch list match related) =
let eq = sym (Stringₚ.toList∘fromList list) in
mkMatch (fromList list)
(subst (Regex._∈ exp) eq match)
(subst (λ str → Regex.Span e _≡_ str input) eq related)
to : Match str e → Regex.Match (Regex.Span e _≡_) input exp
to (mkMatch string match related) =
Regex.mkMatch (toList string) match related
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4