		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-repetition

A repetition parse tree is abstracted to its corresponding repetition.

Signature
(abstract-repetition tree) → repetition
Arguments: tree — Guard (treep tree).
Returns: repetition — Type (repetitionp repetition).

Function: abstract-repetition

(defun abstract-repetition (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail)
                (repetition (repeat-range 0 (nati-finite 0))
                            (element-group nil))))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))))
        (fail))
       (trees-repeat (car treess))
       (trees-element (cadr treess))
       ((unless (consp trees-repeat)) (fail))
       (tree-repeat (car trees-repeat))
       (range (abstract-?repeat tree-repeat))
       ((unless (consp trees-element)) (fail))
       (tree-element (car trees-element))
       (element (abstract-element tree-element)))
    (make-repetition :range range
                     :element element)))