Evaluating with `:x` enters infinite loop

[BartAdv]

Please attach complete source files that exhibit the issue in addition to quoting from them here.

Steps to Reproduce

Given source:

import Lightyear
import Lightyear.Char
import Lightyear.Strings

test : Parser (List Char)
test = many alphaNum

Try following REPL commands:

λΠ> parse test "abc"

λΠ> :x parse test "abc"

Expected Behavior

Both commands should produce the same result:

Right ['a', 'b', 'c'] : Either String (List Char)

Observed Behavior

Expression evaluated with:x enters infinite loop.

From the looks of it, it seems like the fact the many combinator uses some laziness is the culprit. I wasn't able to reproduce it with some simpler code, without external dependency, however.

[ahmadsalim]

Thanks for reporting the issue, please use :exec instead.

[msmorgan]

I tried a similar test with Text.Parser, with interesting results.

$ idris -p contrib
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.1.1-git:916111bf
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris> :module Text.Parser
*Text\Parser> parse (unpack "abc") (many (terminal Just))
Right (['a', 'b', 'c'], []) : Either (ParseError Char) (List Char, List Char)
*Text\Parser> :x parse (unpack "abc") (many (terminal Just))
Left (Error "Help the coverage checker!" []) : Either (ParseError Char)
                                                      (List Char, List Char)
*Text\Parser>

[ziman]

@BartAdv also mentioned on IRC that when this program is compiled, it reduces to Right ['a','b','c'], as expected.

[ziman]

Does :x use a separate case tree compiler?

[BartAdv]

@ahmadsalim thanks, :exec does the job.

[david-christiansen]

:x interprets the case trees that come out of the case tree compiler, my guess is that there's a bug in that. It would be nice if the executor supported Lightyear, because then it would also be useful in type providers. I'd always assumed that the looping was due to laziness being handled wrong, so in some sense it's good to have an example of a different output.

[BartAdv]

because then it would also be useful in type providers

Incidentally, my plan was to write that parser, and then make it work as a type provider :(