		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-process-else

Handler for else directives.

Signature
(vl-process-else loc ppst) → (mv successp ppst)
Arguments: loc — Guard (vl-location-p loc).
Returns: successp — Type (booleanp successp).

Definitions and Theorems

Function: vl-process-else

(defun vl-process-else (loc ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (vl-location-p loc)))
 (let ((__function__ 'vl-process-else))
  (declare (ignorable __function__))
  (b*
   ((istack (vl-ppst->istack))
    ((when (atom istack))
     (let
        ((ppst (vl-ppst-fatal
                    :msg "~a0: found `else, but no `ifdef is open."
                    :args (list loc))))
       (mv nil ppst)))
    ((vl-iframe iframe) (car istack))
    ((when iframe.already-saw-elsep)
     (let
      ((ppst
          (vl-ppst-fatal
               :msg "~a0: found `else, but we already saw an `else."
               :args (list loc))))
      (mv nil ppst)))
    (ppst
     (vl-maybe-ppst-warn
      :when iframe.mi-controller
      :type :vl-warn-include-guard
      :msg
      "~a0: suppressing multiple-include optimization due to `else."
      :args (list loc)))
    (new-activep (and iframe.initially-activep
                      (not iframe.some-thing-satisfiedp)))
    (new-iframe
         (make-vl-iframe :initially-activep iframe.initially-activep
                         :some-thing-satisfiedp t
                         :already-saw-elsep t
                         :mi-controller nil
                         :mi-filename nil))
    (new-istack (cons new-iframe (cdr istack)))
    (ppst (vl-ppst-update-activep new-activep))
    (ppst (vl-ppst-update-istack new-istack)))
   (mv t ppst))))

Theorem: booleanp-of-vl-process-else.successp

(defthm booleanp-of-vl-process-else.successp
  (b* (((mv ?successp ?ppst)
        (vl-process-else loc ppst)))
    (booleanp successp))
  :rule-classes :type-prescription)