Parser combinator library termination

Stream: new members

[Alex]

I'm trying to use the parser combinator library and got very stuck. I want to parse a string that may use " or ' as delimiters, ignoring escaped quotes. In the library code, it uses a recursive function for similar functionality: https://github.com/fgdorais/lean4-parser/blob/a64da3842f409ff01c101d56c4e7b7b789864921/Parser/RegEx/Compile.lean#L119. I tried this:

namespace MyParser
protected abbrev Parser := SimpleParser Substring Char
def strLoop (delimit: Char) (acc : Array Char) : MyParser.Parser (Array Char) :=
  do
    let (next : Char) ← anyToken
    if next == delimit then return acc
    else strLoop delimit (acc ++ #[next])

This gives me an error about termination not being found and suggests I prove
⊢ sizeOf (acc ++ #[next]) < sizeOf acc
Why doesn't Dorais' code have the same problem with with the filter argument and what should I do here?

[Michal Wallace (tangentstorm)]

It sounds like lean is trying to derive a termination proof based on the idea that you're recursing over acc and it gets smaller at each step, but of course that's not what you're doing, and acc actually grows.

Your code here doesn't look very much like the example code for this library. In the JSON example, there's a demonstration of switching based on the initial character (lookAhead anytoken):

https://github.com/fgdorais/lean4-parser/blob/a64da3842f409ff01c101d56c4e7b7b789864921/examples/JSON.lean#L85

You could probably do the same thing to dispatch on " vs ' and then have two different string-parsing rules.

[Henrik Böving]

The function is marked as partial and thus allowed to ignore the termination checker. In general I would suggest to just use it if you don't need to do verification

[Alex]

@Michal Wallace (tangentstorm) I meant I used that code for reference with the recursive part rather than looking ahead.

Henrik Böving Thank you. I see stream code is partial because they can be infinite.

[Henrik Böving]

They cannot be infinite, lean does not habe support for co inductives

[Alex]

@Henrik Böving Yes, I was confused because IO.FS.Stream and Data.Stream have similar names. The documentation for the FS one actually has the same problem: the mid-text link is to the Data one https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO.FS.Stream