		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-alternation

An alternation parse tree is abstracted to its corresponding alternation.

Signature
(abstract-alternation tree) → alternation
Arguments: tree — Guard (treep tree).
Returns: alternation — Type (alternationp alternation).

Function: abstract-alternation

(defun abstract-alternation (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail)) (abstract-fail))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))))
        (fail))
       (trees-concatenation (car treess))
       (trees-concatenations (cadr treess))
       ((unless (consp trees-concatenation))
        (fail))
       (tree-concatenation (car trees-concatenation))
       (concatenation (abstract-concatenation tree-concatenation))
       (concatenations (abstract-alt-rest trees-concatenations)))
    (cons concatenation concatenations)))