		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-inputs

Process the inputs to atj.

Signature
(atj-process-inputs args ctx state) → (mv erp result state)
Arguments: args — Guard (true-listp args).
Returns: result — A tuple (fns-to-translate call-graph pkgs deep$ guards$ no-aij-types$ java-package$ java-class$ output-subdir output-file$ output-file-env$ output-file-test$ tests$ verbose$) satisfying (typed-tuplep symbol-listp symbol-symbollist-alistp string-listp booleanp booleanp booleanp maybe-stringp stringp stringp stringp maybe-stringp maybe-stringp atj-test-listp booleanp result).

We also collect, check, and return the functions for which code must be generated. We also collect and return the packages whose representation must be built in Java; for now these are all the current packages, but it might be possible to reduce them to just the ones referenced by the functions.

Definitions and Theorems

Function: atj-process-inputs

(defun atj-process-inputs (args ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (true-listp args)))
 (let ((__function__ 'atj-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((mv erp targets options)
     (partition-rest-and-keyword-args args *atj-allowed-options*))
    ((when erp)
     (er-soft+
      ctx t nil
      "The inputs must be the names of ~
                              one or more target functions ~
                              followed by the options ~&0."
      *atj-allowed-options*))
    (deep (cdr (assoc-eq :deep options)))
    (guards (b* ((pair? (assoc-eq :guards options)))
              (if (consp pair?) (cdr pair?) t)))
    (no-aij-types (cdr (assoc-eq :no-aij-types options)))
    (java-package (cdr (assoc-eq :java-package options)))
    (java-class (cdr (assoc-eq :java-class options)))
    (output-dir (or (cdr (assoc-eq :output-dir options))
                    "."))
    (tests (cdr (assoc-eq :tests options)))
    (ignore-whitelist (cdr (assoc-eq :ignore-whitelist options)))
    (verbose (cdr (assoc-eq :verbose options)))
    ((er &)
     (atj-process-targets targets deep guards ctx state))
    ((er &)
     (ensure-value-is-boolean$ deep "The :DEEP intput" t nil))
    ((er &)
     (ensure-value-is-boolean$ guards "The :GUARDS intput" t nil))
    ((er &)
     (atj-process-no-aij-types no-aij-types deep guards ctx state))
    ((er &)
     (atj-process-java-package java-package ctx state))
    ((er java-class$)
     (atj-process-java-class java-class ctx state))
    ((er tests$)
     (atj-process-tests tests targets deep guards ctx state))
    ((er (list output-subdir output-file$
               output-file-env$ output-file-test$))
     (atj-process-output-dir output-dir no-aij-types java-package
                             java-class$ tests$ ctx state))
    ((er &)
     (ensure-value-is-boolean$ ignore-whitelist
                               "The :IGNORE-WHITELIST input" t nil))
    ((er &)
     (ensure-value-is-boolean$ verbose "The :VERBOSE input" t nil))
    ((er (list fns-to-translate call-graph))
     (atj-fns-to-translate targets deep guards
                           ignore-whitelist verbose ctx state))
    (pkgs (atj-pkgs-to-translate verbose state)))
   (value (list fns-to-translate
                call-graph pkgs deep guards no-aij-types
                java-package java-class$ output-subdir
                output-file$ output-file-env$
                output-file-test$ tests$ verbose)))))