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:

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.


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

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

declaration {*
  let
    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 zero_class.zero}, _) => no_Fin T t
          | Const (@{const_name one_class.one}, _) => 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]"}
*}

end



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