I think (simple) sections do indeed improve readbility. BUT in the light of your comments I am not keen on them in Isabelle. We do not need yet more syntactic sugar.


On 01/02/2018 16:41, Makarius wrote:
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

isabelle profiling_report

isabelle profiling_report

The tail of the latter looks like this:

            318 List.filter
            481 eq-typ
            521 Term.aconv
            575 Lexicon.tokens_match_ord
            712 Basics.fold
            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: 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?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to