[isabelle-dev] partial_function

[Christian Sternagel]

(Almost) everything back. I merely stumbled across a known issue (which 
in hindsight I vaguely remember, but I did not find the corresponding 
thread).

First I had to increase unify_search_bound (otherwise I obtained an 
error as described in my previous email). What I did *not* notice 
however, was the following message at the end of a very long trace (in 
jEdit):

   Tracing paused.  Stop, or continue with next 100, 1000, 10000 messages?

So, actually jEdit was just waiting for my input and not computing for 
hours (as I thought; I should have observed that from the missing scream 
of my laptops fan).

By setting "unify_trace_bound" to the same value for which 
"unify_search_bound" succeeded, everything was fine again.

Sorry for the false alarm.

cheers

chris

On 08/06/2013 02:40 PM, Christian Sternagel wrote:
> Dear all,
>
> I'm currently checking IsaFoR [1] against the repository versions of
> Isabelle (8d8cb75ab20a) and the AFP (05436df687d1). Doing so, I stumbled
> across a "partial_function" definition that worked with Isabelle2013 but
> aborts now with a "Unification bound exceeded".
>
> Is anybody aware of changes in "partial_function" or unification (or
> somewhere I didn't think of) that could explain this?
>
> The general shape of the function (which is employed to parse XML into
> an internal datatype) is:
>
>    partial_function (parse_result)
>      ...
>    where
>      "parser x y = xml1element ''tag name'' (xml_options [
>        (''tag name 1'', parser_1),
>        (''tag name 2'', parser_2,
>        ...
>        (''tag name N'', parser_N)
>      ]) ..."
>
> where some of the "parser_i" use "parser" recursively. Currently we have
> around 20 parsers in the above list and the error disappears if I reduce
> that to 14 (with "unify_search_bound = 90").
>
> If anybody has the energy to look at the real code ;) see [2], theory
> CPF_Parser.thy, partial function "xml2dp_termination_proof". You will
> also have to apply a patch from my local patch queue (which is
> attached), since the "official" repository is for Isabelle2013.
>
> cheers
>
> chris
>
> [1] http://cl-informatik.uibk.ac.at/software/ceta/
> [2] http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR