printing types in non-ML notation · General

I'm surely working against the pretty-printing and syntax but what I found in Pure/HOL/AFP does not seems to address this issue I am facing.

I want to print a type in postfix notation, e.g. option 'a, in place of prefix notation.

After spelunking in pure_theory.ML I got to the syntax definition for type application and I can override the normal syntax with mine for a custom print mode.

syntax (pvl output)
    "_tapp" :: "type => type_name => type" ("(1_<_>)")

typ "'a option"            (* prints as 'a option    *)
typ (pvl) "'a option" (* prints as 'a<option> *)

I cannot exchange the order of in the mixfix declaration but I can declare a new pattern _pvl_tapp and a translation from _tapp to _pvl_tapp.

syntax (pvl output)
    "_pvl_tapp" :: " type_name => type => type" ("(1_<_>)") (* note inversion of type_name and type in production *)

typ "'a option"            (* prints as 'a option    *)
typ (pvl) "'a option" (* prints as 'a option, expected as I have no translation yet *)

translation
  "_pvl_tapp tc ty" == "_tapp ty tc"


typ "'a option"            (* prints as 'a option    *)
typ (pvl) "'a option" (* prints as 'a option *)

I even got as far as looking at type_syntax but that binds one syntax constant to one type or type synonym.
Decorating the translation with the (type) qualifier (?) yields the error Undefined type name: "_pvl_tapp", example below.

 translation
  (type) "_pvl_tapp tc ty" == (type) "_tapp ty tc"

Is this use-case supported in any way? It's also unclear how to interface with the type pretty printing and I cannot find anybody attempting this.

The second question is, it there a way to scope translations to one printing mode? In the previous example the translation from _tapp to _pvl_tapp makes no sense in normal output so it should be ignored by the system, which is what I am observing now.

Lukas Stevens (Oct 31 2025 at 10:26):

Your approach looks good and I am not sure why it is not working. You might have more luck asking on the mailing list.

Edoardo Putti (Nov 06 2025 at 20:15):

I was able to use the following snippet to replace the production _tapp with the production _pvl_tapp. It does not look like it is possible to do this using the translation command. In the following translation I raise an exception when the print mode is not pvl which scopes it to what I needed.

print_translation "
let
  fun with_pvl_mode f ctxt ast = if Print_Mode.print_mode_active "pvl" then f ctxt ast else raise Match;
  fun print_pvl_tapp ctxt [typeAst, typenameAst] = Ast.Appl [Ast.Constant @{syntax_const  "_pvl_tapp"}, typenameAst, typeAst]
 in
  [
   (@{syntax_const "_tapp"},  with_pvl_mode print_pvl_tapp),
  ]
end
"

Stream: General

Topic: printing types in non-ML notation

Edoardo Putti (Oct 31 2025 at 09:34):

Lukas Stevens (Oct 31 2025 at 10:26):

Edoardo Putti (Nov 06 2025 at 20:15):