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