		Search-engine friendly clone of the ACL2 documentation.

Semantics

Parse!

Parse an unambiguous string.

Signature
(parse! string rulename rules) → tree
Arguments: string — Guard (stringp string).; rulename — Guard (rulenamep rulename).; rules — Guard (rulelistp rules).
Returns: tree — Type (treep tree).

The result is the unique parse tree.

Definitions and Theorems

Function: parse!

(defun parse! (string rulename rules)
 (declare (xargs :guard (and (stringp string)
                             (rulenamep rulename)
                             (rulelistp rules))))
 (declare
      (xargs :guard (string-unambiguousp string rulename rules)))
 (mbe
  :logic (tree-fix (string-parsablep-witness string rulename rules))
  :exec (string-parsablep-witness string rulename rules)))

Theorem: treep-of-parse!

(defthm treep-of-parse!
  (b* ((tree (parse! string rulename rules)))
    (treep tree))
  :rule-classes :rewrite)

Theorem: parse-is-parse!-when-string-unambiguousp

(defthm parse-is-parse!-when-string-unambiguousp
  (implies (string-unambiguousp string rulename rules)
           (equal (parse string rulename rules)
                  (insert (parse! string rulename rules)
                          nil))))