; ACL2 books for typed alists
; Copyright (C) 1997  Computational Logic, Inc.

; This book is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.

; This book is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public License
; along with this book; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

; Written by: Bill Bevier and Bishop Brock
; Computational Logic, Inc.
; 1717 West Sixth Street, Suite 290
; Austin, TX 78703-4776 U.S.A.

(in-package "ACL2")

(include-book "alist-defuns")
(include-book "list-defuns")
(include-book "utilities")

(encapsulate ((domain-elem-type (x) boolean)
	      (domain-type (l) boolean)
	      (range-elem-type (x) boolean)
	      (range-type (l) boolean)
	      (alist-type (a) boolean))
  (local (in-theory '(ground-zero)))
  (local (defun domain-elem-type (x)
	   (symbolp x)))
  (local (defun domain-type (l)
	   (symbol-listp l)))
  (local (defun range-elem-type (x)
	   (integerp x)))
  (local (defun range-type (l)
	   (integer-listp l)))
  (local (defun alist-type (a)
	   (cond ((atom a) (eq a nil))
		 (t (and (consp (car a))
			 (domain-elem-type (caar a))
			 (range-elem-type (cdar a))
			 (alist-type (cdr a)))))))
  (defthm domain-type-domain-elem-type
    (and (domain-type nil)
	 (equal (domain-type (cons x l))
		(and (domain-elem-type x)
		     (domain-type l)))))
  (defthm range-type-range-elem-type
    (and (range-type nil)
	 (equal (range-type (cons x l))
		(and (range-elem-type x)
		     (range-type l)))))
  (defthm alist-type-defun
    (iff (alist-type l)
	 (cond ((atom l) (eq l nil))
	       (t (and (consp (car l))
		       (domain-elem-type (caar l))
		       (range-elem-type (cdar l))
		       (alist-type (cdr l))))))
    :rule-classes ((:rewrite :corollary
			     (implies (atom l)
				      (equal (alist-type l) (null l))))
		   (:rewrite :corollary
			     (equal (alist-type (cons x l))
				    (and (consp x)
					 (domain-elem-type (car x))
					 (range-elem-type (cdr x))
					 (alist-type l))))))
  )


;; Some utility functions

(defun replace-equal (a b l)
  (declare (xargs :guard (true-listp l)))
  (cond ((endp l) nil)
	((equal (car l) a) (cons b (replace-equal a b (cdr l))))
	(t (cons (car l) (replace-equal a b (cdr l))))))

(defun my-conjoin (termlist1 termlist2)
  (declare (xargs :guard (and (true-listp termlist1)
			      (true-listp termlist2)
			      (or (consp termlist1) (consp termlist2)))))
  (let ((termlist (append termlist1 termlist2)))
    (cond ((= (len termlist) 1)
	   (car termlist))
	  (t (fcons-term 'and termlist)))))

(mutual-recursion

 (defun my-conjuncts (term)
   (cond ((eq term t) ())
	 ((atom term) (list term))
	 ((eq (car term) 'and) (my-conjuncts-list (cdr term)))
	 (t (list term))))

 (defun my-conjuncts-list (termlist)
   (cond ((atom termlist) nil)
	 (t (append (my-conjuncts (car termlist))
		    (my-conjuncts-list (cdr termlist))))))
 )


; For each lemma in the theory, the lemma term is defined by a macro
; to make it easy to instantiate. The lemma is then proved. 


; The macros in the following script generate forms that are believed to be
; lemmas about list predicates. The arguments to these macros have the following meanings.
;
; alist-type-fn: a symbol that names a predicate which recognizes a typed alist
; dom-type-fn
; ran-type-fn
; dom-elem-type-fn
; ran-elem-type-fn
; 
; formals:      the formal parameter list to alist-type-fn
;               We assume that the other type fns are unary predicates, either
;               symbols or lambda expressions.
;
; guard         either 't, or an expression in the formal parameters
;
; Example: 
;
;  (defun bound-numberp (x lub) 
;    (and (acl2-numberp x) (acl2-numberp lub) (< x lub)))
;
;  (defun bound-number-listp (l lub) 
;    (cond ((atom l) t)
;          (t (and (bound-numberp (car l) lub)
;                  (bound-number-listp (cdr l) lub)))))
;

(defmacro alist-type-alistp-lemma (alist-type-fn dom-type-fn
						 ran-type-fn
						 dom-elem-type-fn
						 ran-elem-type-fn
						 formals
						 &optional (guard 't))
  (declare (ignore dom-type-fn ran-type-fn
		   dom-elem-type-fn ran-elem-type-fn))
  `(implies ,(my-conjoin (my-conjuncts guard)
			 `((,alist-type-fn ,@formals)))
	    (alistp l)))
					      
(defthm alist-type-alistp
  (alist-type-alistp-lemma alist-type domain-type range-type 
			   domain-elem-type range-elem-type
			   (l))
  :hints (("Goal" :induct t)))

(in-theory (disable alist-type-alistp))

(defmacro alist-type-bind-lemma (alist-type-fn dom-type-fn
					       ran-type-fn
					       dom-elem-type-fn
					       ran-elem-type-fn
					       formals
					       &optional (guard 't))
  (declare (ignore dom-type-fn ran-type-fn))
  (let* ((vars (u::unique-symbols 2 (intern-in-package-of-symbol "X" alist-type-fn) formals))
	 (var1 (car vars))
	 (var2 (cadr vars)))
    `(implies ,(my-conjoin (my-conjuncts guard)
			   `((,alist-type-fn ,@formals)
			     (,dom-elem-type-fn ,var1)
			     (,ran-elem-type-fn ,var2)))
	      (,alist-type-fn ,@(replace-equal 'l 
					       `(bind ,var1 ,var2 l)
					       formals)))))
  
(defthm alist-type-bind
  (alist-type-bind-lemma alist-type domain-type range-type 
			 domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :induct t)))


(defmacro alist-type-fbind-lemma (alist-type-fn dom-type-fn
						ran-type-fn
						dom-elem-type-fn
						ran-elem-type-fn
						formals
						&optional (guard 't))
  (declare (ignore dom-type-fn ran-type-fn))
  (let* ((vars (u::unique-symbols 2 (intern-in-package-of-symbol "X" alist-type-fn) formals))
	 (var1 (car vars))
	 (var2 (cadr vars)))
    `(implies ,(my-conjoin (my-conjuncts guard)
			   `((,alist-type-fn ,@formals)
			     (,dom-elem-type-fn ,var1)
			     (,ran-elem-type-fn ,var2)))
	      (,alist-type-fn ,@(replace-equal 'l 
					       `(fbind ,var1 ,var2 l)
					       formals)))))
  
(defthm alist-type-fbind
  (alist-type-fbind-lemma alist-type domain-type range-type 
			  domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
	   :in-theory (enable alist-type-alistp fbind))))

(defmacro alist-type-binding-lemma (alist-type-fn dom-type-fn
						  ran-type-fn
						  dom-elem-type-fn
						  ran-elem-type-fn
						  formals
						  &optional (guard 't))
  (declare (ignore dom-type-fn ran-type-fn dom-elem-type-fn))
  (let* ((vars (u::unique-symbols 1 (intern-in-package-of-symbol "X" alist-type-fn) formals))
	 (var (car vars)))
    `(implies ,(my-conjoin (my-conjuncts guard)
			   `((,alist-type-fn ,@formals)
			     (bound? ,var l)))
	      (,ran-elem-type-fn (binding ,var l)))))

(defthm alist-type-binding
  (alist-type-binding-lemma alist-type domain-type range-type 
			    domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :in-theory (enable alist-type-alistp binding bound?))))
  
(defmacro alist-type-bound?-lemma (alist-type-fn dom-type-fn
						  ran-type-fn
						  dom-elem-type-fn
						  ran-elem-type-fn
						  formals
						  &optional (guard 't))
  (declare (ignore dom-type-fn ran-type-fn ran-elem-type-fn))
  (let* ((vars (u::unique-symbols 1 (intern-in-package-of-symbol "X" alist-type-fn) formals))
	 (var (car vars)))
    `(implies ,(my-conjoin (my-conjuncts guard)
			   `((,alist-type-fn ,@formals)
			     (not (,dom-elem-type-fn ,var))))
	      (not (bound? ,var l)))))

(defthm alist-type-bound?
  (alist-type-bound?-lemma  alist-type domain-type range-type 
		      domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :in-theory (enable alist-type-alistp bound?))))

(defmacro alist-type-domain-lemma (alist-type-fn dom-type-fn
						 ran-type-fn
						 dom-elem-type-fn
						 ran-elem-type-fn
						 formals
						 &optional (guard 't))
  (declare (ignore ran-type-fn dom-elem-type-fn ran-elem-type-fn))
  `(implies ,(my-conjoin (my-conjuncts guard)
			 `((,alist-type-fn ,@formals)))
	    (,dom-type-fn (domain l))))

(defthm alist-type-domain
  (alist-type-domain-lemma  alist-type domain-type range-type 
			    domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :in-theory (enable alist-type-alistp domain))))

(defmacro alist-type-range-lemma (alist-type-fn dom-type-fn
						 ran-type-fn
						 dom-elem-type-fn
						 ran-elem-type-fn
						 formals
						 &optional (guard 't))
  (declare (ignore dom-type-fn dom-elem-type-fn ran-elem-type-fn))
  `(implies ,(my-conjoin (my-conjuncts guard)
			 `((,alist-type-fn ,@formals)))
	    (,ran-type-fn (range l))))

(defthm alist-type-range
  (alist-type-range-lemma   alist-type domain-type range-type 
			    domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :in-theory (enable alist-type-alistp range))))

(defmacro alist-type-rembind-lemma (alist-type-fn dom-type-fn
						  ran-type-fn
						  dom-elem-type-fn
						  ran-elem-type-fn
						  formals
						  &optional (guard 't))
  (declare (ignore dom-type-fn ran-type-fn dom-elem-type-fn ran-elem-type-fn))
  (let* ((vars (u::unique-symbols 1 (intern-in-package-of-symbol "X" alist-type-fn) formals))
	 (var (car vars)))
    `(implies ,(my-conjoin (my-conjuncts guard)
			   `((,alist-type-fn ,@formals)))
	      (,alist-type-fn ,@(replace-equal 'l `(rembind ,var l) formals)))))

(defthm alist-type-rembind
  (alist-type-rembind-lemma alist-type domain-type range-type 
			    domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :induct t)))

(defmacro alist-type-pairlis$-lemma (alist-type-fn dom-type-fn
						  ran-type-fn
						  dom-elem-type-fn
						  ran-elem-type-fn
						  formals
						  &optional (guard 't))
  (declare (ignore dom-elem-type-fn ran-elem-type-fn))
  (let* ((vars (u::unique-symbols 2 (intern-in-package-of-symbol "X" alist-type-fn) formals))
	 (var1 (car vars))
	 (var2 (cadr vars)))
    `(implies ,(my-conjoin (my-conjuncts guard)
			   `((true-listp ,var1)
			     (,dom-type-fn ,var1)
			     (,ran-type-fn ,var2)
			     (eql (len ,var1) (len ,var2))))
	      (,alist-type-fn ,@(replace-equal 'l
					       `(pairlis$ ,var1 ,var2)
					       formals)))))

(defthm alist-type-pairlis$
  (alist-type-pairlis$-lemma alist-type domain-type range-type 
			     domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :induct t)))

(defmacro alist-type-domain-restrict-lemma  (alist-type-fn dom-type-fn
						  ran-type-fn
						  dom-elem-type-fn
						  ran-elem-type-fn
						  formals
						  &optional (guard 't))
  (declare (ignore dom-type-fn ran-type-fn dom-elem-type-fn ran-elem-type-fn))
  (let* ((vars (u::unique-symbols 1 (intern-in-package-of-symbol "L" alist-type-fn) formals))
	 (var (car vars)))
    `(implies ,(my-conjoin (my-conjuncts guard)
			   `((,alist-type-fn ,@formals)))
	      (,alist-type-fn ,@(replace-equal 'l
					       `(domain-restrict ,var l)
					       formals)))))

(defthm alist-type-domain-restrict 
  (alist-type-domain-restrict-lemma alist-type domain-type range-type 
				    domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :induct t)))

(defmacro alist-type-domain-anti-restrict-lemma  (alist-type-fn dom-type-fn
						  ran-type-fn
						  dom-elem-type-fn
						  ran-elem-type-fn
						  formals
						  &optional (guard 't))
  (declare (ignore dom-type-fn ran-type-fn dom-elem-type-fn ran-elem-type-fn))
  (let* ((vars (u::unique-symbols 1 (intern-in-package-of-symbol "L" alist-type-fn) formals))
	 (var (car vars)))
    `(implies ,(my-conjoin (my-conjuncts guard)
			   `((,alist-type-fn ,@formals)))
	      (,alist-type-fn ,@(replace-equal 'l
					       `(domain-anti-restrict ,var l)
					       formals)))))

(defthm alist-type-domain-anti-restrict 
  (alist-type-domain-anti-restrict-lemma alist-type domain-type range-type 
				    domain-elem-type range-elem-type (l))
  :rule-classes nil
  :hints (("Goal" :induct t)))

; ------------------------------------------------------------
; Typed ALists
; ------------------------------------------------------------

(defconst *defalist-true-fn* '(lambda (x) (declare (ignore x)) t)
  "The single-argument predicate that is always true.")

(defconst *defalist-theory-options*
  '(alistp bind binding bound? domain fbind  
	   domain-restrict domain-anti-restrict pairlis$ range rembind)
  "This list contains all of the symbols recognized as valid options for
   the DEFALIST :THEORY option.")

(defun pack-intern-names (name1 name2)
  (u::pack-intern name1 name1 "-" name2))

(u::defloop pack-intern-all-names (name l)
	    (for ((x in l))
		 (collect (pack-intern-names name x))))

; DEFALIST-DEFTHMS.
; Generate a list of DEFTHM forms. These defthms explain
; the properties of standard list operations with 
; respect to a typed list predicate.
; For arguments, see documentation for DEF-TYPED-LIST
; macro below.

(u::defloop defalist-defthms (alist-type-fn formals dom-elem-type-fn ran-elem-type-fn 
					    dom-type-fn ran-type-fn guard theory binding-rule-classes)
   (declare (xargs :guard (and (symbolp alist-type-fn)
			       (arglistp formals)
			       (consp formals)
			       (symbol-listp theory))
		   :mode :program))
   (for ((fn in theory))
	(collect (let ((lemmaname (pack-intern-names alist-type-fn fn))
		       (lemma-macro-name (u::pack-intern alist-type-fn 'alist-type- fn '-lemma))
		       (rule-classes (case fn
				       (binding binding-rule-classes)
				       (alistp '(:rewrite :forward-chaining))
				       (t '(:rewrite))))
		       (hints (if (or (consp (my-conjuncts guard))
				      (and (equal dom-type-fn *defalist-true-fn*)
					   (not (equal dom-elem-type-fn *defalist-true-fn*)))
				      (and (equal ran-type-fn *defalist-true-fn*)
					   (not (equal ran-elem-type-fn *defalist-true-fn*)))
				      (> (len formals) 1))
				  `(("Goal" :in-theory (enable ,fn ,@(if (eq fn 'binding) '(bound?) ()))))
				;; The functional instance of the domain and range element types are
				;; presented as lambda forms, since these may be defined as macros.
				(let ((domain-elem-type-instance (if (equal dom-elem-type-fn *defalist-true-fn*) 
								     (remove-equal '(declare (ignore x)) dom-elem-type-fn)
								   (cond ((and (consp dom-elem-type-fn)
									       (eq (car dom-elem-type-fn) 'lisp::lambda))
									  dom-elem-type-fn)
									 (t `(lambda (x) (,dom-elem-type-fn x))))))
				      (domain-type-instance (if (equal dom-type-fn *defalist-true-fn*) 
								(remove-equal '(declare (ignore x)) dom-type-fn)
							      dom-type-fn))
				      (range-elem-type-instance (if (equal ran-elem-type-fn *defalist-true-fn*) 
								    (remove-equal '(declare (ignore x)) ran-elem-type-fn)
								  (cond ((and (consp ran-elem-type-fn)
									      (eq (car ran-elem-type-fn) 'lisp::lambda))
									 ran-elem-type-fn)
									(t `(lambda (x) (,ran-elem-type-fn x))))))
				      (range-type-instance (if (equal ran-type-fn *defalist-true-fn*) 
							       (remove-equal '(declare (ignore x)) ran-type-fn)
							     ran-type-fn)))
				  `(("Goal" :do-not-induct t
				     :use  (:functional-instance
					    ,(u::pack-intern alist-type-fn 'alist-type- fn)
					    ;; In the case a type fn is (lambda (x) (declare (ignore x)) t)
					    ;; we have to remove the (declare (ignore x)) to make it a pseudo-lambda
					    ;; expression. See :doc lemma-instance.
					    (domain-elem-type ,domain-elem-type-instance)
					    (domain-type ,domain-type-instance)
					    (range-elem-type ,range-elem-type-instance)
					    (range-type ,range-type-instance)
					    (alist-type ,alist-type-fn))))))))
		   `(defthm ,lemmaname
		      (,lemma-macro-name ,alist-type-fn ,dom-type-fn ,ran-type-fn ,dom-elem-type-fn ,ran-elem-type-fn
					 ,formals ,guard)
		      :rule-classes ,rule-classes
		      :hints ,hints)))))

(defconst *defalist-options* '(:BINDING-RULE-CLASSES :THEORY :OMIT-DEFUN :DOMAIN-TYPE :RANGE-TYPE :THEORY-NAME)
  "This list contains all of the  valid keyword options for DEFALIST.")

(defun defalist-check-syntax (name formals body)
  "Return NIL if no errors, otherwise crash."
  (declare (xargs :mode :program))
  (cond
   ((not (symbolp name))
    (u::bomb 'DEFALIST "The function name must be a symbol, but ~p0 is not."
	     name))
   ((not (true-listp formals))
    (u::bomb 'DEFALIST "The argument list ~p0 is not a true list." formals))
   ((not (arglistp formals))
    (mv-let (elmt msg) (find-first-bad-arg formals)
      (u::bomb 'DEFALIST "The argument list ~p0 is not valid because the ~
                          element ~p1 ~@2." formals elmt msg)))
   ((let* ((formal-strings (u::mapcar-string formals))
	   (l-tail (member-equal "L" formal-strings))
	   (multiple-ls (member-equal "L" (cdr l-tail))))
      (or (not l-tail) multiple-ls))
    (u::bomb 'DEFALIST "The formal argument list to DEFALIST must be a valid ~
                       functional argument list that contains exactly 1 ~
                       symbol whose print-name is \"L\", but ~p0 is not."
	     formals))
   ((null body) (u::bomb 'DEFALIST "The function body is empty!"))
   (t (let* ((last-form (car (last body)))
	     (options? (and (>= (len body) 2)
			    (true-listp last-form)
			    (eq (car last-form) :OPTIONS)))
	     (predicate (if options?
			    (car (last (butlast body 1)))
			  last-form)))
	(cond
	 ((and (consp predicate)
	       (let ((d (car predicate))
		     (r (cdr predicate)))
		 (and (or (symbolp d)
			  (and (true-listp d)
			       (>= (len d) 3)
			       (eq (first d) 'LISP::LAMBDA)
			       (arglistp (second d))
			       (equal (len (second d)) 1)))
		      (or (symbolp r)
			  (and (true-listp r)
			       (>= (len r) 3)
			       (eq (first r) 'LISP::LAMBDA)
			       (arglistp (second r))
			       (equal (len (second r)) 1))))))
	  NIL)
	 (t (u::bomb 'DEFALIST "The DEFALIST predicate designator must be a ~
                             pair (d . r) where d is either a function symbol
                             or a 1-argument LAMBDA function, and r ~
                             is either a function symbol or a 1-argument
                             LAMBDA function. ~p0 does not satisfy this
                             requirement." predicate))))))) 

(deftheory minimal-theory-for-defalist
  (union-theories
   (current-theory 'ground-zero)
   (current-theory 'alist-defuns)))

;; It is ok to avoid placing a type restriction on the domain or range of a defalist.
;; When a type is omitted, certain lemmas should be omitted from the generated theory.
;; This filter weeds out the theory elements that should be avoided in these cases.

(u::defloop filter-alist-theory (theory dom-elem-type-fn ran-elem-type-fn dom-type-fn ran-type-fn)
	    (for ((fn in theory))
		 (when (case fn
			 (binding (not (equal ran-elem-type-fn *defalist-true-fn*)))
			 (bound? (not (equal dom-elem-type-fn *defalist-true-fn*)))
			 (domain (not (equal dom-type-fn *defalist-true-fn*)))
			 (range (not (equal ran-type-fn *defalist-true-fn*)))
			 (pairlis$ (and (not (equal dom-type-fn *defalist-true-fn*))
					(not (equal ran-type-fn *defalist-true-fn*))))					
			 (t t))
		   (collect fn))))
			    
(defmacro defalist (name formals &rest body)
  ":doc-section defalist
  Define a new alist type, and a theory of the alist type.
  ~/
 Examples:

  (defalist symbol-to-integer-alistp (l)
    \"Recognizes an alist mapping symbols to integers.\"
    (symbolp . integerp))   
 
  (defalist symbol-to-bnatural-alistp (l lub)
    \"Recognizes an alists mapping symbols to  naturals bounded by lub.\"
    (symbolp . (lambda (x) (bnaturalp x lub))))
 
  (defalist symbol-alistp (l)
    \"Define an alist theory alists from an unspecified domain type to
     symbols.\"
    ((lambda (x) t) . symbolp)
    (:options :omit-defun (:range-type symbol-listp)))
 
  (defalist string-to-integer-alistp (l)
    \"Recognizes an alist mapping strings to integers. Produce a minimal 
     theory, and store the BINDING lemma as a :TYPE-PRESCRIPTION.\"
    (stringp . integerp)
    (:options (:theory nth put) (:binding-rule-classes :type-prescription)
              (:domain-type string-listp) (:range-type integer-listp)))
 ~/
 Syntax:

   DEFALIST name arglist [documentation] {declaration}* type-pair [option-list]
 
   option-list ::= (:OPTIONS <<!options>>)
 
   options ::= !binding-rule-classes-option |
               !omit-defun-option |
               !theory-option |
               !domain-type-option |
               !range-type-option |
               !theory-name-option 
 
   theory-option ::= (:THEORY <<!alist-functions>>)

   theory-name-option ::= (:THEORY-NAME theory-name)
 
   alist-functions ::= BIND | BINDING | BOUND? | FBIND | DOMAIN | 
                       RANGE | PAIRLIS$ | REMBIND | 
                       DOMAIN-RESTRICT | DOMAIN-ANTI-RESTRICT
 
   binding-rule-classes-option ::= (:BINDING-RULE-CLASSES rule-classes)
 
   omit-defun-option ::= :OMIT-DEFUN

 Arguments and Values:
 
   arglist -- an argument list satisfying ACL2::ARGLISTP, and containing
     exactly one symbol whose `print-name' is \"L\".
 
   declaration -- any valid declaration.
 
   documentation -- a string; not evaluated.
  
   name -- a symbol.

   theory-name -- any symbol that is a legal name for a deftheory event.
  
   type-pair -- A pair (d . r) where d and r are either a function symbol
     or a one argument LAMBDA function or the constant T. 
     d designates a predicate to be applied to each element of the domain 
     of the alist, and r designates a predicate to be applied to each element
     of the range of the alist. T means no type restriction.

   rule-classes -- any form legal as an argument to the :RULE-CLASSES keyword
    of DEFTHM.

   Acl2-theory-expression -- Any legal Acl2 theory expression

 Description:

  DEFALIST defines a recognizer for association lists whose pairs map
  keys of a given type to values of a given type, and by default creates 
  an extensive theory for alists of the newly defined type.

  To define an alist type with DEFALIST you must supply a name for the alist
  recognizer, an argument list for the recognizer, and predicate designator for
  elements of the alist's range. The name may be any symbol.  The argument list
  must be valid as a functional argument list, and must contain exactly one
  symbol whose `print-name'is \"L\".  By convention this is the alist argument
  recognized by the function defined by DEFALIST.

  The type of the domain and range of the alist is given by a pair (d . r)
  where d identifies the type of an element of the alist's domain, and r
  specifies the type of an element of the alist's range. Either of these
  may be specified by a symbol which names a one-argument function (or macro)
  which tests the elements of the domain and range of L. Either of d and r may
  also be specified as a single-argument LAMBDA function. Finally, either of d
  and r may be specified as the constant t, indicating no type constraint.

  Any number of other arguments to the alist functions may be supplied, 
  but only the L argument will change in the recursive structure of the recognizer.

  Note that DEFALIST does not create any guards for L or any other argument.
  Guards may be specified in the usual way since any number of DECLARE forms
  may preceed the predicate specification in the DEFALIST form.  Bear in mind
  that if you are defining a function to be used as a guard, then you are
  advised to consider what impact guarding the arguments of the function may
  have on its utility.  In general the most useful guard functions are those
  that are guard-free.

 Theory:

  By default, DEFALIST creates an extensive theory for the recognized alists.
  This theory contains appropriate lemmas for all of the alist functions 
  appearing in the `alist-functions' syntax description above.  One can select
  a subset of this theory to be generated by using the :THEORY option
  (see below).  DEFALIST always creates a :FORWARD-CHAINING rule from the 
  recognizer to ALISTP.

  DEFALIST also creates a DEFTHEORY event that lists all of the lemmas created
  by the DEFALIST.  The name of the theory is formed by concatenating the
  function name and the string \"-THEORY\", and INTERNing the resulting string
  in the package of the function name.

 Options:

  DEFALIST options are specified with a special :OPTIONS list systax.  If
  present, the :OPTIONS list must appear as the last form in the body of the
  DEFALIST.

  :OMIT-DEFUN

    If the :OMIT-DEFUN keyword is present then the definition will not be
    created.  Instead, only the list theory for the function is
    generated. Use this option to create a list theory for recognizers
    defined elsewhere.

  :THEORY  

   This option is used to specify that only a subset of the list theory be
   created.  In the STRINGP-LISTP example above we specify that only lemmas
   about STRINGP-LISTP viz-a-viz NTH and PUT are to be generated.  By default
   the complete list theory for the recognizer is created.  If the option is
   given as (:THEORY) then the entire theory will be suppressed,
   except for the :FORWARD-CHAINING rule from the recognizer to TRUE-LISTP.

  :BINDING-RULE-CLASSES

   This option specifies a value for the :RULE-CLASSES keyword for the 
   DEFTHM generated for the BINDING function applied to an alist recognized 
   by the DEFALIST recognizer.   The default is :REWRITE.

  :DOMAIN-TYPE

   This option specifies a predicate that recognizes a list of domain elements.
   It may be either a symbol or LAMBDA form. If present, and when not prevented
   by a :THEORY specification, a rewrite rule for the type of the domain
   will be generated. A lemma will be generated to check the compatibility
   of the specified domain type and domain element type.

  :RANGE-TYPE

   This option specifies a predicate that recognizes a list of range elements.
   It may be either a symbol or LAMBDA form. If present, and when not prevented
   by a :THEORY specification, a rewrite rule for the type of the range
   will be generated.  A lemma will be generated to check the compatibility
   of the specified range type and domain element type.

  :THEORY-NAME

   This option allows the user to define the name of the deftheory event
   that is automatically generated, and which includes the defthms that
   are generated. 
   ~/"
  (let*
    ((syntax-err (defalist-check-syntax name formals body))
     (last-form (car (last body)))
     (options? (and (>= (len body) 2)
                    (true-listp last-form)
                    (eq (car last-form) :OPTIONS)))
     (option-list (if options? (cdr last-form) nil))
     (type-pair (if options?
		    (car (last (butlast body 1)))
		  last-form))
     (dom-elemtype (if (eq (car type-pair) t)
		       *defalist-true-fn*
		     (car type-pair)))
     (ran-elemtype (if (eq (cdr type-pair) t)
		       *defalist-true-fn*
		     (cdr type-pair)))
     (l (nth (position$ "L" (u::mapcar-string formals)) formals))
     (guard (u::get-guards-from-body body))
     (ctx 'DEFALIST)
     (option-err (u::get-option-check-syntax
                  ctx option-list *defalist-options* nil nil))
     (omit-defun (u::get-option-as-flag ctx :OMIT-DEFUN option-list))
     (theory (u::get-option-subset
              ctx :THEORY option-list
	      *defalist-theory-options* *defalist-theory-options*))
     (binding-rule-classes (u::get-option-argument
			    ctx :BINDING-RULE-CLASSES option-list :FORM
			    :REWRITE :REWRITE))
     (domain-type (u::get-option-argument
		   ctx :DOMAIN-TYPE option-list :FORM 
		   *defalist-true-fn*
		   *defalist-true-fn*))
     (range-type (u::get-option-argument
		  ctx :RANGE-TYPE option-list :FORM
		  *defalist-true-fn*
		  *defalist-true-fn*))
     (theory-name (u::get-option-argument
		   ctx :THEORY-NAME option-list :FORM
		   (u::pack-intern name name "-THEORY") (u::pack-intern name name "-THEORY")))
     )
    (or
     syntax-err				;Both better be NIL.
     option-err
     (and (equal dom-elemtype *defalist-true-fn*)
	  (not (equal domain-type *defalist-true-fn*)))
     (and (equal ran-elemtype *defalist-true-fn*)
	  (not (equal range-type *defalist-true-fn*)))

     ;; We always generate the alistp event.

     (let ((theory1 
	    (union-equal '(alistp)
			 (filter-alist-theory theory dom-elemtype ran-elemtype domain-type range-type))))
	    
       `(ENCAPSULATE ()

		     ;; We do the definition and proofs in a minimal theory for speed.
		     ;; The first label is for proofs that need the original theory.

		     (LOCAL (DEFLABEL DEFALIST-RESERVED-LABEL))

		     ,@(if omit-defun
			   nil
			 (list
			  `(DEFUN ,name ,formals
			     ,@(butlast body (if options? 2 1))
			     (COND ((ATOM ,l) (NULL ,l))
				   (T (AND (consp (CAR ,l))
					   (,dom-elemtype (caar ,l))
					   (,ran-elemtype (cdar ,l))
					   (,name ,@(replace-equal l `(CDR ,l) formals))))))
			  ))
         
		     ,@(defalist-defthms
			 name formals dom-elemtype ran-elemtype domain-type range-type
			 guard theory1 binding-rule-classes)

		     (DEFTHEORY ,theory-name
		       ',(pack-intern-all-names name theory1))))
    )))

#|

Examples:

(defalist symbol-to-integer-alistp (l)
  "Recognizes an alist mapping symbols to integers."
  (symbolp . integerp)
  (:options (:domain-type symbol-listp)
	    (:range-type integer-listp)))

(defmacro naturalp (n) 
  `(and (integerp ,n) (<= 0 ,n)))

(defun natural-listp (l)
  (if (atom l) t
    (and (naturalp (car l)) (natural-listp (cdr l)))))
 
(defalist symbol-to-natural-alistp (l)
  "Recognizes an alists mapping symbols to  naturals bounded by lub."
  (symbolp . naturalp)
  (:options (:domain-type symbol-listp)
	    (:range-type natural-listp)
	    (:theory binding)
	    (:theory-name sym->nat-theory)))
 
(defalist string-to-integer-alistp (l)
  "Recognizes an alist mapping strings to integers. Produce a minimal 
  theory, and store the BINDING lemma as a :TYPE-PRESCRIPTION."
  (stringp . integerp)
  (:options (:theory bind binding bound?)
	    (:binding-rule-classes :type-prescription)
	    (:domain-type string-listp) 
	    (:range-type integer-listp)))

(defalist symbol-alistp (l)
  "Define an alist theory for alists mapping symbols to an arbitrary range type."
  (symbolp . t)
  (:options :omit-defun (:domain-type symbol-listp)))

(defalist anything-to-integer-alistp (l)
  (t . integerp)
  (:options (:range-type integer-listp)
	    (:theory binding)))

|#