Re: [isabelle] Canonical types of constants

Thanks, that works fine.


On 09/02/2016 13:22, Makarius wrote:
On Tue, 9 Feb 2016, Tobias Nipkow wrote:

In order to obtain the type of a constant c I am using this code snippet:

Proof_Context.read_const {proper = true, strict = false} ctxt c

It gives me back a term Const(c,T) and then I proceed with T. How can I make
sure that the type variables in T have canonical names 'a, 'b etc? Should I be
using some other piece of code?

This correctly produces a type scheme for the constant, according to its
declaration.  It uses schematic type variables, but these are considered
"private" to a declaration and not necessarily canonical in an application context.

The proper way to make schematics visible in a context (and printable) can be
seen in the implementation of the document antiquotation @{const}:

Note that show_question_marks = false produces unreliable results: pretending
that schematic variables are not schematic is fragile. LaTeXsugar.thy seems to
suffer from that wrong assumption.

The background is that in 7f5579b12b0a, constant "card" has type "?'b set =>
nat" instead of "?'a set => nat" as in the past.

The definition of "card" has changed here and thus its internal
type declaration.

Here is an example that illustrates the situation and shows how to make
canonical types inside a given context:

consts a :: 'a
consts b :: 'b

ML â
   fun read_const ctxt s =
       val t = Proof_Context.read_const {proper = true, strict = false} ctxt s;
       val ([t'], _) = Variable.import_terms true [t] ctxt;
     in (t, t') end;

   read_const @{context} "a";
   read_const @{context} "b";
   read_const @{context} "card";

Of course, the result depends on the context.  E.g. within the context of
"context fixes x :: 'a begin" new types start at 'b.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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