base-cgen-rules - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "cgen-rules")

include-book

(include-book "top" :ttags :all)

local

(local (acl2s-defaults :set :use-fixers nil))

tlp-fxrfunction

(defun tlp-fxr
  (l)
  (declare (xargs :guard t))
  (if (atom l)
    nil
    (cons (car l) (tlp-fxr (cdr l)))))

tlp-fxr-typetheorem

(defthm tlp-fxr-type
  (true-listp (tlp-fxr l))
  :rule-classes (:rewrite :type-prescription))

tlp-fxr-type2theorem

(defthm tlp-fxr-type2
  (implies (consp l) (consp (tlp-fxr l)))
  :rule-classes (:rewrite :type-prescription))

tlp-fxr-type3theorem

(defthm tlp-fxr-type3 (equal (len (tlp-fxr l)) (len l)))

in-theory

(in-theory (disable tlp-fxr))

member-fixer1function

(defun member-fixer1
  (x l)
  (declare (xargs :verify-guards t
      :guard (consp l)
      :guard-hints (("Goal" :in-theory (disable mod)))))
  (let ((l (tlp-fxr l)))
    (if (member-equal x l)
      x
      (b* ((n (len l)) (elem (car l))
          (i (nfix (acl2-count elem)))
          (i (mod i n)))
        (nth i l)))))

other

(define-rule member-equal-fixer1
  :hyp (consp l)
  :rule (let ((x (member-fixer1 x l)))
    (member-equal x l))
  :rule-classes :fixer)

member-fixer2function

(defun member-fixer2
  (a l)
  (declare (xargs :guard t))
  (let ((l (tlp-fxr l)))
    (if (member-equal a l)
      l
      (cons a l))))

other

(define-rule member-equal-fixer2-type-fixed
  :rule (let ((l (member-fixer2 a l)))
    (member-equal a l))
  :rule-classes :fixer)

len-fixer/repeatfunction

(defun len-fixer/repeat
  (n l)
  (if (zp n)
    'nil
    (if (endp l)
      (make-list n :initial-element 0)
      (if (>= (len l) n)
        (take n l)
        (append l (len-fixer/repeat (- n (len l)) l))))))

other

(define-rule len-fixer1-with-repetitions
  :hyp (natp n)
  :rule (let ((l (len-fixer/repeat n l)))
    (equal n (len l)))
  :rule-classes :fixer)

other

(define-rule len-fixer1-with-repetitions-symm
  :hyp (natp n)
  :rule (let ((l (len-fixer/repeat n l)))
    (equal (len l) n))
  :rule-classes :fixer)

append-fixer1function

(defun append-fixer1
  (z x1)
  (b* ((n (len x1)) ((when (> n (len z))) (mv z 'nil))
      (x1 (take n z))
      (x2 (nthcdr n z)))
    (mv x1 x2)))

other

(define-rule append-fixer1
  :hyp (true-listp x3)
  :rule (mv-let (x1 x2)
    (append-fixer1 x3 x1)
    (equal x3 (binary-append x1 x2)))
  :rule-classes :fixer)

append-fixer2function

(defun append-fixer2
  (z x2)
  (b* ((n (- (len z) (len x2))) (x1 (take n z)) (x2 (nthcdr n z)))
    (mv x1 x2)))

other

(define-rule append-fixer2
  :hyp (true-listp x3)
  :rule (mv-let (x1 x2)
    (append-fixer2 x3 x2)
    (equal x3 (binary-append x1 x2)))
  :rule-classes :fixer)

intersectp-fix1function

(defun intersectp-fix1
  (x1 x2)
  (declare (xargs :guard (consp x2)))
  (if (intersectp-equal (tlp-fxr x1) (tlp-fxr x2))
    (tlp-fxr x1)
    (b* ((a (member-fixer1 1 x2)))
      (add-to-set-equal a (tlp-fxr x1)))))

other

(define-rule intersectp-fixer1
  :hyp (consp x2)
  :rule (let ((x1 (intersectp-fix1 x1 x2)))
    (intersectp-equal x1 x2))
  :rule-classes :fixer)

other

(define-rule intersectp-fixer2
  :hyp (consp x1)
  :rule (let ((x2 (intersectp-fix1 x2 x1)))
    (intersectp-equal x1 x2))
  :rule-classes :fixer)

_max-lst1function

(defun _max-lst1
  (xs ans)
  (declare (xargs :guard (real/rationalp ans)))
  (if (atom xs)
    ans
    (_max-lst1 (cdr xs) (max (rfix (car xs)) ans))))

_max-lstfunction

(defun _max-lst (xs) (_max-lst1 xs 0))

_make-numlistfunction

(defun _make-numlist
  (curr size)
  (declare (xargs :guard (and (real/rationalp curr) (natp size))))
  (if (zp size)
    'nil
    (cons curr (_make-numlist (1+ curr) (1- size)))))

not-intersectp-fix2function

(defun not-intersectp-fix2
  (x1 x2)
  "fixer for (not (intersectp X1 X2)). preserves the length of X1"
  (if (not (intersectp-equal (tlp-fxr x1) (tlp-fxr x2)))
    (tlp-fxr x1)
    (b* ((common-elements (intersection-equal x1 x2)) (n (len common-elements))
        (m (_max-lst x2))
        (new (_make-numlist (1+ m) n)))
      (append new (set-difference-equal x1 common-elements)))))

other

(define-rule not-intersectp-fixer1
  :rule (let ((x1 (not-intersectp-fix2 x1 x2)))
    (not (intersectp-equal x1 x2)))
  :rule-classes :fixer)

other

(define-rule not-intersectp-fixer2
  :rule (let ((x2 (not-intersectp-fix2 x2 x1)))
    (not (intersectp-equal x1 x2)))
  :rule-classes :fixer)

no-dups-fixfunction

(defun no-dups-fix
  (x)
  (declare (xargs :guard t))
  (remove-duplicates-equal (tlp-fxr x)))

other

(define-rule no-dups-fixer-type-fixed
  :rule (let ((x1 (no-dups-fix x1)))
    (no-duplicatesp-equal x1))
  :rule-classes :fixer)

other

(define-rule nth-fixer2
  :hyp (and (natp n) (< n (len l)))
  :rule (let ((l (update-nth n v (tlp-fxr l))))
    (equal v (nth n l)))
  :rule-classes :fixer)

rem-eql-fixer2function

(defun rem-eql-fixer2
  (a l l1)
  (if (endp l1)
    'nil
    (if (endp l)
      l1
      (b* ((x (car l)) (x1 (car l1))
          (rest (rem-eql-fixer2 a (cdr l) (cdr l1))))
        (if (equal a x)
          (cons a (cons x1 rest))
          (cons x1 rest))))))

other

(define-rule remove-equal-fixer2
  :hyp (and (not (member-equal a l1)) (true-listp l1))
  :rule (let ((l (rem-eql-fixer2 a (tlp-fxr l) l1)))
    (equal l1 (remove-equal a l)))
  :rule-classes :fixer)

remove1-equal-fixer2function

(defun remove1-equal-fixer2 (a l1) (cons a l1))

other

(define-rule remove1-equal-fixer2
  :hyp (true-listp l1)
  :rule (let ((l (remove1-equal-fixer2 a (tlp-fxr l1))))
    (equal l1 (remove1-equal a l)))
  :rule-classes :fixer)

subsetp-fixer1function

(defun subsetp-fixer1
  (x1 x2)
  (if (atom x1)
    'nil
    (if (member-equal (car x1) x2)
      (cons (car x1) (subsetp-fixer1 (cdr x1) x2))
      (subsetp-fixer1 (cdr x1) x2))))

other

(define-rule subsetp-equal-fixer1-type-fixed
  :rule (let ((x1 (subsetp-fixer1 x1 x2)))
    (subsetp-equal x1 x2))
  :rule-classes :fixer)

other

(define-rule subsetp-equal-fixer2-type-fixed
  :rule (let ((x2 (union-equal (tlp-fxr x1) (tlp-fxr x2))))
    (subsetp-equal x1 x2))
  :rule-classes :fixer)

consp-fixer/for-alist-fixerfunction

(defun consp-fixer/for-alist-fixer
  (p)
  (if (consp p)
    p
    (cons p nil)))

alist-fixerfunction

(defun alist-fixer
  (a)
  (if (atom a)
    nil
    (cons (consp-fixer/for-alist-fixer (car a))
      (alist-fixer (cdr a)))))

alist-fixer-typetheorem

(defthm alist-fixer-type
  (alistp (alist-fixer l))
  :rule-classes (:rewrite :type-prescription))

alist-fixer-type2theorem

(defthm alist-fixer-type2
  (implies (consp l) (consp (alist-fixer l)))
  :rule-classes (:rewrite :type-prescription))

alist-fixer-type3theorem

(defthm alist-fixer-type3
  (equal (len (alist-fixer l)) (len l)))

in-theory

(in-theory (disable alist-fixer))

other

(define-rule assoc-equal-fixer2
  :hyp (allp v)
  :rule (let ((a (put-assoc-equal x v (alist-fixer a))))
    (assoc-equal x a))
  :rule-classes :fixer)

assoc-fxr3function

(defun assoc-fxr3
  (x a)
  (let ((a (alist-fixer a)))
    (if (assoc-equal x a)
      a
      (if (endp a)
        (put-assoc-equal x 0 a)
        (put-assoc-equal x (cdr (car a)) a)))))

other

(define-rule assoc-equal-fixer3
  :rule (let ((a (assoc-fxr3 x a)))
    (assoc-equal x a))
  :rule-classes :fixer)

other

(define-rule assoc-equal-fixer1
  :hyp (and (consp a) (alistp a))
  :rule (let ((x (member-fixer1 x (strip-cars a))))
    (assoc-equal x a))
  :rule-classes :fixer)

other

(define-rule assoc-eq-equation-fixer
  :rule (let ((a (put-assoc-equal x v (alist-fixer a))))
    (equal v (cdr (assoc-equal x a))))
  :rule-classes :fixer)