------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: search algorithms
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (DecPoset)
module Text.Regex.Search {a e r} (P? : DecPoset a e r) where
open import Level using (_⊔_)
open import Data.Bool.Base using (if_then_else_; true; false)
open import Data.List.Base using (List; []; _∷_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base using (id; _∘′_; _∘_)
open import Data.List.Relation.Binary.Prefix.Heterogeneous
using (Prefix; []; _∷_) hiding (module Prefix)
open import Data.List.Relation.Binary.Infix.Heterogeneous
using (Infix; here; there) hiding (module Infix)
import Data.List.Relation.Binary.Infix.Heterogeneous.Properties as Infixₚ
open import Data.List.Relation.Binary.Pointwise
as Pointwise using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.Suffix.Heterogeneous
using (Suffix; here; there) hiding (module Suffix)
open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Relation.Nullary.Decidable using (map′)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality.Core
open DecPoset P? using (preorder) renaming (Carrier to A)
open import Text.Regex.Base preorder
open import Text.Regex.Properties P?
open import Text.Regex.Derivative.Brzozowski P?
------------------------------------------------------------------------
-- Type corresponding to a match
-- Users have control over whether the match should start at the
-- beginning or stop at the end. So we have a precise type of spans
-- ensuring their demands are respected
Span : ∀ {r} → Regex → Rel A r → Rel (List A) (a ⊔ r)
Span regex =
if Regex.fromStart regex
then if Regex.tillEnd regex
then Pointwise
else Prefix
else if Regex.tillEnd regex
then Suffix
else Infix
-- All matches are selecting an infix sublist
toInfix : ∀ {r} {R : Rel A r} e → Span e R ⇒ Infix R
toInfix e with Regex.fromStart e | Regex.tillEnd e
... | true | true = Infixₚ.fromPointwise
... | true | false = here
... | false | true = Infixₚ.fromSuffix
... | false | false = id
-- A match is a list, a proof it matches the regular expression,
-- and a proof it is the right sort of sublist.
record Match {s} (R : Rel (List A) s) (xs : List A) (exp : Exp)
: Set (a ⊔ e ⊔ r ⊔ s) where
constructor mkMatch
field
list : List A
match : list ∈ exp
related : R list xs
open Match public
map : ∀ {r s} {R : Rel (List A) r} {S : Rel (List A) s} {xs ys e} →
(∀ {a} → R a xs → S a ys) → Match R xs e → Match S ys e
map f (mkMatch ys ys∈e pys) = mkMatch ys ys∈e (f pys)
------------------------------------------------------------------------
-- Search algorithms
module Prefix where
[]ᴹ : ∀ {xs e} → [] ∈ e → Match (Prefix _≡_) xs e
[]ᴹ p = mkMatch [] p []
[]⁻¹ᴹ : ∀ {e} → Match (Prefix _≡_) [] e → [] ∈ e
[]⁻¹ᴹ (mkMatch .[] p []) = p
infixr 5 _∷ᴹ_ _∷⁻¹ᴹ_
_∷ᴹ_ : ∀ {xs e} x → Match (Prefix _≡_) xs (eat x e) → Match (Prefix _≡_) (x ∷ xs) e
x ∷ᴹ (mkMatch ys ys∈e\x ys≤xs) = mkMatch (x ∷ ys) (eat-sound x _ ys∈e\x) (refl ∷ ys≤xs)
_∷⁻¹ᴹ_ : ∀ {xs x e} → [] ∉ e →
Match (Prefix _≡_) (x ∷ xs) e → Match (Prefix _≡_) xs (eat x e)
[]∉e ∷⁻¹ᴹ (mkMatch .[] []∈e []) = contradiction []∈e []∉e
[]∉e ∷⁻¹ᴹ (mkMatch (._ ∷ ys) ys∈e (refl ∷ ys≤xs)) = mkMatch ys (eat-complete _ _ ys∈e) ys≤xs
shortest : Decidable (Match (Prefix _≡_))
shortest xs ∅ = no (∉∅ ∘ match)
shortest xs e with []∈? e
... | yes []∈e = yes ([]ᴹ []∈e)
shortest [] e | no []∉e = no ([]∉e ∘′ []⁻¹ᴹ)
shortest (x ∷ xs) e | no []∉e with shortest xs (eat x e)
... | yes p = yes (x ∷ᴹ p)
... | no ¬p = no (¬p ∘ ([]∉e ∷⁻¹ᴹ_))
longest : Decidable (Match (Prefix _≡_))
longest [] e = map′ []ᴹ []⁻¹ᴹ ([]∈? e)
longest xs ∅ = no (∉∅ ∘ match)
longest (x ∷ xs) e with longest xs (eat x e)
... | yes p = yes (x ∷ᴹ p)
... | no ¬p with []∈? e
... | yes []∈e = yes ([]ᴹ []∈e)
... | no []∉e = no (¬p ∘ ([]∉e ∷⁻¹ᴹ_))
module Infix where
[]⁻¹ᴹ : ∀ {e acc} → Match (Infix _≡_) [] e ⊎ Match (Prefix _≡_) [] acc → [] ∈ e ⊎ [] ∈ acc
[]⁻¹ᴹ (inj₁ (mkMatch .[] []∈e (here []))) = inj₁ []∈e
[]⁻¹ᴹ (inj₂ (mkMatch .[] []∈acc [])) = inj₂ []∈acc
step : ∀ {e acc} x {xs} → Match (Infix _≡_) xs e ⊎ Match (Prefix _≡_) xs (eat x (acc ∣ e)) →
Match (Infix _≡_) (x ∷ xs) e ⊎ Match (Prefix _≡_) (x ∷ xs) acc
step x (inj₁ (mkMatch ys ys∈e p)) = inj₁ (mkMatch ys ys∈e (there p))
step {e} {acc} x (inj₂ (mkMatch ys ys∈e p)) with eat-sound x (acc ∣ e) ys∈e
... | sum (inj₂ xys∈e) = inj₁ (mkMatch (x ∷ ys) xys∈e (here (refl ∷ p)))
... | sum (inj₁ xys∈e) = inj₂ (mkMatch (x ∷ ys) xys∈e (refl ∷ p))
step⁻¹ : ∀ {e acc} x {xs} →
[] ∉ e → [] ∉ acc →
Match (Infix _≡_) (x ∷ xs) e ⊎ Match (Prefix _≡_) (x ∷ xs) acc →
Match (Infix _≡_) xs e ⊎ Match (Prefix _≡_) xs (eat x (acc ∣ e))
-- can't possibly be the empty match
step⁻¹ x []∉e []∉acc (inj₁ (mkMatch .[] ys∈e (here []))) = contradiction ys∈e []∉e
step⁻¹ x []∉e []∉acc (inj₂ (mkMatch .[] ys∈e [])) = contradiction ys∈e []∉acc
-- if it starts 'there', it's an infix solution
step⁻¹ x []∉e []∉acc (inj₁ (mkMatch ys ys∈e (there p))) = inj₁ (mkMatch ys ys∈e p)
-- if it starts 'here' we're in prefix territory
step⁻¹ {e} {acc} x []∉e []∉acc (inj₁ (mkMatch (.x ∷ ys) ys∈e (here (refl ∷ p))))
= inj₂ (mkMatch ys (eat-complete x (acc ∣ e) (sum (inj₂ ys∈e))) p)
step⁻¹ {e} {acc} x []∉e []∉acc (inj₂ (mkMatch (.x ∷ ys) ys∈e (refl ∷ p)))
= inj₂ (mkMatch ys (eat-complete x (acc ∣ e) (sum (inj₁ ys∈e))) p)
-- search non-deterministically: at each step, the `acc` regex is
-- changed to accomodate the fact the match may be starting just now
searchND : ∀ xs e acc → [] ∉ e → Dec (Match (Infix _≡_) xs e ⊎ Match (Prefix _≡_) xs acc)
searchND xs e acc []∉e with []∈? acc
... | yes []∈acc with Prefix.longest xs acc -- get the best match possible
... | yes longer = yes (inj₂ longer)
... | no noMatch = contradiction (mkMatch [] []∈acc []) noMatch
searchND [] e acc []∉e | no []∉acc = no ([ []∉e , []∉acc ]′ ∘′ []⁻¹ᴹ)
searchND (x ∷ xs) e acc []∉e | no []∉acc
= map′ (step x) (step⁻¹ x []∉e []∉acc) (searchND xs e (eat x (acc ∣ e)) []∉e)
search : Decidable (Match (Infix _≡_))
search xs e with []∈? e
... | yes []∈e = yes (mkMatch [] []∈e (here []))
... | no []∉e with searchND xs e ∅ []∉e
... | no ¬p = no (¬p ∘′ inj₁)
... | yes (inj₁ p) = yes p
... | yes (inj₂ p) = contradiction (match p) ∉∅
module Whole where
whole : ∀ xs e → xs ∈ e → Match (Pointwise _≡_) xs e
whole xs e p = mkMatch xs p (Pointwise.refl refl)
whole⁻¹ : ∀ xs e → Match (Pointwise _≡_) xs e → xs ∈ e
whole⁻¹ xs e (mkMatch ys ys∈e p) with Pointwise.Pointwise-≡⇒≡ p
whole⁻¹ xs e (mkMatch .xs xs∈e p) | refl = xs∈e
search : Decidable (Match (Pointwise _≡_))
search xs e = map′ (whole xs e) (whole⁻¹ xs e) (xs ∈? e)
module Suffix where
[]⁻¹ᴹ : ∀ {e acc} → Match (Suffix _≡_) [] e ⊎ Match (Pointwise _≡_) [] acc → [] ∈ e ⊎ [] ∈ acc
[]⁻¹ᴹ (inj₁ (mkMatch .[] ys∈e (here []))) = inj₁ ys∈e
[]⁻¹ᴹ (inj₂ (mkMatch .[] ys∈acc [])) = inj₂ ys∈acc
step : ∀ {e acc} x {xs} →
Match (Suffix _≡_) xs e ⊎ Match (Pointwise _≡_) xs (eat x (e ∣ acc)) →
Match (Suffix _≡_) (x ∷ xs) e ⊎ Match (Pointwise _≡_) (x ∷ xs) acc
step x (inj₁ (mkMatch ys ys∈e p)) = inj₁ (mkMatch ys ys∈e (there p))
step {e} {acc} x (inj₂ (mkMatch ys ys∈e p)) with eat-sound x (e ∣ acc) ys∈e
... | sum (inj₁ xys∈e) = inj₁ (mkMatch (x ∷ ys) xys∈e (here (refl ∷ p)))
... | sum (inj₂ xys∈acc) = inj₂ (mkMatch (x ∷ ys) xys∈acc (refl ∷ p))
step⁻¹ : ∀ {e acc} x {xs} →
Match (Suffix _≡_) (x ∷ xs) e ⊎ Match (Pointwise _≡_) (x ∷ xs) acc →
Match (Suffix _≡_) xs e ⊎ Match (Pointwise _≡_) xs (eat x (e ∣ acc))
-- match starts later
step⁻¹ x (inj₁ (mkMatch ys ys∈e (there p))) = inj₁ (mkMatch ys ys∈e p)
-- match starts here!
step⁻¹ {e} {acc} x (inj₁ (mkMatch (.x ∷ ys) ys∈e (here (refl ∷ p))))
= inj₂ (mkMatch ys (eat-complete x (e ∣ acc) (sum (inj₁ ys∈e))) p)
step⁻¹ {e} {acc} x (inj₂ (mkMatch (.x ∷ ys) ys∈e (refl ∷ p)))
= inj₂ (mkMatch ys (eat-complete x (e ∣ acc) (sum (inj₂ ys∈e))) p)
searchND : ∀ xs e acc → Dec (Match (Suffix _≡_) xs e ⊎ Match (Pointwise _≡_) xs acc)
searchND [] e acc with []∈? e | []∈? acc
... | yes []∈e | _ = yes (inj₁ (mkMatch [] []∈e (here [])))
... | _ | yes []∈acc = yes (inj₂ (mkMatch [] []∈acc []))
... | no []∉e | no []∉acc = no ([ []∉e , []∉acc ]′ ∘′ []⁻¹ᴹ)
searchND (x ∷ xs) e acc
= map′ (step x) (step⁻¹ x) (searchND xs e (eat x (e ∣ acc)))
search : Decidable (Match (Suffix _≡_))
search xs e with searchND xs e ∅
... | no ¬p = no (¬p ∘′ inj₁)
... | yes (inj₁ p) = yes p
... | yes (inj₂ p) = contradiction (match p) ∉∅
------------------------------------------------------------------------
-- Search for the user-specified span
search : ∀ xs e → Dec (Match (Span e _≡_) xs (Regex.expression e))
search xs e with Regex.fromStart e | Regex.tillEnd e
... | true | true = Whole.search xs (Regex.expression e)
... | true | false = Prefix.shortest xs (Regex.expression e)
... | false | true = Suffix.search xs (Regex.expression e)
... | false | false = Infix.search xs (Regex.expression e)
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