		Search-engine friendly clone of the ACL2 documentation.

Stv2c

Stv2c-header

Generate the header file for an STV.

Signature
(stv2c-header 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-header

(defun stv2c-header (stv acc)
 (declare (xargs :guard (processed-stv-p stv)))
 (let ((__function__ 'stv2c-header))
  (declare (ignorable __function__))
  (b*
   ((in-struct (stv2c-ins-structname stv))
    (out-struct (stv2c-outs-structname stv))
    (run-fn (stv2c-run-fnname stv))
    (acc
     (str::revappend-chars
      "#pragma once

// Warning: Automatically generated file!
// Do not hand edit!

#include \"fourval.h\"

"
      acc))
    (acc (stv2c-ins-structdef stv acc))
    (acc (cons #\Newline acc))
    (acc (stv2c-outs-structdef stv acc))
    (acc (cons #\Newline acc))
    (tmp (str::cat "void " run-fn))
    (acc (str::revappend-chars tmp acc))
    (acc
        (str::revappend-chars (str::cat "(const " in-struct "& in,")
                              acc))
    (acc (cons #\Newline acc))
    (acc (make-list-ac (+ 1 (length tmp))
                       #\Space acc))
    (acc (str::revappend-chars (str::cat out-struct "& out);")
                               acc))
    (acc (cons #\Newline acc)))
   acc)))

Theorem: character-listp-of-stv2c-header

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

Subtopics

Stv2c-run-fnname