The first is intended to make initial experiments with ACL2 somewhat simpler for those unfamiliar with or opposed to Lisp prefix syntax. It is not an inteface for experts, as some of the more advanced aspects of ACL2 are not supported by the infix parser.
The second aids the user in presenting results in nicely formatted conventional syntax. For example, in LaTex mode comments are formatted as running text, events are indexed and substitutions are made of Tex mathematical symbols for various functions. In HTML mode, cross references are created between function usage and definition.
Other documentation is available:
For example:
type ilist = integer *;
function foo (x : integer, y : cons) : ilist { cons(x,y) };
The "type" ilist recognizes lists of integers.
Because ":>" is an infix version of cons, foo could be stated:
function foo (x : integer, y : cons) : ilist { x :> y };
The type and function above are equivalent to the prefix syntax:
(deflist ilist (l) (declare (xargs :verify-guards t)) integerp) (defun foo (x y) (declare (type integer x) (type cons y)) (cons x y)) (defthm foo-type (imples (and (integerp x) (consp y)) (ilist (foo x y))))
There are two approaches.
1. Run the doinfix command (./printer/doinfix). The command with no arguments will provide brief documentation of options.
2. Start up IACL2 (iacl2) and do:
:q ;; to exit the ACL2 loopThe simplest calls are then
(infix-text "file.lisp") ;; produces file.x (infix-latex "file.lisp") ;; produces file.tex (infix-scribe "file.lisp") ;; produces file.mss (infix "file.lisp") ;; if file-syntax.lisp is present
See printer/README.
% iacl2 ;; :out is for output, :in for input, t for both. ACL2 !>(assign infixp :out | t | nil) ;; Optionally ACL2 !>(assign ld-pre-eval-print t) ;; This prints before evaluation, which can be handy if you are ;; in infixp = :out mode, in which case you can enter in ;; standare acl2 and see what your input would be like in infix.
Options :
-m [ ascii, latex, html, scribe, ... ]
Basic mode of output. Default = ascii. Will produce an output
file with the appropriate suffix (.x, .tex, .html, .mss).
-c [ text, verbatim, c, cl]
Comment formatting. Default depends on mode.
Comments may be treated in a variety of ways
The table below lists formats for major comment forms
text verbatim c cl
------------------------------------
; text verbatim comment emphasis
;; text verbatim comment format
;;; verbatim verbatim comment text
#| text verbatim comment text
-prefix Overrides 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 args.
-nolocals Suppress printing of toplevel locals
-noverify Suppress printing verify-guards events.
-format! Format ! commands in comments.
% iacl2 ... ACL2 !>:q ... ;; Then do one of the following. ACL2>(infix-ascii "file.lisp") ;; produces file.x ACL2>(infix-latex "file.lisp") ;; produces file.tex ACL2>(infix-hmtl "file.lisp") ;; produces file.html ACL2>(infix-scribe "file.lisp") ;; produces file.mss ACL2>(infix "file.lisp") ;; if file-syntax.lisp is present
Create a directory in which you wish to build the system and move the tar file there.
Untar the distribution by executing
tar xpf iacl2.tar
This will create subdirectories named `printer', `parser', and `books', which contains the sources and examples, as well as a top level Makefile, README, and other misc. files.
If the shell command, "acl2", will run ACL2 then proceed. Otherwise you will need to edit the Makefile to indicate where the ACL2 saved image resides.
To build the system, cd to the installation directory and execute
makewhich will convert references recursively within the other makefiles, build and install everything and make a core image called iacl2. This does not put iacl2 or doinfix into any sort of local bin directory, that's your job.
make tests