markup-hooks

(in-package "ACL2S-HOOKS")

(include-book "canonical-print")

(include-book "hacking/hacker" :dir :system)

(include-book "hacking/defcode" :dir :system :ttags ((defcode)))

(include-book "hacking/redefun" :dir :system)

(include-book "hacking/rewrite-code" :dir :system)

(program)

(set-state-ok t)

(defun acl2s-markupp
  (state)
  (and (boundp-global 'acl2s-markupp
      state)
    (get-global 'acl2s-markupp
      state)))

(defun acl2s-markup-begin
  (state)
  (assign acl2s-markupp t))

(push-untouchable acl2s-markupp
  nil)

(defun print-checkpoint
  (fmt-string state)
  (pfmx-canonical "$ChEcKpOiNt{$~@0$ChEcKpOiNt}$~%"
    fmt-string))

(defttag :acl2s-markup)

(progn+touchable :all (redefun+rewrite waterfall-msg1
    (:carpat %body%
      :vars %body%
      :repl (pprogn (if (and (acl2s-markupp state)
            (f-boundp-global 'checkpoint-processors
              state)
            (member-eq processor
              (@ checkpoint-processors)))
          (print-checkpoint (tilde-@-clause-id-phrase cl-id)
            state)
          state)
        %body%)))
  (redefun+rewrite waterfall
    (:carpat %body%
      :vars %body%
      :repl (pprogn (if (and (acl2s-markupp state)
            (f-boundp-global 'checkpoint-processors
              state)
            (not (member-eq 'proof-tree
                (@ inhibit-output-lst))))
          (cond ((and (null pool-lst) (eql forcing-round 0)) state)
            (pool-lst (if (member-eq :induct (@ checkpoint-processors))
                (print-checkpoint (tilde-@-pool-name-phrase forcing-round pool-lst)
                  state)
                state))
            (t (if (member-eq :forcing-round (@ checkpoint-processors))
                (print-checkpoint (tilde-@-pool-name-phrase forcing-round pool-lst)
                  state)
                state)))
          state)
        %body%))))

(defttag nil)