		Search-engine friendly clone of the ACL2 documentation.

Parser

Cst2ast-decimal-number

Given a :nonleaf ABNF tree with rulename "decimal-number", return the appropriate literal AST node.

Signature
(cst2ast-decimal-number tree) → ast-node?
Arguments: tree — Guard (abnf::treep tree).
Returns: ast-node? — Type (literal-optionp ast-node?).

Definitions and Theorems

Function: cst2ast-decimal-number

(defun cst2ast-decimal-number (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'cst2ast-decimal-number))
  (declare (ignorable __function__))
  (b*
   ((fringe (abnf::tree->string tree))
    ((unless (unsigned-byte-listp 8 fringe))
     (prog2$
      (er
        hard? 'top-level
        "unexpected type of leafterm nats when parsing idenntifier")
      nil))
    (decimal-number-string (nats=>string fringe))
    (maybe-nat (str::strval decimal-number-string)))
   (if (natp maybe-nat)
       (make-literal-dec-number :get maybe-nat)
     nil))))

Theorem: literal-optionp-of-cst2ast-decimal-number

(defthm literal-optionp-of-cst2ast-decimal-number
  (b* ((ast-node? (cst2ast-decimal-number tree)))
    (literal-optionp ast-node?))
  :rule-classes :rewrite)