		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-fileset

Parse a file set.

Signature
(parse-fileset fileset gcc) → (mv erp tunits)
Arguments: fileset — Guard (filesetp fileset).; gcc — Guard (booleanp gcc).
Returns: tunits — Type (transunit-ensemblep tunits).

We also pass a flag saying whether GCC extensions should be accepted.

We go through each file of the file set and parse it, obtaining a translation unit for each, which we return in an ensemble of translation units that corresponds to the file set. The file paths are the same for the file set and for the translation unit ensembles (they are the keys of the maps).

Definitions and Theorems

Function: parse-fileset-loop

(defun parse-fileset-loop (filemap gcc)
  (declare (xargs :guard (and (filepath-filedata-mapp filemap)
                              (booleanp gcc))))
  (let ((__function__ 'parse-fileset-loop))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((when (omap::emptyp filemap))
          (retok nil))
         ((mv filepath filedata)
          (omap::head filemap))
         ((erp tunit)
          (parse-file filepath (filedata->unwrap filedata)
                      gcc))
         ((erp tunitmap)
          (parse-fileset-loop (omap::tail filemap)
                              gcc)))
      (retok (omap::update (filepath-fix filepath)
                           tunit tunitmap)))))

Theorem: filepath-transunit-mapp-of-parse-fileset-loop.tunitmap

(defthm filepath-transunit-mapp-of-parse-fileset-loop.tunitmap
  (b* (((mv acl2::?erp ?tunitmap)
        (parse-fileset-loop filemap gcc)))
    (filepath-transunit-mapp tunitmap))
  :rule-classes :rewrite)

Theorem: keys-of-parse-fileset-loop

(defthm keys-of-parse-fileset-loop
  (implies (filepath-filedata-mapp filemap)
           (b* (((mv acl2::?erp ?tunitmap)
                 (parse-fileset-loop filemap gcc)))
             (implies (not erp)
                      (equal (omap::keys tunitmap)
                             (omap::keys filemap))))))

Function: parse-fileset

(defun parse-fileset (fileset gcc)
  (declare (xargs :guard (and (filesetp fileset)
                              (booleanp gcc))))
  (let ((__function__ 'parse-fileset))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-transunit-ensemble))
         (filemap (fileset->unwrap fileset))
         ((erp tunitmap)
          (parse-fileset-loop filemap gcc)))
      (retok (transunit-ensemble tunitmap)))))

Theorem: transunit-ensemblep-of-parse-fileset.tunits

(defthm transunit-ensemblep-of-parse-fileset.tunits
  (b* (((mv acl2::?erp ?tunits)
        (parse-fileset fileset gcc)))
    (transunit-ensemblep tunits))
  :rule-classes :rewrite)

Theorem: filepaths-of-parse-fileset

(defthm filepaths-of-parse-fileset
  (b* (((mv acl2::?erp ?tunits)
        (parse-fileset fileset gcc)))
    (implies (not erp)
             (equal (omap::keys (transunit-ensemble->unwrap tunits))
                    (omap::keys (fileset->unwrap fileset))))))