[ Regex ] `search` with `fromStart = true` does not match as expect; request for documentation

[joha2]

First of all: Thanks for this great library! It eases the use of Agda for all kinds of tasks for me tremendously!

In this case, I want to extract the scheme (i.e. the protocol part) from a URL. For this I decided to use the Regex facilities. MWE:

module regex-question where

open import Data.List using (List ; [] ; _∷_)
open import Data.Char using (Char)
open import Data.String using (toList)
open import Data.Bool using (true ; false)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Relation.Nullary.Decidable.Core using (from-yes)
open import Text.Regex.String

open Match

alphaExp : Exp
alphaExp = [ 'a'  ─  'z' ∷ 'A' ─ 'Z' ∷ [] ]

digitExp : Exp
digitExp = [ '0' ─ '9' ∷ [] ]

schemeExp : Exp
schemeExp = alphaExp ∙ ((alphaExp ∣ digitExp ∣ singleton '+' ∣ singleton '-' ∣ singleton '.') ⋆)

testurl : List Char
testurl = toList "https://example.org/bla/blub"

My problem is now, that I don't understand how to match for specific parts of the URL:

The scheme is clearly located at the beginning til the ':' character. If we set fromStart to false, we obtain the correct match https:

match-scheme-fromStart≡false = list (from-yes (search testurl
                                                      (record { fromStart = false ;
                                                                tillEnd = false ;
                                                                expression = schemeExp })))
_ : match-scheme-fromStart≡false ≡ (toList "https")
_ = refl

If we set fromStart to true, the matching only gives the first character.

match-scheme-fromStart≡true = list (from-yes (search testurl
                                                     (record { fromStart = true ;
                                                               tillEnd = false ;
                                                               expression = schemeExp })))
_ : match-scheme-fromStart≡true ≡ (toList "h")
_ = refl

From my understanding it should also match "https".

In Python in contrast,

import re

scheme_regex_fromStart = r"^([a-zA-Z]([a-zA-Z]|[0-9]|\+|-∣\.)*)"
scheme_regex_not_fromStart = r"([a-zA-Z]([a-zA-Z]|[0-9]|\+|-∣\.)*)"

testurl = r"https://example.org/bla/blub"

print(re.findall(scheme_regex_fromStart, testurl))
# [('https', 's')]
print(re.findall(scheme_regex_not_fromStart, testurl))
# [('https', 's'), ('example', 'e'), ('org', 'g'), ('bla', 'a'), ('blub', 'b')]

it only finds the desired pattern if one uses "^" which I would expect.

My question is: Is this a bug or did I miss something? Are the regexps in Python different from the ones used in Agda? (I bet yes, but so fundamentally?)

Further, but this is only a side issue: The documentation of the Regex part is very concise and not exactly for beginners without background in theoretical computer science (like me 😄 ). I thought about how to improve, but fear that (a) my style is more hands-on than precise and not appropriate for the Agda Standard Library, (b) my English is not good enough. What would be a feasible way forward here?

Thanks for your help!