Re: [isabelle] Unwanted type annotations



Am 23.05.2013 um 23:03 schrieb Makarius <makarius at sketis.net>:

> So we are back to figure out what is actually required -- and what is possible.  We should probably continue this in a private mail thread.

We can certainly continue in a private thread, but what we want is plain and might be generally interesting to other people on the mailing list:

1. A string_of_term function such that parse(string_of_term t)) aconv t (or at least they are equivalent for metis) and the output string is highly readable (in particular, not marred by type annotations).

There are of course many issues involved here, including output-only syntaxes, but in practice with Sledgehammer the most urgent problem, already mentioned by Paulson and Susanto in their 2007 paper, is the type annotations. None of the default print modes quite does the trick, quickly leading to replay failures. So we refined goal 1 into goal 1b:

1b. A string_of_term function such that parse(string_of_term t)) aconv t (or at least they are equivalent for metis) and the output contains a (locally) minimal number of type annotations (i.e., removing one would lead to a more general proposition).

Steffen was quite successful with goal 1b -- so far numerals are the only corner case in which his approach fails and sometimes produces not only nonminimal solutions (which we can live with), but also horrors like ((0::'a)::'a) -- which parses OK but it disappointing after spending so much energy tying to come up with minimal annotations.

Jasmin





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