HaskHOL.Core.Printer

This module defines pretty printers for HOLTypes, HOLTerms and HOLThms. Note that the printers for terms and theorems are context dependent as they rely on the same theory extensions that the parsers utilize.

To make printing these objects easier within HOL computations, this module also defines the showHOL and printHOL methods which will automatically retrieve the current working theory to use for pretty printing. Because the pretty printer for HOLTypes is not context dependent it has definitions for both show and showHOL.

Note that, like the parser, there are a number of HOL term forms that the printer does not currently support. Again, these are mainly related to sets and patterns and will be added in when the HaskHOL system has libraries for them.

Pretty Printer Flags

data FlagRevInterface

Flag to indicate whether the interface should be reversed on printing.

Constructors

FlagRevInterface

Instances

Typeable FlagRevInterface

BenignFlag FlagRevInterface

data FlagPrintAllThm

Flag to indicate if the entirety of a theorem should be printed, as opposed to just the conclusion term.

Constructors

FlagPrintAllThm

Instances

Typeable FlagPrintAllThm

BenignFlag FlagPrintAllThm

Extensible Printer Operators

addUnspacedBinop :: String -> HOL Theory thry ()

Specifies a symbol to be recognized as an unspaced, binary operator by the printer. Applications involving these operators will be built with the <> combinator as opposed to <+>.

Note that technically this method should be considered benign, however, for simplicity of implementation it is defined using modifyExt and thus must be tagged a Theory computation.

addPrebrokenBinop :: String -> HOL Theory thry ()

Specifies a symbol to be recognized as a prebroken, binary operator by the printer. Applications involving these operators will have their right-hand side argument printed on the next line using the hang combinator.

Note that technically this method should be considered benign, however, for simplicity of implementation it is defined using modifyExt and thus must be tagged a Theory computation.

removeUnspacedBinop :: String -> HOL Theory thry ()

Specifies a symbol to stop being recognized as an unspaced, binary operator by the printer.

Note that technically this method should be considered benign, however, for simplicity of implementation it is defined using modifyExt and thus must be tagged a Theory computation.

removePrebrokenBinop :: String -> HOL Theory thry ()

Specifies a symbol to stop being recognized as an prebroken, binary operator by the printer.

Note that technically this method should be considered benign, however, for simplicity of implementation it is defined using modifyExt and thus must be tagged a Theory computation.

getUnspacedBinops :: HOLContext thry -> [String]

Returns the list of all symbols current recognized as unspaced, binary operators by the printer.

getPrebrokenBinops :: HOLContext thry -> [String]

Returns the list of all symbols current recognized as prebroken, binary operators by the printer.

Pretty Printers

ppType :: HOLType -> String

Pretty printer for HOLTypes.

ppTerm :: HOLContext thry -> HOLTerm -> String

Pretty printer for HOLTerms.

ppThm :: HOLContext thry -> HOLThm -> String

Pretty printer for HOLTheorems.

Printing in the HOL Monad

class ShowHOL a thry where

The ShowHOL class is functionally equivalent to show lifted to the HOL monad. It is used to retrieve the current working theory to be used with the context sensitive pretty printers for HOLTerms and HOLTypes.

Methods

showHOL :: a -> HOL cls thry String

A version of show lifted to the HOL monad for context sensitive pretty printers.

Instances

ShowHOL String thry

ShowHOL Assoc thry

ShowHOL HOLThm thry

ShowHOL HOLTerm thry

ShowHOL TypeOp thry

ShowHOL HOLType thry

ShowHOL a thry => ShowHOL [a] thry

(ShowHOL a thry, ShowHOL b thry) => ShowHOL (a, b) thry

(ShowHOL a thry, ShowHOL b thry, ShowHOL c thry) => ShowHOL (a, b, c) thry

(ShowHOL a thry, ShowHOL b thry, ShowHOL c thry, ShowHOL d thry) => ShowHOL (a, b, c, d) thry

printHOL :: ShowHOL a thry => a -> HOL cls thry ()

Prints a HOL object with a new line. A composition of putStrLnHOL and showHOL.