Untyped Lambda Calculus: application needs brackets around function

[dvberkel]

Our parser combinator framework returns all possible parsings of an input. Without the bracketed part in the applicationParser

applicationParser : Parser Context Term
applicationParser =
    let
        eventuallyTerm =
            Parser.lazy (\_ -> parser)
    in
    Parser.bracketed '(' ')' eventuallyTerm
        |> Parser.keepThenIgnore (many space)
        |> Parser.followedBy eventuallyTerm
        |> Parser.map (\( l, r ) -> TmApp l r)

could not consume any input and happily go down an infinite stack hole.

Because bracketed consumes '(' in order to succeed, this is prevented.

This is artifical and ideally should be prevented.

[dvberkel]

A possibility could be to define a lazy combinator variant that must consume input otherwise fail 🤔

[dvberkel]

An other option is described in Jeroen Fokkers functional parsers where a first is defined

first : Parser c a -> Parsers c a
first parser context input =
  case parser context input of
    h :: _ -> h :: []
    [] -> []