PLET

parallel version of let 
Major Section:  PARALLEL-PROGRAMMING

This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.

Example Forms:
(plet ((a (fibonacci (- x 1)))
       (b (fibonacci (- x 2))))
      (+ a b))

(plet (declare (granularity (> x 35)))
      ((a (fibonacci (- x 1)))
       (b (fibonacci (- x 2))))
      (+ a b))

General Form:
(plet (declare (granularity expr)) ; optional granularity declaration
      ((var1 val1)
       ...
       (varN valN))
      (declare ...) ... (declare ...) ; optional declarations
      body)
The syntax of plet is identical to the syntax of let, except that plet permits an optional granularity declaration in the first argument position; see granularity. In the logic a call of plet macroexpands to the corresponding call of let, where the granularity declaration (if any) is dropped.

Plet cause the evaluation of each vali above to be done in parallel before processing the body. If the above granularity declaration is present, then its expression (expr above) is first evaluated, and if the result is nil, then such parallelism is avoided. Even if parallelism is not thus avoided, parallelism may be limited by available resources.

See parallelism-at-the-top-level for restrictions on evaluating parallelism primitives from within the ACL2 top-level loop.