		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-all-pkg-methods

Generate all the methods of the classes for all the ACL2 packages.

Signature
(atj-gen-shallow-all-pkg-methods pkgs fns-by-pkg fns fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld) → (mv methods-by-pkg new-qconsts new-mv-typess)
Arguments: pkgs — Guard (string-listp pkgs).; fns-by-pkg — Guard (string-symbollist-alistp fns-by-pkg).; fns — Guard (symbol-listp fns).; fns-that-may-throw — Guard (symbol-listp fns-that-may-throw).; qconsts — Guard (atj-qconstants-p qconsts).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; mv-typess — Guard (atj-type-list-listp mv-typess).; guards$ — Guard (booleanp guards$).; no-aij-types$ — Guard (booleanp no-aij-types$).; verbose$ — Guard (booleanp verbose$).; wrld — Guard (plist-worldp wrld).
Returns: methods-by-pkg — Type (string-jmethodlist-alistp methods-by-pkg), given (string-listp pkgs).; new-qconsts — Type (atj-qconstants-p new-qconsts), given (atj-qconstants-p qconsts).; new-mv-typess — Type (and (atj-type-list-listp new-mv-typess) (cons-listp new-mv-typess)), given (and (atj-type-list-listp mv-typess) (cons-listp mv-typess)).

We go through all the packages in pkgs and construct an alist from the packages there to the corresponding method lists (i.e. the methods of the class that corresponds to the package). If there are no methods for a package, we do not add an entry for the package in the alist.

Definitions and Theorems

Function: atj-gen-shallow-all-pkg-methods

(defun atj-gen-shallow-all-pkg-methods
       (pkgs fns-by-pkg fns fns-that-may-throw
             qconsts pkg-class-names
             fn-method-names mv-typess
             guards$ no-aij-types$ verbose$ wrld)
  (declare (xargs :guard (and (string-listp pkgs)
                              (string-symbollist-alistp fns-by-pkg)
                              (symbol-listp fns)
                              (symbol-listp fns-that-may-throw)
                              (atj-qconstants-p qconsts)
                              (string-string-alistp pkg-class-names)
                              (symbol-string-alistp fn-method-names)
                              (atj-type-list-listp mv-typess)
                              (booleanp guards$)
                              (booleanp no-aij-types$)
                              (booleanp verbose$)
                              (plist-worldp wrld))))
  (declare (xargs :guard (cons-listp mv-typess)))
  (let ((__function__ 'atj-gen-shallow-all-pkg-methods))
    (declare (ignorable __function__))
    (b* (((when (endp pkgs))
          (mv nil qconsts mv-typess))
         (pkg (car pkgs))
         ((mv first-methods qconsts mv-typess)
          (atj-gen-shallow-pkg-methods
               pkg fns-by-pkg fns fns-that-may-throw
               qconsts pkg-class-names
               fn-method-names mv-typess
               guards$ no-aij-types$ verbose$ wrld))
         ((mv rest-methods qconsts mv-typess)
          (atj-gen-shallow-all-pkg-methods
               (cdr pkgs)
               fns-by-pkg fns fns-that-may-throw
               qconsts pkg-class-names
               fn-method-names mv-typess
               guards$ no-aij-types$ verbose$ wrld)))
      (if (null first-methods)
          (mv rest-methods qconsts mv-typess)
        (mv (acons pkg first-methods rest-methods)
            qconsts mv-typess)))))

Theorem: string-jmethodlist-alistp-of-atj-gen-shallow-all-pkg-methods.methods-by-pkg

(defthm
 string-jmethodlist-alistp-of-atj-gen-shallow-all-pkg-methods.methods-by-pkg
 (implies (string-listp pkgs)
          (b* (((mv ?methods-by-pkg
                    ?new-qconsts ?new-mv-typess)
                (atj-gen-shallow-all-pkg-methods
                     pkgs fns-by-pkg fns fns-that-may-throw
                     qconsts pkg-class-names
                     fn-method-names mv-typess
                     guards$ no-aij-types$ verbose$ wrld)))
            (string-jmethodlist-alistp methods-by-pkg)))
 :rule-classes :rewrite)

Theorem: atj-qconstants-p-of-atj-gen-shallow-all-pkg-methods.new-qconsts

(defthm
    atj-qconstants-p-of-atj-gen-shallow-all-pkg-methods.new-qconsts
  (implies (atj-qconstants-p qconsts)
           (b* (((mv ?methods-by-pkg
                     ?new-qconsts ?new-mv-typess)
                 (atj-gen-shallow-all-pkg-methods
                      pkgs fns-by-pkg fns fns-that-may-throw
                      qconsts pkg-class-names
                      fn-method-names mv-typess
                      guards$ no-aij-types$ verbose$ wrld)))
             (atj-qconstants-p new-qconsts)))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-shallow-all-pkg-methods.new-mv-typess

(defthm return-type-of-atj-gen-shallow-all-pkg-methods.new-mv-typess
  (implies (and (atj-type-list-listp mv-typess)
                (cons-listp mv-typess))
           (b* (((mv ?methods-by-pkg
                     ?new-qconsts ?new-mv-typess)
                 (atj-gen-shallow-all-pkg-methods
                      pkgs fns-by-pkg fns fns-that-may-throw
                      qconsts pkg-class-names
                      fn-method-names mv-typess
                      guards$ no-aij-types$ verbose$ wrld)))
             (and (atj-type-list-listp new-mv-typess)
                  (cons-listp new-mv-typess))))
  :rule-classes :rewrite)