		Search-engine friendly clone of the ACL2 documentation.

Vl-location

Vl-string-between-locs

Given a string, extract all text that occurs between two vl-location-ps.

Signature
(vl-string-between-locs x loc1 loc2) → text
Arguments: x — String to extract text from. Typically this should be extracted from a vl-filemap-p. We assume it has the contents of the whole file.
Guard (stringp x).; loc1 — Some location in the file; we ignore the filename but assume it refers to a file whose contents are x.
Guard (vl-location-p loc1).; loc2 — Some other location, treated similarly, may come before or after loc1.
Guard (vl-location-p loc2).
Returns: text — Type (maybe-stringp text).

If both locations refer to valid places in x, we return the substring of x that falls between these locations, inclusively. Otherwise we return nil.

Definitions and Theorems

Function: vl-string-between-locs

(defun vl-string-between-locs (x loc1 loc2)
 (declare (xargs :guard (and (stringp x)
                             (vl-location-p loc1)
                             (vl-location-p loc2))))
 (let ((__function__ 'vl-string-between-locs))
  (declare (ignorable __function__))
  (b*
   ((x (string-fix x))
    ((mv loc1 loc2)
     (if (vl-location-before-nofilename loc1 loc2)
         (mv loc1 loc2)
       (mv loc2 loc1)))
    (xl (length x))
    (tline1 (vl-location->line loc1))
    (tcol1 (vl-location->col loc1))
    (pos1 (vl-string-findloc-aux x 0 xl 1 0 tline1 tcol1))
    ((unless pos1) nil)
    (tline2 (vl-location->line loc2))
    (tcol2 (vl-location->col loc2))
    (pos2
        (vl-string-findloc-aux x pos1 xl tline1 tcol1 tline2 tcol2))
    ((unless pos2) nil))
   (subseq x pos1 pos2))))

Theorem: maybe-stringp-of-vl-string-between-locs

(defthm maybe-stringp-of-vl-string-between-locs
  (b* ((text (vl-string-between-locs x loc1 loc2)))
    (maybe-stringp text))
  :rule-classes :type-prescription)

Subtopics

Vl-location-before-nofilename