		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-grouped-terminals

A ( term1 / ... / termN ) parse tree, where term1, ..., termN are terminal numeric or character value notations, is generally abstracted to its list of natural numbers.

Signature
(abstract-grouped-terminals tree) → nats
Arguments: tree — Guard (treep tree).
Returns: nats — Type (nat-listp nats).

The parse tree must have a root labeled by no rule name, with a single leaf subtree labeled by a list of natural numbers. That list of natural numbers is returned.

Definitions and Theorems

Function: abstract-grouped-terminals

(defun abstract-grouped-terminals (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail)) (abstract-fail))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (consp treess)) (fail))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (subtree (car trees)))
    (abstract-terminals subtree)))

Theorem: nat-listp-of-abstract-grouped-terminals

(defthm nat-listp-of-abstract-grouped-terminals
  (b* ((nats (abstract-grouped-terminals tree)))
    (nat-listp nats))
  :rule-classes :rewrite)