		Search-engine friendly clone of the ACL2 documentation.

Output-files-implementation

Output-files-process-inputs

Process the inputs.

Signature
(output-files-process-inputs arg args progp wrld) → (mv erp code path indent-size paren-nested-conds)
Arguments: args — Guard (true-listp args).; progp — Guard (booleanp progp).; wrld — Guard (plist-worldp wrld).
Returns: code — Type (code-ensemblep code).; path — Type (stringp path).; indent-size — Type (posp indent-size).; paren-nested-conds — Type (booleanp paren-nested-conds).

If progp is t, arg is the required (i.e. non-keyword-option) input of the macro that provides the programmatic interface; if instead progp is nil, arg is nil. In all cases, args are all the remaining inputs of the (event or programmatic) macro.

If progp is nil, the code ensemble is taken from the :const input, which must be present. If instead progp is t, the code ensemble or file set is taken from the required input arg, and the :const input must be absent.

The code result of this function is the code ensemble. The other results are the homonymous inputs (some are sub-inputs of the :printer-options input).

If the :path string is not / but ends with /, we remove the ending /. This is for uniformity when concatenating this with the files specified in the :files input.

Definitions and Theorems

Function: output-files-process-inputs

(defun output-files-process-inputs (arg args progp wrld)
 (declare (xargs :guard (and (true-listp args)
                             (booleanp progp)
                             (plist-worldp wrld))))
 (declare (xargs :guard (implies (not progp) (not arg))))
 (let ((__function__ 'output-files-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-code-ensemble) "" 1 nil)
    ((mv erp extra options)
     (partition-rest-and-keyword-args
          args *output-files-allowed-options*))
    (inputs-desc (msg "a code ensemble and the options ~&0"
                      *output-files-allowed-options*))
    ((when erp)
     (reterr
      (msg
       "The inputs must be ~@0, ~
                      but instead they are ~x1."
       inputs-desc args)))
    ((when extra)
     (reterr
      (msg
       "The inputs must be ~@0, ~
                      but instead the extra inputs ~x1 were supplied."
       inputs-desc extra)))
    ((erp code)
     (output-files-process-const/arg arg options progp wrld))
    ((erp path)
     (output-files-process-path options))
    ((erp indent-size paren-nested-conds)
     (output-files-process-printer-options options)))
   (retok code
          path indent-size paren-nested-conds))))

Theorem: code-ensemblep-of-output-files-process-inputs.code

(defthm code-ensemblep-of-output-files-process-inputs.code
  (b* (((mv acl2::?erp ?code
            ?path ?indent-size ?paren-nested-conds)
        (output-files-process-inputs arg args progp wrld)))
    (code-ensemblep code))
  :rule-classes :rewrite)

Theorem: stringp-of-output-files-process-inputs.path

(defthm stringp-of-output-files-process-inputs.path
  (b* (((mv acl2::?erp ?code
            ?path ?indent-size ?paren-nested-conds)
        (output-files-process-inputs arg args progp wrld)))
    (stringp path))
  :rule-classes :rewrite)

Theorem: posp-of-output-files-process-inputs.indent-size

(defthm posp-of-output-files-process-inputs.indent-size
  (b* (((mv acl2::?erp ?code
            ?path ?indent-size ?paren-nested-conds)
        (output-files-process-inputs arg args progp wrld)))
    (posp indent-size))
  :rule-classes :rewrite)

Theorem: booleanp-of-output-files-process-inputs.paren-nested-conds

(defthm booleanp-of-output-files-process-inputs.paren-nested-conds
  (b* (((mv acl2::?erp ?code
            ?path ?indent-size ?paren-nested-conds)
        (output-files-process-inputs arg args progp wrld)))
    (booleanp paren-nested-conds))
  :rule-classes :rewrite)

Theorem: code-ensemble-unambp-of-output-files-process-inputs

(defthm code-ensemble-unambp-of-output-files-process-inputs
  (b* (((mv acl2::?erp ?code
            ?path ?indent-size ?paren-nested-conds)
        (output-files-process-inputs arg args progp wrld)))
    (implies (not erp)
             (code-ensemble-unambp code))))

Theorem: code-aidentp-of-output-files-process-inputs

(defthm code-aidentp-of-output-files-process-inputs
  (b* (((mv acl2::?erp ?code
            ?path ?indent-size ?paren-nested-conds)
        (output-files-process-inputs arg args progp wrld)))
    (implies (not erp)
             (code-ensemble-aidentp code))))