		Search-engine friendly clone of the ACL2 documentation.

Json2ast

Jsonast-looks-like-function-definition-p

Checks if THING is a JSON AST function definition object member.

Signature
(jsonast-looks-like-function-definition-p thing outer-mangled-name) → yes/no
Arguments: thing — Guard (json::memberp thing).; outer-mangled-name — Guard (stringp outer-mangled-name).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: jsonast-looks-like-function-definition-p

(defun jsonast-looks-like-function-definition-p
       (thing outer-mangled-name)
 (declare (xargs :guard (and (json::memberp thing)
                             (stringp outer-mangled-name))))
 (let ((__function__ 'jsonast-looks-like-function-definition-p))
  (declare (ignorable __function__))
  (and
   (json::memberp thing)
   (let ((inner-fn-val (json::member->value thing)))
    (and
     (json::valuep inner-fn-val)
     (equal :object (json::value-kind inner-fn-val))
     (json::object-has-member-p "identifier" inner-fn-val)
     (json::valuep
          (json::object-member-value "identifier" inner-fn-val))
     (equal
        :string
        (json::value-kind
             (json::object-member-value "identifier" inner-fn-val)))
     (equal
        outer-mangled-name
        (json::value-string->get
             (json::object-member-value "identifier" inner-fn-val)))
     (json::object-has-member-p "input" inner-fn-val)
     (json::object-has-member-p "output" inner-fn-val)
     (json::object-has-member-p "block" inner-fn-val)
     (b*
      ((block-val (json::object-member-value "block" inner-fn-val))
       ((json::pattern
          (:object (:member "statements" json-array-of-statements)))
        block-val))
      (and
       json::match?
       (equal
          :array (json::value-kind json-array-of-statements)))))))))