;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - NFS Share File - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(in-package :user :use '(lisp))

(defun translate-files (files)
  (dolist (file files)
    (translate-file file)))

(defvar *arglists*)
  
(defun translate-file (fname)
  (let ((*arglists*  '((equal x y) (if u v w) (car x) (cdr x) (cons x y) (consp x) (symbolp x))))
    (let ((flg (catch 'bad-event
		 (format t "~%translating ~a.events~%" fname)
		 (let ((tevents (translate-events (read-forms (concatenate 'string fname ".events")))))
		   (format t "writing ~a.i2~%" fname)
		   (pprint-forms tevents (concatenate 'string fname ".i2"))
		   t))))
      (unless flg
	(format t "translate aborted~%")))))

(defun translate-events (events)
  (when events
    (let* ((tevent (translate-event (car events)))
	   (tevents (if (and (consp tevent) (eq (car tevent) 'progn))
			(cdr tevent)
			(list tevent))))
      (if (well-formed-events tevents)
	  (nconc tevents (translate-events (cdr events)))
	  (throw 'bad-event nil)))))

(property-macro event-translator)

(defun translate-event (event)
  (if (or (not (consp event))
	  (not (symbolp (car event))))
      (unrecognized-event event)
      (let* ((eventfun (event-translator (car event))))
	(if eventfun
	    (apply eventfun (cdr event))
	    (unrecognized-event event)))))

(defun unrecognized-event (event)
  (progn (format t "unrecognized event ~s~%" event)
	 '(progn)))

#|
(defevent defn (NAME ARGS BODY &OPTIONAL RELATION-MEASURE-LST)
  relation-measure-lst
  `(define (,(add-bm name) ,@args) ,(translate-term body)))
|#

(defun translate-term (term)
  (put-in-package :bm (da*-expand (translate term))))


#|========================================================================
Selectmatch --- a destructuring macro for common lisp (I can't program without this)

The + translator could have been written as

(DEFTRANSLATOR +
  (selectmatch exp
    ((+ ?x) ?x)
    ((+ ?x 0) ?x)
    ((+ 0 ?x) ?x)
    ((+ ?x ?y) `(+ ,?x ,?y))
    ((+ ?x . ?rest) `(+ ,?x (+ ,@?rest))))
    (:anything (error "illegal syntax for +")))
========================================================================|#

(eval-when (compile load eval)

  (defmacro selectmatch (arg &body cases)
    (let ((arg-var (gentemp)))
      `(block success
	(let ((,arg-var ,arg))
	  ,@(mapcar #'(lambda (case)
			`(block fail
			  ,(unitest (car case)
			    arg-var
			    nil
			    #'(lambda (ignore) ignore
				      `(return-from success
					(progn ,@(cdr case)))))))
		    cases)))))

  (defun variable? (x)
    (and (symbolp x) (string-equal "?" (subseq (string x) 0 1))))

  (defun unitest (pattern object bound-vars body-continuation)
    (cond ((null pattern)
	   `(if ,object
	     (return-from fail nil)
	     ,(funcall body-continuation bound-vars)))
	  ((listp pattern)
	   (let ((car-var (gentemp))
		 (cdr-var (gentemp)))
	     `(if (not (and ,object (listp ,object)))
	       (return-from fail nil)
	       ,(cond ((and (eq (car pattern) :anything)
			    (eq (cdr pattern) :anything))
		       (funcall body-continuation bound-vars))
		      ((eq (car pattern) :anything)
		       `(let ((,cdr-var (cdr ,object)))
			 ,(unitest (cdr pattern) cdr-var bound-vars body-continuation)))
		      ((eq (cdr pattern) :anything)
		       `(let ((,car-var (car ,object)))
			 ,(unitest (car pattern) car-var bound-vars body-continuation)))
		      (t
		       `(let ((,car-var (car ,object))
			      (,cdr-var (cdr ,object)))
			 ,(unitest (car pattern) car-var bound-vars
			   #'(lambda (bound-vars)
			       (unitest (cdr pattern)
					cdr-var
					bound-vars
					body-continuation)))))))))
	  ((eq pattern :anything) (funcall body-continuation bound-vars))
	  ((not (variable? pattern))
	   `(if (not (eq ,object ',pattern))
	     (return-from fail nil)
	     ,(funcall body-continuation bound-vars)))

	  ((member pattern bound-vars)
	   `(if (not (equal ,object ,pattern))
	     (return-from fail nil)
	     ,(funcall body-continuation bound-vars)))
	  (t
	   `(let ((,pattern ,object))
	     ,(funcall body-continuation (cons pattern bound-vars)))))))




#|========================================================================
some other utilities I can't live without
========================================================================|#

(eval-when (compile load eval)

  (defun combine-symbols (s1 s2 &optional (package *package*))
    (intern (concatenate 'string (string s1) "-" (string s2))
	    package))

  (unless (fboundp 'emacs-indent) ;this is just a stub --- the real thing requires ilisp
    (defmacro emacs-indent (&rest args)
      (declare (ignore args))
      nil))

  (defun rprint (x)
    (let ((*print-level* 150)
	  (*print-length* 150))
      (pprint x))))



#|========================================================================
put-in-package

A symbol is said to be "absolute" if it is either one of IF or EQUAL
or it starts with the character "^".
If a symbol is not absolute it is called "relative".  The function
put-in-package adds a package declaration of the form "^xxx^" to the
front of all relative function symbols thereby making them absolute.  For
example

(put-in-package :bm '(foo (^bar x (baz)))) => (^bm^foo (^bar x (^bm^baz)))

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

(defun put-in-package (pkg-sym term)
  (if (symbolp term)
      term
      (selectmatch term
	((?f . ?args)
	 (unless (symbolp ?f)
	   (error "illegal operator ~s" ?f))
	 (let ((newargs (mapcar #'(lambda (arg) (put-in-package pkg-sym arg))
				?args)))
	   (if (absolute? ?f)
	       `(,?f ,@newargs)
	       `(,(add-package pkg-sym ?f) ,@newargs))))
	(:anything
	 (error "illegal term syntax ~s" term)))))

(defun absolute? (x)
  (and (symbolp x)
       (or (member x '(if equal))
	   (string-equal "^" (subseq (string x) 0 1)))))

(defun add-package (pkg-sym sym)
  (intern (concatenate 'string
		       "^"
		       (string pkg-sym)
		       "^"
		       (string sym))))

(defun add-bm (sym)
  (add-package :bm sym))



#|========================================================================
the implementation of cdar notation
This is done by mapping terms to terms where a term is either
a symbol (variable), or an application of the form (f t1 ... tn)
where f is a symbol (function) and each ti is a term.
========================================================================|#

(defun da*-expand (exp)
  (if (symbolp exp)
      exp
      (selectmatch exp
	((?f . ?args)
	 (if (da*? ?f)
	     (progn
	       (unless (= (length ?args)
			  1)
		 (error "illegal syntax ~s" exp))
	       (composition-term (da*-explode ?f) (da*-expand (car ?args))))
	     `(,?f ,@(mapcar #'da*-expand ?args)))))))

(defun da*? (x)
  (and (symbolp x)
       (let ((s (string x)))
	 (and (string-equal (subseq s 0 1) "C")
	      (string-equal (subseq s (1- (length s)) (length s)) "R")
	      (progn (dotimes (i (- (length s) 2))
		       (unless (or (string-equal (subseq s (+ i 1) (+ i 2))
						 "A")
				   (string-equal (subseq s (+ i 1) (+ i 2))
						 "D"))
			 (return-from da*? nil)))
		     t)))))

(defun da*-explode (x)
  (let ((s (string x))
	(result nil))
    (dotimes (i (- (length s) 2))
      (if (string-equal (subseq s (+ i 1) (+ i 2))
			"A")
	  (push 'car result)
	  (push 'cdr result)))
    (reverse result)))

(defun composition-term (ops arg)
  (if (null ops)
      arg
      `(,(car ops) ,(composition-term (cdr ops) arg))))



#|========================================================================
General purpose translation package

Translators are rewrite rules.  Translation rewrites to
normal form.  Rewriting is innermost (innermost rewriting is
confluent).  Only one translator per operator is allowed.
rewriting is not allowed inside the body of quote.

(deftranslator and (x y)
  `(not (or (not ,x) (not ,y))))
========================================================================|#

(defmacro property-macro (symbol)
  `(defmacro ,symbol (x)
     (list 'get x '',symbol)))

(property-macro translator)

(property-macro symbol-translation)

(defmacro deftranslator (symbol &rest body)
  (let ((name (combine-symbols symbol 'translator)))
    `(progn
       (defun ,name (exp) ,@body)
       (setf (translator ',symbol)
	     #',name))))

(defvar *number-translator* 'number-term)

(emacs-indent defstranslator 1)

(defvar *translator-cache* (make-hash-table))

(defun translate (exp)
  (let ((val (translate2 exp)))
    (clrhash *translator-cache*) ;free the intermediate cons cells
    val))

(defun translate2 (exp)
  (or (gethash exp *translator-cache*)
      (let ((val (translate3 exp)))
	(setf (gethash exp *translator-cache*) val)
	val)))

(defun translate3 (exp)
  (cond ((symbolp exp)
	 (or (symbol-translation exp)
	     exp))
	((numberp exp)
	 (funcall *number-translator* exp))
	((atom exp) exp)
	(t
	 (let ((exp2 (if (eq (car exp) 'quote)
			 exp
			 (mapcar #'translate2 exp))))
	   (if (not (and (symbolp (car exp2))
			 (translator (car exp2))))
	       exp2
	       (let ((exp3 (funcall (translator (car exp2)) exp2)))
		 (if (equal exp3 exp)
		     exp3
		     (translate3 exp3))))))))



#|========================================================================
ac operators have steriotypical translators so we provide
a translator generator for them.

(ac-operator + 0)

generates

(DEFTRANSLATOR +
  (selectmatch exp
    ((+ ?x) ?x)
    ((+ ?x 0) ?x)
    ((+ 0 ?x) ?x)
    ((+ ?x ?y) `(+ ,?x ,?y))
    ((+ ?x . ?rest) `(+ ,?x (+ ,@?rest))))
    (:anything (error "illegal syntax for +")))

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

(defmacro ac-operator (op &optional identity)
  (if identity
      `(deftranslator ,op
	(selectmatch exp
	  ((,op ?x) ?x)
	  ((,op ?x ,identity) ?x)
	  ((,op ,identity ?x) ?x)
	  ((,op :anything :anything) exp)
	  ((,op ?x . ?rest) `(,',op ,?x (,',op ,@?rest)))
	  (:anything (error "illegal symtax for ~s" ',op))))
      `(deftranslator ,op
	(selectmatch exp
	  ((,op ?x) ?x)
	  ((,op :anything :anything) exp)
	  ((,op ?x . ?rest) `(,',op ,?x (,',op ,@?rest)))
	  (:anything (error "illegal symtax for ~s" ',op))))))


#|========================================================================
Translation of the extended syntax (section 4.7 of the handbook)
========================================================================|#

(setf (symbol-translation t) '(true))

(setf (symbol-translation 'f) '(false))

(setf (symbol-translation nil) '(^nil))

(ac-operator and)

(ac-operator or)

(ac-operator plus)

(ac-operator times)

(deftranslator list
  (selectmatch exp
    ((list) nil)
    ((list ?x . ?rest) `(cons ,?x (list ,@?rest)))))

(deftranslator cond
  (selectmatch exp
    ((cond) nil)
    ((cond (?test ?body) . ?rest)
     `(if ,?test ,?body (cond ,@?rest)))
    (:anything (error "illegal cond syntax"))))

(deftranslator let
  (selectmatch exp
    ((let ((?var ?val)) ?body)
     (var-subst ?val ?var ?body))
    ((let ((?var ?val) . ?rest) ?body)
     `(let ,?rest (let ((,?var ,?val)) ,?body)))
    (:anything (error "illegal let syntax"))))

(defun var-subst (val var term)
  (cond ((eq term var) val)
	((symbolp term) term)
	((cons (car term) (mapcar #'(lambda (arg) (var-subst val var arg))
				  (cdr term))))))

(deftranslator quote
  (selectmatch exp
    ((quote *1*true) '(true))
    ((quote *1*false) '(false))
    ((quote (*1*quote ?f . ?args))
     `(,?f ,@(mapcar #'(lambda (arg) `(quote ,arg))
	      ?args)))
    ((quote (*1*quote . :anything))
     (error "illegal syntax for *1*quote"))
    ((quote (?x . ?y))
     `(cons (quote ,?x) (quote ,?y)))
    ((quote ?z)
     (if (numberp ?z)
	 ?z
	 (make-bm-symbol ?z)))))


#|========================================================================
translating numerals
========================================================================|#

(defun number-term (n)
  (unless (integerp n)
    (error "unable to handle non-integer ~s" n))
  (if (>= n 0)
      `(^int ,(zero-terminate (reverse (digit-list n))))
      `(minus (^int ,(zero-terminate (reverse (digit-list (- n))))))))

(defun digit-list (n)
  (if (= n 0)
      nil
      (cons (digit-call (mod n 10)) (digit-list (floor (/ n 10))))))

(defun zero-terminate (x)
  (if (null x)
      '(zero)
      `(cons ,(car x) ,(zero-terminate (cdr x)))))

(defun digit-call (n) (list (intern (format nil "^~s" n))))



#|========================================================================
Translating quoted symbols
========================================================================|#

(defun make-bm-symbol (x)
  `(pack ,(codelist x)))

(defun codelist (x)
  (let ((s (string x))
	(result nil))
    (dotimes (n (length s))
      (push (call-for (subseq s n (1+ n))) result))
    (zero-terminate (reverse result))))

(defun call-for (x)
  (let ((c (character x)))
    (if (and (>= (char-code c) 48)
	     (<= (char-code c) 57))
	(list (intern (format nil "^N~a" x)))
	(list (intern (format nil "^~a" x))))))
		 


#|========================================================================
Events.

The following are the events defined in events.lisp of the nqth-1992 release

(DEFEVENT ADD-AXIOM (NAME TYPES TERM))

(DEFEVENT ADD-SHELL
  (SHELL-NAME BTM-FN-SYMB RECOGNIZER DESTRUCTOR-TUPLES))

(DEFEVENT AXIOM (NAME TYPES TERM &OPTIONAL IGNORE)) ;same as add-axiom

(DEFEVENT BOOT-STRAP (&OPTIONAL MODE))

(DEFEVENT CONSTRAIN (NAME TYPES TERM WITNESS-ALIST &OPTIONAL HINTS)) ;conservative extension without defs


(DEFEVENT DCL (NAME ARGS)) ;declares a function with no facts.

(DEFEVENT DEFN (NAME ARGS BODY &OPTIONAL RELATION-MEASURE-LST))

(DEFEVENT DEFTHEORY (NAME EVENTNAMES)) ;associated with hints enable-theory and disable-theory
;can be ignored.

(DEFEVENT DISABLE (OLDNAME))

(DEFEVENT DISABLE-THEORY (THEORY))

(DEFEVENT ENABLE (OLDNAME))

(DEFEVENT ENABLE-THEORY (THEORY))

(DEFEVENT FUNCTIONALLY-INSTANTIATE (NAME TYPES TERM OLD-NAME-OR-LIST FS
                                         &OPTIONAL HINTS))
;I don't understant functionally-instantiate

(DEFEVENT LEMMA (NAME TYPES TERM &OPTIONAL HINTS))

(DEFEVENT PROVE-LEMMA (NAME TYPES TERM &OPTIONAL HINTS))

(DEFEVENT SET-STATUS (NAME NAMES ALIST))

(DEFEVENT TOGGLE (NAME OLDNAME FLG))

(DEFEVENT TOGGLE-DEFINED-FUNCTIONS (NAME FLG))

(DEFEVENT UBT (&OPTIONAL N))

(DEFMACRO COMMENT (&REST REST)
  (DECLARE (IGNORE REST))
  T)
========================================================================|#

(defmacro defevent (symbol arglist &rest body)
  (let ((name (combine-symbols symbol 'translator)))
    `(progn
       (defun ,name ,arglist ,@body)
       (setf (event-translator ',symbol)
	     #',name))))

(emacs-indent defevent 2)

(defun read-forms (filename)
  (let ((forms nil)
	(eof-marker (list 'eof)))
    (with-open-file (istream filename :direction :input)
      (loop
       (let ((form (read istream nil eof-marker)))
	 (if (eq form eof-marker)
	     (return)
	     (push form forms)))))
    (nreverse forms)))

(defun pprint-forms (forms filename)
  (let ((*print-level* 1000)
	(*print-length* 1000)
	(*print-circle* nil))
    (with-open-file (istream filename :direction :output :if-exists :new-version
			     :if-does-not-exist :create)
      (dolist (form forms)
	(pprint form istream)
	(format istream "~%")))))

(defun print-forms (forms filename)
  (let ((*print-level* 1000)
	(*print-length* 1000)
	(*print-circle* nil))
    (with-open-file (istream filename :direction :output :if-exists :new-version
			     :if-does-not-exist :create)
      (dolist (form forms)
	(print form istream)
	(format istream "~%")))))



(defevent add-axiom (name types term)
  name
  types
  `(lemma ,(translate-term term)))

(defevent axiom (name types term)
  name
  types
  `(lemma ,(translate-term term)))

(defevent boot-strap (&optional mode)
  mode
  `(note-lib "nqthm-boot"))

(defevent constrain (NAME TYPES TERM WITNESS-ALIST &OPTIONAL HINTS)
  name types hints
  `(progn
    ,@(mapcan #'(lambda (pair)
		  (selectmatch pair
		    ((?name (lambda ?args ?body))
		     `((define (,(add-bm ?name) ,@?args) ,(translate-term ?body))))
		    ((?name1 ?name2)
		     (let ((arglist (cdr (assoc (add-bm ?name2) *arglists*))))
		       `((define (,(add-bm ?name1) ,@arglist) (,(add-bm ?name2) ,@arglist)))))
		    (:anything nil)))
       witness-alist)
    (lemma ,(translate-term term))))

(defevent dcl (name args)
  `(define (,(add-bm name) ,@args) (cons ',name ,(build-list args))))

(defevent defn (NAME ARGS BODY &OPTIONAL RELATION-MEASURE-LST)
  relation-measure-lst
  `(define (,(add-bm name) ,@args) ,(translate-term body)))

(defmacro null-event (name arglist)
  `(defevent ,name ,arglist ,@arglist '(progn)))

(null-event deftheory (name eventnames))

(null-event disable (name))

(null-event disable-theory (theory))

(null-event enable (name))

(null-event enable-theory (theory))

(NULL-EVENT SET-STATUS (NAME NAMES ALIST))

(NULL-EVENT TOGGLE (NAME OLDNAME FLG))

(NULL-EVENT TOGGLE-DEFINED-FUNCTIONS (NAME FLG))

(null-event compile-uncompiled-defns (flg))

(defevent functionally-instantiate (NAME TYPES TERM OLD-NAME-OR-LIST FS
                                         &OPTIONAL HINTS)
  name types term old-name-or-list fs hints '(progn))

(defevent comment (&rest comments)
  comments
  '(progn))
	    
(defevent lemma (NAME TYPES TERM &OPTIONAL HINTS)
  name types hints
  `(lemma ,(translate-term term)))

(defevent prove-lemma (NAME TYPES TERM &OPTIONAL HINTS)
  name types hints
  `(lemma ,(translate-term term)))

(defevent note-lib (fname flg)
  flg
  `(note-lib ,fname))

(null-event make-lib (fname flg))


#|========================================================================
The add-shell event
========================================================================|#

(defevent add-shell (SHELL-NAME BTM-FN-SYMB RECOGNIZER DESTRUCTOR-TUPLES)
  (setq shell-name (add-bm shell-name))
  (setq btm-fn-symb (when btm-fn-symb (add-bm btm-fn-symb)))
  (setq recognizer (add-bm recognizer))
  (setq destructor-tuples
	(mapcar #'(lambda (tuple)
		    (list (add-bm (car tuple))
			  (when (second tuple)
			    (cons (car (second tuple)) (mapcar #'add-bm (cdr (second tuple)))))
			  (add-bm (third tuple))))
		destructor-tuples))
			  
  (gentemp "X")
  `(progn
    ,@(when btm-fn-symb `((define (,btm-fn-symb) ',btm-fn-symb)))
	
    (define (,recognizer x)
      ,(let ((cons-case `(^bm^and (consp x)
			  (^bm^and (equal (car x) ',shell-name)
			   ,(type-restrictions 'x 1 destructor-tuples)))))
	(fix-boolean (if btm-fn-symb
			 `(^bm^or (equal x ',btm-fn-symb) ,cons-case)
			 cons-case))))

    ,(let ((arglist (mapcar #'(lambda (x) x (gentemp)) destructor-tuples)))
       `(define (,shell-name ,@arglist)
	 ,(build-list `(',shell-name ,@(mapcar #'(lambda (arg tuple)
						       `(if
							 ,(trtest (second tuple) arg)
							 ,arg
							 (,(third tuple))))
					    arglist destructor-tuples)))))
    ,@(let ((index 0)
	    (result nil))
	(dolist (tuple destructor-tuples)
	  (incf index)
	  (push `(define (,(car tuple) x)
		  (if (,recognizer x) ,(nth-code index 'x) (,(third tuple))))
		result))
	(reverse result))))

(defun build-list (x)
  (if (null x)
      ''nil
      `(cons ,(car x) ,(build-list (cdr x)))))


(defun type-restrictions (val n tuples)
  (cond ((null tuples)
	 `(equal ,(nth-cdr-code n val) 'nil))
	(t `(^bm^and (consp ,(nth-cdr-code n val))
	     (^bm^and ,(trtest (second (car tuples)) (nth-code n val))
	      ,(type-restrictions val (1+ n) (cdr tuples)))))))

(defun trtest (test val)
  (cond ((null test) ''true)
	((eq (car test) 'one-of)
	 (one-of-code (cdr test) val))
	(t `(^bm^not ,(one-of-code (cdr test) val)))))

(defun one-of-code (types val)
  (cond ((null types)
	 ''false)
	((null (cdr types))
	 `(,(car types) ,val))
	(t
	 `(^bm^or (,(car types) ,val) ,(one-of-code (cdr types) val)))))

(defun nth-code (n x)
  `(car ,(nth-cdr-code n x)))

(defun nth-cdr-code (n x)
  (if (= n 0) x `(cdr ,(nth-cdr-code (1- n) x))))

(defun fix-boolean (exp)
  (if (or (not (consp exp))
	  (not (member (car exp) '(^bm^and ^bm^or))))
      exp
      (let ((op (car exp))
	    (arg1 (fix-boolean (second exp)))
	    (arg2 (fix-boolean (third exp))))
	(cond ((or (and (eq op '^bm^and) (equal arg2 ''true))
		   (and (eq op '^bm^or) (equal arg2 ''false)))
	       arg1)
	      ((or (and (eq op '^bm^and) (equal arg1 ''true))
		   (and (eq op '^bm^or) (equal arg1 ''false)))
	       arg2)
	      ((eq op '^bm^and)
	       `(if ,arg1 ,arg2 'false))
	      (t `(if ,arg1 'true ,arg2))))))





#|========================================================================
Well formedness testing
========================================================================|#
(defun well-formed-events (events)
  (mapc 'well-formed-event events))

(defun well-formed-event (event)
  (selectmatch event
    ((note-lib ?fname)
     (format t "reading library ~a~%" ?fname)
     (mapc 'install-define (read-forms (concatenate 'string ?fname ".i2"))))
    ((define (?name . ?args) ?body)
     (cond ((not (every #'symbolp ?args))
	    (format t "ill formed argument list ~s~%" `(?name ,@?args))
	    nil)
	   ((not (symbolp ?name))
	    (format t "attempt to define non-symbol ~s~%" ?name)
	    nil)
	   ((assoc ?name *arglists*)
	    (format t "multiple definition of ~s~%" ?name)
	    nil)
	   (t
	    (push (cons ?name ?args) *arglists*)
	    (or (well-formed-term ?body #'(lambda (var) (member var ?args)))
		(progn (format t "in (define ~s ...)~%" `(,?name ,@?args))
		       nil)))))
    ((lemma ?term)
     (or (well-formed-term ?term #'(lambda (var) var t))
	 (progn (format t "in (lemma ... ~s)~%" (conclusion ?term))
		nil)))
    (:anything
     (format t "unrecognized event ~s~%" event)
     nil)))

(defun install-define (event)
  (selectmatch event
    ((note-lib ?fname)
     (format t "reading library ~a~%" ?fname)
     (mapc 'install-define (read-forms (concatenate 'string ?fname ".i2"))))
    ((define (?name . ?args) :anything)
     (push (cons ?name ?args) *arglists*))))

(defun conclusion (term)
  (selectmatch term
    ((^bm^implies :anything ?term2)
     (conclusion ?term2))
    (:anything term)))

(defun well-formed-term (term boundp)
  (cond ((symbolp term)
	 (or (funcall boundp term)
	     (progn (format t "unbound variable ~s~%" term)
		    nil)))
	((or (not (consp term))
	     (not (symbolp (car term))))
	 (format t "ill-formed application ~s~%" term)
	 nil)
	((eq (car term) 'quote)
	 (if (or (not (consp (cdr term)))
		 (cddr term)
		 (not (symbolp (cadr term))))
	     (progn (format t "ill formed quotation ~s~%" term)
		    nil)
	     t))
	(t (let ((pair (assoc (car term) *arglists*)))
	     (cond ((null pair)
		    (progn (format t "undefined function ~s~%" (car term))
			   nil))
		   ((not (= (length term) (length pair)))
		    (progn (format t "wrong number of arguments in ~s~%" term)
			   (break)
			   nil))
		   (t
		    (every #'(lambda (arg) (well-formed-term arg boundp)) (cdr term))))))))