Infix printing for
ACL2 Version 1.9


Copyright (C) 1996-97 Computational Logic, Inc. (CLI). All rights reserved.
This software is subject to the same license agreement as ACL2
See your ACL2 distribution.

Comments, bugs, suggestions to: 

  Michael K. Smith
  Computational Logic Inc.
  1717 W 6th, Suite 290
  Austin, TX 78703-4776

  Fax  : (512) 322-0656
  Email: mksmith@cli.com

  Date : May  4 97 MKS

CONTENTS

  1. USE
  2. DOCUMENTATION
  3. PROBLEMS
  4. INSTALLATION

USE

Doinfix

Doinfix will pretty print acl2 source files in infix format. It will print ascii, LaTeX, html, and Scribe versions based on a mode setting that you supply. The ascii and LaTeX modes have been extensively tested for this release.

The simplest way to run the program is to: 

 doinfix -m latex file.lisp &
This will create file.tex, a translation of file.lisp suitable for processing by LaTeX. There are numerous options. If you type 'doinfix' by itself you will see them: 
mks% doinfix

Usage  : infix [ options ] file
Options: 
 -m [ ASCII, latex, html, scribe, ... ]  | Basic mode of output.
 -c [ text, verbatim, C, cl]            | Comment treatment.
 -index    | Create index or cross references.
 -calls    | Index or cross reference calls.
 -hints    | Print hints.
 -nohints  | Suppress hints.
 -noguards | Suppress guards (except as types).
 -nokeys   | Suppress keyword arguments.
 -nolocals | Suppress top level locals.
 -noverify | Suppress verify-guards.
 -suppress | -nokeys -nohints -noguards -nolocals -noverify.

Comment formatting.

The default depends on mode. Comments may be treated in a variety of ways. The table below lists formats for major comment forms.

Mode
Commenttextverbatimccl
; text verbatim comment emphasis
;; text verbatim comment format
;;; verbatim verbatim comment text
#| text verbatim comment text
;! emphasis verbatim comment emphasis
;- format verbatim comment format
;+ verbatim verbatim comment verbatim
#|- format verbatim comment format


(infix-file ...)

The other approach is as follows:

Connect to the directory containing the ACL2 .lisp files that you want to convert to infix.

Start up IACL2 (iacl2) and do: 

 :q;                          ;; to exit the ACL2 loop
The simplest calls are then 
   (infix-ascii  "file.lisp") ;; produces file.x
   (infix-latex  "file.lisp") ;; produces file.tex
   (infix-html   "file.lisp") ;; produces file.html
   (infix-scribe "file.lisp") ;; produces file.mss
   (infix "file.lisp")        ;; if file-theory.lisp is present
The underlying call is: 
  (infix-file file :mode mode)
where file is the name of a .lisp file and, in the simplest case, mode is one of "ascii", "html", "scribe" or "latex". For example: 
  (infix-file "clock" :mode "latex") 
  (infix-file "clock.lisp" :mode "latex") works too.
See the documentation in infix.lisp for information on user parameterization and extension of modes. In particular, see the section `SETTINGS THAT MAY BE MODIFIED IN MODE-SYNTAX.LISP'.

Just as a note, if you have an events file, say clock.lisp, and create a corresponding syntax file, clock-syntax.lisp, then you can use the even simpler invocation: 

  (infix "clock")
The simplest such a clock-syntax file might just consist of: 
  (in-package "acl2")
  (load-base "latex-syntax" t)
By default, infix expects the -syntax files to be in *infix-directory* or the user's current directory. LOAD-BASE checks there. And they in turn expect their corresponding -init files to be there also.

Other -syntax files may reside in *infix-directory* or in the `current directory' (defined to be the directory returned by (probe-file "./") at execution time). The current directory is checked first.

DOCUMENTATION

See the documentation in infix.lisp for information on user parameterization, formatting within comments, and extension of modes.

PROBLEMS

  1. `!' formatting directives in comments.

    If you depend on this capability (by using INFIX-FILE with `:comment t') then you need to make sure that all uses of ! in your file are acceptable. In general, ! as punctuation will be fine, but things like `{!foo}*' will cause problems, i.e. you may experience unpredictable formatting results, or worse, a break into lisp. In this case, you will need to either correct the problem or run INFIX-FILE with `!' processing suppressed (which is the default). You can guarantee it by: 

     (infix-file "foo" :comment nil)
  2. There is also a problem with deeply indented forms in LaTeX. The depth of indentation permitted depends on your LaTeX installation. On ours, it is 13, which is wired into the file latex-init.lisp, in the variable *latex-indent-number-limit*. If this limit is exceeded the form is printed as lisp, rather than in infix, and we issue a message:

     Warning: Tab limit reached in event local
 Hand massaging required.
  3. There are some tricky interactions between formatting !commands, ACL2 doc string commands, and formatter specific commands.

INSTALLATION

The best way to build the system is as follows:
  1. First build ACL2
  2. Download the iacl2.tar file into the directory where iacl2 will reside.
  3. Untar by doing "tar xpf iacl2.tar".
  4. We depend on the SLOOP package which is built into GCL. If your lisp includes a compatible version (which you can probably only determine by examining all of the uses in this code) you may need to modify the form in infix.lisp, depending on the package and name of the looping macro. 
     (eval-when (load eval compile)
  (defmacro sloop (&rest l) `(sloop::sloop ,@l)))
  5. If the shell command, "acl2", will run ACL2 then type "make". Otherwise you will need to edit the Makefile to indicate where the ACL2 saved image resides.

    It is important to do this make in the directory in which infix resides. For one thing, that's where the makefile is and for another it causes the variable, *infix-directory*, to get set properly.

  6. To perform a simple test of the system and get some idea of what the results look like do: 
     make example
    This will produce infix-examples.x (ASCII) and infix-examples.dvi files (from LaTeX) print them.

  7. You might need to make the script doinfix executable (by `chmod +x doinfix'). You can then infix your files at the shell prompt by 
     doinfix -m latex file.lisp &