Printer
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
efficient.
Subtopics
- Ps
- The printer state stobj.
- Basic-printing
- Primitive routines for printing objects.
- Verilog-printing
- Printing routines for displaying Verilog constructs.
- Printing-locally
- How to use ps to build strings in a local context.
- Formatted-printing
- Higher-level routines for printing objects with a fmt- or
cw-like feel.
- Accessing-printed-output
- How to access the characters that have been printed.
- Vl-printedlist
- A list of strings/characters to print in reverse order.
- Json-printing
- Routines for encoding various ACL2 structures into JSON format.
