util - ACL2 Book

other

(in-package "RTL")

other

(include-book "../localize-macros")

defbvecpmacro

(defmacro defbvecp
  (name formals
    width
    &key
    thm-name
    hyp
    hints)
  (let* ((thm-name (or thm-name
         (intern-in-package-of-symbol (concatenate 'string
             (if (consp width)
               "BV-ARRP$"
               "BVECP$")
             (symbol-name name))
           name))) (x (cons name formals))
      (typed-term (if (consp width)
          (list 'ag 'index x)
          x))
      (bvecp-concl (if (consp width)
          (list 'bv-arrp x (car (last width)))
          (list 'bvecp x width)))
      (concl (list 'and
          (list 'integerp typed-term)
          (list '<= 0 typed-term))))
    (list* 'defthm
      thm-name
      (if hyp
        (list 'implies hyp bvecp-concl)
        bvecp-concl)
      :rule-classes (list :rewrite (list :forward-chaining :trigger-terms (list x))
        (list :type-prescription :corollary (if hyp
            (list 'implies hyp concl)
            concl)
          :typed-term typed-term
          :hints (if (consp width)
            '(("Goal" :in-theory '(implies bvecp
                 bv-arrp-implies-nonnegative-integerp)))
            '(("Goal" :in-theory '(implies bvecp))))))
      (if hints
        (list :hints hints)
        nil))))

sub1-inductionfunction

(defun sub1-induction
  (n)
  (if (zp n)
    n
    (sub1-induction (1- n))))

other

(defconst *rtl-operators-after-macro-expansion*
  '(log= log<>
    log<
    log<=
    log>
    log>=
    comp2<
    comp2<=
    comp2>
    comp2>=
    land
    lior
    lxor
    lnot
    logand1
    logior1
    logxor1
    shft
    cat
    mulcat
    bits
    bitn
    setbits
    setbitn
    ag
    as
    *
    +
    floor
    rem
    decode
    encode
    natp1
    mk-bvarr
    mk-bvec))

split-listfunction

(defun split-list
  (lst lo hi)
  (cond ((endp lst) (mv lo hi))
    ((endp (cdr lst)) (mv (cons (car lst) lo) hi))
    (t (split-list (cddr lst)
        (cons (car lst) lo)
        (cons (cadr lst) hi)))))

fast-and-fnfunction

(defun fast-and-fn
  (conjuncts)
  (declare (xargs :mode :program))
  (cond ((endp conjuncts) ''t)
    ((endp (cdr conjuncts)) (car conjuncts))
    (t (mv-let (hi lo)
        (split-list conjuncts nil nil)
        (list 'if
          (fast-and-fn hi)
          (fast-and-fn lo)
          'nil)))))

fast-andmacro

(defmacro fast-and
  (&rest conjuncts)
  (fast-and-fn conjuncts))

defsigmacro

(defmacro defsig
  (name param body)
  (declare (ignore param))
  (let ((realname (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "$")
         name)))
    `(progn (defund ,RTL::REALNAME (n $path) ,RTL::BODY)
      (defmacro ,RTL::NAME
        (n)
        (list ',RTL::REALNAME n '$path))
      (add-macro-alias ,RTL::NAME ,RTL::REALNAME))))

defsigdmacro

(defmacro defsigd
  (name params body)
  (let ((realname (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "$")
         name)))
    `(progn (defund ,RTL::REALNAME
        (,@RTL::PARAMS $path)
        ,RTL::BODY)
      (defmacro ,RTL::NAME
        ,RTL::PARAMS
        (list ',RTL::REALNAME ,@RTL::PARAMS '$path))
      (add-macro-alias ,RTL::NAME ,RTL::REALNAME))))

defthm-nlmacro

(defmacro defthm-nl
  (&rest thm)
  (declare (xargs :guard (and (true-listp thm) (symbolp (car thm)))))
  `(encapsulate nil
    (local (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
           hist
           pspv))))
    (defthm ,@RTL::THM)))

defthmd-nlmacro

(defmacro defthmd-nl
  (&rest thm)
  (declare (xargs :guard (and (true-listp thm) (symbolp (car thm)))))
  `(encapsulate nil
    (local (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
           hist
           pspv))))
    (defthmd ,@RTL::THM)))

defthm-nl++macro

(defmacro defthm-nl++
  (&rest thm)
  (declare (xargs :guard (and (true-listp thm) (symbolp (car thm)))))
  `(encapsulate nil
    (local (set-default-hints '((nonlinearp-default-hint++ id
           stable-under-simplificationp
           hist
           nil))))
    (defthm ,@RTL::THM)))

defthmd-nl++macro

(defmacro defthmd-nl++
  (&rest thm)
  (declare (xargs :guard (and (true-listp thm) (symbolp (car thm)))))
  `(encapsulate nil
    (local (set-default-hints '((nonlinearp-default-hint++ id
           stable-under-simplificationp
           hist
           nil))))
    (defthmd ,@RTL::THM)))