#|========================================================================
section 4.4
========================================================================|#

(define (^bm^true) 'true)
(define (^bm^false) 'false)

(define (^bm^truep x)
  (if x (^bm^true) (^bm^false)))

(define (^bm^falsep x)
  (if x (^bm^false) (^bm^true)))

(define (^bm^or x y)
  (if x 'true (if y 'true 'false)))

(define (^bm^and x y)
  (if x (if y 'true 'false) 'false))

(define (^bm^not x)
  (if x 'false 'true))

(define (^bm^implies x y)
  (if x (if y 'true 'false) 'true))



#|========================================================================
Section 4.5 most definitions in this section are machine generated
from shell definitions (machine generated definitions
appear in upper case).
========================================================================|#

#|
A Boyer-Moore term is defined to be the translation of a term in the
Boyer-Moore logic into I2 (Induction Interlingua).  The set of values which
can be denoted by Boyer-Moore terms is precisely the set of value recognized
by the following predicate.  This is a natural proper subset of the set of all possible
values.  This subset more natural corresponds to the Herbrand universe of
an infinite set of constructor symbols (of unconstrained arity).  Please
excuse the mutual recursion --- this is for documentation purposes only.

(define (consp x)
  (equal x (cons (car x) (cdr x))))

(define (symbolp x)
  (if (consp x) 'false 'true))

(define (herbrandp x)
  (if (symbolp x)
      'true
      (and (symbolp (car x))
	   (herbrand-arglist (cdr x)))))

(define (herbrand-arglist (cdr x))
  (if (equal x 'nil)
      'true
      (if (symbolp x)
	  'false
	  (and (herbrandp (car x))
	       (herbrand-arglist (cdr x))))))

|#

;(add-shell add1 zero numberp ((sub1 (one-of numberp) zero)))

(DEFINE (^BM^ZERO) '^BM^ZERO)

(DEFINE (^BM^NUMBERP X)
  (IF (EQUAL X '^BM^ZERO)
      'TRUE
      (IF (CONSP X)
	  (IF (EQUAL (CAR X) '^BM^ADD1)
	      (IF (CONSP (CDR X))
		  (IF (^BM^NUMBERP (CAR (CDR X)))
		      (EQUAL (CDR (CDR X)) 'NIL)
		      'FALSE)
		  'FALSE)
	      'FALSE)
	  'FALSE)))

(DEFINE (^BM^ADD1 T76)
  (CONS '^BM^ADD1 (CONS (IF (^BM^NUMBERP T76) T76 (^BM^ZERO)) 'NIL)))

(DEFINE (^BM^SUB1 X) (IF (^BM^NUMBERP X) (CAR (CDR X)) (^BM^ZERO)))

(define (^bm^zerop x)
  (^bm^or (^bm^not (^bm^numberp x)) (equal x (^bm^zero))))

(define (^bm^fix x)
  (if (^bm^numberp x) x (^bm^zero)))

(define (^bm^plus x y)
  (if (^bm^zerop x)
      (^bm^fix y)
      (^bm^add1 (^bm^plus (^bm^sub1 x) y))))

(define (^bm^lessp x y)
  (if (^bm^zerop y)
      (^bm^false)
      (if (^bm^zerop x)
	  (^bm^true)
	  (^bm^lessp (^bm^sub1 x) (^bm^sub1 y)))))

(define (^bm^greaterp i j)
  (^bm^lessp j i))

(define (^bm^leq i j) (^bm^not (^bm^lessp j i)))

(define (^bm^geq i j) (^bm^not (^bm^greaterp j i)))

(define (^bm^max i j)
  (if (^bm^lessp i j) (^bm^fix j) (^bm^fix i)))

(define (^bm^difference i j)
  (if (^bm^zerop i)
      (^bm^zero)
      (if (^bm^zerop j)
          i
          (^bm^difference (^bm^sub1 i) (^bm^sub1 j)))))

(define (^bm^times i j)
  (if (^bm^zerop i)
      (^bm^zero)
      (^bm^plus j (^bm^times (^bm^sub1 i) j))))

(define (^bm^quotient i j)
  (if (^bm^zerop j)
      (^bm^zero)
      (if (^bm^lessp i j)
          (^bm^zero)
          (^bm^add1 (^bm^quotient (^bm^difference i j) j)))))

(define (^bm^remainder i j)
  (if (^bm^zerop j)
      (^bm^fix i)
      (if (^bm^lessp i j)
          (^bm^fix i)
          (^bm^remainder (^bm^difference i j) j))))


(define (^count flg x)
  (if (symbolp x)
      (^bm^zero)
      (if (equal flg 'object)
	  (if (symbolp (car x))
	      (^bm^add1 (^count 'arglist (cdr x)))
	      (^bm^zero))
	  (^bm^plus (^count 'object (car x))
		   (^count 'arglist (cdr x))))))

(define (^bm^count x)
  (^count 'object x))

;(add-shell cons nil listp ((car nil zero) (cdr nil zero)))

(DEFINE (^BM^LISTP X)
  (IF (CONSP X)
      (IF (EQUAL (CAR X) '^BM^CONS)
	  (IF (CONSP (CDR X))
	      (IF (CONSP (CDR (CDR X)))
		  (EQUAL (CDR (CDR (CDR X))) 'NIL)
		  'FALSE)
	      'FALSE)
	  'FALSE)
      'FALSE))

(DEFINE (^BM^CONS T63 T64)
  (CONS '^BM^CONS
	(CONS (IF 'TRUE T63 (^BM^ZERO)) (CONS (IF 'TRUE T64 (^BM^ZERO)) 'NIL))))

(DEFINE (^BM^CAR X) (IF (^BM^LISTP X) (CAR (CDR X)) (^BM^ZERO)))

(DEFINE (^BM^CDR X) (IF (^BM^LISTP X) (CAR (CDR (CDR X))) (^BM^ZERO)))



#|========================================================================
numerals and decimal representation
========================================================================|#

(define (^0) (^bm^zero))

#|
(let ((code nil))
  (dotimes (n 9)
    (push `(define ,(nth (1+ n) *digits*) (^bm^add1 ,(digit-call n)))
	  code))
  `(progn ,@(reverse code)))
|#

(DEFINE (^1) (^BM^ADD1 (^0)))
(DEFINE (^2) (^BM^ADD1 (^1)))
(DEFINE (^3) (^BM^ADD1 (^2)))
(DEFINE (^4) (^BM^ADD1 (^3)))
(DEFINE (^5) (^BM^ADD1 (^4)))
(DEFINE (^6) (^BM^ADD1 (^5)))
(DEFINE (^7) (^BM^ADD1 (^6)))
(DEFINE (^8) (^BM^ADD1 (^7)))
(DEFINE (^9) (^BM^ADD1 (^8)))

(define (^ten) (^bm^add1 (^9)))

(define (^int2 x accum)
  (if (^bm^listp x)
      (^int2 (^bm^cdr x) (^bm^plus (^bm^times accum (^ten)) (^bm^car x)))
      accum))

(define (^int x)
  (^int2 x (^bm^zero)))

;(add-shell pack nil litatom ((unpack (none-of) zero)))

(DEFINE (^BM^LITATOM X)
  (IF (CONSP X)
      (IF (EQUAL (CAR X) '^BM^PACK)
	  (IF (CONSP (CDR X))
	      (IF (^BM^NOT 'FALSE) (EQUAL (CDR (CDR X)) 'NIL) 'FALSE)
	      'FALSE)
	  'FALSE)
      'FALSE))

(DEFINE (^BM^PACK T80)
  (CONS '^BM^PACK (CONS (IF (^BM^NOT 'FALSE) T80 (^BM^ZERO)) 'NIL)))

(DEFINE (^BM^UNPACK X) (IF (^BM^LITATOM X) (CAR (CDR X)) (^BM^ZERO)))

#|
(defun ascii-for (n)
  (char-code (character n)))

(let ((result nil))
  (dolist (c '(a b c d e f g h i j k l m n o p
	       q r s t u v w x y z
	       $ ^ & * _ - + = ~ { } ? < >))
    (push `(define (,(intern (format nil "^~s" c)) )
	    ,(put-in-package :bm (number-term (ascii-for c))))
	  result))
  `(progn ,@(reverse result)))
|#

(DEFINE (^A) (^INT (^BM^CONS (^6) (^BM^CONS (^5) (^BM^ZERO)))))
(DEFINE (^B) (^INT (^BM^CONS (^6) (^BM^CONS (^6) (^BM^ZERO)))))
(DEFINE (^C) (^INT (^BM^CONS (^6) (^BM^CONS (^7) (^BM^ZERO)))))
(DEFINE (^D) (^INT (^BM^CONS (^6) (^BM^CONS (^8) (^BM^ZERO)))))
(DEFINE (^E) (^INT (^BM^CONS (^6) (^BM^CONS (^9) (^BM^ZERO)))))
(DEFINE (^F) (^INT (^BM^CONS (^7) (^BM^CONS (^0) (^BM^ZERO)))))
(DEFINE (^G) (^INT (^BM^CONS (^7) (^BM^CONS (^1) (^BM^ZERO)))))
(DEFINE (^H) (^INT (^BM^CONS (^7) (^BM^CONS (^2) (^BM^ZERO)))))
(DEFINE (^I) (^INT (^BM^CONS (^7) (^BM^CONS (^3) (^BM^ZERO)))))
(DEFINE (^J) (^INT (^BM^CONS (^7) (^BM^CONS (^4) (^BM^ZERO)))))
(DEFINE (^K) (^INT (^BM^CONS (^7) (^BM^CONS (^5) (^BM^ZERO)))))
(DEFINE (^L) (^INT (^BM^CONS (^7) (^BM^CONS (^6) (^BM^ZERO)))))
(DEFINE (^M) (^INT (^BM^CONS (^7) (^BM^CONS (^7) (^BM^ZERO)))))
(DEFINE (^N) (^INT (^BM^CONS (^7) (^BM^CONS (^8) (^BM^ZERO)))))
(DEFINE (^O) (^INT (^BM^CONS (^7) (^BM^CONS (^9) (^BM^ZERO)))))
(DEFINE (^P) (^INT (^BM^CONS (^8) (^BM^CONS (^0) (^BM^ZERO)))))
(DEFINE (^Q) (^INT (^BM^CONS (^8) (^BM^CONS (^1) (^BM^ZERO)))))
(DEFINE (^R) (^INT (^BM^CONS (^8) (^BM^CONS (^2) (^BM^ZERO)))))
(DEFINE (^S) (^INT (^BM^CONS (^8) (^BM^CONS (^3) (^BM^ZERO)))))
(DEFINE (^T) (^INT (^BM^CONS (^8) (^BM^CONS (^4) (^BM^ZERO)))))
(DEFINE (^U) (^INT (^BM^CONS (^8) (^BM^CONS (^5) (^BM^ZERO)))))
(DEFINE (^V) (^INT (^BM^CONS (^8) (^BM^CONS (^6) (^BM^ZERO)))))
(DEFINE (^W) (^INT (^BM^CONS (^8) (^BM^CONS (^7) (^BM^ZERO)))))
(DEFINE (^X) (^INT (^BM^CONS (^8) (^BM^CONS (^8) (^BM^ZERO)))))
(DEFINE (^Y) (^INT (^BM^CONS (^8) (^BM^CONS (^9) (^BM^ZERO)))))
(DEFINE (^Z) (^INT (^BM^CONS (^9) (^BM^CONS (^0) (^BM^ZERO)))))
(DEFINE (^$) (^INT (^BM^CONS (^3) (^BM^CONS (^6) (^BM^ZERO)))))
(DEFINE (^^) (^INT (^BM^CONS (^9) (^BM^CONS (^4) (^BM^ZERO)))))
(DEFINE (^&) (^INT (^BM^CONS (^3) (^BM^CONS (^8) (^BM^ZERO)))))
(DEFINE (^*) (^INT (^BM^CONS (^4) (^BM^CONS (^2) (^BM^ZERO)))))
(DEFINE (^_) (^INT (^BM^CONS (^9) (^BM^CONS (^5) (^BM^ZERO)))))
(DEFINE (^-) (^INT (^BM^CONS (^4) (^BM^CONS (^5) (^BM^ZERO)))))
(DEFINE (^+) (^INT (^BM^CONS (^4) (^BM^CONS (^3) (^BM^ZERO)))))
(DEFINE (^=) (^INT (^BM^CONS (^6) (^BM^CONS (^1) (^BM^ZERO)))))
(DEFINE (^~)
  (^INT (^BM^CONS (^1) (^BM^CONS (^2) (^BM^CONS (^6) (^BM^ZERO))))))
(DEFINE (^{)
  (^INT (^BM^CONS (^1) (^BM^CONS (^2) (^BM^CONS (^3) (^BM^ZERO))))))
(DEFINE (^})
  (^INT (^BM^CONS (^1) (^BM^CONS (^2) (^BM^CONS (^5) (^BM^ZERO))))))
(DEFINE (^?) (^INT (^BM^CONS (^6) (^BM^CONS (^3) (^BM^ZERO)))))
(DEFINE (^<) (^INT (^BM^CONS (^6) (^BM^CONS (^0) (^BM^ZERO)))))
(DEFINE (^>) (^INT (^BM^CONS (^6) (^BM^CONS (^2) (^BM^ZERO)))))

#|
(let ((result nil))
  (dolist (c '("0" "1" "2" "3" "4" "5" "6" "7" "8" "9"))
    (push `(define (,(intern (format nil "^N~a" c))) ,(boot-number-term (ascii-for c)))
	  result))
  `(progn ,@(reverse result)))
|#

(DEFINE (^N0) (^INT (^BM^CONS (^4) (^BM^CONS (^8) (^BM^ZERO)))))
(DEFINE (^N1) (^INT (^BM^CONS (^4) (^BM^CONS (^9) (^BM^ZERO)))))
(DEFINE (^N2) (^INT (^BM^CONS (^5) (^BM^CONS (^0) (^BM^ZERO)))))
(DEFINE (^N3) (^INT (^BM^CONS (^5) (^BM^CONS (^1) (^BM^ZERO)))))
(DEFINE (^N4) (^INT (^BM^CONS (^5) (^BM^CONS (^2) (^BM^ZERO)))))
(DEFINE (^N5) (^INT (^BM^CONS (^5) (^BM^CONS (^3) (^BM^ZERO)))))
(DEFINE (^N6) (^INT (^BM^CONS (^5) (^BM^CONS (^4) (^BM^ZERO)))))
(DEFINE (^N7) (^INT (^BM^CONS (^5) (^BM^CONS (^5) (^BM^ZERO)))))
(DEFINE (^N8) (^INT (^BM^CONS (^5) (^BM^CONS (^6) (^BM^ZERO)))))
(DEFINE (^N9) (^INT (^BM^CONS (^5) (^BM^CONS (^7) (^BM^ZERO)))))

(define (^nil)
  (^bm^pack (^bm^cons (^n) (^bm^cons (^i) (^bm^cons (^l) (^bm^zero))))))



;(add-shell minus nil negativep ((negative-guts (one-of numberp) zero)))

(DEFINE (^BM^NEGATIVEP X)
  (IF (CONSP X)
      (IF (EQUAL (CAR X) '^BM^MINUS)
	  (IF (CONSP (CDR X))
	      (IF (^BM^NUMBERP (CAR (CDR X)))
		  (EQUAL (CDR (CDR X)) 'NIL)
		  'FALSE)
	      'FALSE)
	  'FALSE)
      'FALSE))

(DEFINE (^BM^MINUS T82)
  (CONS '^BM^MINUS (CONS (IF (^BM^NUMBERP T82) T82 (^BM^ZERO)) 'NIL)))

(DEFINE (^BM^NEGATIVE-GUTS X)
        (IF (^BM^NEGATIVEP X) (CAR (CDR X)) (^BM^ZERO)))


#|========================================================================
Section 4.6 is not needed and section 4.7, the extended syntax, is handled
by translation.
========================================================================|#


#|========================================================================
section 4.8.
========================================================================|#

(define (^bm^ord-lessp x y)
  (if (^bm^not (^bm^listp x))
      (if (^bm^not (^bm^listp y))
	  (^bm^lessp x y)
	  'true)
      (if (^bm^not (^bm^listp y))
	  'false
	  (if (^bm^ord-lessp (^bm^car x) (^bm^car y))
	      'true
	      (^bm^and (equal (^bm^car x) (^bm^cdr y))
		      (^bm^ord-lessp (^bm^cdr x) (^bm^cdr y)))))))

(define (^bm^ordinalp x)
  (if (^bm^listp x)
      (^bm^and (^bm^ordinalp (^bm^car x))
	       (^bm^and (^bm^not (equal (^bm^car x) (^bm^zero)))
			(^bm^and (^bm^ordinalp (^bm^cdr x))
				(^bm^or (^bm^not (^bm^listp (cdr x)))
					(^bm^ord-lessp (^bm^car x) (^bm^cdr x))))))
      (^bm^numberp x)))



#|========================================================================
section 4.9
========================================================================|#

(define (^bm^iff x y)
  (equal (^bm^truep x) (^bm^truep y)))

(define (^bm^append x y)
  (if (^bm^listp x)
      (^bm^cons (^bm^car x) (^bm^append (^bm^cdr x) y))
      y))

(define (^bm^nlistp x)
  (^bm^not (^bm^listp x)))

(define (^bm^member x lst)                           
  (if (^bm^nlistp lst)
      (^bm^false)
      (if (equal x (^bm^car lst))
          (^bm^true)
          (^bm^member x (^bm^cdr lst)))))

(define (^bm^union x y)
  (if (^bm^listp x)
      (if (^bm^member (^bm^car x) y)
          (^bm^union (^bm^cdr x) y)
          (^bm^cons (^bm^car x) (^bm^union (^bm^cdr x) y))) y))

(define (^bm^add-to-set x set)
  (if (^bm^member x set)
      set
      (^bm^cons x set)))

(define (^bm^assoc x l)
  (if (^bm^nlistp l)
      (^bm^false)
      (if (equal x (^bm^car (^bm^car l)))
          (^bm^car l)
          (^bm^assoc x (^bm^cdr l)))))

(define (^bm^pairlist x y)
  (if (^bm^listp x)
      (^bm^cons (^bm^cons (^bm^car x) (^bm^car y))
		(^bm^pairlist (^bm^cdr x) (^bm^cdr y)))
      (^nil)))

(define (^bm^identity x) x)

(define (^bm^strip-cars x)
  (if (^bm^listp x)
      (^bm^cons (^bm^car (^bm^car x))
		(^bm^strip-cars (^bm^cdr x)))
      (^nil)))

(define (^bm^sum-cdrs x)
  (if (^bm^listp x)
      (^bm^plus (^bm^cdr (^bm^car x))
		(^bm^sum-cdrs (^bm^cdr x)))
      (^bm^zero)))


#|========================================================================
Sections 4.10, 4.11 and 4.12 are not implemented.  These sections describe
the following functions which are also not implemented.
	  
APPLY-SUBR    2   application of primitive fn to arguments
APPLY$        2   application of fn to arguments
BODY          1   body of a fn definition
EVAL$         3   interpreter for the logic
FIX-COST      2   increments cost if argument is non-F
FOR           6   general purpose quantifier
FORMALS       1   list of formal arguments of a function
QUANTIFIER-INITIAL-VALUE
              1   initial value of a quantifier
QUANTIFIER-OPERATION
              3   operation performed by quantifier
SUBRP         1   recognizes primitive function symbols
V&C$          3   determines value and cost of an expr
V&C-APPLY$    2   determines value and cost of fn application

========================================================================|#



#|========================================================================
support for the translator
========================================================================|#