Filtering...

defcode

books/hacking/defcode

Included Books

hacker progn-bang-enh
other
(in-package "ACL2")
include-book
(include-book "hacker")
other
(program)
other
(set-state-ok t)
defcode-code-listpfunction
(defun defcode-code-listp
  (l)
  (or (null l)
    (and (consp l) (consp (car l)) (not (eq 'lambda (caar l))))))
defcode-ensure-code-listfunction
(defun defcode-ensure-code-list
  (c)
  (if (defcode-code-listp c)
    c
    (list c)))
other
(defttag defcode)
include-book
(include-book "progn-bang-enh" :ttags ((defcode)))
other
(progn+touchable :fns install-event
  (defun defcode-fn
    (loop extend retract state event-form)
    (let* ((loop-lst (defcode-ensure-code-list loop)) (extend-lst (defcode-ensure-code-list extend))
        (retract-lst (defcode-ensure-code-list retract)))
      (er-progn (if loop-lst
          (progn!-fn loop-lst nil state)
          (value nil))
        (if (or extend-lst retract-lst)
          (let* ((event-form (or event-form
                 `(defcode :loop ,LOOP-LST
                   :extend ,EXTEND-LST
                   :retract ,RETRACT-LST))) (wrld (w state))
              (wrld (if extend-lst
                  (putprop 'extend-progn! 'global-value extend-lst wrld)
                  wrld))
              (wrld (if retract-lst
                  (putprop 'retract-progn! 'global-value retract-lst wrld)
                  wrld)))
            (install-event ':invisible
              event-form
              'defcode
              0
              nil
              nil
              nil
              'defcode
              wrld
              state))
          (value nil))))))
other
(modify-raw-defun-permanent add-trip
  pre-defcode-add-trip
  (world-name world-key trip status)
  (progn (pre-defcode-add-trip world-name world-key trip status)
    (when (and (eq (car trip) 'extend-progn!)
        (eq (cadr trip) 'global-value))
      (mv-let (erp val state)
        (state-global-let* ((inhibit-output-lst (union-eq (@ inhibit-output-lst)
               (remove 'error *valid-output-names*))))
          (progn!-fn (cddr trip) nil *the-live-state*))
        (declare (ignore val state))
        (when erp (hard-error 'defcode "Error returned." nil))))))
other
(modify-raw-defun-permanent undo-trip
  pre-defcode-undo-trip
  (world-name world-key trip)
  (progn (pre-defcode-undo-trip world-name world-key trip)
    (when (and (eq (car trip) 'retract-progn!)
        (eq (cadr trip) 'global-value))
      (mv-let (erp val state)
        (state-global-let* ((inhibit-output-lst (union-eq (@ inhibit-output-lst)
               (remove 'error *valid-output-names*))))
          (progn!-fn (cddr trip) nil *the-live-state*))
        (declare (ignore val state))
        (when erp (hard-error 'defcode "Error returned." nil))))))
other
(in-raw-mode (defvar *set-w-reentry-protect* nil))
other
(modify-raw-defun-permanent set-w
  pre-defcode-set-w
  (flag wrld state)
  (declare (special *set-w-reentry-protect*))
  (if *set-w-reentry-protect*
    (hard-error 'defcode
      "Attempt to change world within DEFCODE code."
      nil)
    (let ((*set-w-reentry-protect* t))
      (pre-defcode-set-w flag wrld state))))
defcodemacro
(defmacro defcode
  (&whole event-form &key loop extend retract compile)
  (let ((loop-code-lst `((defcode-fn ',LOOP ',EXTEND ',RETRACT state ',EVENT-FORM))) (compile-code-lst (cond ((atom compile) nil)
          ((and (consp compile)
             (consp (car compile))
             (not (eq 'lambda (caar compile)))) compile)
          (t (list compile)))))
    (if compile-code-lst
      `(progn! (progn! :loop-only . ,LOOP-CODE-LST)
        (progn! :compile-only . ,COMPILE-CODE-LST))
      `(progn! :loop-only . ,LOOP-CODE-LST))))
other
(defcode :extend (in-raw-mode (defmacro progn!
      (&rest r)
      (let ((sym (gensym)))
        `(let ((state *the-live-state*) (,SYM (f-get-global 'acl2-raw-mode-p *the-live-state*)))
          (declare (ignorable state))
          ,@(COND ((NOT (CONSP R)) (LIST NIL)) ((EQ (CAR R) :LOOP-ONLY) (LIST NIL))
        ((EQ (CAR R) :COMPILE-ONLY) (CDR R))
        ((EQ (CAR R) :STATE-GLOBAL-BINDINGS) (CDDR R)) (T R))
          (f-put-global 'acl2-raw-mode-p ,SYM state)
          (value nil))))))
other
(defttag nil)
assert-unboundmacro
(defmacro assert-unbound
  (&rest names)
  `(defcode :loop (in-raw-mode (dolist (name ',NAMES)
        (when (and (not (f-get-global 'ld-redefinition-action *the-live-state*))
            (or (getprop name
                'absolute-event-number
                nil
                'current-acl2-world
                (w *the-live-state*))
              (boundp name)
              (fboundp name)
              (macro-function name)))
          (hard-error 'assert-unbound
            "Already has an ACL2 or raw Lisp definition: ~x0~%"
            (list (cons #\0 name))))))))