inline-book

(defun remove-entry-by-key
  (key alist)
  (if (endp alist)
    nil
    (if (eq key (caar alist))
      (cdr alist)
      (cons (car alist) (remove-entry-by-key key (cdr alist))))))

(defun generate-add-include-book-dir-calls
  (dir-alist)
  (if (or (endp dir-alist) t)
    nil
    (cons `(add-include-book-dir ,(CAAR DIR-ALIST) ,(CDAR DIR-ALIST))
      (generate-add-include-book-dir-calls (cdr dir-alist)))))

(defun compute-inline-book-fn
  (user-book-name dir respect-localp state)
  (declare (xargs :mode :program :stobjs state))
  (let* ((ctx 'inline-book) (wrld0 (w state))
      (saved-acl2-defaults-table (table-alist 'acl2-defaults-table wrld0))
      (saved-acl2-defaults-table-minus-book-dir-alist (remove-entry-by-key :include-book-dir-alist saved-acl2-defaults-table))
      (saved-book-dir-alist (cdr (assoc-eq :include-book-dir-alist saved-acl2-defaults-table))))
    (er-let* ((dir-value (cond (dir (include-book-dir-with-chk soft ctx dir))
           (t (value (cbd))))))
      (mv-let (full-book-string full-book-name
          directory-name
          familiar-name)
        (parse-book-name dir-value user-book-name ".lisp" ctx state)
        (declare (ignore full-book-name directory-name familiar-name))
        (er-progn (chk-input-object-file full-book-string ctx state)
          (er-let* ((ev-lst (read-object-file full-book-string ctx state)))
            (value `(,@(IF RESPECT-LOCALP
      '(ENCAPSULATE NIL)
      '(PROGN)) ,@(IF (EQ :LOGIC (CDR (ASSOC-EQ :DEFUN-MODE SAVED-ACL2-DEFAULTS-TABLE)))
      NIL
      '((LOGIC)))
                ,@(CDR EV-LST)
                ,@(IF RESPECT-LOCALP
      'NIL
      (CONS
       `(TABLE ACL2-DEFAULTS-TABLE NIL
               ',SAVED-ACL2-DEFAULTS-TABLE-MINUS-BOOK-DIR-ALIST :CLEAR)
       (GENERATE-ADD-INCLUDE-BOOK-DIR-CALLS SAVED-BOOK-DIR-ALIST)))
                (value-triple ',FULL-BOOK-STRING)))))))))