Makarius,

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.


Thanks
Tobias

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
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


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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to