CakeML/cakeml

Implement lexer on mlstrings

Aperta

#353 aperta il 26 ott 2017

 (3 commenti) (0 reazioni) (0 assegnatari)Standard ML (98 fork)auto 404
help wanted

Metriche repository

Star
 (1169 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

The CakeML lexer operates on a char list. Therefore the first thing the CakeML compiler does after reading in its input string is explode the string into a list. This is wasteful: I think the lexer can easily be made to work on mlstrings.

This issue is to make the lexer operate on mlstrings and update the compiler accordingly to avoid the explode.

Extension thoughts:

  • The sexp-parsing option would still need to explode the input because the sexp parser operates on char lists in a possibly more unavoidable way. (This issue does not require avoiding the explode for sexps.)
  • For large input, we might want to be even more sophisticated and lex/parse/typecheck incrementally, to catch errors before reading in all the source code. (Obviously this issue doesn't require doing that.)

Guida contributor