RFC: Consider adding Alternative.{many,many1} #1577
Description
I was writing a little parser combinator library, and was surprised that, after defining an Alternative instance, I didn't get these combinators for free, as I'm used to, in Haskell (where many1 is named some).
Is there a reason these combinators aren't defined?
I managed to hack together my own versions, and they seem to work fine.
(I'm brand new to lean though, so this should just be considered a suggestion that this stuff is expressible).
private partial
def manyCore
[Alternative f]
-- Alternative.failure is an example of an inhabitant
[Inhabited (f (Σ n, Vector a n))]
(p : f a) : f (Σ n, Vector a n) :=
let g x xs := ⟨xs.1 + 1, Vector.push xs.2 x⟩
(g <$> p <*> manyCore p) <|> pure ⟨0, emptyVec⟩
def Alternative.many
[Alternative f]
[Inhabited (f (Σ n, Vector a n))]
(p : f a) : f (Σ n, Vector a n) :=
let g | ⟨n, v⟩ => ⟨n, v.reverse⟩
manyCore p <&> g
def Alternative.many1
[Alternative f]
[Inhabited (f (Σ n, Vector a n))]
(p : f a) : f (Σ n, Vector a (n + 1)) :=
let g x xs := ⟨xs.1, by simpa [Nat.add_comm] using Vector.singleton x ++ xs.2⟩
(g <$> p <*> Alternative.many p) <|> Alternative.failure
...
#guard remainder (many $ pref "a") "" = [""]
#guard remainder (many $ pref "a") "b" = ["b"]
#guard remainder (many $ pref "a") "aaa" = [""]
#guard remainder (many $ pref "a") "aabaa" = ["baa"]
#guard remainder (many1 $ pref "a") "" = []
#guard remainder (many1 $ pref "a") "b" = []
#guard remainder (many1 $ pref "a") "aaa" = [""]
#guard remainder (many1 $ pref "a") "aabaa" = ["baa"]There didn't seem to be a Lean version of NonEmpty, so I used Vector _ (n + 1)...
I assume these could be optimized, to remove the reverse in many, and the vector copy in many1...
I was originally looking for a length-indexed cons-list, in place of a NonEmptyList, which wouldn't require either of these things, but I couldn't find one in std/batteries...