#|

 Copyright (C) 1994 by Robert S. Boyer and J Strother Moore.  All Rights
 Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Robert S. Boyer and J Strother Moore PROVIDE ABSOLUTELY NO WARRANTY.  THE
 EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS
 OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
 MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
 THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
 PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
 CORRECTION.

 IN NO EVENT WILL Robert S. Boyer or J Strother Moore BE LIABLE TO YOU FOR ANY
 DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
 CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
 (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
 OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
 POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

(BOOT-STRAP NQTHM)
(DEFN LOGICALP (X)
  (OR (EQUAL X (TRUE))
      (EQUAL X (FALSE))))
(DEFN EXPT (I J)
  (IF (ZEROP J)
      1
      (TIMES I (EXPT I (SUB1 J)))))
(DEFN ZNUMBERP (X)
  (OR (NEGATIVEP X)
      (NUMBERP X)))
(DEFN ZZERO NIL (ZERO))
(DEFN ZPLUS (X Y)
  (IF (NEGATIVEP X)
      (IF (NEGATIVEP Y)
          (MINUS (PLUS (NEGATIVE-GUTS X)
                       (NEGATIVE-GUTS Y)))
          (IF (LESSP Y (NEGATIVE-GUTS X))
              (MINUS (DIFFERENCE (NEGATIVE-GUTS X)
                                 Y))
              (DIFFERENCE Y (NEGATIVE-GUTS X))))
      (IF (NEGATIVEP Y)
          (IF (LESSP X (NEGATIVE-GUTS Y))
              (MINUS (DIFFERENCE (NEGATIVE-GUTS Y)
                                 X))
              (DIFFERENCE X (NEGATIVE-GUTS Y)))
          (PLUS X Y))))
(DEFN ZDIFFERENCE (X Y)
  (IF (NEGATIVEP X)
      (IF (NEGATIVEP Y)
          (IF (LESSP (NEGATIVE-GUTS Y)
                     (NEGATIVE-GUTS X))
              (MINUS (DIFFERENCE (NEGATIVE-GUTS X)
                                 (NEGATIVE-GUTS Y)))
              (DIFFERENCE (NEGATIVE-GUTS Y)
                          (NEGATIVE-GUTS X)))
          (MINUS (PLUS (NEGATIVE-GUTS X)
                       Y)))
      (IF (NEGATIVEP Y)
          (PLUS X (NEGATIVE-GUTS Y))
          (IF (LESSP X Y)
              (MINUS (DIFFERENCE Y X))
              (DIFFERENCE X Y)))))
(DEFN ZTIMES (X Y)
  (IF (NEGATIVEP X)
      (IF (NEGATIVEP Y)
          (TIMES (NEGATIVE-GUTS X)
                 (NEGATIVE-GUTS Y))
          (MINUS (TIMES (NEGATIVE-GUTS X)
                        Y)))
      (IF (NEGATIVEP Y)
          (MINUS (TIMES X (NEGATIVE-GUTS Y)))
          (TIMES X Y))))
(DEFN ZQUOTIENT (X Y)
  (IF (NEGATIVEP X)
      (IF (NEGATIVEP Y)
          (QUOTIENT (NEGATIVE-GUTS X)
                    (NEGATIVE-GUTS Y))
          (MINUS (QUOTIENT (NEGATIVE-GUTS X)
                           Y)))
      (IF (NEGATIVEP Y)
          (MINUS (QUOTIENT X (NEGATIVE-GUTS Y)))
          (QUOTIENT X Y))))
(DEFN ZEXPTZ (I J)
  (IF (ZEROP J)
      1
      (ZTIMES I (ZEXPTZ I (SUB1 J)))))
(DEFN ZNORMALIZE (X)
  (IF (NEGATIVEP X)
      (IF (EQUAL (NEGATIVE-GUTS X)
                 0)
          0 X)
      (FIX X)))
(DEFN ZEQP (X Y)
  (EQUAL (ZNORMALIZE X)
         (ZNORMALIZE Y)))
(DEFN ZNEQP (X Y)
  (NOT (ZEQP X Y)))
(DEFN ZLESSP (X Y)
  (IF (NEGATIVEP X)
      (IF (NEGATIVEP Y)
          (LESSP (NEGATIVE-GUTS Y)
                 (NEGATIVE-GUTS X))
          (NOT (AND (EQUAL (NEGATIVE-GUTS X)
                           0)
                    (ZEROP Y))))
      (IF (NEGATIVEP Y)
          F
          (LESSP X Y))))
(DEFN ZLESSEQP (X Y)
  (NOT (ZLESSP Y X)))
(DEFN ZGREATERP (X Y)
  (ZLESSP Y X))
(DEFN ZGREATEREQP (X Y)
  (NOT (ZLESSP X Y)))
(CONSTRAIN INTEGER-SIZE (REWRITE)
           (AND (NUMBERP (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                (NEGATIVEP (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                (LESSP 200 (NEGATIVE-GUTS
                             (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER)))
                (LESSP 200 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
           ((GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER (LAMBDA () -201))
            (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER (LAMBDA () 201))))
(DEFN EXPRESSIBLE-ZNUMBERP (X)
  (AND (ZLESSP (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER)
               X)
       (ZLESSP X (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))))
(DEFN IABS (I)
  (IF (NEGATIVEP I)
      (NEGATIVE-GUTS I)
      (FIX I)))
(DEFN MOD (X Y)
  (ZDIFFERENCE X (ZTIMES Y (ZQUOTIENT X Y))))
(DEFN MAX0 (I J)
  (IF (ZLESSP I J)
      J I))
(DEFN MIN0 (I J)
  (IF (ZLESSP I J)
      I J))
(DEFN ISIGN (I J)
  (IF (NEGATIVEP J)
      (ZTIMES -1 (IABS I))
      (IABS I)))
(DEFN IDIM (I J)
  (ZDIFFERENCE I (MIN0 I J)))

;;; In the old FORTRAN xxx we used UNDEF for all occurrences of the
;;; substring FORTRAN-UNDEF below.  However, in the quantifier version
;;; of the logic, UNDEF is a function name set up in the bootstrap.
;;; To avoid conflict we have changed the name here.  However, it is
;;; possible that vcs mention UNDEF -- not just the function DEFINEDP
;;; which is still around here.  If so, the vcg will have be to be
;;; changed should we decide to support it.

(ADD-SHELL FORTRAN-UNDEF NIL FORTRAN-UNDEFINED
           ((FORTRAN-UNDEF-GUTS (NONE-OF) ZERO)))
(DEFN DEFINEDP (X)
  (NOT (FORTRAN-UNDEFINED X)))
(DCL ELT1 (A I))
(DCL ELT2 (A I J))
(DCL ELT3 (A I J K))
(DEFN LEX (L1 L2)
  (IF (OR (NLISTP L1)
          (NLISTP L2))
      F
      (OR (LESSP (CAR L1)
                 (CAR L2))
          (AND (EQUAL (CAR L1)
                      (CAR L2))
               (LEX (CDR L1)
                    (CDR L2))))))
(DCL RNUMBERP (X))
(DCL DNUMBERP (X))
(DCL CNUMBERP (X))
(DCL RZERO NIL)
(DCL DZERO NIL)
(DCL CZERO NIL)
(DCL EXPRESSIBLE-RNUMBERP (X))
(DCL EXPRESSIBLE-DNUMBERP (X))
(DCL EXPRESSIBLE-CNUMBERP (X))
(DCL RPLUS (X Y))
(DCL RTIMES (X Y))
(DCL RDIFFERENCE (X Y))
(DCL RQUOTIENT (X Y))
(DCL RLESSP (X Y))
(DCL RLESSEQP (X Y))
(DCL REQP (X Y))
(DCL RNEQP (X Y))
(DCL RGREATEREQP (X Y))
(DCL RGREATERP (X Y))
(DCL DPLUS (X Y))
(DCL DTIMES (X Y))
(DCL DDIFFERENCE (X Y))
(DCL DQUOTIENT (X Y))
(DCL DLESSP (X Y))
(DCL DLESSEQP (X Y))
(DCL DEQP (X Y))
(DCL DNEQP (X Y))
(DCL DGREATEREQP (X Y))
(DCL DGREATERP (X Y))
(DCL CPLUS (X Y))
(DCL CTIMES (X Y))
(DCL CDIFFERENCE (X Y))
(DCL CQUOTIENT (X Y))
(DCL CEQP (X Y))
(DCL CNEQP (X Y))
(DCL REXPTZ (X Y))
(DCL DEXPTZ (X Y))
(DCL CEXPTZ (X Y))
(DCL REXPTR (X Y))
(DCL REXPTD (X Y))
(DCL DEXPTR (X Y))
(DCL DEXPTD (X Y))
(DCL ABS (I))
(DCL DABS (I))
(DCL AINT (I))
(DCL INT (I))
(DCL IDINT (I))
(DCL AMOD (I J))
(DCL AMAX0 (I J))
(DCL AMAX1 (I J))
(DCL MAX1 (I J))
(DCL DMAX1 (I J))
(DCL AMIN0 (I J))
(DCL AMIN1 (I J))
(DCL MIN1 (I J))
(DCL DMIN1 (I J))
(DCL FLOAT (I))
(DCL IFIX (I))
(DCL SIGN (I J))
(DCL DSIGN (I J))
(DCL DIM (I J))
(DCL SNGL (I))
(DCL REAL (I))
(DCL AIMAG (I))
(DCL DBLE (I))
(DCL CMPLX (I J))
(DCL CONJG (I))
(DCL EXP (I))
(DCL DEXP (I))
(DCL CEXP (I))
(DCL ALOG (I))
(DCL DLOG (I))
(DCL CLOG (I))
(DCL ALOG10 (I))
(DCL DLOG10 (I))
(DCL SIN (I))
(DCL DSIN (I))
(DCL CSIN (I))
(DCL COS (I))
(DCL DCOS (I))
(DCL CCOS (I))
(DCL TANH (I))
(DCL SQRT (I))
(DCL DSQRT (I))
(DCL CSQRT (I))
(DCL ATAN (I))
(DCL DATAN (I))
(DCL ATAN2 (I J))
(DCL DATAN2 (I J))
(DCL DMOD (I J))
(DCL CABS (I))

(DEFN ALMOST-EQUAL1 (A1 A2 U V I E)
  (IF (OR (ZEROP V)
          (LESSP V U))
      T
      (AND (IF (EQUAL V I)
               (EQUAL (ELT1 A2 V)
                      E)
               (EQUAL (ELT1 A2 V)
                      (ELT1 A1 V)))
           (ALMOST-EQUAL1 A1 A2 U (SUB1 V)
                          I E))))
(PROVE-LEMMA PLUS-0 (REWRITE)
             (EQUAL (PLUS X 0)
                    (FIX X)))
(PROVE-LEMMA PLUS-NON-NUMBERP (REWRITE)
             (IMPLIES (NOT (NUMBERP Y))
                      (EQUAL (PLUS X Y)
                             (FIX X))))
(PROVE-LEMMA PLUS-ADD1 (REWRITE)
             (EQUAL (PLUS X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (ADD1 (PLUS X Y))
                        (ADD1 X))))
(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS (REWRITE)
             (EQUAL (PLUS X (PLUS Y Z))
                    (PLUS Y (PLUS X Z))))
(PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE)
             (EQUAL (PLUS X Y)
                    (PLUS Y X)))
(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS (REWRITE)
             (EQUAL (PLUS (PLUS X Y)
                          Z)
                    (PLUS X (PLUS Y Z))))
(PROVE-LEMMA TIMES-0 (REWRITE)
             (EQUAL (TIMES X 0)
                    0))
(PROVE-LEMMA TIMES-NON-NUMBERP (REWRITE)
             (IMPLIES (NOT (NUMBERP Y))
                      (EQUAL (TIMES X Y)
                             0)))
(PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-PLUS (REWRITE)
             (EQUAL (TIMES X (PLUS Y Z))
                    (PLUS (TIMES X Y)
                          (TIMES X Z))))
(PROVE-LEMMA TIMES-ADD1 (REWRITE)
             (EQUAL (TIMES X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (PLUS X (TIMES X Y))
                        (FIX X))))
(PROVE-LEMMA COMMUTATIVITY2-OF-TIMES (REWRITE)
             (EQUAL (TIMES X (TIMES Y Z))
                    (TIMES Y (TIMES X Z))))
(PROVE-LEMMA COMMUTATIVITY-OF-TIMES (REWRITE)
             (EQUAL (TIMES X Y)
                    (TIMES Y X)))
(PROVE-LEMMA ASSOCIATIVITY-OF-TIMES (REWRITE)
             (EQUAL (TIMES (TIMES X Y)
                           Z)
                    (TIMES X (TIMES Y Z))))
(PROVE-LEMMA EQUAL-TIMES-0 (REWRITE)
             (EQUAL (EQUAL (TIMES X Y)
                           0)
                    (OR (ZEROP X)
                        (ZEROP Y))))
(PROVE-LEMMA EQUAL-LESSP (REWRITE)
             (EQUAL (EQUAL (LESSP X Y)
                           Z)
                    (IF (LESSP X Y)
                        (EQUAL T Z)
                        (EQUAL F Z))))
(PROVE-LEMMA ALMOST-EQUAL1-IN-RANGE (REWRITE)
             (IMPLIES (AND (NOT (EQUAL (ELT1 A2 J)
                                       W))
                           (EQUAL W (IF (EQUAL J I)
                                        E
                                        (ELT1 A1 J)))
                           (NOT (ZEROP U))
                           (NOT (LESSP J U))
                           (NOT (LESSP V J)))
                      (NOT (ALMOST-EQUAL1 A1 A2 U V I E))))
(PROVE-LEMMA ALMOST-EQUAL1-IN-RANGE-OPENED-UP (REWRITE)
                       (IMPLIES (AND (NOT (EQUAL (ELT1 A2 J)
                                                 W))
                                     (EQUAL W (IF (EQUAL J I)
                                                  E
                                                  (ELT1 A1 J)))
                                     (NOT (ZEROP U))
                                     (LEQ U J)
                                     (LEQ J V)
                                     (NOT (ZEROP V))
                                     (NOT (LESSP V U))
                                     (NOT (EQUAL V I))
                                     (EQUAL (ELT1 A2 V)
                                            (ELT1 A1 V)))
                                (NOT (ALMOST-EQUAL1 A1 A2 U (SUB1 V)
                                                    I E)))
                       ((USE (ALMOST-EQUAL1-IN-RANGE))
                        (DISABLE ALMOST-EQUAL1-IN-RANGE)))
(PROVE-LEMMA ALMOST-EQUAL1-CONTRACTS (REWRITE)
             (IMPLIES (AND (ALMOST-EQUAL1 A1 A2 U V I E)
                           (NOT (ZEROP U))
                           (NOT (LESSP X U))
                           (NOT (LESSP V Y)))
                      (ALMOST-EQUAL1 A1 A2 X Y I E))
             NIL)

(MAKE-LIB "fortran" T)