Re: [isabelle] Exception Chr raised while processing "fun" (Isabelle 2016)
Dear Eugene, dear Lars, dear Andreas,
I remember writing this line ten years ago as part of my bachelor
thesis equivalent. It survived ten years of refinements, but Makarius
pointed out in 2012 already in a review that this function does not
scale. It just seems that no one actually reported the issue in
practice, nor did someone take time to consider a proper solution. I
have added to my todo list for the next Isabelle 2017; I won't have
time to get things done for Isabelle 2016-1. If anyone else has more
working time please feel free to take over.
On Mon, Oct 17, 2016 at 12:33 PM, Lars Hupel <hupel at in.tum.de> wrote:
> Hi Eugene,
>> (* exception Chr raised (line 268 of "./basis/String.sml") *)
> this is a fun problem!
> By looking at the exception trace (to be enabled with "declare
> [[ML_exception_trace]]" before "fun"), we can see the culprit:
> This function formats the message you see when the function package is
> unable to find a termination order. In this specific case it fails
> because it tries to come up with some alphabetic index:
> val gc = map (fn i => chr (i + 96)) (1 upto length table)
> Because there function definition explodes in size internally, the
> argument passed to "chr" is simply out of range.
> I'm pretty sure the author of the function package did not anticipate
> such large functions ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and