Filtering...

defp

books/misc/defp

Included Books

defpun
other
(in-package "ACL2")
include-book
(include-book "defpun")
defpun-add-testfunction
(defun defpun-add-test
  (test tests-and-stuff-lst)
  (declare (xargs :guard (and (alistp tests-and-stuff-lst)
        (true-list-listp (strip-cars tests-and-stuff-lst)))))
  (if (endp tests-and-stuff-lst)
    nil
    (let ((tests (caar tests-and-stuff-lst)) (call (cdar tests-and-stuff-lst)))
      (cons (cons (cons test tests) call)
        (defpun-add-test test (cdr tests-and-stuff-lst))))))
other
(verify-termination dumb-negate-lit)
defpun-calls-tests-and-args-lstfunction
(defun defpun-calls-tests-and-args-lst
  (fn term)
  (case-match term
    ((!fn . args) (list (cons nil args)))
    (('if test tbr fbr) (let ((tbr-tests-and-args-lst (defpun-calls-tests-and-args-lst fn tbr)) (fbr-tests-and-args-lst (defpun-calls-tests-and-args-lst fn fbr)))
        (append (defpun-add-test test tbr-tests-and-args-lst)
          (defpun-add-test (dumb-negate-lit test)
            fbr-tests-and-args-lst))))
    (& nil)))
defpun-tests-and-base-lstfunction
(defun defpun-tests-and-base-lst
  (fn term)
  (case-match term
    ((!fn . &) nil)
    (('if test tbr fbr) (let ((tbr-base (defpun-tests-and-base-lst fn tbr)) (fbr-base (defpun-tests-and-base-lst fn fbr)))
        (append (defpun-add-test test tbr-base)
          (defpun-add-test (dumb-negate-lit test) fbr-base))))
    (& (list (cons nil term)))))
map-conjoinfunction
(defun map-conjoin
  (lst)
  (declare (xargs :guard (true-list-listp lst)))
  (if (endp lst)
    nil
    (cons (conjoin (car lst)) (map-conjoin (cdr lst)))))
defpun-disjoin-testsfunction
(defun defpun-disjoin-tests
  (tests-and-args-lst)
  (declare (xargs :guard (and (alistp tests-and-args-lst)
        (true-list-listp (strip-cars tests-and-args-lst)))))
  (let ((tests-lst (strip-cars tests-and-args-lst)))
    (disjoin (map-conjoin tests-lst))))
other
(program)
defpun-make-nth-argfunction
(defun defpun-make-nth-arg
  (tests-and-args-lst n)
  (declare (xargs :guard (and (alistp tests-and-args-lst)
        (true-list-listp (strip-cars tests-and-args-lst)))))
  (if (endp (cdr tests-and-args-lst))
    (nth n (cdar tests-and-args-lst))
    (fcons-term* 'if
      (conjoin (caar tests-and-args-lst))
      (nth n (cdar tests-and-args-lst))
      (defpun-make-nth-arg (cdr tests-and-args-lst) n))))
defpun-make-callfunction
(defun defpun-make-call
  (fn tests-and-args-lst n acc)
  (if (zp n)
    (cons-term fn acc)
    (let ((n (1- n)))
      (defpun-make-call fn
        tests-and-args-lst
        n
        (cons (defpun-make-nth-arg tests-and-args-lst n) acc)))))
defpun-make-basefunction
(defun defpun-make-base
  (tests-and-base-lst)
  (if (endp (cdr tests-and-base-lst))
    (cdar tests-and-base-lst)
    (fcons-term* 'if
      (conjoin (caar tests-and-base-lst))
      (cdar tests-and-base-lst)
      (defpun-make-base (cdr tests-and-base-lst)))))
defpmacro
(defmacro defp
  (g vars body &key (rule-classes ':definition))
  `(make-event (er-progn (if (function-symbolp ',G (w state))
        (value nil)
        (defstub ,G ,VARS t))
      (er-let* ((tbody0 (translate ',BODY t t nil '(defp . ,G) (w state) state)))
        (let* ((tbody (remove-lambdas tbody0)) (tests-and-args-lst (defpun-calls-tests-and-args-lst ',G tbody))
            (call (defpun-make-call ',G tests-and-args-lst ,(LENGTH VARS) nil))
            (tests-and-base-lst (defpun-tests-and-base-lst ',G tbody))
            (base (defpun-make-base tests-and-base-lst))
            (test (defpun-disjoin-tests tests-and-base-lst))
            (new-body (list 'if
                (untranslate test nil (w state))
                (untranslate base nil (w state))
                (untranslate call nil (w state)))))
          (if (ffnnamep ',G base)
            (mv (msg "Unable to process the suggested definition as tail ~
                      recursive.  Possible debug info: A problem call has ~
                      been collected into the base case:~|~%  ~x0"
                (untranslate base nil (w state)))
              nil
              state)
            (value (list 'encapsulate
                '((,G ,VARS t))
                (list 'local
                  (list 'defpun ',G ',VARS new-body :rule-classes nil))
                (list 'defthm
                  ',(PACKN-POS (LIST G "$DEF") G)
                  (list 'equal (cons ',G ',VARS) ',BODY)
                  :hints '(("Goal" :in-theory (theory 'minimal-theory)
                     :use ,(PACKN-POS (LIST G "-DEF") G)))
                  :rule-classes ',RULE-CLASSES)))))))))