		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

One-way-unify$

A logic-mode guard-verified version of one-way-unify.

Signature
(one-way-unify$ pat term state) → (mv okp subst)
Arguments: pat — Guard (pseudo-termp pat).; term — Guard (pseudo-termp term).
Returns: okp — Type (booleanp okp).; subst — Type (symbol-pseudoterm-alistp subst).

The built in one-way-unify matches a term to a pattern, returning a substituion of terms to variables if successful. The first result is a boolean indicating if the matching was successful or not; the second result is the substitution.

This one-way-unify$ function takes a state as additional argument, which it needs to call magic-ev-fncall on one-way-unify. It also ensures that the first result is a boolean and that, if the first result is t, then the second one is a substitution, i.e. an alist from symbols (variables) to terms.

Definitions and Theorems

Function: one-way-unify$

(defun one-way-unify$ (pat term state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp pat)
                             (pseudo-termp term))))
 (let ((__function__ 'one-way-unify$))
   (declare (ignorable __function__))
   (b*
    (((mv erp okp+subst)
      (magic-ev-fncall 'one-way-unify
                       (list pat term)
                       state nil t))
     ((when erp)
      (raise "Internal error: ~@0" erp)
      (mv nil nil))
     ((unless (and (true-listp okp+subst)
                   (= (len okp+subst) 2)))
      (raise "Internal error: ONE-WAY-UNIFY returned ~x0."
             okp+subst)
      (mv nil nil))
     (okp (first okp+subst))
     (subst (second okp+subst))
     ((unless (booleanp okp))
      (raise "Internal error: ONE-WAY-UNIFY's first result is ~x0."
             okp)
      (mv nil nil))
     ((unless (symbol-pseudoterm-alistp subst))
      (raise "Internal error: ONE-WAY-UNIFY's second result is ~x0."
             subst)
      (mv nil nil)))
    (mv okp subst))))

Theorem: booleanp-of-one-way-unify$.okp

(defthm booleanp-of-one-way-unify$.okp
  (b* (((mv ?okp common-lisp::?subst)
        (one-way-unify$ pat term state)))
    (booleanp okp))
  :rule-classes :rewrite)

Theorem: symbol-pseudoterm-alistp-of-one-way-unify$.subst

(defthm symbol-pseudoterm-alistp-of-one-way-unify$.subst
  (b* (((mv ?okp common-lisp::?subst)
        (one-way-unify$ pat term state)))
    (symbol-pseudoterm-alistp subst))
  :rule-classes :rewrite)