		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-patalist-compare

Perform skip-detection for a single expression.

Signature
(sd-patalist-compare dom x y ctx) → probs
Arguments: dom — In practice, this is the strip-cars of x. That is, it is the list of all pattern names that were found in the expression, and which we need to investigate.; x — The pattern produced for some particular expression.
Guard (sd-patalist-p x).; y — The global sd-patalist-p that we assume was produced for the entire module.
Guard (sd-patalist-p y).; ctx — Where this expression came from.
Guard (vl-context1-p ctx).
Returns: probs — Type (sd-problemlist-p probs), given the guard.

We recur over dom. For each pattern named in the expression, we use sd-keylist-find-skipped to try to find any skipped wires, collecting any problems that have been reported.

Definitions and Theorems

Function: sd-patalist-compare

(defun sd-patalist-compare (dom x y ctx)
 (declare (xargs :guard (and (sd-patalist-p x)
                             (sd-patalist-p y)
                             (vl-context1-p ctx))))
 (let ((__function__ 'sd-patalist-compare))
  (declare (ignorable __function__))
  (if (atom dom)
      nil
    (let
       ((first (sd-keylist-find-skipped (cdr (hons-get (car dom) x))
                                        (cdr (hons-get (car dom) y))
                                        ctx))
        (rest (sd-patalist-compare (cdr dom)
                                   x y ctx)))
      (if first (cons first rest) rest)))))

Theorem: sd-problemlist-p-of-sd-patalist-compare

(defthm sd-problemlist-p-of-sd-patalist-compare
  (implies (and (force (sd-patalist-p x))
                (force (sd-patalist-p y))
                (force (vl-context1-p ctx)))
           (b* ((probs (sd-patalist-compare dom x y ctx)))
             (sd-problemlist-p probs)))
  :rule-classes :rewrite)