defun-plus - ACL2 Book

other

(in-package "ACL2")

strip-dcls-program-mode1function

(defun strip-dcls-program-mode1
  (fields lst)
  (declare (xargs :mode :program))
  (cond ((endp lst) nil)
    ((member-eq (caar lst) '(type ignore ignorable)) (cond ((member-eq (caar lst) fields) (strip-dcls-program-mode1 fields (cdr lst)))
        (t (cons (car lst) (strip-dcls-program-mode1 fields (cdr lst))))))
    (t (let ((temp (strip-keyword-list fields (cdar lst))))
        (cond ((null temp) (strip-dcls-program-mode1 fields (cdr lst)))
          (t (cons (cons 'xargs temp)
              (strip-dcls-program-mode1 fields (cdr lst)))))))))

strip-dcls-program-modefunction

(defun strip-dcls-program-mode
  (fields lst)
  (declare (xargs :mode :program))
  (cond ((endp lst) nil)
    ((stringp (car lst)) (cond ((member-eq 'comment fields) (strip-dcls-program-mode fields (cdr lst)))
        (t (cons (car lst) (strip-dcls-program-mode fields (cdr lst))))))
    (t (let ((temp (strip-dcls-program-mode1 fields (cdar lst))))
        (cond ((null temp) (strip-dcls-program-mode fields (cdr lst)))
          (t (cons (cons 'declare temp)
              (strip-dcls-program-mode fields (cdr lst)))))))))

fetch-dcl-fields-program-mode2function

(defun fetch-dcl-fields-program-mode2
  (field-names kwd-list acc)
  (declare (xargs :mode :program))
  (cond ((endp kwd-list) acc)
    (t (let ((acc (fetch-dcl-fields-program-mode2 field-names
             (cddr kwd-list)
             acc)))
        (if (member-eq (car kwd-list) field-names)
          (cons (cadr kwd-list) acc)
          acc)))))

fetch-dcl-fields-program-mode1function

(defun fetch-dcl-fields-program-mode1
  (field-names lst)
  (declare (xargs :mode :program))
  (cond ((endp lst) nil)
    ((member-eq (caar lst) '(type ignore ignorable)) (if (member-eq (caar lst) field-names)
        (cons (cdar lst)
          (fetch-dcl-fields-program-mode1 field-names (cdr lst)))
        (fetch-dcl-fields-program-mode1 field-names (cdr lst))))
    (t (fetch-dcl-fields-program-mode2 field-names
        (cdar lst)
        (fetch-dcl-fields-program-mode1 field-names (cdr lst))))))

fetch-dcl-fields-program-modefunction

(defun fetch-dcl-fields-program-mode
  (field-names lst)
  (declare (xargs :mode :program))
  (cond ((endp lst) nil)
    ((stringp (car lst)) (if (member-eq 'comment field-names)
        (cons (car lst)
          (fetch-dcl-fields-program-mode field-names (cdr lst)))
        (fetch-dcl-fields-program-mode field-names (cdr lst))))
    (t (append (fetch-dcl-fields-program-mode1 field-names (cdar lst))
        (fetch-dcl-fields-program-mode field-names (cdr lst))))))

fetch-dcl-field-program-modefunction

(defun fetch-dcl-field-program-mode
  (field-name lst)
  (declare (xargs :mode :program))
  (fetch-dcl-fields-program-mode (list field-name) lst))

generate-output-lemma-namefunction

(defun generate-output-lemma-name
  (name number)
  (if (not number)
    (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-OUTPUT-LEMMA")
      name)
    (intern-in-package-of-symbol (concatenate 'string
        (symbol-name name)
        "-OUTPUT-LEMMA-"
        (coerce (explode-atom number 10) 'string))
      name)))

generate-output-lemma-singlefunction

(defun generate-output-lemma-single
  (name guards output output-hints)
  `((defthm ,(GENERATE-OUTPUT-LEMMA-NAME NAME NIL)
     (implies ,GUARDS ,OUTPUT)
     :hints ,OUTPUT-HINTS)))

generate-output-lemma-multiplefunction

(defun generate-output-lemma-multiple
  (name guards output number)
  (if (atom output)
    nil
    (cons `(defthm ,(GENERATE-OUTPUT-LEMMA-NAME NAME NUMBER)
        (implies ,GUARDS ,(CAR OUTPUT)))
      (generate-output-lemma-multiple name
        guards
        (cdr output)
        (1+ number)))))

generate-output-lemmasfunction

(defun generate-output-lemmas
  (name guards output output-hints)
  (if (not (equal (car output) 'and))
    (generate-output-lemma-single name
      guards
      output
      output-hints)
    (generate-output-lemma-multiple name guards (cdr output) 1)))

defun+macro

(defmacro defun+
  (name formals dcl body &key disable)
  (let* ((guards (car (fetch-dcl-field-program-mode :guard (list dcl)))) (output (car (fetch-dcl-field-program-mode :output (list dcl))))
      (output-hints (car (fetch-dcl-field-program-mode :output-hints (list dcl))))
      (new-dcls (car (strip-dcls-program-mode '(:output) (list dcl))))
      (new-dcls (car (strip-dcls-program-mode '(:output-hints) (list new-dcls)))))
    `(progn (defun ,NAME ,FORMALS ,NEW-DCLS ,BODY)
      ,@(IF OUTPUT
      (GENERATE-OUTPUT-LEMMAS NAME GUARDS OUTPUT OUTPUT-HINTS)
      `((VALUE-TRIPLE NIL)))
      ,(IF DISABLE
     `(IN-THEORY (DISABLE ,NAME))
     '(VALUE-TRIPLE NIL)))))

local

(local (defun+ baz
    (x y z)
    (declare (xargs :guard (and (integerp x) (integerp y) (integerp z))
        :output (integerp (baz x y z))))
    (+ x y z)))

local

(local (defun+ baz
    (x y z)
    (declare (xargs :guard (and (integerp x) (integerp y) (integerp z))
        :output (integerp (baz x y z))
        :output-hints (("Goal" :do-not-induct t))))
    (+ x y z)))

local

(local (defun+ faz
    (x y z)
    (declare (xargs :guard (and (integerp x) (integerp y) (integerp z))
        :output (integerp (faz x y z))))
    (+ x y z)
    :disable t))

local

(local (defun+ foo
    (x y)
    (declare (xargs :guard (and (integerp x) (integerp y))
        :output (and (equal (mv-nth 0 (foo x y)) 0)
          (integerp (mv-nth 1 (foo x y))))))
    (mv 0 (+ x y))
    :disable t))