idris-lang/Idris-dev — pull request #1729 by projedi (2014-11-16 20:50:25+00:00)
Title: Custom syntax optimization

Brief description
---------------------

Previously all custom syntax rules were tried one after the other
with full rollback (via `try`). Now they are tried one after the other
but with a minimal rollback.

Introduces datatype `SyntaxRules` which contains a list of rules and
4 "precomputed" parsers (`expr`/`simpleExpr` * term/pattern). Every time
new syntax rule is introduced parsers are rebuilt. Expression parsers
use an appropriate parser.

Example: for the following 5 rules
```idris
syntax "[" [start] ".." ...
syntax "[" [start] "," ...
syntax [from] "={" ...
syntax [expr] "QED" ...
syntax "if" [test] ...
```
previously resulting parser conceptually was
```haskell
choice [ try (symbol "[" >> expr >> symbol ".." >> ...)
, try (symbol "[" >> expr >> symbol "," >> ...)
, try (expr >> symbol "={" >> ...)
, try (expr >> symbol "QED" >> ...)
, try (symbol "if" >> expr >> ...)
]
```
now it conceptually is
```haskell
choice [ try (symbol "[" >>
choice [ try (expr >>
choice [ try (symbol ".." >> ...)
, try (symbol "," >> ...)
])
])
, try (expr >>
choice [ try (symbol "={" >> ...)
, try (symbol "QED" >> ...)
])
, try (symbol "if" >>
choice [ try (expr >> ...)
])
]
```
Profit is in transition between rules 1-2 (and rules 3-4):
if rule 1 fails after `expr` was evaluated it would have
been reevaluated again in the rule 2. Now it wouldn't.

Some numbers
----------------------------

Running `idris --check +RTS -s -RTS` on the following file:
```idris
module Main

f : List (List (List (List (List a))))
f = [ [ [ [ [ ] ] ] ] ]
```
previosly printed:
```
20,965,042,608 bytes allocated in the heap
3,218,410,464 bytes copied during GC
77,810,384 bytes maximum residency (19 sample(s))
1,439,912 bytes maximum slop
226 MB total memory in use (0 MB lost due to fragmentation)

Tot time (elapsed) Avg pause Max pause
Gen 0 40416 colls, 0 par 3.80s 3.81s 0.0001s 0.0011s
Gen 1 19 colls, 0 par 0.95s 0.95s 0.0499s 0.0967s

TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

INIT time 0.00s ( 0.00s elapsed)
MUT time 6.57s ( 6.58s elapsed)
GC time 4.75s ( 4.76s elapsed)
EXIT time 0.02s ( 0.02s elapsed)
Total time 11.34s ( 11.36s elapsed)

Alloc rate 3,191,136,017 bytes per MUT second

Productivity 58.1% of total user, 58.0% of total elapsed

gc_alloc_block_sync: 0
whitehole_spin: 0
gen[0].sync: 0
gen[1].sync: 0
```
now prints
```
1,122,171,504 bytes allocated in the heap
365,460,136 bytes copied during GC
75,578,376 bytes maximum residency (10 sample(s))
1,459,752 bytes maximum slop
160 MB total memory in use (0 MB lost due to fragmentation)

Tot time (elapsed) Avg pause Max pause
Gen 0 2157 colls, 0 par 0.22s 0.22s 0.0001s 0.0011s
Gen 1 10 colls, 0 par 0.24s 0.24s 0.0237s 0.0958s

TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

INIT time 0.00s ( 0.00s elapsed)
MUT time 0.25s ( 0.25s elapsed)
GC time 0.46s ( 0.46s elapsed)
EXIT time 0.01s ( 0.01s elapsed)
Total time 0.72s ( 0.72s elapsed)

Alloc rate 4,499,652,767 bytes per MUT second

Productivity 36.3% of total user, 36.2% of total elapsed

gc_alloc_block_sync: 0
whitehole_spin: 0
gen[0].sync: 0
gen[1].sync: 0
```
(for completeness) running without deleting generated .ibc file produces similar results
```
967,627,104 bytes allocated in the heap
335,371,872 bytes copied during GC
75,578,376 bytes maximum residency (10 sample(s))
1,447,464 bytes maximum slop
160 MB total memory in use (0 MB lost due to fragmentation)

Tot time (elapsed) Avg pause Max pause
Gen 0 1860 colls, 0 par 0.18s 0.18s 0.0001s 0.0005s
Gen 1 10 colls, 0 par 0.24s 0.24s 0.0243s 0.0973s

TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

INIT time 0.00s ( 0.00s elapsed)
MUT time 0.17s ( 0.17s elapsed)
GC time 0.42s ( 0.42s elapsed)
EXIT time 0.01s ( 0.01s elapsed)
Total time 0.60s ( 0.60s elapsed)

Alloc rate 5,729,211,059 bytes per MUT second

Productivity 30.3% of total user, 30.3% of total elapsed

gc_alloc_block_sync: 0
whitehole_spin: 0
gen[0].sync: 0
gen[1].sync: 0
```
Idris executable was built with profiling turned off and optimization set to 2.

Why
------

Speeds up parsing of nested lists (e.g. when building [Rose tree](http://en.wikipedia.org/wiki/Rose_tree) instances in code).