		Search-engine friendly clone of the ACL2 documentation.

Jmethod

Make-jmethod

Basic constructor macro for jmethod structures.

Syntax

(make-jmethod [:access <access>] 
              [:abstract? <abstract?>] 
              [:static? <static?>] 
              [:final? <final?>] 
              [:synchronized? <synchronized?>] 
              [:native? <native?>] 
              [:strictfp? <strictfp?>] 
              [:result <result>] 
              [:name <name>] 
              [:params <params>] 
              [:throws <throws>] 
              [:body <body>])

This is the usual way to construct jmethod structures. It simply conses together a structure with the specified fields.

This macro generates a new jmethod structure from scratch. See also change-jmethod, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-jmethod

(defmacro make-jmethod (&rest args)
  (std::make-aggregate 'jmethod
                       args
                       '((:access)
                         (:abstract?)
                         (:static?)
                         (:final?)
                         (:synchronized?)
                         (:native?)
                         (:strictfp?)
                         (:result)
                         (:name)
                         (:params)
                         (:throws)
                         (:body))
                       'make-jmethod
                       nil))

Function: jmethod

(defun jmethod (access abstract? static?
                       final? synchronized? native? strictfp?
                       result name params throws body)
  (declare (xargs :guard (and (jaccessp access)
                              (booleanp abstract?)
                              (booleanp static?)
                              (booleanp final?)
                              (booleanp synchronized?)
                              (booleanp native?)
                              (booleanp strictfp?)
                              (jresultp result)
                              (stringp name)
                              (jparam-listp params)
                              (string-listp throws)
                              (jblockp body))))
  (declare (xargs :guard t))
  (let ((__function__ 'jmethod))
    (declare (ignorable __function__))
    (b* ((access (mbe :logic (jaccess-fix access)
                      :exec access))
         (abstract? (mbe :logic (acl2::bool-fix abstract?)
                         :exec abstract?))
         (static? (mbe :logic (acl2::bool-fix static?)
                       :exec static?))
         (final? (mbe :logic (acl2::bool-fix final?)
                      :exec final?))
         (synchronized? (mbe :logic (acl2::bool-fix synchronized?)
                             :exec synchronized?))
         (native? (mbe :logic (acl2::bool-fix native?)
                       :exec native?))
         (strictfp? (mbe :logic (acl2::bool-fix strictfp?)
                         :exec strictfp?))
         (result (mbe :logic (jresult-fix result)
                      :exec result))
         (name (mbe :logic (str-fix name) :exec name))
         (params (mbe :logic (jparam-list-fix params)
                      :exec params))
         (throws (mbe :logic (string-list-fix throws)
                      :exec throws))
         (body (mbe :logic (jblock-fix body)
                    :exec body)))
      (list (cons 'access access)
            (cons 'abstract? abstract?)
            (cons 'static? static?)
            (cons 'final? final?)
            (cons 'synchronized? synchronized?)
            (cons 'native? native?)
            (cons 'strictfp? strictfp?)
            (cons 'result result)
            (cons 'name name)
            (cons 'params params)
            (cons 'throws throws)
            (cons 'body body)))))