		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Parse-def

Parse string into a PFCS definition in AST form.

Signature
(parse-def pfcs-string) → sys
Arguments: pfcs-string — Guard (stringp pfcs-string).
Returns: sys — Type (definition-resultp sys).

Lexes, tokenizes, and parses a PFCS system containing a single definition and no extra constraints, as a string of ACL2 characters whose char-codes are UTF-8 bytes. Returns a PFCS definition AST (abstract syntax tree).

If any step fails, returns a reserr. The parse consumes the entire string or a reserr is returned. If the parsed PFCS system contains other than one definition and zero constraints, returns a reserr.

Since ACL2 strings are sequences of characters with codes from 0 to 255, pfcs-string, when converted to codes, is required to be valid UTF-8.

Definitions and Theorems

Function: parse-def

(defun parse-def (pfcs-string)
  (declare (xargs :guard (stringp pfcs-string)))
  (let ((__function__ 'parse-def))
    (declare (ignorable __function__))
    (b* ((cst (parse-from-string-to-cst pfcs-string))
         ((when (reserrp cst)) cst)
         (ast (abs-system cst))
         ((when (reserrp ast))
          (reserrf (cons :problem-abstracting cst)))
         (defs (system->definitions ast))
         (constraints (system->constraints ast))
         ((unless (and (consp defs) (null constraints)))
          (reserrf (cons :wrong-number-of-system-components cst))))
      (first defs))))

Theorem: definition-resultp-of-parse-def

(defthm definition-resultp-of-parse-def
  (b* ((sys (parse-def pfcs-string)))
    (definition-resultp sys))
  :rule-classes :rewrite)