Applicative "printer" for building strings.
We implement a printer as a stobj name ps, and use it as the
back-end for formatting our source code and for other output tasks. Our
printer is applicative and the act of printing only accumulates characters or
strings into a list. These printed elements are kept in reverse order, which
makes the sequential printing of small chunks of text reasonably
- The printer state stobj.
- Primitive routines for printing objects.
- Printing routines for displaying Verilog constructs.
- How to use ps to build strings in a local context.
- Higher-level routines for printing objects with a fmt- or
- How to access the characters that have been printed.
- A list of strings/characters to print in reverse order.
- Routines for encoding various ACL2 structures into JSON format.