print_from_grammars : (type_grammar.grammar * term_grammar.grammar) -> (hol_type Parse.pprinter * term Parse.pprinter)

- STRUCTURE
- SYNOPSIS
- Returns printing functions based on the supplied grammars.
- LIBRARY
- Parse
- DESCRIPTION
- When given a pair consisting of a type and term grammar (such a pair is exported with every theory, under the name <thy>_grammars), this function returns printing functions that use those grammars to render terms and types using the system’s standard pretty-printing stream type.
- FAILURE
- Never fails.
- EXAMPLE
- With arithmeticTheory loaded, arithmetic expressions and numerals print pleasingly:The printing of these terms is controlled by the global grammar, which is augmented when the theory of arithmetic is loaded. Printing functions based on the grammar of the base theory bool can be defined:
- load "arithmeticTheory"; > val it = () : unit - ``3 + x * 4``; > val it = ``3 + x * 4`` : term

These functions can then be used to print arithmetic terms (note that neither the global parser nor printer are disturbed by this activity), using the Portable.pprint function (or Lib.ppstring, which returns a string):> val (typepp, termpp) = print_from_grammars bool_grammars; val termpp = fn : term Parse.pprinter val typepp = fn : hol_type Parse.pprinter

Not only have the fixities of + and * been ignored, but the constants in the term, belonging to arithmeticTheory, are all printed in “long identifier” form because the grammars from boolTheory don’t know about them.> Portable.pprint termpp ``3 + x * 4``; arithmetic$+ (arithmetic$NUMERAL (arithmetic$BIT1 (arithmetic$BIT1 arithmetic$ZERO))) (arithmetic$* x (arithmetic$NUMERAL (arithmetic$BIT2 (arithmetic$BIT1 arithmetic$ZERO)))) > val it = () : unit

- USES
- Printing terms with early grammars such as bool_grammars can remove layers of potentially confusing pretty-printing, including complicated concrete syntax and overloading, and even the underlying representation of numerals.
- SEEALSO

HOL Kananaskis-14