		Search-engine friendly clone of the ACL2 documentation.

Parser-abstractor-interface

Ast-from-fragment

Parse and abstract to AST.

Signature
(ast-from-fragment rule-name source-code) → ast-result
Arguments: rule-name — Guard (stringp rule-name).; source-code — Guard (stringp source-code).
Returns: ast-result — Type (or (file-resultp ast-result) (statement-resultp ast-result) (expression-resultp ast-result) (identifier-resultp ast-result) (literal-resultp ast-result)) .

Supported grammar rule names are file, statement, expression, and token.

If the given rule cannot be parsed or if there are tokens left over, or if the resulting CST cannot be abstracted to AST, then a reserr is returned.

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

Definitions and Theorems

Function: ast-from-fragment

(defun ast-from-fragment (rule-name source-code)
 (declare (xargs :guard (and (stringp rule-name)
                             (stringp source-code))))
 (let ((__function__ 'ast-from-fragment))
  (declare (ignorable __function__))
  (b* ((cst (parse-fragment-to-cst rule-name source-code))
       ((when (reserrp cst)) cst))
   (if (equal rule-name "file")
       (abs-file cst)
    (if (equal rule-name "statement")
        (abs-statement cst)
     (if (equal rule-name "expression")
         (abs-expression cst)
      (if
        (equal rule-name "token")
        (b* (((okf rulename?)
              (abnf::check-tree-nonleaf? cst))
             ((when (equal rulename? "identifier"))
              (abs-identifier cst))
             ((when (equal rulename? "atomic-literal"))
              (abs-atomic-literal cst)))
          (reserrf (cons :not-yet-supported-token-type rulename?)))
       (reserrf
        (cons
           :not-yet-supported-top-level-rule-name rule-name)))))))))

Theorem: return-type-of-ast-from-fragment

(defthm return-type-of-ast-from-fragment
  (b* ((ast-result (ast-from-fragment rule-name source-code)))
    (or (file-resultp ast-result)
        (statement-resultp ast-result)
        (expression-resultp ast-result)
        (identifier-resultp ast-result)
        (literal-resultp ast-result)))
  :rule-classes :rewrite)