Filtering...

save-time

books/misc/save-time
other
(in-package "ACL2")
save-time-initmacro
(defmacro save-time-init
  nil
  '(make-event (pprogn (f-put-global 'save-time-alist nil state)
      (f-put-global 'save-time-temp-stack nil state)
      (value '(value-triple nil)))
    :check-expansion t))
other
(save-time-init)
save-time-startmacro
(defmacro save-time-start
  (eventp)
  (let ((form '(mv-let (start-time state)
         (read-run-time state)
         (f-put-global 'save-time-temp-stack
           (cons start-time
             (cond ((eql 0 (f-get-global 'make-event-debug-depth state)) nil)
               (t (f-get-global 'save-time-temp-stack state))))
           state))))
    (cond (eventp `(local (make-event (pprogn ,FORM
              (value '(value-triple :save-time-started :on-skip-proofs t))))))
      (t `(pprogn ,FORM (value nil))))))
save-time-stopmacro
(defmacro save-time-stop
  (name eventp)
  (let* ((last-form (cond (eventp '(value '(value-triple :save-time-stopped :on-skip-proofs t)))
         (t `(value ',NAME)))) (form `(let ((stack (f-get-global 'save-time-temp-stack state)))
          (mv-let (stop-time state)
            (read-run-time state)
            (pprogn (f-put-global 'save-time-alist
                (put-assoc ',NAME
                  (- stop-time (car stack))
                  (f-get-global 'save-time-alist state)
                  :test 'eq)
                state)
              (f-put-global 'save-time-temp-stack (cdr stack) state)
              ,LAST-FORM)))))
    (cond (eventp `(local (make-event ,FORM))) (t form))))
save-time-namefunction
(defun save-time-name
  (form)
  (let ((er-string "The form ~x0  is not of the form (_ s ...) where s is a ~
                    symbol.  Supply a :NAME argument for save-time."))
    (case-match form
      (('local f) (save-time-name f))
      ((& name . &) (cond ((atom name) name)
          (t (er hard 'save-time er-string form))))
      (& nil))))
save-timemacro
(defmacro save-time
  (form &key name eventp)
  (let ((prog (if eventp
         'progn
         'er-progn)))
    `(,PROG (save-time-start ,EVENTP)
      ,FORM
      (save-time-stop ,(OR NAME (SAVE-TIME-NAME FORM)) ,EVENTP))))
merge-cdr->function
(defun merge-cdr->
  (l1 l2)
  (declare (xargs :mode :program))
  (cond ((null l1) l2)
    ((null l2) l1)
    ((> (cdr (car l1)) (cdr (car l2))) (cons (car l1) (merge-cdr-> (cdr l1) l2)))
    (t (cons (car l2) (merge-cdr-> l1 (cdr l2))))))
merge-sort-cdr->function
(defun merge-sort-cdr->
  (l)
  (declare (xargs :mode :program))
  (cond ((null (cdr l)) l)
    (t (merge-cdr-> (merge-sort-cdr-> (evens l))
        (merge-sort-cdr-> (odds l))))))
print-saved-times-alistfunction
(defun print-saved-times-alist
  (raw alist ch state)
  (declare (xargs :mode :program :stobjs state))
  (cond ((endp alist) (newline ch state))
    (t (pprogn (newline ch state)
        (princ$ (caar alist) ch state)
        (princ$ ": " ch state)
        (if raw
          (princ$ (cdar alist) ch state)
          (print-rational-as-decimal (cdar alist) ch state))
        (print-saved-times-alist raw (cdr alist) ch state)))))
saved-timesmacro
(defmacro saved-times
  (&key (sort ':times) channel raw)
  (let ((channel (or channel '*standard-co*)))
    `(with-output :off summary
      (make-event (let ((alist (f-get-global 'save-time-alist state)) (sort ,SORT))
          (pprogn (print-saved-times-alist ,RAW
              (cond ((eq sort :names) (merge-sort-lexorder alist))
                ((eq sort :times) (merge-sort-cdr-> alist))
                (t alist))
              ,CHANNEL
              state)
            (value (list 'value-triple :times-printed))))))))
last-timemacro
(defmacro last-time
  nil
  `(let ((alist (f-get-global 'save-time-alist state)))
    (cond (alist (cdar alist)) (t nil))))
print-last-timemacro
(defmacro print-last-time
  nil
  `(let ((alist (f-get-global 'save-time-alist state)))
    (cond (alist (pprogn (print-rational-as-decimal (cdar alist)
            (standard-co state)
            state)
          (princ$ " seconds" (standard-co state) state)
          (newline (standard-co state) state)
          (value :invisible)))
      (t (er soft
          'print-last-time
          "There is no last-time to print!  Use SAVE-TIME first.")))))