Parser.foldl isn't (always?) tail recursive

[badly-drawn-wizards]

The way the code is structured suggests that it is intended to be. I'm using SimpleParserT with my own monad if that contributes anything to it not functioning as it should. I can push example code if need be.

[fgdorais]

It is certainly intended to be tail recursive but I don't think this was carefully tested. Yes, please add an example. That would be very helpful.

[badly-drawn-wizards]

Here in Day3.lean: https://github.com/badly-drawn-wizards/advent-of-code-2023 (d073aef973765fc2b8dd7c12a52b6cf2e6fa01ce)

I'll try make a more minimal reproduction later, but this is what sent me here

The stack trace from the core dump:

#0  __pthread_kill_implementation (threadid=<optimized out>, signo=signo@entry=6, no_tid=no_tid@entry=0)
    at pthread_kill.c:44
#1  0x00007f1b0d0ffde3 in __pthread_kill_internal (signo=6, threadid=<optimized out>) at pthread_kill.c:78
#2  0x00007f1b0d0b09c6 in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#3  0x00007f1b0d0998fa in __GI_abort () at abort.c:79
#4  0x00000000035e1d53 in segv_handler ()
#5  <signal handler called>
#6  0x0000000000a85ee5 in l_Parser_tokenMap___at_parsePart___spec__10 ()
#7  0x0000000000a87075 in l_parseSymbol___lambda__1 ()
#8  0x00000000035ccbad in lean_apply_2 ()
#9  0x0000000000a7fd8b in l_Parser_lookAhead___at_parseSymbol___spec__5 ()
#10 0x0000000000a810c2 in l_parseSymbol ()
#11 0x0000000000a90244 in l_parseNextEntry ()
#12 0x0000000000a91854 in l___private_Parser_Basic_0__Parser_foldAux_rest___at_parseLine___spec__1 ()
#13 0x0000000000a92136 in l_parseLine ()
#14 0x0000000000a93cf4 in l___private_Parser_Basic_0__Parser_foldAux_rest___at_parseLines___spec__1 ()
#15 0x0000000000a93f2c in l___private_Parser_Basic_0__Parser_foldAux_rest___at_parseLines___spec__1 ()
#16 0x0000000000a93f2c in
...
#73 0x0000000000a93f2c in l___private_Parser_Basic_0__Parser_foldAux_rest___at_parseLines___spec__1 ()

[badly-drawn-wizards]

In the process of trying to come up with a minimal example, I caused an internal panic instead 😭.

import Parser 
import Parser.Char

open Parser Parser.Char Std

abbrev P := SimpleParser Substring Char

def test : IO Unit := do
  let x := Parser.run (Parser.foldl (fun _ _ => ()) (pure ()) (pure ()) : P Unit) ""
  match x with
  | .ok _ res => pure res
  | .error err => IO.println err
def main : IO Unit := test

stdout/stderr

INTERNAL PANIC: unreachable code has been reached

[fgdorais]

Quick update: foldl and many other functions are tail recursive in form only. The issue is with the try ... catch and I need to redesign a lot of code.

The other code appears to have a different issue. Somehow the IR compilation of test is: def test (x_1 : @& obj) : obj := ⊥ ! No wonder it panics!

Anyway, lots of fun work to do on my end!

[fgdorais]

I now have a fix where foldl is tail recursive, see PR #6.

I'm looking into the other issue.

[fgdorais]

Ah! The other issue is because pure () doesn't consume any input, so test is an infinite loop. It seems that the lean compiler somehow realized this and optimized test to just panic... With the new foldl this test loops forever, as expected.

[fgdorais]

I'll fix some other defs that aren't actually tail recursive in PR #6. In the mean time, you can use branch foldl instead of main to move forward with your project. This issue will be closed when PR #6 gets merged and you will then get a notification, which will be the signal to switch back to main.