		Search-engine friendly clone of the ACL2 documentation.

Semantics

Parse

Parse a string.

Signature
(parse string rulename rules) → result
Arguments: string — Guard (stringp string).; rulename — Guard (rulenamep rulename).; rules — Guard (rulelistp rules).
Returns: result — Type (or (tree-setp result) (equal result :infinite)).

If the string has a finite number of parse trees, return the finite set of its parse trees. Otherwise, return :infinite to indicate that the string has an infinite number of parse trees.

Definitions and Theorems

Function: parse

(defun parse (string rulename rules)
 (declare (xargs :guard (and (stringp string)
                             (rulenamep rulename)
                             (rulelistp rules))))
 (if (string-has-finite-parse-trees-p string rulename rules)
     (string-has-finite-parse-trees-p-witness string rulename rules)
   :infinite))

Theorem: return-type-of-parse

(defthm return-type-of-parse
  (b* ((result (parse string rulename rules)))
    (or (tree-setp result)
        (equal result :infinite)))
  :rule-classes :rewrite)

Theorem: distinguish-infinite-from-trees

(defthm distinguish-infinite-from-trees
  (not (tree-setp :infinite)))

Theorem: parse-when-not-string-parsablep

(defthm parse-when-not-string-parsablep
  (implies (not (string-parsablep string rulename rules))
           (equal (parse string rulename rules)
                  nil)))

Theorem: parse-when-string-unambiguousp

(defthm parse-when-string-unambiguousp
 (implies
     (string-unambiguousp string rulename rules)
     (equal (parse string rulename rules)
            (insert (string-parsablep-witness string rulename rules)
                    nil))))

Theorem: not-string-parsablep-when-parse-nil

(defthm not-string-parsablep-when-parse-nil
  (implies (equal (parse string rulename rules)
                  nil)
           (not (string-parsablep string rulename rules))))

Theorem: string-unambiguousp-when-parse-one

(defthm string-unambiguousp-when-parse-one
 (implies
     (equal (parse string rulename rules)
            (insert (string-parsablep-witness string rulename rules)
                    nil))
     (string-unambiguousp string rulename rules)))