1. Introduction

We describe the use of a pretty-printer for Acl2 events. The syntax produced is either standard ACL2 or conventional mathematical notation with formatted comments and doc-strings. Targets include LaTeX, HTML, Scribe and ASCII text. The printer is user extensible.

This document describes how to invoke the printer, how to control it via its numerous flags, details of formatting instructions in doc strings and comments, and how to modify its behavior via -syntax files.

For information on installation, see the README file in the parent directory of the one containing this file. The local README file in this directory also contains some useful information, but most of it is repeated in this document.

This text was extracted from the code and is, with the code and the Guide to IACL2 Synax, the primary documentation for this facility. Criticism of all sorts solicited.

2. Basic Use

There are 4 basic modes: ASCII, LaTeX, HTML and Scribe. You can build on top of these to customize the printing of functions in your syntax. All mode sensitivity should be contained in the file mode-syntax.lisp. Normally this file also loads a basic file called mode-init.lisp. The idea is that the -init files contain the minimal required information for INFIX to do its job with respect to a particular text formatter. The -syntax file contains the details of how you want the functions in your syntax to be printed.

In order to customize printing for a particular file of events we suggest the following approach.

First, assume we have a file, clock.lisp that we wish to format for LaTeX. HTML and ASCII modes would be extended in a similar fashion. It is assumed to be in proper syntactic form for acceptance by LD. That is to say, suppose that the file clock.lisp contains only legal event commands such as defun's and defthm's, Lisp style comments, and the few other sorts of miscellaneous instructions documented as legal instructions to LD.

1. Create clock-syntax.lisp. It should have a similar form to the following (which is specialized to LaTeX):

     (load-base "latex-syntax.lisp")
     ... 
      Your extensions and/or redefinitions belong here.  
      See in particular the documentation in section [OPERATOR]. 
   
   
      INFIX-SETTINGS provides some simple control over an assortment
      of formatting options.  See section [MODIFIED]. 
   
   
     (infix-settings :mode "clock" :extension "tex" ...)
   

2. Save clock-syntax.lisp, preferably in the same directory with clock.lisp.

3. Invoke doinifx. The simplest call (where ``%`` is a shell prompt would be just

     % doinfix clock.lisp
   

   which will result in the file clock.tex.

4. Run LaTeX.

     % latex clock
   

5. Indices in LaTeX require two passes.

     % makeindex clock
     % latex clock
   

ONE NOTE OF CAUTION: It is important that you know what text formatter you are targetting, since the bulk of your comments will be copied literally into the text input file. It is up to you to ensure that the interaction of your comments with the formatting convention of choice for the various comment types results in legal text formatting commands. That is, if you are in Scribe mode and a comment contains an email message with net addresss you should quote occurences of "@" as "@@". More importantly, if you decide that ";\" introduces a line to be formatted as raw LaTex (the default in "latex" mode), you need to ensure that any occurrence of "" or other LaTeX special characters on such a line results in a meaningful formatting command. To ensure the safeset transformations of event files to LaTeX you can use : COMMENT-FORMAT (= 'VERBATIM). This causes most comments to be formatted within verbatim environments, which are not so picky about special characters. Scribe is more forgiving of these problems because it only has the single special character, "@" that needs to be watched out for. (See section [MODIFIED].)

Coverage

The infix-file function should handle the entirety of the Acl2 term syntax checked by ld. It is our intention that any valid Acl2 file can be processed to a format specific file that will not break the target formatting program. We do not guarantee that the result will be pretty.

Motivation

We hope this notation will facilitate the communication of work with Acl2 to those who do not happily read Lisp notation. But we have no expectation that this notation will make it easier for the Acl2 user to formulate or to prove theorems.

WARNING: No Error Checking

In general, user-callable subroutines of Acl2 do extensive syntactic checking on their input and explicitly report syntactic errors. But this pretty printer does not do such syntactic checking. Rather, we assume the given input is known to be syntactically correct, namely as though checked by `LD'. Failure to provide input in correct syntactic form can result in nasty, brutish, and short Lisp errors.

Invoking the Printer

DOINFIX - the Shell Command

The simplest invocation of the printer is via the shell command, DOINFIX. The example below shows the help you get when typing doinfix with no options or files. None of these options are required, though it is likely that you will normally want to provide a mode using the ``-m'' option. The other flags have various defaults that depend on the mode selected.

% doinfix
Usage  : doinfix [ options ] files
Options: 
 -m [ ascii, latex, html, scribe, ... ] | Basic mode of output.
 -c [ c, text, verbatim, cl]            | Comment treatment.
 -prefix   | Override infix printing.
 -index    | Create index or cross references.
 -calls    | Index or cross reference calls.
 -hints    | Print hints.
 -nohints  | Suppress hints.
 -noguards | Suppress printing of guards (except as types).
 -nokeys   | Suppress printing of all keyword arguments.
 -nolocals | Suppress printing of toplevel locals.
 -noverify | Suppress printing verify-* events.
 -suppress | -nokeys -nohints -noguards -nolocals -noverify.
 -handsoff | Do not quote special chars in comments.
 -format!  | Format ! commands in comments.
 -acl2com  | Apply acl2 formatting to comments.
 -acl2doc  | Apply acl2 formatting to doc strings.

INFIX-FILE - the Lisp Function

Within IACL2 you can call infix-file directly. Below is such a call with keywords supplied with their defaults. All keywords are optional.

    (infix-file fl :print-case :downcase :mode ``ascii'' 
                   :chars-wide 77 :comment t)

[:print-case] - must be one of :downcase, :upcase, or :capitalize. DEFAULT: :downcase.

[:mode] - if not provided (thus defaulting to nil) we look for fl-syntax.lisp and load it if present. If not, we use the mode of the last successfull call to infix-file or query which of the known modes you want to use. Simplest is to create a trivial -syntax file in the same directory as the event files that just loads appropriate predefined -syntax file.

[:chars-wide] - approximate width in characters of the formatted output. Controls where infix inserts line breaks within expressions.

[:comment] - If t, then certain specially marked Acl2 expressions in comments are replaced with their conventional notation. See the documentation of the function nqfmt2fmt below for a description of the special syntax for this replacement process. Set by the mode or modified by the :format-!-in-comments keyword in (infix-settings ...)

3. Comment Handling

Based upon the comment style, see section , different types of comments may be formatted in a variety of ways, depending on the character immediately following the ``;'' or ``#|''. A comment may be turned into:

1. Running TEXT. The comment characters are eliminated and the text is copied to the output file.

2. A FORMAT environment. The comment chars (see definition following) are eliminated, line breaks and spaces are preserved, and the font is the default document font.

3. A VERBATIM environment. The comment chars may or may not be preserved, line breaks and spaces are preserved and the font is a fixed width font.

4. An EMPHASIS environment. Like format, but the font is italic.

5. A COMMENT environment. Typically wraps a comment form around text. The C version, for example, puts /* ... */ around the text. LaTeX precedes each line with a %, which means they won't show up in the .dvi file.

6. A SECTION heading. Should not extend across multiple lines.

Comment Transformations

• text - Prefers to produce running text. The default in LaTeX, scribe and html mode.
• verbatim - inserts most comments in an verbatim environment.
• cl - sensitive to Common Lisp style
• c - attempts to preserve the comment environment. The default in ascii mode. In LaTeX, Scribe or HTML, the comment text won't show up in the generated or displayed document. In ascii mode these will print as /* ... */ comments.

Description

BT begins running text, with no environment modifiers.
BF ... EF corresponds to begin(format) ... end(format)
BV ... EV corresponds to begin(verbatim) ... end(verbatim)
BE ... EE corresponds to begin(emphasis) ... end(emphasis)
BS ... ES corresponds to begin(section-name) ... end(section-name)
BC ... EC corresponds to begin(comment) ... end(comment)

Formatting WITHIN Comments and Documentation String

Comments may include markup commands of various sorts. See section [MARKUP]. There are 3 (at least) kinds of imbedded formatting commands that can occur in comments and doc strings. They are handled in distinct phases of processing.

1. ~ ACL2 doc string formatting commands.
2. ! Infix commands.
3. Text formatter commands (Scribe or LaTeX or HTML)

Note the difference between the backslash in comments and the backslash in doc strings. In doc strings, because they are read as strings, they need to be quoted (e.g. doubled).

To ensure that your text formatter (type 3) commands are preserved during processing steps 1 and 2, the simplest approach is to enclose the commands that you wish to preserve in the ~id[...] form or between ~bid[] .. ~eid[] pairs. See Bug description at [bugs].

Comments and doc strings are preprocessed to translate their ACL2 formatting commands to our target formatter. Note that the ACL2 doc formatter goes to great lengths to make sure weird characters in the target dialect are quoted. So if you want such things preserved, you need to use the ~id forms above. Because we now pass comment text through the ACL2 doc formatter, you will need to treat comments as you treat doc strings. You also need ;; to be careful of occurences of "~". If a "~" is not followed by an ACL2 formatting command, we will complain.

Commands

Although we may extend this set of replacement commands, we *promise* to give special meanings only to alphabetic characters after !. Thus we promise never to give !! a replacement effect. ~ forms currently include ~-, but that is the only non-alphabetic formatting instruction. In every case, for the replacement instruction, upper or lower case has the same effect.

Let fm be either an Acl2 event form, e.g., (defun foo (x) 3) or an Acl2 term, e.g., (plus x y) and sym be a symbol

!Tfm

Format inline (term or event). Results in conventional mathematical notation for fm, without line breaks or indentation. Mnemonic: T -- think Term.

!T*fm

Format (term or event). As above, but with paragraph breaks before and after and line breaks and indentation possible.

!Vsym

Sym is printed in typewriter font, with special characters quoted. Mnemonic: V -- think Verbatim.

!V[ .. ]

Verbatim (inline).

!V*[ .. ]

Verbatim. Honors line breaks and indentation.

!Isym

Italic.

!Bsym

Bold.

!Qsym

`fn'. where fn is a symbol, results in fn surrounded by single quotes, after formatting sensitive characters have been quoted, e.g., !qfoo results in `foo' in TeX. Useful for distinguishing function symbols from other words in a sentence, since function symbols appear in Roman. Mnemonic: Q -- think Quoted.

!section[ text ]

Format text as a section header.

!subsection[ text ]

Format test as a subsection header.

!nsym

Label for Xref

!xsym

Xref

!Lsym

Literal, ignoring special chars of formatter.

!L(..)

Literal, ignoring special chars of formatter.

!Eexpr

[E]val.
Begin HACK ALERT. The expr is evaled in Lisp. This allows you to do things like dynamically change the margin (*rightmost-char-number*) turn indexing on (SETQ *DO-NOT-INDEX* NIL) and off (SETQ *DO-NOT-INDEX* T), or even redefine a printer. End HACK ALERT

ACL2 Doc String Formatting Commands

~-[]    ---
~B[]    bold font
~BF[]   begin format, like verbatim, but if possible don't change font
~EF[]   end format
~BID[]  begin implementation dependent
~EID[]  end implementation dependent
~BQ[]   begin quotation
~EQ[]   end quotation
~BV[]   begin verbatim
~EV[]   end verbatim
~C[]    originally @code, but we don't want `' in info file
~EM[]   emphasis
~GIF[]  gif files, e.g., ~gif["foo.gif"  align=top]
~I[]    italics font
~ID[]   implementation dependent  
~NL[]   newline
~PAR[]  paragraph mark, of no significance for latex
~PL[]   used for parenthetical crossrefs
~SC[]   small caps
~ST[]   strong emphasis
~T[]    typewriter font


~IL[aaa rest]   invisible link, for true hypertext environments
~ILC[aaa rest]  invisible link, but use code if such links don't show
~L[aaa rest]    link at beginning of sentence
~TERMINAL[]  terminal only, ignore
~WARN[]      noop
~CLICK-HERE[]   Html specific.  See :DOC ~ss
~PCLICK-HERE[]  Html specific.  see :DOC ~ss )
~FLY[]   Html/ACL2 doc specific.  Flying Tour: see :DOC ~ss )
~WALK[]  Html/ACL2 doc specific.  Walking Tour: see :DOC ~ss )

Examples

(print-examples) creates a stand-alone, file named "infix-examples.tex" or "infix-examples.mss", which is a summary of the syntax we print in terms of the official Acl2 syntax. This file will also correctly report any user modifications made to the syntax by invocation of the make... functions described later. We hope that users will want to include this file in reports about Acl2 use to make clear what syntactic conventions they are using.

4. User extension of Syntax

If you were to define you own new mode from scratch, section [REQUIRED] identifies the functions that you must define. Much simpler is to base you formatting on the existing -init and -syntax files. For example, to extend LaTeX formatting, begin your mode-syntax.lisp file with <pre>(load-base ``latex-syntax.lisp''t)</pre>

Functions That Must Be Defined in mode-init.lisp.

() -> t :  function of no args, returning arbitrary type

            begin-tabbing                end-tabbing
            begin-normal-text            end-normal-text
            set-margin                   pop-margin
            get-margin                   pop-tab
            do-tab
            begin-flushright             end-flushright


(t) -> t :  function of one arbitray arg, returning arbitrary type

            flushright
            roman-font


(t) -> t :  function of one optional arg, returning arbitrary type

            set-tab


(character) -> t :  function of one character arg, returning arbitrary type

            handle-special-chars
            handle-special-chars-in-string

Settings That May Be Modified in mode-syntax.lisp

The things you can control with INFIX-SETTINGS are listed below. The first choice is the default, so if you are happy with the default you don't need to fool with the setting. See examples after the enumeration. These are all keyword arguments to INFIX-SETTINGS.

To see current settings use (SHOW-INFIX-SETTINGS). To change settings use INFIX-SETTINGS and supply the keyword arguments for settings you wish to modify. Defaults are in caps.

1. MODE: a string naming the syntax we have defined. It should correspont to the prefix of a -syntax filename. The default is constructed the the name of the events file. If no corresponding -syntax file is found, query the user. Known modes are ``latex'', ``html'', ``ascii'', and ``scribe''.

2. EXTENSION: type of output file ("mss", "tex", ...)

3. COMMENT-FORMAT: ['text, 'verbatim, 'cl, 'c] Chooses from one of the predefined conventions for determining how to format comments. This interacts with your use of native-mode formatting commands in comments in the events file.

   For your own control over this, use (DEFINE-COMMENT-FORMAT name format). See the description of comment handling in section [COMMENTS] for more information.

4. FORMAT-!-IN-COMMENTS: [T, nil] If true, run NQFMT2FMT over comments. See section [NQFMT2FMT].

5. ACL2-FORMAT-COMMENTS: [T, nil] If true, run the acl2 doc string formatting process over comments. See section [DOCSTRINGS].

6. ACL2-FORMAT-DOC-STRINGS: [T, nil] If true, run the acl2 doc string formatting process over doc strings. See section [DOCSTRINGS].

7. NO-INDEX: boolean [NIL, t]. If T, then no index is generated.

8. NO-INDEX-CALLS: boolean [NIL, T] or list. If you want all function calls indexed, NIL. If you do not want any function use indexed, T. If you want to exclude certain function calls, provide a list of function names to be ignored.

9. :hints: boolean [NIL, t]. If T, print hints.

10. :no-guards: boolean [NIL, t]. If T, suppress guard printing.

11. :no-keys: boolean [t, NIL]. Suppress keyword args.
    

12. :no-top-locals: boolean [t, NIL]. Suppress toplevel LOCALs.
    

13. :no-verify-guards: boolean [t, NIL]. Suppress VERIFY-GUARDS.
    

14. :suppress: boolean [ t, NIL]. Suppress above 5.
    

The minimal call on INFIX-SETTINGS requires a mode and extension.

(INFIX-SETTINGS :mode "scribe" :extension "mss")

The maximal call, setting everything explicitly. The following shows infix-settings with all of the default settings as arguments. The comments indicate required types of values.

(INFIX-SETTINGS
 :MODE                    "scribe" ; string ["scribe","latex","html"...]
 :EXTENSION               "mss"    ; string ["mss","tex","html"]
 :COMMENT-FORMAT          'TEXT    ; ['TEXT,'VERBATIM,'CL,'C...]
 :FORMAT-!-IN-COMMENTS    NIL      ; [t,nil]
 :ACL2-FORMAT-COMMENTS    T        ; [t,nil]
 :ACL2-FORMAT-DOC-STRINGS T        ; [t,nil]
 :NO-INDEX                NIL      ; [t,nil]
 :NO-INDEX-CALLS          NIL      ; [t,nil,l]
 :NO-GUARDS               NIL      ; [t,NIL]
 :HINTS                   NIL      ; [t,NIL] )

5. Implementation Notes

The 4 `tables' that govern the printing are the variables:

1. *atom-alist*, which governs printing of variables, numbers, T, F, and NIL.

2. *fn-alist*, which governs the printing of any term that starts with a function symbol, including LET, COND, CASE, LIST, LIST*, and FOR.

3. *event-printer-alist*, which governs the printing of events.

4. *special-quoted-forms-alist*, which governs the special printing of selected quoted symbols.

Each table is an alist. Each member of any of these alists is a list (symbol fn), where symbol is the car of a form (or in the case of a non-consp form, the form itself) which is about to be printed. fn is a Common Lisp function of one argument which is called on the form in question to do the printing. For each alist, there is a default function that is returned if a symbol is not explicitly represented. One such default is the function default-fn-printer, which is a good function to study before contemplating serious modifications to this file.

Although adding new members to these alists, and defining corresponding special purpose functions, is certainly sensible and easy, there are several points to be made.

1. It is unlikely that there will be any call to edit `*atom-alist*' until and unless TRANSLATE is changed.

2. *fn-alist* can be most easily modified by the use of the macros make-infix-op, make-unary-prefix-op, make-unary-suffix-op, make-infix-multiple-op, and make-prefix-multiple-op. See the very end of the file for many examples of how syntax operators can be easily established.

We really do assume throughout this code that the input file has passed through LD, e.g., we assume that the last test in a `cond' is on T, the last test in a case is an `otherwise', and that the third argument to `defthm' is something that translate can accept.

*ATOM-ALIST*

*atom-alist* is one of the three tables off of which this printer is driven. It determines how a variable symbol is printed. It is unlikely that anyone would want to change this unless translate changes because t, f, and nil are the only symbols that translate treats specially as constants instead of as variable symbols.

We would like to put this at the beginning of the file but cannot, so we put a special declaration up there. This is defined ni font-printers.

*FN-ALIST*

*fn-alist* is considerably extended via calls to make-... at the end of this file. This initial value given here picks up the very few entries for which we have totally ad hoc handling. Although LIST and LIST* are essentially macros, we handle them by the default-fn-printer, since they evaluate all their arguments. We could have handled IF this default way, too. It was essential that we handle QUOTE, COND, CASE, LET, and FOR specially because they do not evaluate all their arguments but `parse' them to some extent.

We would like to put this at the top but have to put it after the functions are defined.

Standard Output Used

Printing. We do *all* of our printing of formulas to *standard-output*, so we call princ and write-char on just one argument, the thing to be printed.

Tabbing

Infix-File generates text that uses the Latex `tabbing' or Scribe `format' environment, setting a tab for each new level of indentation. We find this a convenient sublanguage to target.

It appears based upon various experiment that perhaps Latex cannot handle tabs more than about 14 deep, or so.

The parameter, *latex-indent-number-limit*, could perhaps be increased if one had a Latex wherein this limit has been raised. However, it is a relatively rare function that needs terms that are more than 13 function calls deep. When infix-file hits this limit in Latex mode, it falls back upon the standard Acl2 pretty-printer, and puts the result in a verbatim environment.

All of the following should be defined in the text-formatting init file, e.g., latex-init.lisp or scribe-init.lisp.

Parentheses and Precedence

That being said, an objective in printing a formula is clarity. We know of very, very few cases (e.g., + and *) where precedence is something on which people agree.

We drop the outermost parentheses of a formula when the formula is an argument of a function that is being printed in the usual f(x,y) notation, with subterms separated by parentheses and commas.

DEBUGGING

Other Formatters

There are some functions that we use that take advantage of similarities between LaTeX and Scribe. They are marked with `WARNING: Latex/Scribe dependency'. If you want to generate input to some other formatter you may want to take a look at these. Not guaranteed to be complete. In order to built a -init.lisp file for some other formatter make sure you look at section [REQUIRED].

6. NQFMT2FMT

(NQFMT2FMT "foo") copies the file foo.lisp to the file "foo.tex" or "foo.mss", but along the way, Acl2 terms preceded by an exclamation mark and certain alphabetic characters are replaced with the formatting commands for the conventional notation this printer generates. For example, when in latex mode, if nqfmt2fmt encounters !t(gcd x (difference y x)) in a file, it will replace it with {\rm{gcd}}\({\it{x\/}}, {\it{y\/}} $-$ {\it{x\/}}). We find the former much easier to read in a file. nqfmt2fmt thus permits one to keep Acl2 forms in files to be read and edited by humans, e.g., in comments in Acl2 event files. Ordinary uses of !, e.g., uses of it followed by white space or punctuation characters, are, of course, unaltered.

nqfmt2fmt (fl \&key
              ((:print-case *print-case*) :downcase)
              ((:left-margin *left-margin*) 5)
               (just-remove-! nil))

Copies the file fl.nqxxx file to the file fl.xxx file and honors ! and ~ formatting commands, replacing Acl2 forms preceded by a formatting instructions with the results described below. If an exclamation mark or ~ is not followed by one of these special characters, then the following form is preserved unchanged, and the mark and the character following it are preserved, too.

Although we may extend this set of replacement commands, we *promise* to give special meanings only to alphabetic characters after !. Thus we promise never to give !! a replacement effect. ~ forms currently include ~-, but that is the only non-alphabetic formatting instruction.

In every case, for the replacement instruction, upper or lower case has the same effect.

One can certainly use nqfmt2fmt on the result of running infix-file, but one must do so deliberately by first running infix-file, then renaming the resulting file, say foo.tex, to be foo.nqtex, and then running nqfmt2fmt. More convenient is to run infix-file with the :comment keyword parameter set to t, which causes infix-file first to generate a .nqtex file and second to run nqfmt2fmt on that file.

If the :just-remove-! keyword is t, then a file named root.stripped is created, with all of our special ! commands options removed.

Implementation note. In all the cases we treat explicitly, except for !L, the characters after ! are read with the Lisp function READ-PRESERVING-WHITESPACE, which is just the same as READ except that it doesn't gratuitously consume whitespace at the end of a READ.

Warning: Because we use a relative of READ to obtain the forms immediately after the two character exclamation commands, the user must beware that if a form to be read extends for more than a line, and if a semicolon (comment character) is encountered on the next line, say at the beginning, READ will skip that line from the semicolon on, which may not be what the user intends. Thus it can be safer to use the #| ... |# construct for comments containing !, especially if one is in the habit of using the Emacs command M-x fill paragraph to rearrange paragraphs that begin with the comment delimiter semicolon.

Printing An Example Document

Illustrates the current syntax via a brief sample document.

(print-examples mode)

7. User Modifiable Table Setup

make-infix-op, make-unary-prefix-op, and make-unary-suffix-op take an optional argument, *neg-str*, which indicates how to print an the negation of an application of the function symbol in question.

In TeX or Latex, one can do astonishingly clever things. But the strings that we have in mind should do nothing clever involving motion, they should only result in characters being placed at the current location. While being printed, the strings will be passed no arguments or information about the context in which printing is to take place. Typically, these strings should be nothing more than instructions to print a single symbol. The strings are processed in `math mode', and in fact, they are automatically embedded in $...$.

None of the operators below are built into this printer anywhere else except by the code below. The meaning of `not', defined above, is wired in because it gives the meaning to the optional *neg-str* arguments.

Constant-Ops

Sometimes you want to print a function as a constant, particularly if it is one. (make-constant-op op str) causes (op ..) to print as str.

Infix-Ops

infix-ops (infix operators) should be function symbols of two or more arguments for which it is desired that one symbol come out between every adjacent pair of arguments. E.g., invoking (make-infix-op plus "+") causes the term (plus a b c d) to be printed as (a + b + c + d). Invoking (make-infix-op equal "=" "\neq") causes the term (equal x y) to be printed as (x = y) and it also causes the term (not (equal x y)) to be printed as (x y).

Thus, for example, if one introduces a new function, say join, and wants to print terms of the form (join x y) as (x `Triangle' y) in LaTeX, then simply add the following to your -syntax file.

  (make-infix-op join "\\bigtriangledown")

Note that throughout the following examples, we have used two backslashes to get one because, in Common Lisp, backslash is a character for quoting other characters.

Examples of make-infix-op are contained in latex-syntax.lisp. Look for INFIX OPERATORS.

Unary-Prefix-Ops, Unary-Suffix-Ops, and Unary-Abs-Ops

Use make-unary-prefix-op and make-unary-suffix-op only for function symbols of one argument. The string str will be printed before or after the argument.

  (make-unary-suffix-op numberp "\\;in \\;rm\\;bf{N}" "\\;not\\;in \\;rm\\;bf{N}")

To create syntax like that for absolute value, use (make-unary-absolute-op lhs-str rhs-str), where lhs-str and rhs-str are the strings to print on the left and right of the argument. (make-unary-abs-op foo str1 str2) makes (foo x) print as (str1 x str2). E.g.

  (make-unary-abs-op mod "\\{}floor\\;" "\\;\\{}floor")

Defining New Comment Format Conventions.

The format argument has two parts, one ``;'' comments and the other for #| ... |# comments. The assignment below corresponds to Boyer's initial setting.

 (define-comment-format 'boyer
   '((#\; (("\\"   nil   text)) nil verbatim #\;)
     (#\# (("\\"   nil   text))   t verbatim )))

  type      ::= (label (substring*) spaces-p format [char])
  substring ::= (string spaces-p format [char])

LABEL indicates which of the two types of comments we are looking at, either those that start with a ``;'' or those that start with ``#|''. We determine what to do in the various cases (which amounts to choosing SPACES-P, FORMAT, and CHAR) based on whether the comment type indicated by LABEL is followed by any of the strings that begin SUBSTRINGS or not. If it matches, we use the components of the matching substring, otherwise we use the default for the comment type, i.e. the elements of the type list.

If SPACES-P, consume one space if there is one.
Begin formatting according to FORMAT.
Insert CHAR.

So, for the example above, the first sublist, whose car is the ";" character, describes how to format comments that begin with a ";" followed by specific strings. There are two possibilites. If the ";" is not followed by a back-slash (\), we don't look for a space, we ensure we are in a verbatim environment, and print a ";". If ";" is followed by a back-slash, we don't look for a space and ensure that we are in a text environment.

Thus, if we encounter a comment beginning ";\", the comment should be inserted as top level text with no special formatting. The ";\" will not show up in the output.

8. Major Modification History

1996-97

• Added variables to suppress hint and guard printing. Guards that contribute to type information should be unaffected.

• Added ASCII and HTML modes.

  ASCII mode output should generally be parsable by the infix printer except that the printer is designed to print arbitrary ACL2 and the parser only accepts a subset.

1995

• Added ACL2 ~ formatting conventions in doc strings and comments. DEFAULT SETTING OF VARIABLES BELOW IGNORES THEM:
  *acl2-format-comments* => nil, *acl2-format-doc-strings* => nil.
  TO SET:
  *acl2-format-comments* => t, *acl2-format-doc-strings* => t.

  We handle doc strings by calling an ACL2 function that takes a doc string and 2 tables and returns a doc string, with the ACL2 formatting done.

  In order to handle arbitrary formatting within doc strings `~id[x]` will eventually map to `x`. Thus, in scribe mode, ~id[@section](Testing) will come out as @section(Testing). Whereas @section(Testing) would come out as @@section(Testing)

Bugs

• In comments !p(implies a b) produces different results from !p(IMPLIES a b) Case is honored when reading comments. !p may need to adjust case. We could just store things redundantly under `IMPLIES' and `implies', but then we would fail on `Implies'

• "~ID[\\it foo]" does not map to "\\it foo". The braces get quoted. Matt Kaufmann may fix this. Until then, the user can either not use any special formatting other that that provided by ! and ~, or can turn off ACL2 formatting, by setting *acl2-format-doc-strings* and *acl2-format-comments* to nil. (See keyword args to INFIX-FILE and INFIX-SETTINGS.) With this turned off you can still use ! and whatever native text formatting conventions you wish.

• "!cfoo" when processed by nqftm2fmt will result in an attempt to eval foo. This may break, if the user is not taking advantage of this !c `feature'.