		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-tailrec-elimination

Atj-serialize-parallel-asg

Generate a block that performs a parallel assignment of the given expressions to the given variables, according to the supplied serialization.

Signature
(atj-serialize-parallel-asg serialization vars exprs) → block
Arguments: serialization — Guard (string-listp serialization).; vars — Guard (string-listp vars).; exprs — Guard (jexpr-listp exprs).
Returns: block — Type (jblockp block).

When the dependencies in a parallel assignment are not circular, it is possible to realize the parallel assignment via a sequence of single assignment that respects the dependencies. This function does that, based on the given serialization, which is calculated elsewhere via a topological sort.

We go through the serialization, and for each element (i.e. variable name) we find the position in the vars list, and use that position to pick the corresponding expression to use in the assignment.

We exclude trivial assignments of a variable to itself. These arise when formal arguments of tail-recursive ACL2 functions are passed unchanged as actual arguments to the recursive calls.

Definitions and Theorems

Function: atj-serialize-parallel-asg

(defun atj-serialize-parallel-asg (serialization vars exprs)
  (declare (xargs :guard (and (string-listp serialization)
                              (string-listp vars)
                              (jexpr-listp exprs))))
  (declare (xargs :guard (and (= (len vars) (len exprs))
                              (subsetp-equal serialization vars))))
  (let ((__function__ 'atj-serialize-parallel-asg))
    (declare (ignorable __function__))
    (b* (((when (endp serialization)) nil)
         (var (car serialization))
         (pos (index-of var vars))
         (expr (nth pos exprs))
         ((when (jexpr-equiv expr (jexpr-name var)))
          (atj-serialize-parallel-asg (cdr serialization)
                                      vars exprs))
         (first-asg (jblock-asg (jexpr-name var) expr))
         (rest-asg (atj-serialize-parallel-asg (cdr serialization)
                                               vars exprs)))
      (append first-asg rest-asg))))

Theorem: jblockp-of-atj-serialize-parallel-asg

(defthm jblockp-of-atj-serialize-parallel-asg
 (b* ((block (atj-serialize-parallel-asg serialization vars exprs)))
   (jblockp block))
 :rule-classes :rewrite)