Isabelle syntax translations: Force eta-expansion?

Question

Isabelle’s List theory has set up a syntax translation for filter:

syntax
  -- {* Special syntax for filter *}
  "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")

translations
  "[x<-xs . P]"== "CONST filter (%x. P) xs"

and indeed term "filter (λ x. ¬(P x)) l" will nicely print

"[x←l . ¬ P x]"  :: "int list"

But if the expression is simple, e.g. ilter (λ x. P x) l, eta-contraction seems to happen and I get shown

"filter P l" :: "int list"

Can I somehow force the nice syntax (i.e. [x←l . P x]) here as well?

Answer 1

You can avoid eta-contraction by installing an appropriate print_translation. There are several examples for binders and tuples in the HOL sources, e.g., for THE in HOL.thy. They are easy to adapt to filter, for example:

print_translation {*
  [(@{const_syntax filter}, fn _ => fn [Abs abs, xs] =>
    let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    in Syntax.const @{syntax_const "_filter"} $ x $ t $ xs end)]
*}  -- {* To avoid eta-contraction of body *}