[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Makarius]

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
Encodability_Process_Calculi

isabelle build -d '$AFP' -o threads=1 -o profiling=time HOL-ODE-Numerics
Encodability_Process_Calculi

isabelle profiling_report
~/.isabelle/heaps/polyml-5.7.1_x86-linux/log/HOL-ODE-Numerics.gz

isabelle profiling_report
~/.isabelle/heaps/polyml-5.7.1_x86-linux/log/Encodability_Process_Calculi.gz

The tail of the latter looks like this:

           318 List.filter
           338 Same.map
           481 eq-typ
           521 Term.aconv
           575 Lexicon.tokens_match_ord
           712 Basics.fold
           771 List.map
           944 GARBAGE COLLECTION (minor collection)
           944 GARBAGE COLLECTION (total)
          1147 Table().lookup_key
          1168 Table().defined
          2034 Table().lookup
          2178 Table().modify

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?


	Makarius