defalist

(in-package "ACL2")

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

(defloop defalist-defthms
  (alist-type-fn formals
    dom-elem-type-fn
    ran-elem-type-fn
    dom-type-fn
    ran-type-fn
    guard
    theory
    binding-equal-rule-classes)
  (declare (xargs :guard (and (symbolp alist-type-fn)
        (arglistp formals)
        (consp formals)
        (symbol-listp theory))
      :mode :program))
  (for ((fn in theory))
    (append (let ((lemmaname (pack-intern-names alist-type-fn fn)) (lemma-macro-name (pack-intern alist-type-fn 'alist-type- fn '-lemma))
          (rule-classes (case fn
              (binding-equal binding-equal-rule-classes)
              (alistp '(: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-EQUAL)
      '(BOUND?-EQUAL)
      NIL))))
              (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) '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) '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)
                     (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) ,@(IF (AND (EQ FN 'ASSOC-EQUAL)
           (NOT (EQUAL RAN-ELEM-TYPE-FN *DEFALIST-TRUE-FN*)))
      `((DEFTHM ,(PACK-INTERN-NAMES ALIST-TYPE-FN (PACK-INTERN-NAMES 'CDR FN))
                (,(U::PACK-INTERN ALIST-TYPE-FN
                   'ALIST-TYPE-CDR-ASSOC-EQUAL-LEMMA)
                 ,ALIST-TYPE-FN ,DOM-TYPE-FN ,RAN-TYPE-FN ,DOM-ELEM-TYPE-FN
                 ,RAN-ELEM-TYPE-FN ,FORMALS ,GUARD)
                :RULE-CLASSES ,BINDING-EQUAL-RULE-CLASSES :HINTS
                ,(SUBST
                  (PACK-INTERN-NAMES 'ALIST-TYPE (PACK-INTERN-NAMES 'CDR FN))
                  (U::PACK-INTERN ALIST-TYPE-FN 'ALIST-TYPE- FN) HINTS)))
      NIL))))))

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

(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-equal (not (equal ran-elem-type-fn *defalist-true-fn*)))
        (bound?-equal (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*))))
        (bind-all-equal (and (not (equal dom-type-fn *defalist-true-fn*))
            (not (equal ran-type-fn *defalist-true-fn*))))
        (all-bound?-equal (not (equal dom-type-fn *defalist-true-fn*)))
        (collect-bound-equal (not (equal dom-type-fn *defalist-true-fn*)))
        (all-bindings-equal (not (equal ran-type-fn *defalist-true-fn*)))
        (t t))
      (collect fn))))

(defsection defalist
  :parents (data-structures)
  :short "Define a new alist type, and a theory of the alist type."
  :long "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-EQUAL lemma as a :TYPE-PRESCRIPTION."
    (stringp . integerp)
    (:options (:theory nth put) (:binding-equal-rule-classes :type-prescription)
              (:domain-type string-listp) (:range-type integer-listp)))
})

<p>Syntax:</p>

@({
   DEFALIST name arglist [documentation] {declaration}* type-pair [option-list]

   option-list ::= (:OPTIONS <<!options>>)

   options ::= !binding-equal-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 ::= acons | alistp | all-bindings-equal| all-bound?-equal | append |
                       assoc-equal | bind-all-equal | bind-equal | bind-pairs-equal |
                       binding-equal | bound?-equal | collect-bound-equal | domain |
                       domain-restrict-equal | pairlis$ | range | rembind-all-equal |
                       rembind-equal

   binding-equal-rule-classes-option ::= (:BINDING-EQUAL-RULE-CLASSES rule-classes)

   omit-defun-option ::= :OMIT-DEFUN
})

<p>Arguments and Values:</p>

@({
   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
})

<h3>Description:</h3>

<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

<h3>Theory</h3>

<p>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.</p>

<p>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.</p>

<h3>Options</h3>

<p>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.</p>

<dl>
<dt>:OMIT-DEFUN</dt>
<dd>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.</dd>

<dt>:THEORY</dt>
<dd>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.</dd>

<dt>:BINDING-EQUAL-RULE-CLASSES</dt>
<dd>This option specifies a value for the :RULE-CLASSES keyword for the
   DEFTHM generated for the BINDING-EQUAL function (and for CDRASSOC) applied to
   an alist recognized by the DEFALIST recognizer.  The default is :REWRITE.</dd>

<dt>:DOMAIN-TYPE</dt>
<dd>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.</dd>

<dt>:RANGE-TYPE</dt>
<dd>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.</dd>

<dt>:THEORY-NAME</dt>
<dd>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.</dd>
</dl>")