wizard - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "da-base")

include-book

(include-book "clause-processors/unify-subst" :dir :system)

other

(def-primitive-aggregate wizadvice
  (pattern restrict msg args)
  :tag :advice-form)

collect-matches-from-termmutual-recursion

(mutual-recursion (defun collect-matches-from-term
    (pattern x acc)
    (b* (((mv matchp sigma) (simple-one-way-unify pattern x nil)) (acc (if matchp
            (cons sigma acc)
            acc))
        ((when (or (atom x) (eq (car x) 'quote))) acc))
      (collect-matches-from-term-list pattern (cdr x) acc)))
  (defun collect-matches-from-term-list
    (pattern x acc)
    (b* (((when (atom x)) acc) (acc (collect-matches-from-term pattern (car x) acc)))
      (collect-matches-from-term-list pattern (cdr x) acc))))

simpler-trans-evalfunction

(defun simpler-trans-eval
  (x alist state)
  (declare (xargs :stobjs state :mode :program))
  (b* (((mv er (cons ?trans eval)) (simple-translate-and-eval-error-double x
         alist
         nil
         (msg "Term was ~x0" x)
         'simpler-trans-eval
         (w state)
         state
         t
         (f-get-global 'safe-mode state)
         (gc-off state))))
    (or (not er)
      (er hard?
        'simpler-trans-eval
        "Evaluation somehow failed for ~x0: ~@1"
        x
        er))
    eval))

simpler-trans-eval-listfunction

(defun simpler-trans-eval-list
  (x alist state)
  (declare (xargs :stobjs state :mode :program))
  (b* (((mv er (cons ?trans eval)) (simple-translate-and-eval-error-double x
         alist
         nil
         (msg "Term was ~x0" x)
         'simpler-trans-eval
         (w state)
         state
         t
         (f-get-global 'safe-mode state)
         (gc-off state))))
    (or (not er)
      (er hard?
        'simpler-trans-eval
        "Evaluation somehow failed for ~x0: ~@1"
        x
        er))
    eval))

filter-sigmas-by-restrictionfunction

(defun filter-sigmas-by-restriction
  (restrict sigmas state)
  (declare (xargs :stobjs state :mode :program))
  (b* (((when (atom sigmas)) nil) (evaluation (simpler-trans-eval restrict (car sigmas) state))
      ((unless evaluation) (filter-sigmas-by-restriction restrict (cdr sigmas) state))
      (rest (filter-sigmas-by-restriction restrict (cdr sigmas) state)))
    (cons (car sigmas) rest)))

wizard-print-advicefunction

(defun wizard-print-advice
  (sigma advice state)
  (declare (xargs :stobjs state :mode :program))
  (b* (((wizadvice advice) advice) (args-evaled (simpler-trans-eval advice.args sigma state))
      (msg (cons (concatenate 'string "~|~%Wizard: " advice.msg "~%")
          (pairlis2 '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)
            args-evaled))))
    (cw "~@0" msg)
    nil))

wizard-print-advice-listfunction

(defun wizard-print-advice-list
  (sigmas advice state)
  (declare (xargs :stobjs state :mode :program))
  (if (atom sigmas)
    nil
    (prog2$ (wizard-print-advice (car sigmas) advice state)
      (wizard-print-advice-list (cdr sigmas) advice state))))

wizard-do-advicefunction

(defun wizard-do-advice
  (clause advice state)
  (declare (xargs :stobjs state :mode :program))
  (b* (((wizadvice advice) advice) (sigmas (collect-matches-from-term-list advice.pattern clause nil))
      (sigmas (remove-duplicates-equal sigmas))
      (sigmas (if advice.restrict
          (filter-sigmas-by-restriction advice.restrict sigmas state)
          sigmas)))
    (wizard-print-advice-list sigmas advice state)))

wizard-do-advice-listfunction

(defun wizard-do-advice-list
  (clause advices state)
  (declare (xargs :stobjs state :mode :program))
  (if (atom advices)
    nil
    (prog2$ (wizard-do-advice clause (car advices) state)
      (wizard-do-advice-list clause (cdr advices) state))))

other

(table wizard-advice)

get-wizard-advicefunction

(defun get-wizard-advice
  (world)
  (cdr (assoc 'wizadvice (table-alist 'wizard-advice world))))

add-wizard-advicemacro

(defmacro add-wizard-advice
  (&key pattern restrict msg args)
  `(table wizard-advice
    'wizadvice
    (cons (make-wizadvice :pattern ',PATTERN
        :restrict ',RESTRICT
        :msg ,MSG
        :args ',ARGS)
      (get-wizard-advice world))))

wizard-fnfunction

(defun wizard-fn
  (stable-under-simplificationp clause state)
  (declare (xargs :stobjs state :mode :program))
  (if (not stable-under-simplificationp)
    nil
    (let ((advices (get-wizard-advice (w state))))
      (prog2$ (wizard-do-advice-list clause advices state) nil))))

wizardmacro

(defmacro wizard
  nil
  `(wizard-fn stable-under-simplificationp clause state))

enable-wizardmacro

(defmacro enable-wizard nil `(add-default-hints '((wizard))))