Re: [isabelle] Canonical types of constants



Thanks, that works fine.

Tobias

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}:
Variable.import_terms.

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
http://isabelle.in.tum.de/repos/isabelle/rev/9f4f0dc7be2c 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 =
     let
       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.


     Makarius

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



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