		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) → problems
Arguments: ctxexprs — Guard (vl-ctxexprlist-p ctxexprs).; global-pats — Guard (sd-patalist-p global-pats).
Returns: problems — Type (sd-problemlist-p problems), given (sd-patalist-p global-pats).

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

ctxexprs is an vl-ctxexprlist that associates expressions with their contexts. Generally we expect that this alist includes every expression in a module.
global-pats is the sd-patalist 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-ctxexprlist-p ctxexprs)
                             (sd-patalist-p global-pats))))
 (let ((__function__ 'sd-analyze-ctxexprs))
  (declare (ignorable __function__))
  (if (atom ctxexprs)
      nil
   (b* (((vl-ctxexpr x1) (car ctxexprs))
        (expr-names (vl-expr-varnames x1.expr))
        (expr-keys (sd-keygen-list expr-names nil))
        (expr-pats (make-sd-patalist expr-keys))
        (dom (strip-cars expr-pats))
        (report1
             (sd-patalist-compare dom expr-pats global-pats x1.ctx))
        (- (flush-hons-get-hash-table-link expr-pats)))
     (append report1
             (sd-analyze-ctxexprs (cdr ctxexprs)
                                  global-pats))))))

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

(defthm sd-problemlist-p-of-sd-analyze-ctxexprs
  (implies
       (sd-patalist-p global-pats)
       (b* ((problems (sd-analyze-ctxexprs ctxexprs global-pats)))
         (sd-problemlist-p problems)))
  :rule-classes :rewrite)

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

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