acl2x-help - ACL2 Book

other

(in-package "ACL2")

other

(set-state-ok t)

acl2x-replace-fnfunction

(defun acl2x-replace-fn
  (pass1 pass2 single-pass outside-certification)
  `(make-event (cond ((not (f-get-global 'certify-book-info state)) ',OUTSIDE-CERTIFICATION)
      ((not (f-get-global 'write-acl2x state)) ',SINGLE-PASS)
      (t '(progn (value-triple '(:acl2x-pass2 ,PASS2)) ,PASS1)))))

acl2x-replacemacro

(defmacro acl2x-replace
  (pass1 pass2
    &key
    (single-pass 'nil single-p)
    (outside-certification 'nil outside-p))
  (acl2x-replace-fn pass1
    pass2
    (if single-p
      single-pass
      pass2)
    (if outside-p
      outside-certification
      pass2)))

use-acl2x-replacemacro

(defmacro use-acl2x-replace
  nil
  '(acl2x-replace (defattach (acl2x-expansion-alist acl2x-expansion-alist-replacement)
      :system-ok t)
    (value-triple :invisible)))

use-acl2x-replace!macro

(defmacro use-acl2x-replace!
  nil
  '(defattach (acl2x-expansion-alist acl2x-expansion-alist-replacement)
    :system-ok t))

other

(verify-termination hons-copy-with-state)

other

(verify-guards hons-copy-with-state)

no-acl2x-replacemacro

(defmacro no-acl2x-replace
  nil
  '(defattach (acl2x-expansion-alist hons-copy-with-state)
    :system-ok t))

no-acl2x-replace!macro

(defmacro no-acl2x-replace!
  nil
  '(defattach (acl2x-expansion-alist hons-copy-with-state)
    :system-ok t))

maybe-skip-proofsmacro

(defmacro maybe-skip-proofs
  (form)
  `(acl2x-replace (skip-proofs ,FORM)
    ,FORM
    :single-pass ,FORM
    :outside-certification (skip-proofs ,FORM)))

with-guard1macro

(defmacro with-guard1
  (guard form)
  `(cond (,GUARD ,FORM)
    (t (er hard?
        'with-guard1
        "Unexpected with-guard1 failure, ~x0"
        ',GUARD))))

local

(local (defthm true-listp-of-revappend
    (implies (true-listp x) (true-listp (revappend y x)))))

local

(local (defthm true-listp-of-first-n-ac
    (implies (true-listp x) (true-listp (first-n-ac i l x)))))

acl2x-expansion-alist-replacement2mutual-recursion

(mutual-recursion (defun acl2x-expansion-alist-replacement2
    (form state)
    (declare (xargs :guard t :stobjs state))
    (case-match form
      (('record-expansion & y) (acl2x-expansion-alist-replacement2 y state))
      (('progn . x) (case-match x
          ((('value-triple ('quote (':acl2x-pass2 form))) &) (acl2x-expansion-alist-replacement2 form state))
          ((('value-triple ('quote (':acl2x-load-state-global symbol))) &) (if (and (symbolp symbol) (boundp-global symbol state))
              (f-get-global symbol state)
              (er hard?
                'acl2x-expansion-alist-replacement2
                "Found an acl2x-load-state-global form with an unbound variable~%")))
          (& (with-guard1 (true-listp x)
              (hons 'progn
                (acl2x-expansion-alist-replacement2-lst x state))))))
      (('encapsulate sigs . x) (with-guard1 (true-listp x)
          (hons 'encapsulate
            (hons sigs (acl2x-expansion-alist-replacement2-lst x state)))))
      (('local x) (hons-copy (list 'local (acl2x-expansion-alist-replacement2 x state))))
      (('skip-proofs x) (hons-copy (list 'skip-proofs
            (acl2x-expansion-alist-replacement2 x state))))
      (('with-output . x) (with-guard1 (true-listp x)
          (hons 'with-output
            (append (butlast x 1)
              (list (acl2x-expansion-alist-replacement2 (car (last x)) state))))))
      (& form)))
  (defun acl2x-expansion-alist-replacement2-lst
    (x state)
    (declare (xargs :guard (true-listp x)))
    (cond ((endp x) nil)
      (t (hons (acl2x-expansion-alist-replacement2 (car x) state)
          (acl2x-expansion-alist-replacement2-lst (cdr x) state))))))

acl2x-expansion-alist-replacement1function

(defun acl2x-expansion-alist-replacement1
  (alist acc state)
  (declare (xargs :guard (and (alistp alist) (alistp acc))
      :stobjs state))
  (cond ((endp alist) (hons-copy (reverse acc)))
    (t (acl2x-expansion-alist-replacement1 (cdr alist)
        (acons (caar alist)
          (acl2x-expansion-alist-replacement2 (cdar alist) state)
          acc)
        state))))

acl2x-expansion-alist-replacementfunction

(defun acl2x-expansion-alist-replacement
  (alist state)
  (declare (xargs :guard t :stobjs state)
    (ignorable state))
  (with-guard1 (alistp alist)
    (acl2x-expansion-alist-replacement1 alist nil state)))

other

(use-acl2x-replace!)