		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-analyze-ctxexprs

Perform skip-detection for a list of expressions.

Signature: (sd-analyze-ctxexprs ctxexprs global-pats) returns a list of sd-problem-ps.

ctxexprs is an vl-exprctxalist-p that associates expressions with their contexts. Generally we expect that this alist includes every expression in a module.
global-pats is the sd-patalist-p that was constructed for all names in the module, which is needed by sd-patalist-compare.

We just call sd-patalist-compare for every expression in ctxexprs and combine the results.

Definitions and Theorems

Function: sd-analyze-ctxexprs

(defun sd-analyze-ctxexprs (ctxexprs global-pats)
 (declare (xargs :guard (and (vl-exprctxalist-p ctxexprs)
                             (sd-patalist-p global-pats))))
 (if (atom ctxexprs)
     nil
  (b* ((expr (caar ctxexprs))
       (ctx (vl-context1-fix (cdar ctxexprs)))
       (expr-names (vl-expr-names expr))
       (expr-keys (sd-keygen-list expr-names nil))
       (expr-pats (sd-patalist expr-keys))
       (dom (strip-cars expr-pats))
       (report1 (sd-patalist-compare dom expr-pats global-pats ctx))
       (- (flush-hons-get-hash-table-link expr-pats)))
    (append report1
            (sd-analyze-ctxexprs (cdr ctxexprs)
                                 global-pats)))))

Theorem: true-listp-of-sd-analyze-ctxexprs

(defthm true-listp-of-sd-analyze-ctxexprs
  (true-listp (sd-analyze-ctxexprs ctxexprs global-pats))
  :rule-classes :type-prescription)

Theorem: sd-problemlist-p-of-sd-analyze-ctxexprs

(defthm sd-problemlist-p-of-sd-analyze-ctxexprs
 (implies
     (and (force (vl-exprctxalist-p ctxexprs))
          (force (sd-patalist-p global-pats)))
     (sd-problemlist-p (sd-analyze-ctxexprs ctxexprs global-pats))))