		Search-engine friendly clone of the ACL2 documentation.

Stv2c

Stv2c-outs-structdef

Structure definition for the STV outputs.

Signature
(stv2c-outs-structdef stv acc) → new-acc
Arguments: stv — Guard (processed-stv-p stv).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: stv2c-outs-structdef

(defun stv2c-outs-structdef (stv acc)
       (declare (xargs :guard (processed-stv-p stv)))
       (let ((__function__ 'stv2c-outs-structdef))
            (declare (ignorable __function__))
            (b* ((outs (stv->outs stv))
                 (c-structname (stv2c-outs-structname stv))
                 (c-fieldnames (stv2c-c-symbol-names outs))
                 ((unless (uniquep c-fieldnames))
                  (raise "Name clash for STV output C names: ~x0."
                         (duplicated-members c-fieldnames)))
                 (acc (str::revappend-chars "class " acc))
                 (acc (str::revappend-chars c-structname acc))
                 (acc (cons #\Newline acc))
                 (acc (str::revappend-chars "{" acc))
                 (acc (cons #\Newline acc))
                 (acc (str::revappend-chars "  public:" acc))
                 (acc (cons #\Newline acc))
                 (acc (stv2c-outs-structfields outs stv acc))
                 (acc (str::revappend-chars "};" acc))
                 (acc (cons #\Newline acc)))
                acc)))

Theorem: character-listp-of-stv2c-outs-structdef

(defthm character-listp-of-stv2c-outs-structdef
        (implies (character-listp acc)
                 (b* ((new-acc (stv2c-outs-structdef stv acc)))
                     (character-listp new-acc)))
        :rule-classes :rewrite)

Subtopics

Stv2c-outs-structfields
Stv2c-outs-structname