Re: [isabelle] Exception Chr raised while processing "fun" (Isabelle 2016)



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.