		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>] 
                 [:assigned-var <assigned-var>] 
                 [:assign <assign>] 
                 [:match <match>] 
                 [:match-conds <match-conds>] 
                 [:assign-cond <assign-cond>] 
                 [:hyp <hyp>] 
                 [:equiv <equiv>] 
                 [: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)
                         (:assigned-var)
                         (:assign)
                         (:match)
                         (:match-conds)
                         (:assign-cond quote 't)
                         (:hyp)
                         (:equiv)
                         (:ruletype))
                       'make-ctrex-rule
                       nil))

Function: ctrex-rule

(defun ctrex-rule (name assigned-var assign match match-conds
                        assign-cond hyp equiv ruletype)
 (declare (xargs :guard (and (symbolp name)
                             (pseudo-var-p assigned-var)
                             (pseudo-termp assign)
                             (pseudo-term-subst-p match)
                             (pseudo-term-subst-p match-conds)
                             (pseudo-termp assign-cond)
                             (pseudo-termp hyp)
                             (pseudo-fnsym-p equiv)
                             (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))
        (assigned-var (mbe :logic (pseudo-var-fix assigned-var)
                           :exec assigned-var))
        (assign (mbe :logic (pseudo-term-fix assign)
                     :exec assign))
        (match (mbe :logic (pseudo-term-subst-fix match)
                    :exec match))
        (match-conds (mbe :logic (pseudo-term-subst-fix match-conds)
                          :exec match-conds))
        (assign-cond (mbe :logic (pseudo-term-fix assign-cond)
                          :exec assign-cond))
        (hyp (mbe :logic (pseudo-term-fix hyp)
                  :exec hyp))
        (equiv (mbe :logic (pseudo-fnsym-fix equiv)
                    :exec equiv))
        (ruletype (mbe :logic (ctrex-ruletype-fix ruletype)
                       :exec ruletype)))
     (std::prod-cons
          (std::prod-cons (std::prod-cons name assigned-var)
                          (std::prod-cons assign match))
          (std::prod-cons
               (std::prod-cons match-conds assign-cond)
               (std::prod-cons hyp
                               (std::prod-cons equiv ruletype)))))))