		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-file

Pretty-print a file.

Signature
(pprint-file file include options) → lines
Arguments: file — Guard (filep file).; include — Guard (maybe-stringp include).; options — Guard (pprint-options-p options).
Returns: lines — Type (msg-listp lines).

We start with a line comment saying that the file is generated by ATC.

The include parameter of this pretty-printing ACL2 function says whether we should generate (when non-nil, an #include directive with double quotes and the file name specified by the string. Note that our abstract syntax does not yet have a representation of #include directives; instead, since for now we only generate very simple such directives, we generate them in this ad hoc fashion for now.

Definitions and Theorems

Function: pprint-file

(defun pprint-file (file include options)
  (declare (xargs :guard (and (filep file)
                              (maybe-stringp include)
                              (pprint-options-p options))))
  (let ((__function__ 'pprint-file))
    (declare (ignorable __function__))
    (b* (((file file) file))
      (append (list "// This file is generated by ATC.~%")
              (and include
                   (list (str::cat "~%#include \"" include "\"~%")))
              (pprint-ext-declon-list file.declons options)))))

Theorem: msg-listp-of-pprint-file

(defthm msg-listp-of-pprint-file
  (b* ((lines (pprint-file file include options)))
    (msg-listp lines))
  :rule-classes :rewrite)