feat: generalized Parsec

[hargoniX]

For experimentation by @the-sofi-uwu.

I also have an efficient number parser in LeanSAT that I am planning to upstream after we have sufficiently bikeshed this change.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 95b8095fa6a8d925121addd93d3b5917d851634b --onto 7aec6c9ae7a54935ada0df0b4cc1efafc2291007. (2024-07-17 13:41:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 95b8095fa6a8d925121addd93d3b5917d851634b --onto ba3565f441a4533490c339ead6d9ee5b1220110b. (2024-07-18 08:34:44)

[TwoFX]

By switching around the namespaces and naming you have practically guaranteed to break every single downstream user of Lean.Parsec. Do we have an idea how many people are affected by this? Are the error messages comprehensible so that affected users know what they need to do? Can we avoid the breakage entirely in some way?

[hargoniX]

Looking around the Lean Zulip there is 1 thread about parsec every couple of months, so I would hope the user base is currently rather small. I know that doc-gen's dependency closure does do a bit with Parsec and LeanSAT of course as well, apart from that I'm not aware of projects that do use Parsec.

My main motivation for organising the namespaces as they are was mostly the original Haskell parsec which has one ParsecT top level monad transformer that's generic over the input and then one Parser specialization for the built-in supported input variants.

As for the error messages you would basically end up with:

▶ 62:12-62:25: error:
type expected, got
  (Parsec String : Type → Type)

as well as of course a couple of missing identifiers that moved to the String sub namespace:

unknown identifier 'asciiLetter'

These are obviously not as helpful as they could be. I would hope that with a little explanation in the release notes we could help migrate the few users that do exist?

Alternatively we can turn Parsec into ParsecM and have Parsec be the String.Iterator alias of it that has a deprecated pointer to ParsecM/Parser. However this does not solve the issue of not having certain String specific parsers in namespace anymore. Putting these into the top level namespace as well would make it very inconvenient to work with the ByteArray parsers as they would constantly be colliding.