		Search-engine friendly clone of the ACL2 documentation.

Vl-lex

Vl-lex-timescale

Try to read a `timescale directive and turn it into a whitespace token.

Signature
(vl-lex-timescale echars) → (mv token/nil remainder)
Arguments: echars — Guard (vl-echarlist-p echars).

This is a special, unusual hack. We try to read a `timescale directive, i.e.,:

timescale_compiler_directive ::= `timescale time_unit / time_precision

Where the time_unit is 1, 10, or 100, and the time_precision is one of: s, ms, us, ns, ps, or fs.

On success we just turn this into a whitespace token which will get dropped before parsing.

We used to remove `timescale directives as part of the preprocessor, but we eventually found that it was better to do it as part of lexing because otherwise it is hard to support things like `timescale `foo.

Definitions and Theorems

Function: vl-lex-timescale

(defun vl-lex-timescale (echars)
 (declare (xargs :guard (vl-echarlist-p echars)))
 (declare (xargs :guard (and (consp echars)
                             (equal (vl-echar->char (car echars))
                                    #\`))))
 (let ((__function__ 'vl-lex-timescale))
  (declare (ignorable __function__))
  (b* (((mv grv remainder)
        (mv (car echars) (cdr echars)))
       ((mv ts remainder)
        (vl-read-literal "timescale" remainder))
       ((mv ws1 remainder)
        (vl-read-while-whitespace remainder))
       ((mv tu-val remainder)
        (vl-read-some-literal (list "100" "10" "1")
                              remainder))
       ((mv ws2 remainder)
        (vl-read-while-whitespace remainder))
       ((mv tu-type remainder)
        (vl-read-some-literal (list "fs" "ps" "ns" "us" "ms" "s")
                              remainder))
       ((mv ws3 remainder)
        (vl-read-while-whitespace remainder))
       ((mv div remainder)
        (vl-read-literal "/" remainder))
       ((mv ws4 remainder)
        (vl-read-while-whitespace remainder))
       ((mv tp-val remainder)
        (vl-read-some-literal (list "100" "10" "1")
                              remainder))
       ((mv ws5 remainder)
        (vl-read-while-whitespace remainder))
       ((mv tp-type remainder)
        (vl-read-some-literal (list "fs" "ps" "ns" "us" "ms" "s")
                              remainder)))
   (if
    (and ts tu-val tu-type div tp-val tp-type)
    (mv
     (make-vl-plaintoken
       :type :vl-ws
       :etext (cons grv
                    (append ts ws1 tu-val ws2
                            tu-type ws3 div ws4 tp-val ws5 tp-type))
       :breakp nil)
     remainder)
    (mv nil echars)))))

Theorem: vl-token-p-of-vl-lex-timescale

(defthm vl-token-p-of-vl-lex-timescale
  (implies (and (force (vl-echarlist-p echars)) t)
           (equal (vl-token-p (mv-nth 0 (vl-lex-timescale echars)))
                  (if (mv-nth 0 (vl-lex-timescale echars))
                      t
                    nil))))

Theorem: true-listp-of-vl-lex-timescale

(defthm true-listp-of-vl-lex-timescale
 (equal (true-listp (mv-nth 1 (vl-lex-timescale echars)))
        (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
      :corollary
      (implies (true-listp echars)
               (true-listp (mv-nth 1 (vl-lex-timescale echars)))))))

Theorem: vl-echarlist-p-of-vl-lex-timescale

(defthm vl-echarlist-p-of-vl-lex-timescale
  (implies
       (force (vl-echarlist-p echars))
       (equal (vl-echarlist-p (mv-nth 1 (vl-lex-timescale echars)))
              t)))

Theorem: append-of-vl-lex-timescale

(defthm append-of-vl-lex-timescale
 (implies
  (and (mv-nth 0 (vl-lex-timescale echars))
       (force (vl-echarlist-p echars))
       t)
  (equal
      (append (vl-token->etext (mv-nth 0 (vl-lex-timescale echars)))
              (mv-nth 1 (vl-lex-timescale echars)))
      echars)))

Theorem: no-change-loser-of-vl-lex-timescale

(defthm no-change-loser-of-vl-lex-timescale
  (implies (not (mv-nth 0 (vl-lex-timescale echars)))
           (equal (mv-nth 1 (vl-lex-timescale echars))
                  echars)))

Theorem: acl2-count-of-vl-lex-timescale-weak

(defthm acl2-count-of-vl-lex-timescale-weak
  (<= (acl2-count (mv-nth 1 (vl-lex-timescale echars)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-lex-timescale-strong

(defthm acl2-count-of-vl-lex-timescale-strong
  (implies (and (mv-nth 0 (vl-lex-timescale echars))
                t)
           (< (acl2-count (mv-nth 1 (vl-lex-timescale echars)))
              (acl2-count echars)))
  :rule-classes ((:rewrite) (:linear)))

Subtopics

Vl-lex-timescale-token/remainder-thms: Token and remainder theorems for vl-lex-timescale, automatically generated by def-token/remainder-thms.