Generate a block that performs a parallel assignment of the given expressions to the given variables, according to the supplied serialization.
(atj-serialize-parallel-asg serialization vars exprs) → 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
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.
Function:
(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:
(defthm jblockp-of-atj-serialize-parallel-asg (b* ((block (atj-serialize-parallel-asg serialization vars exprs))) (jblockp block)) :rule-classes :rewrite)