		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-fns-to-translate

Collect the names of all the ACL2 functions to be translated to Java, checking that they satisfy all the necessary constraints.

Signature
(atj-fns-to-translate targets$ deep$ guards$ ignore-whitelist$ verbose$ ctx state) → (mv erp result state)
Arguments: targets$ — Guard (symbol-listp targets$).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).; ignore-whitelist$ — Guard (booleanp ignore-whitelist$).; verbose$ — Guard (booleanp verbose$).; ctx — Guard (ctxp ctx).
Returns: result — A tuple (fns-to-translate call-graph) satisfying (typed-tuplep symbol-listp symbol-symbollist-alistp result).

See the overview of the worklist algorithm first.

We start the worklist iteration with the targets supplied by the user.

The returned list of function names should have no duplicates, but we double-check that for robustness. The list is in no particular order.

We also return the call graph of those functions.

Definitions and Theorems

Function: atj-fns-to-translate

(defun atj-fns-to-translate
       (targets$ deep$ guards$
                 ignore-whitelist$ verbose$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp targets$)
                             (booleanp deep$)
                             (booleanp guards$)
                             (booleanp ignore-whitelist$)
                             (booleanp verbose$)
                             (ctxp ctx))))
 (let ((__function__ 'atj-fns-to-translate))
  (declare (ignorable __function__))
  (b*
   (((run-when verbose$)
     (cw "~%ACL2 functions to translate to Java:~%"))
    (worklist-gen targets$)
    ((er (list fns call-graph))
     (atj-worklist-iterate worklist-gen
                           nil nil nil nil deep$ guards$
                           ignore-whitelist$ verbose$ ctx state))
    ((unless (no-duplicatesp-eq fns))
     (value
      (raise
       "Internal error: ~
                       the list ~x0 of collected function names ~
                       has duplicates."
       fns))))
   (value (list fns call-graph)))))