		Search-engine friendly clone of the ACL2 documentation.

Fileset

Make-fileset

Basic constructor macro for fileset structures.

Syntax

(make-fileset [:path-wo-ext <path-wo-ext>] 
              [:dot-h <dot-h>] 
              [:dot-c <dot-c>])

This is the usual way to construct fileset structures. It simply conses together a structure with the specified fields.

This macro generates a new fileset structure from scratch. See also change-fileset, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-fileset

(defmacro make-fileset (&rest args)
  (std::make-aggregate 'fileset
                       args '((:path-wo-ext) (:dot-h) (:dot-c))
                       'make-fileset
                       nil))

Function: fileset

(defun fileset (path-wo-ext dot-h dot-c)
  (declare (xargs :guard (and (stringp path-wo-ext)
                              (file-optionp dot-h)
                              (filep dot-c))))
  (declare (xargs :guard t))
  (let ((__function__ 'fileset))
    (declare (ignorable __function__))
    (b* ((path-wo-ext (mbe :logic (str-fix path-wo-ext)
                           :exec path-wo-ext))
         (dot-h (mbe :logic (file-option-fix dot-h)
                     :exec dot-h))
         (dot-c (mbe :logic (file-fix dot-c)
                     :exec dot-c)))
      (cons :fileset (list (cons 'path-wo-ext path-wo-ext)
                           (cons 'dot-h dot-h)
                           (cons 'dot-c dot-c))))))