[isabelle-dev] NEWS: op <infix> -> (<infix>)
makarius at sketis.net
Thu Feb 1 16:41:24 CET 2018
On 01/02/18 07:41, Tobias Nipkow wrote:
> At the time I was also wondering whether to allow `sections', eg "(+ 1)"
> or (1 +)" but did not want to overdo it. It sounds like that at least
> with your parser imporvements it might be ok?
I am unsure -- my changes barely recovered the old performance. Anyway,
this is how to do measurements on the most relevant AFP sessions:
isabelle build -d '$AFP' -R -b -j4 HOL-ODE-Numerics
isabelle build -d '$AFP' -o threads=1 -o profiling=time HOL-ODE-Numerics
The tail of the latter looks like this:
944 GARBAGE COLLECTION (minor collection)
944 GARBAGE COLLECTION (total)
Addition of grammar productions (for local syntax) shows up as
Table().lookup, Table().modify, Lexicon.tokens_match_ord. Actual parsing
also as List.filter.
Note that infix sections will require more than just a few grammar
changes: you need to introduce a lambda or auxiliary combinator for the
right section (+ a). Maybe based on some "abbreviation (input)"?
Here are also some notes from Haskell:
https://wiki.haskell.org/Section_of_an_infix_operator that immediately
raise more questions:
* What to do with prefix "-" vs. infix "-"?
* What to do with iterated sections (a + b +)?
* Does all that actually help readability of expressions (e.g. for
mathematicians) or just appeal to strange Haskelloids?
More information about the isabelle-dev