		Search-engine friendly clone of the ACL2 documentation.

Vl-gather

Vl-module-original-source

Signature
(vl-module-original-source mod filemap) → original-source
Arguments: mod — Guard (vl-module-p mod).; filemap — Guard (vl-filemap-p filemap).
Returns: original-source — Type (stringp original-source).

Definitions and Theorems

Function: vl-module-original-source

(defun
 vl-module-original-source (mod filemap)
 (declare (xargs :guard (and (vl-module-p mod)
                             (vl-filemap-p filemap))))
 (let
  ((__function__ 'vl-module-original-source))
  (declare (ignorable __function__))
  (b*
   (((vl-module mod) mod)
    (minloc mod.minloc)
    (maxloc mod.maxloc)
    ((vl-location minloc) minloc)
    ((vl-location maxloc) maxloc)
    ((unless (equal minloc.filename maxloc.filename))
     (raise
      "Expected modules to begin/end in the same file, but ~s0 ~
                starts at ~s1 and ends at ~s2."
      mod.name (vl-location-string minloc)
      (vl-location-string maxloc))
     "")
    (file (cdr (hons-assoc-equal minloc.filename filemap)))
    ((unless file)
     (raise "File not found in the file map: ~s0"
            minloc.filename)
     "")
    (maxloc
      (change-vl-location maxloc
                          :col (+ maxloc.col (length "endmodule"))))
    (lines (vl-string-between-locs file minloc maxloc))
    ((unless lines)
     (raise "Error extracting module contents for ~s0"
            mod.name)
     ""))
   (cat "// " mod.name " from "
        minloc.filename ":" (natstr minloc.line)
        *nls* lines))))

Theorem: stringp-of-vl-module-original-source

(defthm
     stringp-of-vl-module-original-source
     (b* ((original-source (vl-module-original-source mod filemap)))
         (stringp original-source))
     :rule-classes :type-prescription)