Filtering...

subsumption

books/hacking/subsumption

Included Books

doc-section
other
(in-package "ACL2")
include-book
(include-book "doc-section")
other
(program)
other
(set-state-ok t)
ttags-seen-at-defttagfunction
(defun ttags-seen-at-defttag
  (name path wrld last)
  (if (endp wrld)
    (er hard
      'subsume-ttags-since-defttag
      "Error retrieving old ttags-seen.")
    (if (and (consp (car wrld))
        (eq 'ttags-seen (caar wrld))
        (consp (cdar wrld))
        (eq 'global-value (cadar wrld)))
      (let ((c (assoc-eq name (cddar wrld))))
        (if (and (consp c) (member-equal path (cdr c)))
          (ttags-seen-at-defttag name
            path
            (cdr wrld)
            (cddar wrld))
          last))
      (ttags-seen-at-defttag name
        path
        (cdr wrld)
        last))))
ttags-seen-at-current-defttagfunction
(defun ttags-seen-at-current-defttag
  (state)
  (let ((wrld (w state)))
    (ttags-seen-at-defttag (ttag wrld)
      (active-book-name wrld state)
      wrld
      (global-val 'ttags-seen wrld))))
subsume-ttags-since-defttagmacro
(defmacro subsume-ttags-since-defttag
  nil
  '(defcode :loop (progn!=touchable :fns install-event
      (let ((original-ttags-seen (ttags-seen-at-current-defttag state)) (current-ttags-seen (global-val 'ttags-seen (w state))))
        (if (equal original-ttags-seen current-ttags-seen)
          (value :redundant)
          (install-event ':invisible
            '(subsume-ttags-since-defttag)
            'subsume-ttags-since-defttag
            0
            nil
            nil
            nil
            'subsume-ttags-since-defttag
            (putprop 'ttags-seen
              'global-value
              original-ttags-seen
              (w state))
            state))))))
other
(push-untouchable saved-ttags-seen nil)
other
(push-untouchable saved-ttag nil)
restore-ttags-seenmacro
(defmacro restore-ttags-seen
  nil
  '(progn!-with-bindings ((temp-touchable-fns '(install-event) set-temp-touchable-fns))
    (if (implies (boundp-global 'saved-ttags-seen state)
        (equal (@ saved-ttags-seen)
          (global-val 'ttags-seen (w state))))
      (stop-redundant-event '(restore-ttags-seen) state)
      (install-event ':invisible
        '(restore-ttags-seen)
        'restore-ttags-seen
        0
        nil
        nil
        nil
        'restore-ttags-seen
        (putprop 'ttags-seen
          'global-value
          (@ saved-ttags-seen)
          (w state))
        state))))
progn!+subsume-ttagsmacro
(defmacro progn!+subsume-ttags
  (ttag-spec &rest form-lst)
  `(progn!-with-bindings ((progn!+subsume-ttags_saved-ttv (@ temp-touchable-vars)) (temp-touchable-vars '(ttags-allowed saved-ttag saved-ttags-seen)
        set-temp-touchable-vars))
    (progn!-with-bindings ((ttags-allowed (@ ttags-allowed)) (saved-ttags-seen (global-val 'ttags-seen (w state)))
        (saved-ttag (ttag (w state))))
      (progn! (defcode :loop ((er-let* ((ttags (chk-well-formed-ttags ',TTAG-SPEC
                  (cbd)
                  'progn!+subsume-ttags
                  state)))
             (assign ttags-allowed ttags)) (set-temp-touchable-vars (@ progn!+subsume-ttags_saved-ttv)
              state)))
        ,@FORM-LST
        (defcode :loop ((if (eq (@ saved-ttag) (ttag (w state)))
             (value :invisible)
             (er soft
               'progn!+subsume-ttags
               "Please do not change the currently active ttag within the ~
                body of ~x0."
               'progn!+subsume-ttags)) (restore-ttags-seen)))))))
progn+subsume-ttagsmacro
(defmacro progn+subsume-ttags
  (ttag-spec &rest form-lst)
  `(progn!+subsume-ttags ,TTAG-SPEC (progn . ,FORM-LST)))