Filtering...

categorize-input

books/acl2s/distribution/acl2s-hooks/categorize-input
other
(in-package "ACL2S-HOOKS")
other
(include-book "canonical-print")
other
(defconst *query-fns*
  '(pbt pc
    pcb
    pcb!
    pcs
    pe
    pe!
    pf
    pl
    pr
    pr!
    trans
    trans1
    trans!
    thm
    props
    test?
    help
    docs
    doc
    doc!
    xdoc
    args
    more
    more!
    nqthm-to-acl2
    pso
    pso!
    pstack
    verbose-pstack
    value
    value-triple
    ttags-seen
    print-package-imports
    print-keyword-info
    categorize-input
    print-input-categorization))
other
(defconst *undoable-fns*
  '(in-package in-package-fn
    defpkg
    defpkg-fn
    set-ld-skip-proofsp
    set-ld-redefinition-action
    set-ld-prompt
    set-ld-pre-eval-filter
    set-ld-error-triples
    set-ld-error-action
    set-ld-query-control-alist
    set-cbd
    set-cbd-fn
    set-guard-checking
    set-raw-mode
    set-raw-mode-fn
    set-tainted-okp
    trace$
    trace*
    trace!
    trace$-lst
    trace$-fn
    untrace$
    untrace$-fn
    maybe-untrace$
    maybe-untrace$-fn
    reset-prehistory
    reset-prehistory-fn
    set-ccg-verbose))
other
(defconst *critical-settings-globals*
  '(current-package ld-skip-proofsp
    ld-redefinition-action
    ld-pre-eval-filter
    ld-error-triples
    ld-error-action
    ld-query-control-alist
    connected-book-directory
    guard-checking-on
    acl2-raw-mode-p
    raw-mode-restore-lst
    saved-output-token-lst
    tainted-okp
    skipped-proofsp
    temp-touchable-vars
    temp-touchable-fns
    ttags-allowed))
other
(defconst *monitor-settings-globals*
  '(trace-specs gstackp brr-monitored-runes make-event-debug))
other
(defconst *presentation-settings-globals*
  '(ld-prompt ld-pre-eval-print
    ld-post-eval-print
    ld-evisc-tuple
    ld-verbose
    prompt-function
    triple-print-prefix
    print-base
    print-case
    proofs-co
    inhibit-output-lst
    print-clause-ids
    ccg-verbose
    gag-mode
    checkpoint-forced-goals
    checkpoint-processors
    checkpoint-summary-limit
    saved-output-p
    saved-output-token-lst
    evalable-ld-printingp
    evalable-printing-abstractions))
other
(defconst *settings-globals*
  (append *critical-settings-globals*
    *monitor-settings-globals*
    *presentation-settings-globals*))
other
(defconst *restorable-transient-globals*
  '(gag-state gag-state-saved saved-output-reversed))
other
(program)
other
(set-state-ok t)
er-ormacro
(defmacro er-or
  (form &rest forms)
  `(mv-let (er-or-erp er-or-val
      state)
    ,ACL2S-HOOKS::FORM
    (if er-or-erp
      ,(IF (CONSP ACL2S-HOOKS::FORMS)
     (CONS 'ACL2S-HOOKS::ER-OR ACL2S-HOOKS::FORMS)
     '(ACL2S-HOOKS::MV T ACL2S-HOOKS::ER-OR-VAL ACL2S-HOOKS::STATE))
      (mv nil
        er-or-val
        state))))
nil-listpfunction
(defun nil-listp
  (lst)
  (or (null lst)
    (and (consp lst)
      (null (car lst))
      (nil-listp (cdr lst)))))
er-trans-stobjs-out-fnfunction
(defun er-trans-stobjs-out-fn
  (form state)
  (mv-let (flg val
      bindings
      state)
    (translate1 form
      :stobjs-out '((:stobjs-out . :stobjs-out))
      t
      'check-input
      (w state)
      state)
    (declare (ignore val))
    (mv flg
      (translate-deref :stobjs-out bindings)
      state)))
chk-in-package-fnfunction
(defun chk-in-package-fn
  (form state)
  (cond ((and (consp form)
       (eq (car form) 'in-package)
       (consp (cdr form))
       (member-equal (cadr form)
         (non-hidden-package-list))
       (null (cddr form))) (value :invisible))
    (t (mv t nil state))))
chk-begin-book-fnfunction
(defun chk-begin-book-fn
  (form state)
  (cond ((and (consp form)
       (eq (car form) 'begin-book)
       (true-listp (cdr form))) (er-progn (er-trans-stobjs-out-fn form
          state)
        (value :invisible)))
    (t (mv t nil state))))
other
(make-event (if (getprop 'primitive-event-macros
      'symbol-class
      nil
      'current-acl2-world
      (w state))
    (value '(value-triple 'primitive-event-macros))
    (value '(defun primitive-event-macros
        nil
        (declare (xargs :guard t :mode :logic))
        *primitive-event-macros*))))
chk-top-level-event-fnfunction
(defun chk-top-level-event-fn
  (form state)
  (chk-embedded-event-form form
    form
    (w state)
    'top-level
    state
    (primitive-event-macros)
    nil
    nil
    nil))
chk-value-triple-fnfunction
(defun chk-value-triple-fn
  (form state)
  (cond ((and (consp form)
       (true-listp (cdr form))
       (symbolp (car form))
       (eq (car form) 'value-triple)) (value :invisible))
    ((and (consp form)
       (true-listp (cdr form))
       (member (car form)
         '(progn er-progn))) (er-progn (chk-value-triple-fn (cadr form)
          state)
        (if (consp (cddr form))
          (chk-value-triple-fn (cons 'progn (cddr form))
            state)
          (value :invisible))
        (value :invisible)))
    (t (mv t nil state))))
chk-query-fnfunction
(defun chk-query-fn
  (form state)
  (cond ((and (consp form)
       (true-listp (cdr form))
       (symbolp (car form))
       (member (car form) *query-fns*)) (value :invisible))
    ((and (consp form)
       (true-listp (cdr form))
       (member (car form)
         '(progn er-progn))) (er-progn (chk-query-fn (cadr form)
          state)
        (if (consp (cddr form))
          (chk-query-fn (cons 'progn (cddr form))
            state)
          (value :invisible))
        (value :invisible)))
    (t (mv t nil state))))
chk-command-fnfunction
(defun chk-command-fn
  (form state)
  (cond ((and (consp form)
       (true-listp (cdr form))
       (symbolp (car form))
       (or (member (car form) *undoable-fns*)
         (member (car form) *query-fns*)
         (and (eq (car form) 'assign)
           (consp (cdr form))
           (member (cadr form)
             (if (boundp-global 'super-history-globals
                 state)
               (@ super-history-globals)
               *settings-globals*)))
         (and (member (car form)
             '(f-put-global put-global))
           (consp (cdr form))
           (consp (cadr form))
           (eq (caadr form) 'quote)
           (consp (cdadr form))
           (member (cadadr form)
             (if (boundp-global 'super-history-globals
                 state)
               (@ super-history-globals)
               *settings-globals*))))) (value :invisible))
    ((and (consp form)
       (true-listp (cdr form))
       (member (car form)
         '(progn er-progn))) (er-progn (chk-command-fn (cadr form)
          state)
        (if (consp (cddr form))
          (chk-command-fn (cons 'progn (cddr form))
            state)
          (value :invisible))
        (value :invisible)))
    (t (mv t nil state))))
chk-pkg-string-fnfunction
(defun chk-pkg-string-fn
  (form state)
  (if (and (stringp form)
      (member-equal form
        (non-hidden-package-list)))
    (value :invisible)
    (mv t nil state)))
categorize-input-fnfunction
(defun categorize-input-fn
  (form state)
  (state-global-let* ((inhibit-output-lst *valid-output-names*))
    (if (raw-mode-p state)
      (er-or (er-progn (chk-query-fn form
            state)
          (value :query))
        (if (atom form)
          (value :value)
          (value :raw)))
      (er-or (er-progn (chk-in-package-fn form
            state)
          (value :in-package))
        (er-progn (chk-begin-book-fn form
            state)
          (value :begin-book))
        (er-progn (chk-value-triple-fn form
            state)
          (value :value-triple))
        (er-progn (chk-query-fn form
            state)
          (value :query))
        (er-progn (chk-top-level-event-fn form
            state)
          (value :event))
        (er-progn (chk-pkg-string-fn form
            state)
          (value :command))
        (er-progn (chk-command-fn form
            state)
          (value :command))
        (er-let* ((stobjs-out (er-trans-stobjs-out-fn form
               state)))
          (if (nil-listp stobjs-out)
            (if (symbolp form)
              (mv-let (erp v state)
                (ld (list form)
                  :ld-error-action :return :ld-user-stobjs-modified-warning t)
                (if (or erp (equal v :error))
                  (value :bad)
                  (value :value)))
              (value :value))
            (value :action)))
        (value :bad)))))
categorize-inputmacro
(defmacro categorize-input
  (form-expr)
  `(categorize-input-fn ,ACL2S-HOOKS::FORM-EXPR
    state))
print-input-categorizationmacro
(defmacro print-input-categorization
  (form)
  `(mv-let (erp val state)
    (categorize-input-fn ',ACL2S-HOOKS::FORM
      state)
    (if (or erp (not (symbolp val)))
      (mv t :invisible state)
      (fmx-canonical "CATEGORY~y0~%"
        val))))
colon-qmacro
(defmacro colon-q
  nil
  '(exit-ld state))
no-lambda-keywordspfunction
(defun no-lambda-keywordsp
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (cond ((null lst) t)
    ((lambda-keywordp (car lst)) nil)
    (t (no-lambda-keywordsp (cdr lst)))))
get-keyword-infofunction
(defun get-keyword-info
  (key state)
  (let* ((wrld (w state)) (aliases (ld-keyword-aliases state))
      (name (symbol-name key))
      (sym (intern name "ACL2"))
      (temp (assoc-eq key
          aliases)))
    (cond (temp (cdr temp))
      ((eq sym 'q) (list 0 'colon-q))
      ((function-symbolp sym
         wrld) (list (length (formals sym wrld))
          sym))
      ((getprop sym
         'macro-body
         nil
         'current-acl2-world
         wrld) (let ((margs (getprop sym
               'macro-args
               '(:error "See LD-READ-KEYWORD-COMMAND.")
               'current-acl2-world
               wrld)))
          (if (no-lambda-keywordsp margs)
            (list (length margs) sym)
            :lambda-keywords)))
      (t :undefined))))
keyword-infomacro
(defmacro keyword-info
  (key-expr)
  `(get-keyword-info ,ACL2S-HOOKS::KEY-EXPR
    state))
print-keyword-infomacro
(defmacro print-keyword-info
  (key)
  `(print-canonical (keyword-info ',ACL2S-HOOKS::KEY)))