		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-tailrec-elimination

Atj-make-parallel-asg

Generate a block that performs a parallel assignment of the given expressions to the given variables.

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

This is used in the context of turning tail-recursions into loops, but it is more general.

A recursive method call performs, in substance, a parallel assignment of the actual arguments to the formal parameters, and then proceeds to re-execute the method's body. When we turn such a recursive call into a continue so that we can re-execute the (loop's) body, we first need to assign, to the method's formal parameters, the expressions for the actual arguments. This function generates that assignment.

As mentioned before, the assignment must be parallel: in general we cannot assign the new values in order, because earlier assignments may incorrectly change the value of expressions for later assignments. We first attempt to topologically sort the variables according to their dependencies: if there are no circularities, we perform the assignments in the topological order (note that we need to reverse the ordered list returned by depgraph::toposort, which starts with variables that do not depend on other variables, and which we must assign last). If instead there are circularities, for now we use a very simple strategy: we create temporary variables for all the method's arguments, we initialize them with the expressions, and then we assign the temporary variables to the method's parameters. This can be improved, by reducing the number of temporary variables to just where there are circular dependencies.

The temporary variables are called $1, $2, etc., which does not conflict with any other variables generated by ATJ's translation. Their types are the same as the ones of the method's parameters, which are passed to these function along with their names, and the expressions to assign.

We use a recursive auxiliary function that produces the block with the temporary variable declarations and initializations separately from the block with the assignments to the parameters. The main function concatenates them into an overall block.

Definitions and Theorems

Function: atj-make-parallel-asg-aux

(defun atj-make-parallel-asg-aux (vars types exprs i)
  (declare (xargs :guard (and (string-listp vars)
                              (jtype-listp types)
                              (jexpr-listp exprs)
                              (posp i))))
  (declare (xargs :guard (and (= (len vars) (len types))
                              (= (len types) (len exprs)))))
  (let ((__function__ 'atj-make-parallel-asg-aux))
    (declare (ignorable __function__))
    (b* (((when (endp vars)) (mv nil nil))
         (var (car vars))
         (type (car types))
         (expr (car exprs))
         (tmp (str::cat "$" (nat-to-dec-string i)))
         (first-tmp (jblock-locvar type tmp expr))
         (first-asg (jblock-asg (jexpr-name var)
                                (jexpr-name tmp)))
         ((mv rest-tmp rest-asg)
          (atj-make-parallel-asg-aux (cdr vars)
                                     (cdr types)
                                     (cdr exprs)
                                     (1+ i))))
      (mv (append first-tmp rest-tmp)
          (append first-asg rest-asg)))))

Theorem: jblockp-of-atj-make-parallel-asg-aux.tmp-block

(defthm jblockp-of-atj-make-parallel-asg-aux.tmp-block
  (b* (((mv ?tmp-block ?asg-block)
        (atj-make-parallel-asg-aux vars types exprs i)))
    (jblockp tmp-block))
  :rule-classes :rewrite)

Theorem: jblockp-of-atj-make-parallel-asg-aux.asg-block

(defthm jblockp-of-atj-make-parallel-asg-aux.asg-block
  (b* (((mv ?tmp-block ?asg-block)
        (atj-make-parallel-asg-aux vars types exprs i)))
    (jblockp asg-block))
  :rule-classes :rewrite)

Function: atj-make-parallel-asg

(defun atj-make-parallel-asg (vars types exprs)
 (declare (xargs :guard (and (string-listp vars)
                             (jtype-listp types)
                             (jexpr-listp exprs))))
 (declare (xargs :guard (and (= (len vars) (len types))
                             (= (len types) (len exprs)))))
 (let ((__function__ 'atj-make-parallel-asg))
  (declare (ignorable __function__))
  (b*
   ((graph (atj-parallel-asg-depgraph vars exprs))
    ((mv acyclicp serialization)
     (depgraph::toposort graph))
    ((unless (string-listp serialization))
     (raise
      "Internal error: ~
                topological sort of graph ~x0 of strings ~
                has generated non-strings ~x1."
      graph serialization))
    (serialization (rev serialization))
    ((when acyclicp)
     (atj-serialize-parallel-asg serialization vars exprs))
    ((mv tmp-block asg-block)
     (atj-make-parallel-asg-aux vars types exprs 1)))
   (append tmp-block asg-block))))

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

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