Filtering...

defenum

books/std/util/defenum
other
(in-package "STD")
other
(include-book "support")
other
(include-book "std/strings/cat" :dir :system)
other
(include-book "centaur/fty/fixtype" :dir :system)
other
(set-state-ok t)
other
(defxdoc defenum
  :parents (std/util)
  :short "Introduce an enumeration type, like an @('enum') in C."
  :long "<p>General form:</p>
@({
 (defenum name
   elements
   &key mode         ; current defun-mode by default
        parents      ; nil by default
        short        ; nil by default
        long         ; nil by default
        )
})

<p>For example,</p>

@({
 (defenum day-p
   (:monday :tuesday :wednesday :thursday :friday :saturday :sunday))
})

<p>results in a new function, @('(day-p x)'), that recognizes @(':monday'),
@(':tuesday'), etc.</p>

<h3>Usage and Options</h3>

<p>I often use keyword symbols as the elements, but any objects (even conses)
can be used.</p>

<p>The optional @(':mode') keyword can be set to @(':logic') or @(':program')
to introduce the recognizer in logic or program mode.  The default is whatever
the current default defun-mode is for ACL2, i.e., if you are already in program
mode, it will default to program mode, etc.</p>

<p>The optional @(':parents'), @(':short'), and @(':long') parameters are like
those in @(see xdoc::defxdoc).</p>

<p>If keyword @(':disable-fc') is set, it causes the generated forward chaining
rule to be disabled, which can make the admission of the defenum form and
subsequent proofs much faster when the number of elements is large.</p>

<p>If keyword @(':member') is set, then the body of the recognizer uses a
@('member-eq') check rather than an @('or').  This can speed up compilation
when the number of elements is large.  It is probably necessary to have some
rules about @('member-equal') available; loading the @('std/lists/sets') should
be sufficient.</p>

<h3>Performance Notes</h3>

<p>The recognizer just tests its argument against the elements, in order.
Because of this, you might want to order your elements so that the most common
elements come first.  For instance, @('day-p') will be fastest on @(':monday')
and slowest on @(':sunday').</p>

<p>The recognizer uses @(see eq) or @(see eql) checks where possible, so if
your enumeration includes a mix of, say, conses and atom like symbols, you may
wish to put the atoms first.</p>

<p>Checking the argument against each element is probably a perfectly good
strategy when the number of elements is small (perhaps fewer than 20) and when
the equality checks are relatively fast (e.g., symbols, characters, numbers).
It is probably is not a good strategy otherwise.  If you want to use defenum
for something more complex, it might be best to modify it to adaptively use a
fast alist or other schemes, based on the elements it is given.</p>")
other
(defund defenum-members-to-tests
  (members xvar)
  (declare (xargs :guard t))
  (if (atom members)
    nil
    (let ((e (car members)))
      (cons (cond ((symbolp e) `(eq ,STD::XVAR ',STD::E))
          ((eqlablep e) `(eql ,STD::XVAR ',STD::E))
          (t `(equal ,STD::XVAR ',STD::E)))
        (defenum-members-to-tests (cdr members) xvar)))))
other
(defund defenum-members-to-tests-equal
  (members xvar)
  (declare (xargs :guard t))
  (if (atom members)
    nil
    (let ((e (car members)))
      (cons `(equal ,STD::XVAR ',STD::E)
        (defenum-members-to-tests-equal (cdr members)
          xvar)))))
defenum-deduce-type-setfunction
(defun defenum-deduce-type-set
  (members)
  (declare (xargs :mode :program))
  (if (atom members)
    0
    (ts-union (type-set-quote (car members))
      (defenum-deduce-type-set (cdr members)))))
dumb-collect-duplicatesfunction
(defun dumb-collect-duplicates
  (x acc)
  (declare (xargs :mode :program))
  (cond ((atom x) acc)
    ((and (member-equal (car x) (cdr x))
       (not (member-equal (car x) acc))) (dumb-collect-duplicates (cdr x)
        (cons (car x) acc)))
    (t (dumb-collect-duplicates (cdr x) acc))))
strip-p-from-symbolfunction
(defun strip-p-from-symbol
  (name)
  (let* ((sname (symbol-name name)) (len (length sname)))
    (if (and (<= 2 len)
        (equal (char sname (- len 1)) #\P)
        (equal (char sname (- len 2)) #\-))
      (intern-in-package-of-symbol (subseq sname 0 (- len 2))
        name)
      name)))
other
(defconst *defenum-keywords*
  '(:mode :parents :short :long :default :fix :equiv :disable-fc :member))
defenum-fnfunction
(defun defenum-fn
  (name members rest-args state)
  (declare (xargs :mode :program))
  (b* ((__function__ 'defenum) ((unless (symbolp name)) (raise "Name must be a symbol, but is ~x0." name))
      (ctx `(defenum ,STD::NAME))
      ((mv kwd-alist rest) (extract-keywords ctx
          *defenum-keywords*
          rest-args
          nil))
      ((when rest) (raise "Extra non-keyword arguments to ~x0: ~x1~%"
          ctx
          rest))
      (mode (let ((look (assoc :mode kwd-alist)))
          (if look
            (cdr look)
            (default-defun-mode (w state)))))
      (parents (let ((look (assoc :parents kwd-alist)))
          (if look
            (cdr look)
            (or (get-default-parents (w state))
              '(undocumented)))))
      (short (cdr (assoc :short kwd-alist)))
      (long (cdr (assoc :long kwd-alist)))
      (default-look (assoc :default kwd-alist))
      (defaultp (consp default-look))
      (default (if defaultp
          (cdr default-look)
          (car (last members))))
      (?mksym-package-symbol name)
      (x (intern-in-package-of-symbol "X" name))
      ((unless (consp members)) (raise "There must be at least one member."))
      ((unless (no-duplicatesp-equal members)) (raise "The members must be a list of unique, but there are duplicate ~
                entries for ~x0."
          (reverse (dumb-collect-duplicates members nil))))
      ((unless (or (eq mode :logic) (eq mode :program))) (raise ":mode must be one of :logic or :program, but is ~x0."
          mode))
      (body (if (cdr (assoc :member kwd-alist))
          `(and (member-eq ,STD::X ',STD::MEMBERS) t)
          (cons 'or
            (defenum-members-to-tests members x))))
      (def `(defund ,STD::NAME
          (,STD::X)
          (declare (xargs :guard t))
          ,STD::BODY))
      (long `(cat ,(OR STD::LONG "")
          "<p>This is an ordinary @(see std::defenum).</p>"
          "@(def "
          ,(SYMBOL-NAME STD::NAME)
          ")"))
      (doc `(defxdoc ,STD::NAME
          :parents ,STD::PARENTS
          :short ,STD::SHORT
          :long ,STD::LONG))
      ((when (eq mode :program)) `(encapsulate nil (program) ,STD::DOC ,STD::DEF))
      (long `(cat ,STD::LONG
          "@(gthm type-when-"
          ,(SYMBOL-NAME STD::NAME)
          ")"))
      (doc `(defxdoc ,STD::NAME
          :parents ,STD::PARENTS
          :short ,STD::SHORT
          :long ,STD::LONG))
      (ts (defenum-deduce-type-set members))
      ((mv ts-concl &) (convert-type-set-to-term x
          ts
          (ens state)
          (w state)
          nil))
      (fc-rule `(,(IF (CDR (ASSOC :DISABLE-FC STD::KWD-ALIST))
     'STD::DEFTHMD
     'STD::DEFTHM) ,(STD::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME STD::NAME) "-POSSIBILITIES") STD::NAME)
          (implies (,STD::NAME ,STD::X)
            (or . ,(STD::DEFENUM-MEMBERS-TO-TESTS-EQUAL STD::MEMBERS STD::X)))
          :rule-classes :forward-chaining))
      (name-without-p (strip-p-from-symbol name))
      (fixname (or (cdr (assoc :fix kwd-alist))
          (intern-in-package-of-symbol (concatenate 'string
              (symbol-name name-without-p)
              "-FIX")
            name)))
      (equivname (or (cdr (assoc :equiv kwd-alist))
          (intern-in-package-of-symbol (concatenate 'string
              (symbol-name name-without-p)
              "-EQUIV")
            name)))
      (fix `(defund-inline ,STD::FIXNAME
          (,STD::X)
          (declare (xargs :guard (,STD::NAME ,STD::X)))
          (mbe :logic (if (,STD::NAME ,STD::X)
              ,STD::X
              ',STD::DEFAULT)
            :exec ,STD::X)))
      (fix-type `(defthm ,(STD::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING "RETURN-TYPE-OF-" (SYMBOL-NAME STD::FIXNAME)) STD::NAME)
          (,STD::NAME (,STD::FIXNAME ,STD::X))))
      (fix-id `(defthm ,(STD::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME STD::FIXNAME) "-IDEMPOTENT") STD::NAME)
          (implies (,STD::NAME ,STD::X)
            (equal (,STD::FIXNAME ,STD::X) ,STD::X)))))
    `(encapsulate nil
      (logic)
      ,STD::DOC
      ,STD::DEF
      (local (in-theory (enable ,STD::NAME)))
      (with-output :off observation
        (defthm ,(STD::MKSYM 'STD::TYPE-WHEN- STD::NAME)
          (implies (,STD::NAME ,STD::X) ,STD::TS-CONCL)
          :rule-classes :compound-recognizer))
      ,STD::FC-RULE
      (local (in-theory (disable ,STD::NAME)))
      ,STD::FIX
      (local (in-theory (enable ,STD::FIXNAME)))
      ,STD::FIX-TYPE
      ,STD::FIX-ID
      (table defenum-table
        ',STD::NAME
        ',(LIST (CONS :MEMBERS STD::MEMBERS) (CONS :FIX STD::FIXNAME)
       (CONS :EQUIV STD::EQUIVNAME) (CONS :MODE STD::MODE)
       (CONS :DEFAULT STD::DEFAULT)))
      (local (in-theory (disable ,STD::FIXNAME)))
      (deffixtype ,STD::NAME
        :pred ,STD::NAME
        :fix ,STD::FIXNAME
        :equiv ,STD::EQUIVNAME
        :define t))))
defenummacro
(defmacro defenum
  (name members &rest keys)
  `(make-event (defenum-fn ',STD::NAME
      ',STD::MEMBERS
      ',STD::KEYS
      state)))