		Search-engine friendly clone of the ACL2 documentation.

Vl-lex

Vl-lex-main-exec

Tail recursive implementation.

Signature
(vl-lex-main-exec echars breakp nrev st warnings) → (mv successp nrev warnings)
Arguments: echars — Guard (vl-echarlist-p echars).; breakp — Guard (booleanp breakp).; nrev — Guard (vl-tokenlist-p (nrev-copy nrev)).; st — Guard (vl-lexstate-p st).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-lex-main-exec

(defun vl-lex-main-exec (echars breakp nrev st warnings)
 (declare (xargs :stobjs (nrev)))
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (booleanp breakp)
                             (vl-tokenlist-p (nrev-copy nrev))
                             (vl-lexstate-p st)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-lex-main-exec))
  (declare (ignorable __function__))
  (b*
   ((nrev (nrev-fix nrev))
    ((when (atom echars)) (mv t nrev (ok)))
    ((mv tok remainder warnings)
     (vl-lex-token echars breakp st warnings))
    ((when tok)
     (let*
      ((nrev (nrev-push tok nrev))
       (breakp
          (and (eq (vl-token->type tok) :vl-ws)
               (vl-echarlist-has-newline-p (vl-token->etext tok)))))
      (vl-lex-main-exec remainder breakp nrev st warnings)))
    (- (cw "About to cause an error.~%"))
    (prev-chars (nrev-copy nrev))
    (prev-chop (nthcdr (nfix (- (length prev-chars) 30))
                       prev-chars))
    (prev-str
         (vl-echarlist->string (vl-tokenlist->etext prev-chop))))
   (mv
    (cw
     "Lexer error (~s0): unable to identify a valid token.~%~
             [[ Previous  ]]: ~s1~%~
             [[ Remaining ]]: ~s2~%"
     (vl-location-string (vl-echar->loc (car echars)))
     prev-str
     (vl-echarlist->string (first-n (min 30 (len echars)) echars)))
    nrev warnings))))

Theorem: vl-warninglist-p-of-vl-lex-main-exec.warnings

(defthm vl-warninglist-p-of-vl-lex-main-exec.warnings
  (b* (((mv ?successp acl2::?nrev ?warnings)
        (vl-lex-main-exec echars breakp nrev st warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)