Re: [isabelle] translations and numerals

On Tue, 21 Jan 2014, Tobias Nipkow wrote:

I am using Library/Extended that defines a datatype with a unary constructor Fin. I want to print terms like "Fin 5" as "5" and am using the following translations:

"_Numeral i" <= "CONST Fin(_Numeral i)"
"0" <= "CONST Fin 0"
"1" <= "CONST Fin 1"

Printing is a black art, especially when using the AST representation of 'translations', which can contain additional annotations unexpectedly.

The configuration option syntax_ast_trace generally helps to see what happens to happen in a particular situation, and it shows additional constraints and markup in the rich document output of Isabelle/PIDE.

In other print modes, there can be different add-ons.

Instead of these fragile and complicated syntax translations, the usual way to modify term output systematically is via the "uncheck" phase. It has the advantage that it operates on regular type-correct lambda terms: that requires a few more cases to cover (in Isabelle/ML), but there is no black magic.

The included theory No_Fin demonstrates that. Note that I am using a fully official constant no_Fin here, which is not printed in the end due to its special notation.

theory No_Fin
imports Main "~~/src/HOL/Library/Extended"

definition "no_Fin = Fin"
notation (output) no_Fin  ("_")

declaration {*
    fun is_num (Const (@{const_name Num.One}, _)) = true
      | is_num (Const (@{const_name Num.Bit0}, _) $ t) = is_num t
      | is_num (Const (@{const_name Num.Bit1}, _) $ t) = is_num t
      | is_num _ = false;
    fun no_Fin T t = Const (@{const_name no_Fin}, T) $ t;

    fun uncheck (tm as Const (@{const_name Fin}, T) $ t) =
          (case t of
            Const (@{const_name}, _) => no_Fin T t
          | Const (@{const_name}, _) => no_Fin T t
          | Const (@{const_name numeral}, _) $ u => if is_num u then no_Fin T t else tm
          | _ => tm)
      | uncheck (t $ u) = uncheck t $ uncheck u
      | uncheck (Abs (x, T, t)) = Abs (x, T, uncheck t)
      | uncheck t = t;
  in fn _ => Syntax_Phases.term_uncheck 0 "no_Fin" (fn _ => map uncheck) end

term "\<lambda>y::nat. [Fin 0, Fin 1, Fin 5, Fin x, Fin y]"

text {*
  @{term "\<lambda>y::nat. [Fin 0, Fin 1, Fin 5, Fin x, Fin y]"}


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