help with std.internal.parsec terminations

Stream: general

[lorã]

Hello! I'm trying to use the Std.Internal.Parsec. A very common thing is that mutual recursions and array accessing creates problems with terminations.

But.. The Parsec itself is used as a monad so.. There's a more practical way to dealing with these situations or to avoiding them? Currently i am dealing with this termination problem:

mutual
def pfunCall : Parser Expr := do {
  let name <- pcamelCase

  skipChar '(';
  let args <- pexpr sepBy ',';
  skipChar ')';

  return EFunCall name args
}

def pexpr : Parser Expr :=
  choice [
    pliteral
  , pfunCall
  , pvar
  ]
end

I am getting this output from lean:
"fail to show termination for
pfunCall
pexpr
with errors
failed to infer structural recursion:
no parameters suitable for structural recursion
well-founded recursion cannot be used, 'pfunCall' does not take any (non-fixed) arguments"

So.. because parser is a monad, how i could get fixed arguments right? I think that, this time, it should terminate because all the inputs are finite :p.

~ Ty

[Henrik Böving]

Just make it partial def, the parser monad is not build for reasoning