[isabelle] Unwanted type annotations

[Steffen Juilf Smolka]

Hi,

For some reason, I can't get Isabelle to print the following term without type annotations:

val t = @{term "0∷'a∷comm_monoid_add"}

I have tried

val ctxt = @{context}
|> Config.put show_markup false
|> Config.put show_types false
|> Config.put show_free_types false
|> Config.put show_all_types false
|> Config.put show_sorts false
val _ = t |> Syntax.string_of_term ctxt |> writeln

which produces the output "0∷'a". Am I doing something wrong?

Best Regards,
Steffen

[Peter Lammich]

I think this behaviour is hard-coded into the pretty-printer. On
numerals with variable types, it always prints the type.

Peter

[Makarius]

The question is what all these flags mean in detail, also what you mean by
"unwanted". Do you just don't want to see it as end-user, or does some ML
code of yours depend critically on a certain behaviour?

The inner syntax pretty printing infrastructure of Isabelle is very
flexible, and many details are determined by translation functions in user
space (here the HOL library).

You can search the Isabelle/HOL sources for the syntax const "_constrain"
to get an idea where certain notation takes special care about such extra
type constraints. You can then make educated guesses on which kind of
behaviour you can bet, or better not.


Makarius

[Brian Huffman]

On Thu, May 16, 2013 at 2:32 PM, Peter Lammich <lam...@in.tum.de> wrote:
> I think this behaviour is hard-coded into the pretty-printer. On
> numerals with variable types, it always prints the type.

Pretty-printing for numerals is implemented with a
"typed_print_translation (advanced)" command in HOL/Num.thy. The bit
of ML code there implements the logic for deciding when to add a type
annotation.

This is an intentional feature. Without it, a numeral like "0" might
be parsed with a too-general type like "0::'a::zero" without the
user's knowledge, leading to much confusion.

- Brian

[Steffen Juilf Smolka]

> Do you just don't want to see it as end-user, or does some ML code of yours depend critically on a certain behaviour?

In Sledgehammer, we generate proof texts with a minimal amount of type annotations. The code assumes that only the annotations introduced with Type.constraint will be printed. (Therefore, I refer to any other annotations procuced by the pretty printer as "unwanted").

The example I posted is the first one I encountered for which this assumption does not hold. The "unwanted annotations" do not break the generated Isar-Proof, they just look ugly (and are useless).

-- Steffen

[Steffen Juilf Smolka]

Is there a way to turn this feature off or to predict reliably when annotations are inserted?
From the code it seems that numerals with polymorphic types are annotated, then again i know @{term 1} is polymorhpic but printed without annotation. I guess I don't understand the code completely…

The code I am working on equips terms with a minimal set of type annotations which ensures the types of the terms are preserved (when printing and reparsing the terms).

Thanks for you help!
Steffen

[Jasmin Blanchette]

Hi Steffen,

Am 21.05.2013 um 17:42 schrieb Steffen Juilf Smolka <steffen...@in.tum.de>:

> Is there a way to turn this feature off or to predict reliably when annotations are inserted?

> From the code it seems that numerals with polymorphic types are annotated, then again i know @{term 1} is polymorhpic but printed without annotation. I guess I don't understand the code completely�

>
> The code I am working on equips terms with a minimal set of type annotations which ensures the types of the terms are preserved (when printing and reparsing the terms).

I think I found a workaround. There seems to be no requirement that the term that's printed is type-correct. Hence, you could type all numerals with the type "nat" or "real" or probably even "unit" to avoid the spurious type annotations. For example:

ML {*
@{term "0::nat"}
|> Type.constraint @{typ "'b"}
|> Syntax.string_of_term @{context}
|> warning
*}

Cheers,

Jasmin

[Steffen Juilf Smolka]

That does the trick!

Thanks,
Steffen

[Makarius]

On Tue, 21 May 2013, Jasmin Blanchette wrote:

> Am 21.05.2013 um 17:42 schrieb Steffen Juilf Smolka
> <steffen...@in.tum.de>:
>
>> Is there a way to turn this feature off or to predict reliably when
>> annotations are inserted? From the code it seems that numerals with
>> polymorphic types are annotated, then again i know @{term 1} is
>> polymorhpic but printed without annotation. I guess I don't understand

>> the code completely…

These syntax applications in the Isabelle/HOL library should be understood
as examples of what could be done in typical (ambitious) applications.
Studying such empirical material is then the starting point for trying to
pin down a situation that successfully work under certain minimal
assumptions. This requires revisit the question what "unwanted" actually
means here.

BTW, the syntax layers of Isabelle are even thicker than seen here wrt.
parse/print translations. In particular, there are also check/uncheck
phases with multiple stages that could do quite sophisticated things to
term input and output.

>> The code I am working on equips terms with a minimal set of type
>> annotations which ensures the types of the terms are preserved (when
>> printing and reparsing the terms).
>
> I think I found a workaround. There seems to be no requirement that the
> term that's printed is type-correct. Hence, you could type all numerals
> with the type "nat" or "real" or probably even "unit" to avoid the
> spurious type annotations. For example:
>
> ML {*
> @{term "0::nat"}
> |> Type.constraint @{typ "'b"}
> |> Syntax.string_of_term @{context}
> |> warning
> *}

Here is another example:

declare [[show_markup = false]]

ML {*
fun test s =
let
val ctxt = @{context};
val t = Syntax.read_term ctxt s;
val t' = map_types (fn _ => dummyT) t;
in
writeln (Syntax.string_of_term ctxt t);
writeln (Syntax.string_of_term ctxt t')
end
*}

ML_command {* test "0" *}
ML_command {* test "1" *}

ML_command {* test "x ⟷ y" *}
ML_command {* test "x ≠ y" *}


Types are not strictly necessary for printing, but the presence or absence
of types is important for certain fine points. In the examples above the
difference is merely the folding of term abbreviations; without proper
types this "uncheck" stage is omitted. There are further things that
break down without types.


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.


Makarius

[Jasmin Blanchette]

Am 23.05.2013 um 23:03 schrieb Makarius <maka...@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