package goblint-cil
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=796ad26120b5c6b939a57e8623088aef
sha512=01a58ac6d928afead21c8a97af5865715114cd0562234d1d4aef9e4ac5d91415d040a15927c52cb896dbb39a53e915627f498ebe2d026a548c3ff597682041b2
doc/goblint-cil/Pretty/index.html
Module Pretty
Utility functions for pretty-printing. The major features provided by this module are
- An
fprintf-style interface with support for user-defined printers - The printout is fit to a width by selecting some of the optional newlines
- Constructs for alignment and indentation
- Print ellipsis starting at a certain nesting depth
- Constructs for printing lists and arrays
Pretty-printing occurs in two stages:
- Construct a
Pretty.docobject that encodes all of the elements to be printed along with alignment specifiers and optional and mandatory newlines - Format the
Pretty.docto a certain width and emit it as a string, to an output stream or pass it to a user-defined function
The formatting algorithm is not optimal but it does a pretty good job while still operating in linear time. The original version was based on a pretty printer by Philip Wadler which turned out to not scale to large jobs.
API
The type of unformated documents. Elements of this type can be * constructed in two ways. Either with a number of constructor shown below, * or using the Pretty.dprintf function with a printf-like interface. * The Pretty.dprintf method is slightly slower so we do not use it for * large jobs such as the output routines for a compiler. But we use it for * small jobs such as logging and error messages.
Constructors for the doc type.
val nil : docConstructs an empty document
Concatenates two documents. This is an infix operator that associates to the left.
val text : string -> docA document that prints the given string
val num : int -> docA document that prints an integer in decimal form
val num64 : int64 -> docA document that prints a 64-bit int in decimal form
val real : float -> docA document that prints a real number
val chr : char -> docA document that prints a character. This is just like Pretty.text with a one-character string.
val line : docA document that consists of a mandatory newline. This is just like (text "\n"). The new line will be indented to the current indentation level, unless you use Pretty.leftflush right after this.
val leftflush : docUse after a Pretty.line to prevent the indentation. Whatever follows * next will be flushed left. Indentation resumes on the next line.
val break : docA document that consists of either a space or a line break. Also called an optional line break. Such a break will be taken only if necessary to fit the document in a given width. If the break is not taken a space is printed instead.
val align : docMark the current column as the current indentation level. Does not print anything. All taken line breaks will align to this column. The previous alignment level is saved on a stack.
val unalign : docReverts to the last saved indentation level.
val mark : docMark the beginning of a markup section. The width of a markup section is * considered 0 for the purpose of computing identation
val unmark : docThe end of a markup section
Syntactic sugar
Indents the document. Same as ((text " ") ++ align ++ doc ++ unalign), with the specified number of spaces.
Prints a document as markup. The marked document cannot contain line * breaks or alignment constructs.
Formats a sequence. sep is a separator, doit is a function that * converts an element to a document.
An alternative function for printing a list. The unit argument is there * to make this function more easily usable with the Pretty.dprintf * interface. The first argument is a separator, by default a comma.
sm: Yet another list printer. This one accepts the same kind of * printing function that Pretty.dprintf does, and itself works * in the dprintf context. Also accepts * a string as the separator since that's by far the most common.
Formats an array. A separator and a function that prints an array element. The default separator is a comma.
val d_int32 : int32 -> docPrint an int32
val f_int32 : unit -> int32 -> docval d_int64 : int64 -> docval f_int64 : unit -> int64 -> docmodule MakeMapPrinter (Map : sig ... end) : sig ... endFormat maps.
module MakeSetPrinter (Set : sig ... end) : sig ... endFormat sets.
This function provides an alternative method for constructing doc objects. The first argument for this function is a format string argument (of type ('a, unit, doc) format; if you insist on understanding what that means see the module Printf). The format string is like that for the printf function in C, except that it understands a few more formatting controls, all starting with the @ character.
See the gprintf function if you want to pipe the result of dprintf into some other functions.
The following special formatting characters are understood (these do not correspond to arguments of the function):
- @[ Inserts an
Pretty.align. Every format string must have matchingPretty.alignandPretty.unalign. - @] Inserts an
Pretty.unalign. - @! Inserts a
Pretty.line. Just like "\n" - @? Inserts a
Pretty.break. - @< Inserts a
Pretty.mark. - @> Inserts a
Pretty.unmark. - @^ Inserts a
Pretty.leftflushShould be used immediately after @! or "\n". - @@ : inserts a @ character
In addition to the usual printf % formatting characters the following two new characters are supported:
- %t Corresponds to an argument of type
unit -> doc. This argument is invoked to produce a document - %a Corresponds to two arguments. The first of type
unit -> 'a -> docand the second of type'a. (The extraunitis do to the peculiarities of the built-in support for format strings in Ocaml. It turns out that it is not a major problem.) Here is an example of how you use this:
dprintf "Name=%s, SSN=%7d, Children=\@\[%a\@\]\n"
pers.name pers.ssn (docList (chr ',' ++ break) text)
pers.childrenThe result of dprintf is a Pretty.doc. You can format the document and emit it using the functions Pretty.fprint and Pretty.sprint.
Like Pretty.dprintf but more general. It also takes a function that is * invoked on the constructed document but before any formatting is done. The * type of the format argument means that 'a is the type of the parameters of * this function, unit is the type of the first argument to %a and %t * formats, doc is the type of the intermediate result, and 'b is the type of * the result of gprintf.
val fprint : out_channel -> width:int -> doc -> unitFormat the document to the given width and emit it to the given channel
val sprint : width:int -> doc -> stringFormat the document to the given width and emit it as a string
val fprintf : out_channel -> ('a, unit, doc) format -> 'aLike Pretty.dprintf followed by Pretty.fprint
Like Pretty.fprintf applied to stdout
Like Pretty.fprintf applied to stderr
Invokes a thunk, with printDepth temporarily set to the specified value
The following variables can be used to control the operation of the printer
val printDepth : int refSpecifies the nesting depth of the align/unalign pairs at which everything is replaced with ellipsis
val printIndent : bool refIf false then does not indent
val fastMode : bool refIf set to true then optional breaks are taken only when the document has exceeded the given width. This means that the printout will looked more ragged but it will be faster
val flushOften : bool refIf true the it flushes after every print
val flattenBeforePrint : bool refWhether to rebalance doc before printing it to avoid stack-overflows
val countNewLines : int refKeep a running count of the taken newlines. You can read and write this * from the client code if you want