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.

Best regards,


On Mon, Oct 17, 2016 at 12:33 PM, Lars Hupel <hupel at> 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:
>   Lexicographic_Order.no_order_msg
> 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 ...
> Cheers
> Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.