Filtering...

ihs-init

books/ihs/ihs-init

Included Books

ihs-doc-topic utilities
other
(in-package "ACL2")
include-book
(include-book "ihs-doc-topic")
include-book
(include-book "data-structures/utilities" :dir :system)
other
(defxdoc ihs-init
  :parents (ihs)
  :short "The root of the IHS (Integer Hardware Specification) library hierarchy."
  :long "<p>The @('ihs-init') book is included by every book in the IHS
hierarchy.  It contains:</p>

<ul>

<li>Definitions of CLTL functions that should be part of the ACL2 BOOT-STRAP
theory.  Since ACL2 won't let us redefine any Common Lisp symbol, these
functions are uniformly named by @('<CLTL name>$').</li>

<li>Functions that are not defined by CLTL, but that are otherwise candidates
for the ACL2 boot-strap theory.</li>

<li>Unassigned functions that are general purpose, and will probably find a
place in another book someday.</li>

<li>Definition of macros, macro helper-functions, and utility functions that
are used throughout the IHS libraries.  We have no thought of ever verifying
any of these.  Thus, the guards of certain functions may be just strong enough
to get the functions admitted.</li>

</ul>")
when$clmacro
(defmacro when$cl
  (test &rest forms)
  (if (consp forms)
    (if (consp (cdr forms))
      `(if ,TEST
        (progn ,@FORMS)
        nil)
      `(if ,TEST
        ,@FORMS
        nil))
    `(if ,TEST
      nil
      nil)))
unless$clmacro
(defmacro unless$cl
  (test &rest forms)
  (if (consp forms)
    (if (consp (cdr forms))
      `(if ,TEST
        nil
        (progn ,@FORMS))
      `(if ,TEST
        nil
        ,@FORMS))
    `(if ,TEST
      nil
      nil)))
pairwise-listfunction
(defun pairwise-list
  (x y)
  "Like PAIRLIS, but LISTs instead of CONSes."
  (declare (xargs :guard (and (true-listp x)
        (true-listp y)
        (eql (length x) (length y)))))
  (cond ((endp x) nil)
    (t (cons (list (car x) (car y))
        (pairwise-list (cdr x) (cdr y))))))
let*$fnfunction
(defun let*$fn
  (bindings body)
  "LET* for the case that BODY is a single form."
  (declare (xargs :guard (eqlable-alistp bindings)))
  (cond ((endp bindings) body)
    (t `(let (,(CAR BINDINGS))
        ,(LET*$FN (CDR BINDINGS) BODY)))))
let*$macro
(defmacro let*$
  (bindings &rest body)
  "A redefinition of LET* that handles declarations, and removes the old
  `no-duplicatesp' guard."
  (declare (xargs :guard (eqlable-alistp bindings)))
  (cond ((and (consp body) (consp (cdr body))) (let ((unique-vars (remove-duplicates (strip-cars bindings))))
        (let ((unique-bindings (pairwise-list unique-vars unique-vars)))
          (let ((new-body `(let ,UNIQUE-BINDINGS
                 ,@BODY)))
            (let*$fn bindings new-body)))))
    (t (let*$fn bindings (car body)))))
constant-syntaxpfunction
(defun constant-syntaxp
  (x)
  (declare (xargs :guard t))
  (and (consp x) (eq (car x) 'quote)))
other
(defxdoc ihs-utilities
  :parents (ihs-init)
  :short "Utility macros and functions used throughout the IHS books.")
other
(import-as-macros a-unique-symbol-in-the-u-package
  bomb
  defloop
  pack-intern
  pack-string)
mlambda-fnfunction
(defun mlambda-fn
  (args form)
  (declare (xargs :guard (symbol-listp args)))
  (cond ((atom form) (cond ((member form args) form) (t (list 'quote form))))
    (t (list 'cons
        (mlambda-fn args (car form))
        (mlambda-fn args (cdr form))))))
other
(defsection mlambda
  :parents (ihs-utilities)
  :short "Macro LAMBDA form."
  :long "<p>Example:</p>

   @({

  (DEFMACRO X/Y-GUARD (X Y)
    (MLAMBDA (X Y) (AND (RATIONALP X) (RATIONALP Y) (NOT (EQUAL Y 0)))))

    =

  (DEFMACRO X/Y-GUARD (X Y)
    (LIST 'AND (LIST 'RATIONALP X) (LIST 'RATIONALP Y)
          (LIST (LIST 'NOT (LIST 'EQUAL Y 0)))))

  =

  (DEFMACRO X/Y-GUARD (X Y)
    `(AND (RATIONALP ,X) (RATIONALP ,Y) (NOT (EQUAL ,Y 0))))
  })

  <p>MLAMBDA is a macro LAMBDA.  MLAMBDA converts form to a lisp macro body,
  substituting all symbols except those that appear in the args with the quoted
  symbol.</p>"
  (defmacro mlambda
    (args form)
    (declare (xargs :guard (symbol-listp args)))
    (mlambda-fn args form)))
other
(defsection enable-theory
  :parents (ihs-utilities)
  :short "Creates an @(see IN-THEORY) event that is equivalent to ENABLEing the
   theory-expression.  Note that theory-expression is evaluated."
  (defmacro enable-theory
    (theory-expression)
    `(in-theory (union-theories (current-theory :here) ,THEORY-EXPRESSION))))
other
(defsection disable-theory
  :parents (ihs-utilities)
  :short "Creates an IN-THEORY event that is equivalent to DISABLEing the
  theory-expression.  Note that theory-expression is evaluated."
  (defmacro disable-theory
    (theory-expression)
    `(in-theory (set-difference-theories (current-theory :here)
        ,THEORY-EXPRESSION))))
other
(defsection rewrite-theory
  :parents (ihs-utilities)
  :short "Collects all of the :REWRITE runes from theory."
  (defun rewrite-theory-rec
    (theory ans)
    (declare (xargs :guard (and (true-listp theory) (true-listp ans))))
    (cond ((endp theory) (reverse ans))
      ((and (consp (car theory)) (equal (caar theory) :rewrite)) (rewrite-theory-rec (cdr theory) (cons (car theory) ans)))
      (t (rewrite-theory-rec (cdr theory) ans))))
  (defun rewrite-theory
    (theory)
    (declare (xargs :guard (true-listp theory)))
    (rewrite-theory-rec theory nil)))
other
(defsection rewrite-free-theory
  :parents (ihs-utilities)
  :short "Returns the theory with all :REWRITE rules deleted."
  (defun rewrite-free-theory-rec
    (theory ans)
    (declare (xargs :guard (and (true-listp theory) (true-listp ans))))
    (cond ((endp theory) (reverse ans))
      ((and (consp (car theory)) (equal (caar theory) :rewrite)) (rewrite-free-theory-rec (cdr theory) ans))
      (t (rewrite-free-theory-rec (cdr theory)
          (cons (car theory) ans)))))
  (defun rewrite-free-theory
    (theory)
    (declare (xargs :guard (true-listp theory)))
    (rewrite-free-theory-rec theory nil)))
other
(defsection definition-theory
  :parents (ihs-utilities)
  :short "Collects all of the :DEFINITION runes from theory."
  (defun definition-theory-rec
    (theory ans)
    (declare (xargs :guard (and (true-listp theory) (true-listp ans))))
    (cond ((endp theory) (reverse ans))
      ((and (consp (car theory)) (equal (caar theory) :definition)) (definition-theory-rec (cdr theory) (cons (car theory) ans)))
      (t (definition-theory-rec (cdr theory) ans))))
  (defun definition-theory
    (theory)
    (declare (xargs :guard (true-listp theory)))
    (definition-theory-rec theory nil)))
other
(defsection definition-free-theory
  :parents (ihs-utilities)
  :short "Returns the theory with all :DEFINITION rules deleted."
  (defun definition-free-theory-rec
    (theory ans)
    (declare (xargs :guard (and (true-listp theory) (true-listp ans))))
    (cond ((endp theory) (reverse ans))
      ((and (consp (car theory)) (equal (caar theory) :definition)) (definition-free-theory-rec (cdr theory) ans))
      (t (definition-free-theory-rec (cdr theory)
          (cons (car theory) ans)))))
  (defun definition-free-theory
    (theory)
    (declare (xargs :guard (true-listp theory)))
    (definition-free-theory-rec theory nil)))
other
(defsection defun-theory
  :parents (ihs-utilities)
  :short "Collects and returns a special set of runes."
  :long "<p>@(call defun-theory) searches the theory and collects
the :DEFINITION, :INDUCTION, :TYPE-PRESCRIPTION, and :EXECUTABLE-COUNTERPART
runes that were put into the theory by (DEFUN name ... ), for each name in
@('names').</p>

<p>The default for the theory argument is (UNIVERSAL-THEORY :HERE).  Normally
the function will crash if any of the names in names do not have a :DEFINITION
in the theory.  Call with :QUIET T to avoid this behavior.  Note however that
limitations in ACL2 make it impossible to produce even a warning message if you
specify :QUIET T.</p>"
  (defun defun-theory-fn-rec
    (names theory quiet missing ans)
    (declare (xargs :guard (and (symbol-listp names) (true-listp ans))
        :verify-guards nil))
    (cond ((endp names) (cond ((or quiet (null missing)) (reverse ans))
          (t (er hard
              'defun-theory
              "The following names you supplied to DEFUN-THEORY do ~
                       not have a :DEFINITION in the theory you supplied.  ~
                       Check to make sure that the theory is correct (it ~
                       defaults to (UNIVERSAL-THEORY :HERE)) and that these ~
                       are not the names of macros. To avoid this message ~
                       specify :QUIET T in the call to DEFUN-THEORY. Missing ~
                       names: ~p0"
              missing))))
      (t (let* ((name (car names)) (defrune `(:definition ,NAME))
            (execrune `(:executable-counterpart ,NAME))
            (inductrune `(:induction ,NAME))
            (typerune `(:type-prescription ,NAME))
            (tail (member-equal defrune theory)))
          (cond ((not tail) (defun-theory-fn-rec (cdr names)
                theory
                quiet
                (cons name missing)
                ans))
            (t (defun-theory-fn-rec (cdr names)
                theory
                quiet
                missing
                (append (if (member-equal typerune tail)
                    (list typerune)
                    nil)
                  (if (member-equal inductrune tail)
                    (list inductrune)
                    nil)
                  (if (member-equal execrune tail)
                    (list execrune)
                    nil)
                  (cons defrune ans)))))))))
  (defun defun-theory-fn
    (names theory quiet missing)
    (declare (xargs :guard (symbol-listp names) :verify-guards nil))
    (defun-theory-fn-rec names theory quiet missing nil))
  (defmacro defun-theory
    (names &key (theory '(universal-theory :here)) quiet)
    `(defun-theory-fn ,NAMES ,THEORY ,QUIET nil)))
other
(defsection defun-type/exec-theory
  :parents (ihs-utilities)
  :short "Collects and returns a special set of runes."
  :long "<p>@(call DEFUN-TYPE/EXEC-THEORY) searches the theory and collects
the :TYPE-PRESCRIPTION, :EXECUTABLE-COUNTERPART, and :INDUCTION runes that were
put into the theory by (DEFUN name ... ), for each name in names.  Thus,
DEFUN-TYPE/EXEC-THEORY is a "constructive" dual of (DIASBLE . names).</p>

<p>The default for the theory argument is (UNIVERSAL-THEORY :HERE).  Normally
the function will crash if any of the names in names do not have a single rune
in the theory. Call with :QUIET T to avoid this behavior.  Note however that
limitations in ACL2 make it impossible to produce even a warning message if you
specify :QUIET T.</p>"
  (defun defun-type/exec-theory-fn-rec
    (names theory quiet missing ans)
    (declare (xargs :guard (and (symbol-listp names) (true-listp ans))
        :verify-guards nil))
    (cond ((endp names) (cond ((or quiet (null missing)) (reverse ans))
          (t (er hard
              'defun-type/exec-theory
              "The following names you supplied to ~
                       DEFUN-TYPE/EXEC-THEORY do not have an :INDUCTION, ~
                       :EXECUTABLE-COUNTERPART, or any :TYPE-PRESECRIPTIONs ~
                       in the theory you supplied.  Check to make sure that ~
                       the theory is correct (it defaults to ~
                       (UNIVERSAL-THEORY :HERE)) and that these are not the ~
                       names of macros. To avoid this message specify :QUIET ~
                       T in the call to DEFUN-TYPE/EXEC-THEORY. Missing ~
                       names: ~p0"
              missing))))
      (t (let* ((name (car names)) (execrune `(:executable-counterpart ,NAME))
            (inductrune `(:induction ,NAME))
            (typerune `(:type-prescription ,NAME))
            (thy (append (if (member-equal typerune theory)
                  (list typerune)
                  nil)
                (if (member-equal inductrune theory)
                  (list inductrune)
                  nil)
                (if (member-equal execrune theory)
                  (list execrune)
                  nil))))
          (cond ((null thy) (defun-type/exec-theory-fn-rec (cdr names)
                theory
                quiet
                (cons name missing)
                ans))
            (t (defun-type/exec-theory-fn-rec (cdr names)
                theory
                quiet
                missing
                (append thy ans))))))))
  (defun defun-type/exec-theory-fn
    (names theory quiet missing)
    (declare (xargs :guard (symbol-listp names) :verify-guards nil))
    (defun-type/exec-theory-fn-rec names
      theory
      quiet
      missing
      nil))
  (defmacro defun-type/exec-theory
    (names &key (theory '(universal-theory :here)) quiet)
    `(defun-type/exec-theory-fn ,NAMES ,THEORY ,QUIET nil)))