Re: [isabelle] Unwanted type annotations

On Tue, 21 May 2013, Jasmin Blanchette wrote:

Am 21.05.2013 um 17:42 schrieb Steffen Juilf Smolka <steffen.smolka at>:

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 =
      val ctxt = @{context};
      val t = Syntax.read_term ctxt s;
      val t' = map_types (fn _ => dummyT) t;
      writeln (Syntax.string_of_term ctxt t);
      writeln (Syntax.string_of_term ctxt t')

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.


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