		Search-engine friendly clone of the ACL2 documentation.

Json2ast

J2f-struct-declarations

Converts list of members, all of which are supposed to be struct declarations, to a list of leo::topdecl.

Signature
(j2f-struct-declarations json-structs) → (mv erp leo-top-struct-declarations)
Arguments: json-structs — Guard (json::member-listp json-structs).
Returns: erp — Type (booleanp erp).; leo-top-struct-declarations — Type (topdecl-listp leo-top-struct-declarations).

Definitions and Theorems

Function: j2f-struct-declarations

(defun j2f-struct-declarations (json-structs)
  (declare (xargs :guard (json::member-listp json-structs)))
  (let ((__function__ 'j2f-struct-declarations))
    (declare (ignorable __function__))
    (if (endp json-structs)
        (mv nil nil)
      (b* ((first-json-struct (first json-structs))
           ((mv erp first-leo-struct)
            (j2f-struct-declaration first-json-struct))
           ((when erp)
            (mv erp (list first-leo-struct)))
           (rest-json-structs (rest json-structs))
           ((mv erp rest-leo-structs)
            (j2f-struct-declarations rest-json-structs))
           ((when erp) (mv erp rest-leo-structs)))
        (mv nil
            (cons first-leo-struct rest-leo-structs))))))