Portability | unknown |
---|---|

Stability | unstable |

Maintainer | ecaustin@ittc.ku.edu |

Safe Haskell | None |

This module defines pretty printers for `HOLType`

s, `HOLTerm`

s and `HOLThm`

s.
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 `HOLType`

s 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.

- data FlagRevInterface = FlagRevInterface
- data FlagPrintAllThm = FlagPrintAllThm
- addUnspacedBinop :: String -> HOL Theory thry ()
- addPrebrokenBinop :: String -> HOL Theory thry ()
- removeUnspacedBinop :: String -> HOL Theory thry ()
- removePrebrokenBinop :: String -> HOL Theory thry ()
- getUnspacedBinops :: HOLContext thry -> [String]
- getPrebrokenBinops :: HOLContext thry -> [String]
- ppType :: HOLType -> String
- ppTerm :: HOLContext thry -> HOLTerm -> String
- ppThm :: HOLContext thry -> HOLThm -> String
- class ShowHOL a thry where
- printHOL :: ShowHOL a thry => a -> HOL cls thry ()

# Pretty Printer Flags

data FlagRevInterface Source

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

data FlagPrintAllThm Source

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

# Extensible Printer Operators

addUnspacedBinop :: String -> HOL Theory thry ()Source

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 ()Source

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 ()Source

removePrebrokenBinop :: String -> HOL Theory thry ()Source

getUnspacedBinops :: HOLContext thry -> [String]Source

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

getPrebrokenBinops :: HOLContext thry -> [String]Source

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

# Pretty Printers

ppThm :: HOLContext thry -> HOLThm -> StringSource

Pretty printer for `HOLTheorem`

s.

# Printing in the `HOL`

Monad

class ShowHOL a thry whereSource

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 `HOLTerm`

s and `HOLType`

s.

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 |