ACL2 Infix Version 1.9
Miscellaneous Notes

 books
 convert
 convert.perl
 infix
 makefile

 BINDIR = /home/mksmith/bin           : where you want to store the
                                        scripts that start things up
 INCDIR = /usr/cli/projects/cacl2     : typically, this directory.
 VERSION = /import                    : this can be an empty string or
                                        the name of the current dir,
					if INCDIR is set to its parent.

axiom% runacl2 ...

----------------------------------------------------------------------
Return-Path: 
From: moore (J Strother Moore)
Date: Wed, 5 Jun 96 22:27:18 CDT
To: MkSmith
Subject: /slocal/src/acl2/v1-9/infix/acl2-sources/INFIX-README

Ok, I think it works well enough for you to experiment with.
The INFIX-README file has been changed slightly but is basically
what I showed you.

Here is a session.  I have put some comments in **** boxes.

duck% /slocal/src/acl2/v1-9/infix/acl2-sources/saved_acl2
GCL (GNU Common Lisp)  Version(2.2) Tue Dec 12 17:43:47 CST 1995
Licensed under GNU Public Library License
Contains Enhancements by W. Schelter

 ACL2 Version 1.9 built June 5, 1996  20:41:55.
 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*
                      NIL).
 See :doc note9 for recent changes.

 NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
 look under the ACL2 source directory in interface/emacs/README.doc; 
 and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
 command loop.   Look in the ACL2 documentation under PROOF-TREE.

ACL2 Version 1.9.  Level 1.  Cbd "/home3/moore/".
Type :help for help.

*******************************************************************************
* Infix syntax can be turned on and off.  Initially it is on.                 *
*******************************************************************************

ACL2 !>$ (car '(a b c))
A
ACL2 !>$ (assign infixp nil)
 NIL
ACL2 !>(car '(a b c))
A
ACL2 !>(assign infixp t)
 T
*******************************************************************************
* Here is a definition.  Note that the output prints in lower case with a     *
* dollar sign, showing that it is being printed by my stubbed out infix       *
* printer.  Some stuff, like the runes, are printed as objects not terms.     *
*******************************************************************************

ACL2 !>$ (defun app (x y) (if (consp x) (cons (car x)(app (cdr x) y)) y))

The admission of APP is trivial, using the relation E0-ORD-< (which
is known to be well-founded on the domain recognized by E0-ORDINALP)
and the measure $ (acl2-count x).  We observe that the type of APP
is described by the theorem $ (or (consp (app x y)) (equal (app x y) y)).
We used primitive type reasoning.

Summary
Form:  ( DEFUN APP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.43 seconds (prove: 0.00, print: 0.03, other: 0.40)
 APP

*******************************************************************************
* Another definition.                                                         *
*******************************************************************************

ACL2 !>$ (defun rev (x) (if (consp x) (app (rev (cdr x))(list (car x))) nil))

The admission of REV is trivial, using the relation E0-ORD-< (which
is known to be well-founded on the domain recognized by E0-ORDINALP)
and the measure $ (acl2-count x).  We observe that the type of REV
is described by the theorem $ (or (consp (rev x)) (equal (rev x) nil)).
We used the :type-prescription rule APP and primitive type reasoning.

Summary
Form:  ( DEFUN REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION APP))
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.02, other: 0.02)
 REV

*******************************************************************************
* Ok, now a theorem.  Note the lower case terms printed.  You will note two   *
* problems immediately.  One is that some terms are printed as objects, e.g., *
* (:P X) in the induction scheme message should be $ (:p x) but I apparently  *
* forgot to untranslate it in the original code and so I missed it when I     *
* went through to find the places I print terms.  Any place you see an upper  *
* case term printed without a $ you know I missed an occurrence.  There are   *
* several and I'll have to handle them when I get back.                       *
*                                                                             *
* The other problem is that the period at the end of each formula is on a new *
* line.  That's because the spec of my stubbed out infix prettyprinter is to  *
* end with a newline but I sometimes then print a period.  You might want to  *
* allow the prettyprinter to be passed a punctuation char (or nil) which it   *
* prints at the end, before its newline.  But I'll have to add the appropriate*
* stuff to my code to exploit your new feature.  In the meantime, you'll have *
* to just live with these silly punctuation marks.  Sorry I didn't think of   *
* that earlier.                                                               *
*                                                                             *
* By and large though, most terms are being printed where I want.             *
*******************************************************************************

ACL2 !>$ (thm (implies (true-listp x) (equal (rev (rev x)) x)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (REV X).  If we let
 (:P X) denote *1 above then the induction scheme we'll use is
$ (and (implies (not (consp x)) (:p x))
       (implies (and (consp x) (:p (cdr x))) (:p x)))
.
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP).  When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.

Subgoal *1/3
$ (implies (and (not (consp x)) (true-listp x))
           (equal (rev (rev x)) x))
.

But simplification reduces this to T, using the :executable-counterparts
of REV, EQUAL and CONSP, primitive type reasoning and the :definition
TRUE-LISTP.

Subgoal *1/2
$ (implies (and (consp x) (equal (rev (rev (cdr x))) (cdr x))
                (true-listp x))
           (equal (rev (rev x)) x))
.

This simplifies, using the :definitions TRUE-LISTP and REV, to

Subgoal *1/2'
$ (implies (and (consp x) (equal (rev (rev (cdr x))) (cdr x))
                (true-listp (cdr x)))
           (equal (rev (app (rev (cdr x)) (list (car x)))) x))
.

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing $ (car x) to
X1 and $ (cdr x) to X2.  This produces the following goal.

Subgoal *1/2''
$ (implies (and (consp (cons x1 x2)) (equal (rev (rev x2)) x2)
                (true-listp x2))
           (equal (rev (app (rev x2) (list x1))) (cons x1 x2)))
.

This simplifies, using the :type-prescription rule REV and primitive
type reasoning, to

Subgoal *1/2'''
$ (implies (and (equal (rev (rev x2)) x2) (true-listp x2))
           (equal (rev (app (rev x2) (list x1))) (cons x1 x2)))
.

We now use the first hypothesis by cross-fertilizing $ (rev (rev x2))
for $ x2 and throwing away the hypothesis.  This produces

Subgoal *1/2'4'
$ (implies (true-listp x2)
           (equal (rev (app (rev x2) (list x1)))
                  (cons x1 (rev (rev x2)))))
.

We generalize this conjecture, replacing $ (rev x2) by RV.  This produces

Subgoal *1/2'5'
$ (implies (true-listp x2)
           (equal (rev (app rv (list x1))) (cons x1 (rev rv))))
.

We suspect that the term $ (true-listp x2) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1/2'6'
$ (equal (rev (app rv (list x1))) (cons x1 (rev rv)))
.

Name the formula above *1.1.

Subgoal *1/1
$ (implies (and (consp x) (not (true-listp (cdr x))) (true-listp x))
           (equal (rev (rev x)) x))
.

But we reduce the conjecture to T, by primitive type reasoning.

So we now return to *1.1, which is

(EQUAL (REV (APP RV (LIST X1)))
       (CONS X1 (REV RV))).

Perhaps we can prove *1.1 by induction.  Two induction schemes are
suggested by this conjecture.  Subsumption reduces that number to one.

We will induct according to a scheme suggested by (REV RV).  If we
let  (:P RV X1) denote *1.1 above then the induction scheme we'll use
is
$ (and (implies (not (consp rv)) (:p rv x1))
       (implies (and (consp rv) (:p (cdr rv) x1)) (:p rv x1)))
.
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT RV) is decreasing according to the
relation E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP).  When applied to the goal at hand the above
induction scheme produces the following two nontautological subgoals.

Subgoal *1.1/2
$ (implies (not (consp rv))
           (equal (rev (app rv (list x1))) (cons x1 (rev rv))))
.

But simplification reduces this to T, using the :definitions REV and
APP, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :executable-counterparts of CONSP and REV.

Subgoal *1.1/1
$ (implies (and (consp rv)
                (equal (rev (app (cdr rv) (list x1)))
                       (cons x1 (rev (cdr rv)))))
           (equal (rev (app rv (list x1))) (cons x1 (rev rv))))
.

But simplification reduces this to T, using the :definitions REV and
APP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-
CONS.

That completes the proofs of *1.1 and *1.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION IMPLIES)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:DEFINITION TRUE-LISTP)
        (:ELIM CAR-CDR-ELIM)
        (:TYPE-PRESCRIPTION REV)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART REV)
        (:DEFINITION REV)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:DEFINITION APP))
Warnings:  None
Time:  0.77 seconds (prove: 0.52, print: 0.10, other: 0.15)

Proof succeeded.
ACL2 !>

----------------------------------------------------------------------
PLUG IN FUNCTIONS

The four functions are

(defun parse-infix (file eof) ...)
(defun ppr-infix (x width rpc col file eviscp) ...)
(defun flat-infix (x file eviscp) ...)
(defun flatsize-infix (x j max eviscp) ...)

You can use meta-. to find the current definitions and read the comments that
tell you what the expected functionality is.

------------------------------------------------------------------------------
(defun parse-infix (file eof)

; File is an open input file.  Eof is an arbitrary lisp object.  If file is
; empty, return eof.  This way we can repeatedly parse forms from a file until
; we get back the eof object.  Otherwise, parse one well-formed expression from
; file and return the corresponding s-expr.  If the file is exhausted before
; the parse finishes or if the parse is unsuccessful, cause a hard lisp error.

; In the current hackish implementation, the infix language is just a dollar
; sign followed by the s-expr.

  (let (dollar sexpr)
    (setq dollar (read file nil eof))
    (cond ((eq dollar eof) eof)
          ((eq dollar '$)
; The following read could cause an error if the user types bad lisp syntax.
           (setq sexpr (read file nil eof))
           (cond ((eq sexpr eof)
                  (error "Ill-formed infix input.  File ended on a $"))
                 (t sexpr)))
          (t (error
              "Ill-formed infix input.  You were supposed to type a $ ~
               followed by an s-expression and you typed ~s instead."
              dollar)))))

------------------------------------------------------------------------------
(defun ppr-infix (x width rpc col file eviscp)

; X is an s-expression denoting a term.  File is an open output file.
; Prettyprint x in infix notation to file.  End with a newline.  If eviscp is t
; then we are to give special treatment to the :evisceration-mark; otherwise
; not.

; This hook is modeled after the ACL2 pretty-printer, which has the following
; additional features.  These features need not be implemented in the infix
; prettyprinter.  The printer is assumed to be in column col, where col=0 means
; it is on the left margin.  We are supposed to print our first character in
; that column.  We are supposed to print in a field of width width.  That is,
; the largest column into which we might print is col+width-2.  Finally, assume
; that on the last line of the output somebody is going to write rpc additional
; characters and arrange for this not to overflow the col+width-2 limit.  Rpc
; is used when, for example, we plan to print some punctuation, like a comma,
; after a form and want to insure that we can do it without overflowing the
; right margin.  (One might think that the desired effect could be obtained by
; setting width smaller, but that is wrong because it narrows the whole field
; and we only want to guarantee space on the last line.)  Here is an example.
; Use ctrl-x = in emacs to see what columns things are in.  The semi-colons are
; in column 0.  Pretend they are all spaces, as they would be if the printing
; had been done by fmt-ppr.

; (foobar
;   (here is a long arg)
;   a)                  

; Here, col = 2, width = 23, and rpc = 19!

; Infix Hack:
; We simply print out $ followed by the expression.  We print the
; expression in lower-case.

  (declare (ignore width rpc col eviscp))
  (let ((*print-case* :downcase)
        (*print-pretty* t))
    (princ "$ " file)
    (prin1 x file)
    (terpri file)))

------------------------------------------------------------------------------
(defun flat-infix (x file eviscp)

; Print x flat (without terpri's) in infix notation to the open output file
; file.  Give special treatment to :evisceration-mark iff eviscp.  We only call
; this function if flatsize-infix assures us that x will fit on the line.

  (declare (ignore eviscp))
  (let ((*print-case* :downcase)
        (*print-pretty* nil))
    (princ "$ " file)
    (prin1 x file)))

------------------------------------------------------------------------------
(defun flatsize-infix (x j max eviscp)

; Suppose that printing x flat in infix notation causes k characters to come
; out.  Then we return j+k.  All answers greater than max are equivalent.

; If you think of j as the column into which you start printing flat,
; then this returns the column you'll print into after printing x.
; If that column exceeds max, which is the right margin, then it doesn't
; matter by how far it exceeds max.

; Infix Hack:  Our flat output has two extra chars in it, the $ and space.

  (+ 2 (flsz1 x j max *the-live-state* eviscp))

This page is URL http://www.computationallogic.com/software/caeti/infix/README.html