interaction-hooks

(in-package "ACL2S-HOOKS")

(include-book "canonical-print")

(include-book "categorize-input")

(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)

(include-book "super-history" :ttags ((:acl2s-super-history) (defcode)))

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

(include-book "protection-hooks" :ttags ((:acl2s-protection) (:acl2s-super-history)
    (defcode)))

(program)

(set-state-ok t)

(defun dump-environment-info
  (state)
  (declare (xargs :mode :program :stobjs state))
  (mv-let (erp in-wormhole
      state)
    (wormhole-p state)
    (declare (ignore erp))
    (mv (list (@ current-package)
        (@ ld-level)
        (if in-wormhole
          1
          0)
        (if (raw-mode-p state)
          1
          0)
        (non-hidden-package-list)
        (max-absolute-event-number (w state))
        (if (boundp-global 'super-history
            state)
          (len (@ super-history))
          0)
        (if (boundp-global 'super-history-reverted
            state)
          (len (@ super-history-reverted))
          0))
      state)))

(defun begin-environment
  (state)
  (mv-let (env-info state)
    (dump-environment-info state)
    (mv-let (erp val state)
      (with-upcase-base10 (mv-let (col state)
          (fmt1 "$~@p{$~%~xx$~@p$"
            (list (cons #\p "EnViRoNmEnT")
              (cons #\x env-info))
            0
            *standard-co*
            state
            nil)
          (mv nil col state)))
      (declare (ignore erp val))
      state)))

(defun end-environment
  (state)
  (mv-let (irrel-col state)
    (fmt1 "$~@p}$~%"
      (list (cons #\p "EnViRoNmEnT"))
      0
      *standard-co*
      state
      nil)
    (declare (ignore irrel-col))
    state))

(defun acl2s-interactionp
  (state)
  (and (f-boundp-global 'acl2s-interactionp
      state)
    (f-get-global 'acl2s-interactionp
      state)))

(defttag :acl2s-interaction)

(progn+touchable :all (redefun+rewrite ld-print-prompt
    (:carpat %body%
      :vars %body%
      :repl (pprogn (if (and (acl2s-interactionp state)
            (eq (standard-oi state)
              *standard-oi*))
          (begin-environment state)
          state)
        (mv-let (col state)
          %body%
          (pprogn (if (and (acl2s-interactionp state)
                (eq (standard-oi state)
                  *standard-oi*))
              (end-environment state)
              state)
            (mv col state))))))
  (redefun+rewrite ld-read-eval-print
    :seq (:carpat %body%
      :vars %body%
      :repl (let ((old-std-oi-interaction (standard-oi state)))
        %body%))
    (:carpat (ld-print-results %trans-ans%
        state)
      :vars %trans-ans%
      :mult 1
      :repl (pprogn (if (and (equal old-std-oi-interaction
              *standard-oi*)
            (acl2s-interactionp state))
          (prog2$ (fmx-to-comment-window "${~@0}$~%" "SuCcEsS")
            state)
          state)
        (ld-print-results %trans-ans%
          state))))
  (redefun+rewrite defpkg-fn
    (:carpat (let* ((imports %val%) . %rst%)
        %body%)
      :vars (%val% %rst% %body%)
      :mult 1
      :repl (let* ((imports %val%) . %rst%)
        (pprogn (if (acl2s-interactionp state)
            (pfmx-canonical "$~@0{$~%~x1~%$~@0}$~%"
              "DeFpKg"
              (cons name imports))
            state)
          %body%))))
  (defun dump-pkgs
    (names state)
    (if (endp names)
      state
      (pprogn (let ((imports (package-imports (car names))))
          (if (consp imports)
            (pfmx-canonical "$~@0{$~%~x1~%$~@0}$~%"
              "DeFpKg"
              (cons (car names) imports))
            state))
        (dump-pkgs (cdr names)
          state))))
  (redefun+rewrite prove
    (:carpat (state-global-let* ((guard-checking-on nil) . %bindings-rest%)
        %body%)
      :vars (%body% %bindings-rest%)
      :mult *
      :repl (state-global-let* ((guard-checking-on (if (and (equal (@ guard-checking-on) :none)
               (boundp-global 'trace-specs state)
               (@ trace-specs))
             :none nil)) . %bindings-rest%)
        %body%))))

(defttag nil)

(make-event (pprogn (f-put-global 'acl2s-interactionp
      nil
      state)
    (value '(value-triple nil))))

(defun acl2s-interaction-begin
  (state)
  (pprogn (f-put-global 'acl2s-interactionp
      t
      state)
    (dump-pkgs (non-hidden-package-list)
      state)
    (value t)))

(push-untouchable acl2s-interactionp
  nil)