Printer (nholz)

Printer Module

Namespace: HOL
Assembly: nholz.dll

This module implements the type, term and theorem pretty printers, for outputting quotation representations of internal types/terms/theorems. The printers take into account identifier fixity status and enumeration bracket settings (see 'Names' module), certain special-case theory objects (whose declarations in later modules are anticipated here), and the display modes (see 'DModes' module). This module is a trusted component of the system, since the user will normally rely on it to determine what has been proved and what has been asserted.

Functions and values

Function or value	Description
`annotate_preterm pty_ ptm` Full Usage: `annotate_preterm pty_ ptm` Parameters: pty_ : `pretype option` ptm : `preterm` Returns: `preterm`	This gives a preterm for the supplied term, annotated with any types that are needed for printing. If 'fl' is set, then the type of the overall term is taken as given when decided type annotations. Note that the use of 'check_preterm_annotations' on the result removes the need to trust the relatively complicated type annotation routine. pty_ : `pretype option` ptm : `preterm` Returns: `preterm`
`is_compound_preterm ptm` Full Usage: `is_compound_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`ndest_binargs_preterm n ptm` Full Usage: `ndest_binargs_preterm n ptm` Parameters: n : `int` ptm : `preterm` Returns: `preterm list`	n : `int` ptm : `preterm` Returns: `preterm list`
`need_prec_brkts fl0 (l0, n0) (l1, n1)` Full Usage: `need_prec_brkts fl0 (l0, n0) (l1, n1)` Parameters: fl0 : `bool` l0 : `'a` n0 : `'b` l1 : `'a` n1 : `'b` Returns: `bool`	This is for determining whether precedence brackets are needed for a subexpression. Returns "true" if brackets are needed when going from a construct at parse-level 'l0', precedence 'n0' and extra flag 'fl0' to a construct at parse-level 'l1', precedence 'n1'. If going to a higher parse-level or the same parse-level but higher precedence then no brackets are needed. Flag 'fl0' being set means that brackets are needed if the parse level and precedence are the same. fl0 : `bool` l0 : `'a` n0 : `'b` l1 : `'a` n1 : `'b` Returns: `bool`
`need_separation ss0 s1` Full Usage: `need_separation ss0 s1` Parameters: ss0 : `int list` s1 : `int` Returns: `bool`	This is for determining whether separation (be it brackets or spacing) is required between juxtaposed tokens, given the boundary classes of their names. The following classification is used: alphanumerics 1 symbolics 2 quoted/other 0 Separation is never required with something of class 0 or with something of a different class. The 'ss0' arg is a list of boundary classes that could juxtapose - in some cases it's easier to consider the list of possibilities rather than work out which one it is, and over-use of separation is always safe. ss0 : `int list` s1 : `int` Returns: `bool`
`print_atom ptm` Full Usage: `print_atom ptm` Parameters: ptm : `preterm` Returns: `string`	ptm : `preterm` Returns: `string`
`print_close_brkt ()` Full Usage: `print_close_brkt ()` Parameters: () : `unit` Returns: `string`	() : `unit` Returns: `string`
`print_close_brkt_if b` Full Usage: `print_close_brkt_if b` Parameters: b : `bool` Returns: `string`	b : `bool` Returns: `string`
`print_full_preterm ptm` Full Usage: `print_full_preterm ptm` Parameters: ptm : `preterm` Returns: `string`	ptm : `preterm` Returns: `string`
`print_full_preterm0 (fl0, pr0) ptm` Full Usage: `print_full_preterm0 (fl0, pr0) ptm` Parameters: fl0 : `bool` pr0 : `int * int` ptm : `preterm` Returns: `string`	fl0 : `bool` pr0 : `int * int` ptm : `preterm` Returns: `string`
`print_open_brkt ()` Full Usage: `print_open_brkt ()` Parameters: () : `unit` Returns: `string`	() : `unit` Returns: `string`
`print_open_brkt_if b` Full Usage: `print_open_brkt_if b` Parameters: b : `bool` Returns: `string`	b : `bool` Returns: `string`
`print_preterm ptm` Full Usage: `print_preterm ptm` Parameters: ptm : `preterm` Returns: `string`	ptm : `preterm` Returns: `string`
`print_pretype ty` Full Usage: `print_pretype ty` Parameters: ty : `pretype` Returns: `string`	ty : `pretype` Returns: `string`
`print_pretype0 (ss0, fl0, pr0) pty` Full Usage: `print_pretype0 (ss0, fl0, pr0) pty` Parameters: ss0 : `int list` fl0 : `bool` pr0 : `int * int` pty : `pretype` Returns: `string`	ss0 : `int list` fl0 : `bool` pr0 : `int * int` pty : `pretype` Returns: `string`
`print_prim_preterm ptm` Full Usage: `print_prim_preterm ptm` Parameters: ptm : `preterm` Returns: `string`	ptm : `preterm` Returns: `string`
`print_prim_preterm0 (fl0, pr0) ptm` Full Usage: `print_prim_preterm0 (fl0, pr0) ptm` Parameters: fl0 : `bool` pr0 : `int * int` ptm : `preterm` Returns: `string`	fl0 : `bool` pr0 : `int * int` ptm : `preterm` Returns: `string`
`print_qterm tm` Full Usage: `print_qterm tm` Parameters: tm : `term` Returns: `string`	tm : `term` Returns: `string`
`print_qtype ty` Full Usage: `print_qtype ty` Parameters: ty : `hol_type` Returns: `string`	ty : `hol_type` Returns: `string`
`print_sep x ()` Full Usage: `print_sep x ()` Parameters: x : `'a` () : `unit` Returns: `'a`	x : `'a` () : `unit` Returns: `'a`
`print_seplist print_fn print_sep_fn xs` Full Usage: `print_seplist print_fn print_sep_fn xs` Parameters: print_fn : `'a -> string` print_sep_fn : `unit -> string` xs : `'a list` Returns: `string`	print_fn : `'a -> string` print_sep_fn : `unit -> string` xs : `'a list` Returns: `string`
`print_sp_seplist sp print_fn print_sep_fn xs` Full Usage: `print_sp_seplist sp print_fn print_sep_fn xs` Parameters: sp : `bool` print_fn : `'a -> string` print_sep_fn : `unit -> string` xs : `'a list` Returns: `string`	sp : `bool` print_fn : `'a -> string` print_sep_fn : `unit -> string` xs : `'a list` Returns: `string`
`print_space ()` Full Usage: `print_space ()` Parameters: () : `unit` Returns: `string`	() : `unit` Returns: `string`
`print_space_if b` Full Usage: `print_space_if b` Parameters: b : `bool` Returns: `string`	b : `bool` Returns: `string`
`print_splist print_fn xs` Full Usage: `print_splist print_fn xs` Parameters: print_fn : `'a -> string` xs : `'a list` Returns: `string`	print_fn : `'a -> string` xs : `'a list` Returns: `string`
`print_term tm` Full Usage: `print_term tm` Parameters: tm : `term` Returns: `string`	tm : `term` Returns: `string`
`print_thm th` Full Usage: `print_thm th` Parameters: th : `thm` Returns: `string`	th : `thm` Returns: `string`
`print_type ty` Full Usage: `print_type ty` Parameters: ty : `hol_type` Returns: `string`	ty : `hol_type` Returns: `string`
`printing_preterm fl tm` Full Usage: `printing_preterm fl tm` Parameters: fl : `bool` tm : `term` Returns: `preterm`	fl : `bool` tm : `term` Returns: `preterm`
`term_name_form x` Full Usage: `term_name_form x` Parameters: x : `string` Returns: `int`	x : `string` Returns: `int`
`term_printable_name x` Full Usage: `term_printable_name x` Parameters: x : `string` Returns: `string`	x : `string` Returns: `string`
`thm_printing_preterms th` Full Usage: `thm_printing_preterms th` Parameters: th : `thm` Returns: `preterm list * preterm`	th : `thm` Returns: `preterm list * preterm`
`type_name_form x` Full Usage: `type_name_form x` Parameters: x : `string` Returns: `int`	x : `string` Returns: `int`
`type_printable_name x` Full Usage: `type_printable_name x` Parameters: x : `string` Returns: `string`	x : `string` Returns: `string`
`tyvar_printable_name x` Full Usage: `tyvar_printable_name x` Parameters: x : `string` Returns: `string`	x : `string` Returns: `string`
`var_printable_name x` Full Usage: `var_printable_name x` Parameters: x : `string` Returns: `string`	x : `string` Returns: `string`