		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-repeat

A repeat parse tree is abstracted to its correspoding repetition range.

Signature
(abstract-repeat tree) → range
Arguments: tree — Guard (treep tree).
Returns: range — Type (repeat-rangep range).

The two alternatives of the repeat rule both consist of singleton concatenations, so a repeat parse tree must have a list of one list of trees. For the first alternative, the list of trees must consist of one or more DIGIT parse trees; for the second alternative, the list of trees must consist of a single (*DIGIT "*" *DIGIT) parse tree. The latter kind of parse tree is distinguished from the former kind by having a nil rule for the (*DIGIT "*" *DIGIT) group.

Definitions and Theorems

Function: abstract-repeat

(defun abstract-repeat (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail)
                (repeat-range 0 (nati-finite 0))))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (consp treess)) (fail))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (1st-subtree (car trees))
       ((unless (tree-case 1st-subtree :nonleaf))
        (fail)))
    (if (tree-nonleaf->rulename? 1st-subtree)
        (b* ((num (abstract-*digit trees)))
          (make-repeat-range :min num
                             :max (nati-finite num)))
      (b* (((mv min max)
            (abstract-*digit-star-*digit 1st-subtree)))
        (make-repeat-range :min min
                           :max max)))))

Theorem: repeat-rangep-of-abstract-repeat

(defthm repeat-rangep-of-abstract-repeat
  (b* ((range (abstract-repeat tree)))
    (repeat-rangep range))
  :rule-classes :rewrite)