Filtering...

apply-prim

books/system/apply/apply-prim

Included Books

apply-prim-support evaluator-metatheorems
other
(in-package "ACL2")
include-book
(include-book "apply-prim-support")
local
(local (include-book "centaur/misc/evaluator-metatheorems" :dir :system))
local
(local (in-theory (enable apply$-primp badge-prim)))
badge-prim-typeencapsulate
(encapsulate nil
  (local (defthm apply$-badgep-properties
      (implies (apply$-badgep x)
        (and (consp x)
          (natp (access apply$-badge x :arity))
          (natp (access apply$-badge x :out-arity))
          (or (eq (access apply$-badge x :ilks) t)
            (and (true-listp (access apply$-badge x :ilks))
              (equal (len (access apply$-badge x :ilks))
                (access apply$-badge x :arity))))))
      :rule-classes ((:compound-recognizer :corollary (implies (apply$-badgep x) (consp x))) (:linear :corollary (implies (apply$-badgep x) (<= 0 (car (cdr x)))))
        (:rewrite :corollary (implies (apply$-badgep x) (integerp (car (cdr x)))))
        (:linear :corollary (implies (apply$-badgep x) (<= 0 (car (cdr (cdr x))))))
        (:rewrite :corollary (implies (apply$-badgep x) (integerp (car (cdr (cdr x))))))
        (:rewrite :corollary (implies (and (apply$-badgep x) (not (eq (cdr (cdr (cdr x))) t)))
            (and (true-listp (cdr (cdr (cdr x))))
              (equal (len (cdr (cdr (cdr x)))) (car (cdr x)))))))))
  (local (defun check-it!
      (alist)
      (cond ((atom alist) t)
        (t (and (consp (car alist))
            (apply$-badgep (cdr (car alist)))
            (eq (access apply$-badge (cdr (car alist)) :ilks) t)
            (check-it! (cdr alist)))))))
  (local (defthm check-it!-works
      (implies (check-it! alist)
        (implies (hons-get fn alist)
          (and (consp (hons-get fn alist))
            (apply$-badgep (cdr (hons-get fn alist)))
            (eq (access apply$-badge (cdr (hons-get fn alist)) :ilks) t))))
      :rule-classes nil))
  (defthm badge-prim-type
    (implies (apply$-primp fn)
      (and (apply$-badgep (badge-prim fn))
        (eq (cdr (cdr (cdr (badge-prim fn)))) t)))
    :hints (("Goal" :use (:instance check-it!-works (alist *badge-prim-falist*))
       :in-theory (disable check-it! hons-get)))
    :rule-classes ((:rewrite :corollary (implies (apply$-primp fn)
         (and (apply$-badgep (badge-prim fn))
           (eq (cdr (cdr (cdr (badge-prim fn)))) t)))) (:forward-chaining :corollary (implies (apply$-primp fn) (apply$-badgep (badge-prim fn)))))))
n-car-cadr-caddr-etcfunction
(defun n-car-cadr-caddr-etc
  (n x)
  (declare (xargs :guard (natp n)))
  (if (zp n)
    nil
    (cons `(car ,X) (n-car-cadr-caddr-etc (- n 1) `(cdr ,X)))))
other
(set-rewrite-stack-limit 4000)
meta-apply$-primfunction
(defun meta-apply$-prim
  (term)
  (declare (xargs :guard (pseudo-termp term) :verify-guards nil))
  (cond ((and (consp term)
       (eq (ffn-symb term) 'apply$-prim)
       (quotep (fargn term 1))
       (symbolp (cadr (fargn term 1)))) (let* ((fn (cadr (fargn term 1))) (args (fargn term 2))
          (temp (hons-get fn *badge-prim-falist*)))
        (cond ((null temp) term)
          (t (if (int= (access apply$-badge (cdr temp) :out-arity) 1)
              `(,FN ,@(N-CAR-CADR-CADDR-ETC (ACCESS APPLY$-BADGE (CDR TEMP) :ARITY) ARGS))
              `(mv-list ',(ACCESS APPLY$-BADGE (CDR TEMP) :OUT-ARITY)
                (,FN ,@(N-CAR-CADR-CADDR-ETC (ACCESS APPLY$-BADGE (CDR TEMP) :ARITY) ARGS))))))))
    (t term)))
other
(make-event `(encapsulate nil
    (with-output :off (prove event)
      (defevaluator apply$-prim-meta-fn-ev
        apply$-prim-meta-fn-ev-list
        ((apply$-prim fn args) ,@(STRIP-CARS *FIRST-ORDER-LIKE-TERMS-AND-OUT-ARITIES*))))
    (local (with-output :off (prove event)
        (def-evaluator-expander apply$-prim-meta-fn-ev)))
    (local (defthm n-car-cadr-caddr-etc-opener
        (implies (natp n)
          (equal (n-car-cadr-caddr-etc (+ 1 n) args)
            (cons (list 'car args)
              (n-car-cadr-caddr-etc n (list 'cdr args)))))))
    (local (defthm hide-is-identity
        (equal (hide x) x)
        :hints (("Goal" :expand ((hide x))))))
    (local (make-event `(defthm open-apply$-prim-of-quote
          (implies (syntaxp (quotep fn))
            (equal (apply$-prim fn args)
              ,(BODY 'APPLY$-PRIM NIL (W STATE))))
          :instructions (:promote (:drop 1)
            (:prove :hints (("goal" :by apply$-prim)))))))
    (defthm apply$-prim-meta-fn-correct
      (equal (apply$-prim-meta-fn-ev term alist)
        (apply$-prim-meta-fn-ev (meta-apply$-prim term) alist))
      :instructions ((quiet! (:bash ("Goal" :in-theory '((:definition hons-assoc-equal) (:definition hons-equal)
               (:definition hons-get)
               (:definition meta-apply$-prim)
               (:definition quotep)
               (:executable-counterpart car)
               (:executable-counterpart cdr)
               (:executable-counterpart consp))))
         (:in-theory (union-theories '((:rewrite open-apply$-prim-of-quote) (:definition n-car-cadr-caddr-etc)
               (:meta apply$-prim-meta-fn-ev-expander-correct)
               (:rewrite apply$-prim-meta-fn-ev-constraint-8)
               (:rewrite apply$-prim-meta-fn-ev-constraint-975)
               (:rewrite apply$-prim-meta-fn-ev-constraint-976)
               (:rewrite apply$-prim-meta-fn-ev-constraint-187)
               n-car-cadr-caddr-etc-opener
               (natp)
               apply$-prim-meta-fn-ev-constraint-2
               quotep
               car-cons
               cdr-cons
               hide-is-identity)
             (union-theories *expandable-boot-strap-non-rec-fns*
               (intersection-theories (current-theory :here)
                 (executable-counterpart-theory :here)))))
         (:repeat :prove)))
      :rule-classes ((:meta :trigger-fns (apply$-prim))))
    (defthm apply$-primp-implies-symbolp
      (implies (apply$-primp fn) (symbolp fn))
      :rule-classes :forward-chaining)))
in-theory
(in-theory (disable apply$-prim apply$-primp))