Filtering...

bridge

books/hacking/bridge

Included Books

doc-section
other
(in-package "ACL2")
include-book
(include-book "doc-section")
other
(program)
other
(set-state-ok t)
replace-last-cltl-command-wrldfunction
(defun replace-last-cltl-command-wrld
  (cltl-command wrld)
  (declare (xargs :mode :program))
  (cond ((endp wrld) nil)
    ((and (consp (car wrld))
       (eq (caar wrld) 'cltl-command)
       (consp (cdar wrld))
       (eq (cadar wrld) 'global-value)) (cons (list* 'cltl-command 'global-value cltl-command)
        (cdr wrld)))
    (t (cons (car wrld)
        (replace-last-cltl-command-wrld cltl-command (cdr wrld))))))
replace-last-cltl-commandmacro
(defmacro replace-last-cltl-command
  (cltl-command)
  `(progn!=touchable :fns set-w!
    :loop-only (pprogn (set-w! (replace-last-cltl-command-wrld ,(IF (AND (CONSP CLTL-COMMAND) (SYMBOLP (CAR CLTL-COMMAND))
          (MEMBER-EQ (CAR CLTL-COMMAND)
                     '(DEFUNS DEFSTOBJ DEFPKG DEFCONST DEFMACRO MEMOIZE
                              UNMEMOIZE)))
     `',CLTL-COMMAND
     CLTL-COMMAND)
          (w state))
        state)
      (value :invisible))))
remove-last-cltl-command-wrldfunction
(defun remove-last-cltl-command-wrld
  (wrld)
  (declare (xargs :mode :program))
  (cond ((endp wrld) nil)
    ((and (consp (car wrld))
       (eq (caar wrld) 'cltl-command)
       (consp (cdar wrld))
       (eq (cadar wrld) 'global-value)) (cdr wrld))
    (t (cons (car wrld) (remove-last-cltl-command-wrld (cdr wrld))))))
remove-last-cltl-commandmacro
(defmacro remove-last-cltl-command
  nil
  '(progn!=touchable :fns set-w!
    :loop-only (pprogn (set-w! (remove-last-cltl-command-wrld (w state)) state)
      (value :invisible))))
reconstruct-declare-lstfunction
(defun reconstruct-declare-lst
  (spec)
  (cond ((atom spec) nil)
    ((eq 'declare (car spec)) (list spec))
    ((consp (car spec)) (list (cons 'declare spec)))
    (t (list (list 'declare spec)))))
defun-bridgemacro
(defmacro defun-bridge
  (name ll
    &key
    (logic 'nil logic-p)
    (logic-declare 'nil)
    (program 'nil program-p)
    (program-declare 'nil)
    (raw 'nil raw-p)
    (raw-declare 'nil)
    (doc 'nil))
  (declare (xargs :guard (and (or (and logic-p program-p (not raw-p))
          (and logic-p (not program-p) raw-p)
          (and (not logic-p) program-p raw-p))
        (implies doc (stringp doc))))
    (ignorable program-p))
  (let* ((ignorable-decl-lst (and ll `((declare (ignorable . ,LL))))) (raw-def-tuple `(,NAME ,LL
          ,@IGNORABLE-DECL-LST . ,(IF RAW-P
     (APPEND (RECONSTRUCT-DECLARE-LST RAW-DECLARE) (LIST RAW))
     (APPEND (RECONSTRUCT-DECLARE-LST PROGRAM-DECLARE) (LIST PROGRAM)))))
      (loop-def `(defun ,NAME
          ,LL
          ,@(AND DOC (LIST DOC)) . ,(IF LOGIC-P
     (APPEND (LIST '(DECLARE (XARGS :MODE :LOGIC))) IGNORABLE-DECL-LST
             (RECONSTRUCT-DECLARE-LST LOGIC-DECLARE) (LIST LOGIC))
     (APPEND (LIST '(DECLARE (XARGS :MODE :PROGRAM))) IGNORABLE-DECL-LST
             (RECONSTRUCT-DECLARE-LST PROGRAM-DECLARE) (LIST PROGRAM)))))
      (code (list loop-def
          (if raw-p
            '(remove-last-cltl-command)
            `(replace-last-cltl-command (defuns ,(IF LOGIC-P
     :LOGIC
     :PROGRAM)
                nil
                ,RAW-DEF-TUPLE))))))
    `(progn (assert-unbound ,NAME)
      ,@(IF LOGIC-P
      NIL
      `((ENSURE-PROGRAM-ONLY-FLAG ,NAME)))
      (ensure-special-raw-definition-flag ,NAME)
      (defcode :loop ,CODE
        ,@(AND RAW-P
       `(:EXTEND
         (IN-RAW-MODE (MAYBE-PUSH-UNDO-STACK 'DEFUN ',NAME)
          (DEFUN . ,RAW-DEF-TUPLE) (DEFUN-*1* ,NAME ,LL (,NAME . ,LL)))
         :RETRACT (IN-RAW-MODE (MAYBE-POP-UNDO-STACK ',NAME))))
        :compile ((defun . ,RAW-DEF-TUPLE) . ,(AND RAW-P `((DEFUN-*1* ,NAME ,LL (,NAME . ,LL)))))))))