Filtering...

super-history

books/acl2s/distribution/acl2s-hooks/super-history
other
(in-package "ACL2S-HOOKS")
other
(include-book "canonical-print")
other
(include-book "categorize-input")
other
(include-book "hacking/hacker" :dir :system)
other
(include-book "hacking/defcode" :dir :system :ttags ((defcode)))
other
(include-book "hacking/redefun" :dir :system)
other
(include-book "hacking/rewrite-code" :dir :system)
other
(program)
other
(set-state-ok t)
other
(defconst *debug-super-history*
  nil)
super-history-activepfunction
(defun super-history-activep
  (state)
  (and (boundp-global 'super-history
      state)
    (boundp-global 'super-history-reverted
      state)
    (boundp-global 'super-history-globals
      state)
    (boundp-global 'super-history-match-globals
      state)
    (consp (@ super-history))))
put-trace-specsfunction
(defun put-trace-specs
  (trace-specs state)
  (let ((old-trace-specs (@ trace-specs)))
    (if (equal old-trace-specs
        trace-specs)
      state
      (mv-let (erp val state)
        (er-progn (untrace$-fn nil state)
          (trace$-lst trace-specs
            'put-trace-specs
            state))
        (declare (ignore erp val))
        state))))
other
(defttag :acl2s-super-history)
other
(progn+touchable :vars :all (defun put-globals
    (vars vals state)
    (if (endp vars)
      state
      (pprogn (f-put-global (car vars)
          (car vals)
          state)
        (put-globals (cdr vars)
          (cdr vals)
          state)))))
other
(progn+touchable :vars :all (defun restore-globals
    (vars vals state)
    (if (endp vars)
      state
      (pprogn (let ((var (car vars)) (val (car vals)))
          (cond ((eq var 'trace-specs) (put-trace-specs val
                state))
            (t (f-put-global var
                val
                state))))
        (restore-globals (cdr vars)
          (cdr vals)
          state)))))
other
(progn+touchable :fns set-w!
  (defun restore-current-super-history
    (state)
    (if (not (super-history-activep state))
      state
      (let* ((cur (car (@ super-history))))
        (pprogn (restore-globals (@ super-history-globals)
            (cdr cur)
            state)
          (set-w! (car cur)
            state))))))
other
(defttag nil)
get-globalsfunction
(defun get-globals
  (vars state)
  (if (endp vars)
    nil
    (cons (f-get-global (car vars)
        state)
      (get-globals (cdr vars)
        state))))
cmp-globalsfunction
(defun cmp-globals
  (vars vals state)
  (or (endp vars)
    (and (if (equal (car vals)
          (f-get-global (car vars)
            state))
        t
        (if *debug-super-history*
          (cw "~%Super history: ~x0: ~x1 -> ~x2~%~%"
            (car vars)
            (car vals)
            (f-get-global (car vars)
              state))
          nil))
      (cmp-globals (cdr vars)
        (cdr vals)
        state))))
unbound-globalsfunction
(defun unbound-globals
  (vars state)
  (if (endp vars)
    nil
    (if (boundp-global (car vars)
        state)
      (unbound-globals (cdr vars)
        state)
      (cons (car vars)
        (unbound-globals (cdr vars)
          state)))))
current-super-historymacro
(defmacro current-super-history
  nil
  '(cons (w state)
    (get-globals (@ super-history-globals)
      state)))
start-super-historyfunction
(defun start-super-history
  (match-globals restore-only-globals
    state)
  (if (super-history-activep state)
    state
    (let* ((all-globals (append match-globals
           restore-only-globals)) (unbound-vars (unbound-globals all-globals
            state))
        (nil-vals (make-list (len unbound-vars))))
      (pprogn (put-globals unbound-vars
          nil-vals
          state)
        (f-put-global 'super-history-globals
          all-globals
          state)
        (f-put-global 'super-history-match-globals
          match-globals
          state)
        (f-put-global 'super-history
          (list (current-super-history))
          state)
        (f-put-global 'super-history-reverted
          nil
          state)))))
update-super-historyfunction
(defun update-super-history
  (state)
  (if (not (super-history-activep state))
    state
    (let* ((hist (@ super-history)) (prev (car hist)))
      (if (and (equal (car prev)
            (w state))
          (cmp-globals (@ super-history-match-globals)
            (cdr prev)
            state))
        state
        (pprogn (f-put-global 'super-history
            (cons (current-super-history)
              hist)
            state)
          (f-put-global 'super-history-reverted
            nil
            state))))))
clear-reverted-super-historyfunction
(defun clear-reverted-super-history
  (state)
  (f-put-global 'super-history-reverted
    nil
    state))
take-rev-prependfunction
(defun take-rev-prepend
  (n src dst)
  (if (or (zp n)
      (endp src))
    dst
    (take-rev-prepend (1- n)
      (cdr src)
      (cons (car src) dst))))
revert-super-historyfunction
(defun revert-super-history
  (n state)
  (cond ((not (super-history-activep state)) (er soft
        'revert-super-history
        "SUPER-HISTORY not active"))
    ((not (posp n)) (er soft
        'top-level
        "Bad value for SUPER-HISTORY: ~x0."
        n))
    (t (let* ((hist (@ super-history)) (rvrt (@ super-history-reverted))
          (histlen (len hist))
          (rvrtlen (len rvrt)))
        (cond ((= n histlen) (pprogn (restore-current-super-history state)
              (value :invisible)))
          ((< n histlen) (pprogn (f-put-global 'super-history
                (nthcdr (- histlen n)
                  hist)
                state)
              (f-put-global 'super-history-reverted
                (take-rev-prepend (- histlen n)
                  hist
                  rvrt)
                state)
              (restore-current-super-history state)
              (value :invisible)))
          ((<= n
             (+ histlen rvrtlen)) (pprogn (f-put-global 'super-history-reverted
                (nthcdr (- n histlen)
                  rvrt)
                state)
              (f-put-global 'super-history
                (take-rev-prepend (- n histlen)
                  rvrt
                  hist)
                state)
              (restore-current-super-history state)
              (value :invisible)))
          (t (er soft
              'top-level
              "Bad value for SUPER-HISTORY: ~x0."
              n)))))))
revert-super-history-on-errormacro
(defmacro revert-super-history-on-error
  (form)
  `(let ((revert-super-history-on-error-temp (if (super-history-activep state)
         (len (@ super-history))
         (w state))))
    (acl2-unwind-protect "revert-super-history-on-error"
      (check-vars-not-free (revert-super-history-on-error-temp)
        ,ACL2S-HOOKS::FORM)
      (if (integerp revert-super-history-on-error-temp)
        (mv-let (erp val state)
          (revert-super-history revert-super-history-on-error-temp
            state)
          (declare (ignore erp val))
          state)
        (set-w! revert-super-history-on-error-temp
          state))
      state)))
other
(push-untouchable (super-history super-history-reverted
    super-history-globals
    super-history-match-globals)
  nil)
other
(push-untouchable (put-globals restore-globals)
  t)
other
(defttag :acl2s-super-history)
other
(progn+touchable :all (redefun+rewrite ld-read-eval-print
    (:carpat (revert-world-on-error %form%)
      :recvars %form%
      :mult 1
      :repl (if (= 1 (@ ld-level))
        (revert-super-history-on-error %form%)
        (revert-world-on-error %form%))))
  (redefun+rewrite ld-read-eval-print
    :seq (:carpat %body%
      :vars %body%
      :repl (let ((old-std-oi-super-history (standard-oi state)))
        %body%))
    (:carpat (ld-print-results %trans-ans%
        state)
      :vars %trans-ans%
      :mult 1
      :repl (pprogn (if (equal old-std-oi-super-history
            *standard-oi*)
          (update-super-history state)
          state)
        (ld-print-results %trans-ans%
          state)))))
other
(defttag nil)
superlen-for-maxevt1function
(defun superlen-for-maxevt1
  (maxevt super-history)
  (if (endp super-history)
    0
    (let ((wrld (caar super-history)))
      (if (and (<= (max-absolute-event-number wrld)
            maxevt)
          (eq (caar wrld) 'command-landmark)
          (eq (cadar wrld) 'global-value))
        (len super-history)
        (superlen-for-maxevt1 maxevt
          (cdr super-history))))))
superlen-for-maxevtfunction
(defun superlen-for-maxevt
  (maxevt state)
  (superlen-for-maxevt1 maxevt
    (@ super-history)))
ubt-cd-to-superlenfunction
(defun ubt-cd-to-superlen
  (cd state)
  (er-let* ((cd-wrld (er-decode-cd cd
         (w state)
         ':ubt
         state)))
    (value (superlen-for-maxevt (max-absolute-event-number (scan-to-command (cdr cd-wrld)))
        state))))
print-ubt-superlenmacro
(defmacro print-ubt-superlen
  (cd)
  `(er-let* ((n (ubt-cd-to-superlen ',ACL2S-HOOKS::CD
         state)))
    (fmx-canonical "INDEX:~p0~%" n)))
ubu-cd-to-superlenfunction
(defun ubu-cd-to-superlen
  (cd state)
  (er-let* ((cd-wrld (er-decode-cd cd
         (w state)
         ':ubu
         state)))
    (value (superlen-for-maxevt (max-absolute-event-number cd-wrld)
        state))))
print-ubu-superlenmacro
(defmacro print-ubu-superlen
  (cd)
  `(er-let* ((n (ubu-cd-to-superlen ',ACL2S-HOOKS::CD
         state)))
    (fmx-canonical "INDEX:~p0~%" n)))