		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-system

Parse a PFCS system.

Signature
(parse-system 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 PFCS system CST. We get the first token (if any), then we parse zero or more definitions followed by zero or more constraints that may use those definitions, and return a CST. If there is no error, there should be no next token and no remaining input, and that should be checked by the caller.

Since definition is the only construct using the operator := and is the only construct using the the separator } with which it terminates the definition, it is safe and unambiguous to first try to parse as many definitions as possible and then to parse the constraints.

Definitions and Theorems

Function: parse-system

(defun parse-system (input)
 (declare (xargs :guard (abnf::tree-listp input)))
 (let ((__function__ 'parse-system))
  (declare (ignorable __function__))
  (b* (((mv token input) (parse-token input))
       ((pok trees1)
        (parse-*-definition token input))
       ((pok trees2)
        (parse-*-constraint token input)))
   (mv (abnf::make-tree-nonleaf :rulename? (abnf::rulename "system")
                                :branches (list trees1 trees2))
       token input))))

Theorem: tree-resultp-of-parse-system.tree

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

Theorem: tree-optionp-of-parse-system.next-token

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

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

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

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

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

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

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