		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-struct-declaration

Converts a single member of the structs of a file to a leo::topdecl-struct.

Signature
(j2f-struct-declaration json-struct) → (mv erp leo-top-struct-declaration)
Arguments: json-struct — Guard (json::memberp json-struct).
Returns: erp — Type (booleanp erp).; leo-top-struct-declaration — Type (topdeclp leo-top-struct-declaration).

Definitions and Theorems

Function: j2f-struct-declaration

(defun j2f-struct-declaration (json-struct)
 (declare (xargs :guard (json::memberp json-struct)))
 (let ((__function__ 'j2f-struct-declaration))
  (declare (ignorable __function__))
  (if
   (not (and (json::memberp json-struct)
             (jsonast-looks-like-struct-declaration-p json-struct)))
   (mv t *error-definition*)
   (b*
    ((struct-name-with-span (json::member->name json-struct))
     (struct-name (extract-identifier-name struct-name-with-span))
     ((unless (identifier-string-p struct-name))
      (mv t *error-definition*))
     (inner-struct-val (json::member->value json-struct))
     ((unless (equal :object (json::value-kind inner-struct-val)))
      (mv t *error-definition*))
     (array-of-struct-members
          (json::object-member-value "members" inner-struct-val))
     ((unless
          (equal :array (json::value-kind array-of-struct-members)))
      (mv t *error-definition*))
     (json-struct-members
          (json::value-array->elements array-of-struct-members))
     ((mv erp leo-members)
      (j2f-struct-members json-struct-members))
     ((when erp)
      (mv
       t
       (make-topdecl-struct
          :get (make-structdecl
                    :name (make-identifier :name "ERROR_in_members")
                    :components leo-members))))
     (leo-struct
          (make-structdecl :name (make-identifier :name struct-name)
                           :components leo-members)))
    (mv nil
        (make-topdecl-struct :get leo-struct))))))