let
Major Section: 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.