		Search-engine friendly clone of the ACL2 documentation.

Vl-includeskips

Vl-includeskips-install-controller

Install the controlling define into the vl-includeskips. This should be done when the final `endif is encountered and determined to be ok.

Signature
(vl-includeskips-install-controller realfile controller iskips) → new-iskips
Arguments: realfile — Guard (stringp realfile).; controller — Guard (stringp controller).; iskips — Guard (vl-includeskips-p iskips).
Returns: new-iskips — Type (vl-includeskips-p new-iskips).

Definitions and Theorems

Function: vl-includeskips-install-controller

(defun vl-includeskips-install-controller
       (realfile controller iskips)
 (declare (xargs :guard (and (stringp realfile)
                             (stringp controller)
                             (vl-includeskips-p iskips))))
 (let ((__function__ 'vl-includeskips-install-controller))
  (declare (ignorable __function__))
  (b*
   ((realfile (string-fix realfile))
    (iskips (vl-includeskips-fix iskips))
    (entry (cdr (hons-get realfile iskips)))
    ((unless entry)
     (raise
      "Programming error: missing initial entry in includeskips ~
                for ~f0.  Expected entries to be created upon initial load, ~
                so this should never happen."
      realfile)
     iskips)
    (entry (change-vl-iskipinfo entry
                                :controller controller)))
   (hons-acons realfile entry iskips))))

Theorem: vl-includeskips-p-of-vl-includeskips-install-controller

(defthm vl-includeskips-p-of-vl-includeskips-install-controller
  (b* ((new-iskips (vl-includeskips-install-controller
                        realfile controller iskips)))
    (vl-includeskips-p new-iskips))
  :rule-classes :rewrite)