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

[Tobias Nipkow]

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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180201/970862db/attachment.bin>