printer.ml: insert space before ":" when annotated head ends symbolically

[aqjune-aws]

Under print_types_of_subterms := 2 (or := 1 with invented type variables), pp_print_term wraps a head h as "(s:type)". When s ends in a symbolic character — e.g. "&" — the printed text "&:num->real" would lex back as a single Ident ("&:" is one token per lex), so the round trip parse_term o string_of_term failed. print_atom now inserts a single space before the ":" when the printed name ends in a symbolic character; for prefix/infix/binder names that are wrapped as "(op)" the trailing ")" suppresses this and printing is unchanged.

The initial fix was authored by Balaji Rao in
kings-crown/hol-light@281d03ec ("Made the printer insert a space between a symbolic printed head and the following type annotation colon"). This commit adopts that one-line check and surrounds it with regression tests.

UnitTests/printer_tests.ml: add show_types regression cases for &n, -- &n, &1 + &2, plus a check_roundtrip helper that builds terms via mk_const/mk_comb/mk_numeral/mk_binop and verifies aconv equality of the reparse with print_types_of_subterms := 2 — independent of the parser surface syntax.

Also broaden the associativity coverage that surrounds these cases:

• num: add EXP, DIV, MOD left-associativity tests (correct the comment that called subtraction the only left-associative num arith op).
• int: add div, rem, pow associativity tests and note that int has no MOD or EXP and that zpow is real-only.
• real: add /, pow, zpow associativity tests with the same notes.

107/107 printer tests pass.

Co-authored-by: Balaji Rao brao@stevens.edu
Co-Authored-By: Claude Opus 4.7 noreply@anthropic.com

[jrh13]

This is great, thanks! As far as I can see this now makes the print-then-parse round trip completely robust.