		Search-engine friendly clone of the ACL2 documentation.

Ctrex-rule

Make-ctrex-rule

Basic constructor macro for ctrex-rule structures.

Syntax

(make-ctrex-rule [:name <name>] 
                 [:match <match>] 
                 [:unify-subst <unify-subst>] 
                 [:target <target>] 
                 [:deps <deps>] 
                 [:dep-success-vars <dep-success-vars>] 
                 [:success <success>] 
                 [:priority <priority>] 
                 [:value <value>] 
                 [:order <order>] 
                 [:ruletype <ruletype>])

This is the usual way to construct ctrex-rule structures. It simply conses together a structure with the specified fields.

This macro generates a new ctrex-rule structure from scratch. See also change-ctrex-rule, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-ctrex-rule

(defmacro make-ctrex-rule (&rest args)
  (std::make-aggregate 'ctrex-rule
                       args
                       '((:name)
                         (:match)
                         (:unify-subst)
                         (:target)
                         (:deps)
                         (:dep-success-vars)
                         (:success)
                         (:priority)
                         (:value)
                         (:order)
                         (:ruletype))
                       'make-ctrex-rule
                       nil))

Function: ctrex-rule

(defun ctrex-rule (name match
                        unify-subst target deps dep-success-vars
                        success priority value order ruletype)
 (declare (xargs :guard (and (symbolp name)
                             (pseudo-termp match)
                             (fgl-object-bindings-p unify-subst)
                             (pseudo-termp target)
                             (pseudo-term-subst-p deps)
                             (pseudo-term-subst-p dep-success-vars)
                             (pseudo-termp success)
                             (pseudo-termp priority)
                             (pseudo-termp value)
                             (natp order)
                             (ctrex-ruletype-p ruletype))))
 (declare (xargs :guard t))
 (let ((__function__ 'ctrex-rule))
   (declare (ignorable __function__))
   (b*
     ((name (mbe :logic (acl2::symbol-fix name)
                 :exec name))
      (match (mbe :logic (pseudo-term-fix match)
                  :exec match))
      (unify-subst (mbe :logic (fgl-object-bindings-fix unify-subst)
                        :exec unify-subst))
      (target (mbe :logic (pseudo-term-fix target)
                   :exec target))
      (deps (mbe :logic (pseudo-term-subst-fix deps)
                 :exec deps))
      (dep-success-vars
           (mbe :logic (pseudo-term-subst-fix dep-success-vars)
                :exec dep-success-vars))
      (success (mbe :logic (pseudo-term-fix success)
                    :exec success))
      (priority (mbe :logic (pseudo-term-fix priority)
                     :exec priority))
      (value (mbe :logic (pseudo-term-fix value)
                  :exec value))
      (order (mbe :logic (nfix order) :exec order))
      (ruletype (mbe :logic (ctrex-ruletype-fix ruletype)
                     :exec ruletype)))
     (list (cons 'name name)
           (cons 'match match)
           (cons 'unify-subst unify-subst)
           (cons 'target target)
           (cons 'deps deps)
           (cons 'dep-success-vars
                 dep-success-vars)
           (cons 'success success)
           (cons 'priority priority)
           (cons 'value value)
           (cons 'order order)
           (cons 'ruletype ruletype)))))