		Search-engine friendly clone of the ACL2 documentation.

Stv2c

Stv2c-main

Signature
(stv2c-main stv &key (state 'state)) → state
Arguments: stv — Guard (processed-stv-p stv).

Definitions and Theorems

Function: stv2c-main-fn

(defun
 stv2c-main-fn (stv state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (processed-stv-p stv)))
 (let
  ((__function__ 'stv2c-main))
  (declare (ignorable __function__))
  (b*
   (((processed-stv stv) stv)
    (c-name (stv2c-c-symbol-name stv.name))
    (header-filename (str::cat c-name ".h"))
    (impl-filename (str::cat c-name ".cc"))
    (header-txt (str::rchars-to-string (stv2c-header stv nil)))
    (impl-txt
     (b*
      ((acc nil)
       (acc
        (str::revappend-chars
         "// Warning: automatically generated file!
// Do not hand edit!

#include \""
         acc))
       (acc (str::revappend-chars header-filename acc))
       (acc (cons #\" acc))
       (acc (cons #\Newline acc))
       (acc (cons #\Newline acc))
       (acc (stv2c-make-run-fn stv acc)))
      (str::rchars-to-string acc)))
    (state (stv2c-write header-filename header-txt state))
    (state (stv2c-write impl-filename impl-txt state)))
   state)))