Re: [isabelle] Canonical types of constants



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


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