Text.Parser: support for stateful grammars

[msmorgan]

This PR adds simple state support (state type is constant) to Text.Parser.

Grammar has been renamed GrammarT, and is additionally parameterized by a state type.
Grammar is now a type-level function producing a GrammarT type with unit state.

Introduces get, put, modify, and gets.
Introduces parseState, which parses according to a grammar and an initial state.

Items that need feedback:

• Function/type names, argument order.
• Is this advanced enough, or should something with pre- and postconditions such as Control.ST be investigated instead?
• Does the Failure constructor of ParseResult really need to include a state? Update: State has been removed from the ParseResult.Failure constructor.
• How to implement runGrammar : innerST -> GrammarT innerST tok c a -> GrammarT outerST tok c (a, innerST). Update: This is implemented, but the compiler hangs.

[msmorgan]

The latest update causes the compiler to hang when processing the doParse function.

I've added State directly to the Grammar type (now GrammarST), rather than adapting the StateT type to work with it. I attempted to do this, but I encountered problems with the productivity heuristic for totality and infinite types. Because >>= needs to unpack and repack the ST constructor of StateT, Idris cannot verify that applications of >>= are total as it can with Grammar. This works with Grammar alone, because >>= reduces to one of two constructors of Grammar, satisfying the productivity heuristic.

A fix to the above problem with StateT might be to add a new totality heuristic, the likes of "remains infinite in output". If the input to a function is wrapped in Inf, its evaluation must be wrapped in Inf in the output to that function. Such a rule might be enough for Idris to consider the code linked above to be total.

[msmorgan]

It turns out Idris doesn't hang indefinitely, but it does take an additional 19 minutes on my machine to build contrib with these changes.

[ahmadsalim]

@msmorgan Hmm, that seems not nice. I know it is not your fault, but that is a significant slowdown.

[msmorgan]

As an experiment, I removed the Run constructor and the code that supports it. The compile time went down drastically, now only 2 minutes longer than before this PR.

However, as Run is used in the implementation of lift, it seems too important to omit from this PR.

[ahmadsalim]

@msmorgan Any status on this PR?

Also, the tests are currently failing.

[msmorgan]

The tests are failing because the builds are timing out, as I mentioned earlier. I'm not sure how to correct this. If I get the time, I could try one of the following approaches. Which do you think has the best chance of speeding up the compiler?

• Refactor doParse by splitting it into several helper functions that are mutually recursive with doParse.
• Refactor doParse by modifying the return type somehow.
• Modify doParse to accept a Stream of input tokens instead of a List, and change the return type to be infinite. I think it's possible to retain totality using this approach, but I don't know if it would be possible to make a total finite interface to this function without assert_total. For example, if this function takes a List tok argument, it could pass a Stream (Maybe tok) to the new, infinite doParse. The problem would arise in the portion that processes the potentially-infinite (even though we know it isn't) result.

The third option doesn't sounds like a very good idea, now that I've written it out.

[ahmadsalim]

@msmorgan Have you considered doing partial evaluation on the input grammar?

[msmorgan]

@ahmadsalim I have not, nor do I know what it is.

[ahmadsalim]

@msmorgan You can annotate a term with %static if you want Idris to partially evaluate it.

Partial evaluation tries to specialize the code for that argument, and hopefully generate more efficient code 😄

[msmorgan]

I tried annotating various arguments to doParse with %static, but observed no improvement in compile time. If I understand the documentation page, the best code generation improvement would come from annotating the grammar argument, (act : GrammarT st tok c ty).

I built Idris with profiling enabled, removed the %static annotations and profiled idris --check Text/Parser/Core.idr. The report indicates that compiler spends the majority of the time in the totality checker, namely the inner function Idris.Totality.checkMP.tryPath. It also appears that a large amount of time is used comparing Idris.Core.TT.Name objects, using the derived Eq.(==) and Ord.compare functions. Perhaps comparison on these objects could be improved via memoization, hashing, or both; or maybe the compiler is sorting Name objects much too frequently for whatever reason.

I've uploaded the full profiling dump (which weighs in at 118 MB) as a 5.5 MB zip archive here.

[ahmadsalim]

@msmorgan Maybe integrating https://hackage.haskell.org/package/intern in Eq and compare would be good? 😄

[msmorgan]

The issue seems to be one of asymptotic complexity, causing this function to be called hundreds of thousands of times while compiling doParse. Speeding up name lookup would be helpful but wouldn't solve the problem.

[msmorgan]

I ran profiling for this compile and have uploaded the results here. Be warned: the uncompressed file is enormous.