		Search-engine friendly clone of the ACL2 documentation.

Comp-db-entry

Make-comp-db-entry

Basic constructor macro for comp-db-entry structures.

Syntax

(make-comp-db-entry [:exec <exec>] 
                    [:directory <directory>] 
                    [:output <output>] 
                    [:arguments <arguments>])

This is the usual way to construct comp-db-entry structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-comp-db-entry

(defmacro make-comp-db-entry (&rest args)
  (std::make-aggregate 'comp-db-entry
                       args
                       '((:exec)
                         (:directory)
                         (:output)
                         (:arguments))
                       'make-comp-db-entry
                       nil))

Function: comp-db-entry

(defun comp-db-entry (exec directory output arguments)
  (declare (xargs :guard (and (stringp exec)
                              (stringp directory)
                              (string-optionp output)
                              (comp-db-arg-listp arguments))))
  (declare (xargs :guard t))
  (b* ((exec (mbe :logic (acl2::str-fix exec)
                  :exec exec))
       (directory (mbe :logic (acl2::str-fix directory)
                       :exec directory))
       (output (mbe :logic (acl2::string-option-fix output)
                    :exec output))
       (arguments (mbe :logic (comp-db-arg-list-fix arguments)
                       :exec arguments)))
    (list (cons 'exec exec)
          (cons 'directory directory)
          (cons 'output output)
          (cons 'arguments arguments))))