		Search-engine friendly clone of the ACL2 documentation.

Input-parser

Parse-input-file

Parse an input-file.

Signature
(parse-input-file input) → (mv tree next-token rest-input)
Arguments: input — Guard (abnf::tree-listp input).
Returns: tree — Type (abnf::tree-resultp tree).; next-token — Type (abnf::tree-optionp next-token).; rest-input — Type (abnf::tree-listp rest-input).

This is the top-level function that organizes a list of tokens into a CST. We get the first token (if any), and then we parse zero or more declarations, and return an input-file CST. If there is no error, there is no next token and no remaining input.

Definitions and Theorems

Function: parse-input-file

(defun parse-input-file (input)
  (declare (xargs :guard (abnf::tree-listp input)))
  (let ((__function__ 'parse-input-file))
    (declare (ignorable __function__))
    (b* (((mv token input) (parse-token input))
         ((pok trees)
          (parse-*-input-section token input))
         ((when (or token (consp input)))
          (mv (reserrf :impossible) token input))
         (tree (abnf::make-tree-nonleaf
                    :rulename? (abnf::rulename "input-file")
                    :branches (list trees))))
      (mv tree nil nil))))

Theorem: tree-resultp-of-parse-input-file.tree

(defthm tree-resultp-of-parse-input-file.tree
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-input-file input)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-optionp-of-parse-input-file.next-token

(defthm tree-optionp-of-parse-input-file.next-token
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-input-file input)))
    (abnf::tree-optionp next-token))
  :rule-classes :rewrite)

Theorem: tree-listp-of-parse-input-file.rest-input

(defthm tree-listp-of-parse-input-file.rest-input
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-input-file input)))
    (abnf::tree-listp rest-input))
  :rule-classes :rewrite)

Theorem: parse-input-file-of-tree-list-fix-input

(defthm parse-input-file-of-tree-list-fix-input
  (equal (parse-input-file (abnf::tree-list-fix input))
         (parse-input-file input)))

Theorem: parse-input-file-tree-list-equiv-congruence-on-input

(defthm parse-input-file-tree-list-equiv-congruence-on-input
  (implies (abnf::tree-list-equiv input input-equiv)
           (equal (parse-input-file input)
                  (parse-input-file input-equiv)))
  :rule-classes :congruence)