# 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.*