		Search-engine friendly clone of the ACL2 documentation.

Json2ast

Json2ast-mutual-recursion-statements

Converts a Leo statement from JSON AST to fixtype AST.

Definitions and Theorems

Function: j2f-iteration-statement

(defun j2f-iteration-statement (json-iteration-statement)
 (declare (xargs :guard (json::memberp json-iteration-statement)))
 (let ((__function__ 'j2f-iteration-statement))
  (declare (ignorable __function__))
  (b*
   (((unless
        (and (json::memberp json-iteration-statement)
             (equal "Iteration"
                    (json::member->name json-iteration-statement))))
     (mv t *error-iteration-statement*))
    (contents (json::member->value json-iteration-statement))
    ((json::pattern
      (:object
       (:member "variable" (:string itervar))
       (:member "type_" iter-type)
       (:member "start" lb-expr)
       (:member "stop" ub-expr)
       (:member "inclusive" true-or-false)
       (:member
          "block"
          (:object (:member "statements" block-statements-array)))))
     contents)
    ((unless
        (and json::match?
             (eq :object (json::value-kind lb-expr))
             (eq :object (json::value-kind ub-expr))
             (json::value-case true-or-false
                               :true t
                               :false t
                               :otherwise nil)
             (eq :array (json::value-kind block-statements-array))))
     (mv t *error-iteration-statement*))
    (cleaned-id-value (extract-identifier-name itervar))
    ((unless (identifier-string-p cleaned-id-value))
     (mv t *error-iteration-statement*))
    (itervar-identifier (make-identifier :name cleaned-id-value))
    ((mv type-erp leo-type)
     (j2f-type iter-type))
    ((mv lb-erp leo-lb)
     (j2f-expression lb-expr))
    ((mv ub-erp leo-ub)
     (j2f-expression ub-expr))
    ((when (or lb-erp ub-erp type-erp))
     (mv t *error-iteration-statement*))
    ((mv erp leo-statements)
     (j2f-statements
          (json::value-array->elements block-statements-array)))
    ((when erp)
     (mv t *error-iteration-statement*)))
   (mv nil
       (make-statement-for :name itervar-identifier
                           :type leo-type
                           :from leo-lb
                           :to leo-ub
                           :inclusivep nil
                           :body leo-statements)))))

Function: j2f-statement

(defun j2f-statement (json-statement)
 (declare (xargs :guard (json::valuep json-statement)))
 (let ((__function__ 'j2f-statement))
  (declare (ignorable __function__))
  (b* (((unless (and (json::valuep json-statement)
                     (json::value-case json-statement :object)))
        (mv t *error-return-statement*))
       (json-stmt-object-members
            (json::value-object->members json-statement))
       ((unless (and (= 1 (len json-stmt-object-members))
                     (consp json-stmt-object-members)
                     (endp (cdr json-stmt-object-members))))
        (mv t *error-return-statement*))
       (json-member (first json-stmt-object-members))
       (json-statement-type (json::member->name json-member))
       ((unless (stringp json-statement-type))
        (mv t *error-return-statement*)))
    (if (equal "Return" json-statement-type)
        (j2f-return-statement json-member)
      (if (equal "Console" json-statement-type)
          (j2f-console-statement json-member)
        (if (equal "Definition" json-statement-type)
            (j2f-let-or-const-statement json-member)
          (if (equal "Assign" json-statement-type)
              (j2f-assign-statement json-member)
            (if (equal "Iteration" json-statement-type)
                (j2f-iteration-statement json-member)
              (if (equal "Conditional" json-statement-type)
                  (j2f-if-statement json-member)
                (if (equal "Block" json-statement-type)
                    (j2f-block-statement json-member)
                  (prog2$ (cw "ERROR: unknown statement type ~x0~%"
                              json-statement-type)
                          (mv t *error-return-statement*))))))))))))

Function: j2f-statements

(defun j2f-statements (json-statements)
  (declare (xargs :guard (json::value-listp json-statements)))
  (let ((__function__ 'j2f-statements))
    (declare (ignorable __function__))
    (b* (((when (endp json-statements))
          (mv nil nil))
         (stmt (first json-statements))
         ((mv erp leo-stmt) (j2f-statement stmt))
         ((when erp) (mv t nil))
         ((mv erp rest-leo-stmts)
          (j2f-statements (rest json-statements)))
         ((when erp) (mv t nil)))
      (mv nil (cons leo-stmt rest-leo-stmts)))))

Function: j2f-block-statement

(defun j2f-block-statement (json-block-statement)
 (declare (xargs :guard (json::memberp json-block-statement)))
 (let ((__function__ 'j2f-block-statement))
  (declare (ignorable __function__))
  (b*
   (((unless
          (and (json::memberp json-block-statement)
               (equal "Block"
                      (json::member->name json-block-statement))))
     (mv t *error-block-statement*))
    ((json::pattern (:object (:member "statements"
                                      (:array inner-statements..))))
     (json::member->value json-block-statement))
    ((unless (and json::match?
                  (json::value-listp inner-statements..)))
     (mv t *error-block-statement*))
    ((mv erp leo-statements)
     (j2f-statements inner-statements..))
    ((when erp)
     (mv t *error-block-statement*)))
   (mv nil
       (make-statement-block :get leo-statements)))))

Function: j2f-if-statement

(defun j2f-if-statement (json-conditional-statement)
 (declare (xargs :guard (json::memberp json-conditional-statement)))
 (let ((__function__ 'j2f-if-statement))
  (declare (ignorable __function__))
  (b*
   (((unless
      (and (json::memberp json-conditional-statement)
           (equal "Conditional"
                  (json::member->name json-conditional-statement))))
     (mv t *error-conditional-statement*))
    ((json::pattern
      (:object
          (:member "condition" branch-1-condition-expr)
          (:member
               "then"
               (:object (:member "statements" branch-1-statements)))
          (:member "otherwise"
                   remaining-branches-and-last-else)))
     (json::member->value json-conditional-statement))
    ((unless
        (and json::match?
             (eq :object (json::value-kind branch-1-condition-expr))
             (eq :array (json::value-kind branch-1-statements))))
     (mv t *error-conditional-statement*))
    ((mv erp leo-b1-condition)
     (j2f-expression branch-1-condition-expr))
    ((when erp)
     (mv t *error-conditional-statement*))
    ((mv erp leo-b1-statements)
     (j2f-statements
          (json::value-array->elements branch-1-statements)))
    ((when erp)
     (mv t *error-conditional-statement*))
    (leo-first-branch (make-branch :test leo-b1-condition
                                   :body leo-b1-statements))
    ((mv erp
         remaining-branches last-else-statements)
     (j2f-if-statement-tail remaining-branches-and-last-else))
    ((when erp)
     (mv t *error-conditional-statement*)))
   (mv nil
       (make-statement-if
            :branches (cons leo-first-branch remaining-branches)
            :else last-else-statements)))))

Function: j2f-if-statement-tail

(defun j2f-if-statement-tail (json-conditional-next-value)
 (declare (xargs :guard (json::valuep json-conditional-next-value)))
 (let ((__function__ 'j2f-if-statement-tail))
  (declare (ignorable __function__))
  (b*
   (((unless (json::valuep json-conditional-next-value))
     (mv t nil nil))
    ((when
          (eq :null (json::value-kind json-conditional-next-value)))
     (mv nil nil nil))
    ((json::pattern
      (:object
       (:member
            "Block"
            (:object (:member "statements" last-else-statements)))))
     json-conditional-next-value)
    ((when json::match?)
     (if
      (eq :array (json::value-kind last-else-statements))
      (mv-let
           (erp statement-list)
           (j2f-statements
                (json::value-array->elements last-else-statements))
        (if erp (mv t nil nil)
          (mv nil nil statement-list)))
      (mv t nil nil)))
    ((json::pattern
      (:object
          (:member
               "Conditional"
               (:object (:member "condition" c)
                        (:member "then"
                                 (:object (:member "statements" s)))
                        (:member "otherwise" n)))))
     json-conditional-next-value)
    ((unless (and json::match?
                  (eq :object (json::value-kind c))
                  (eq :array (json::value-kind s))))
     (mv t nil nil))
    ((mv erp leo-condition)
     (j2f-expression c))
    ((when erp) (mv t nil nil))
    ((mv erp leo-statements)
     (j2f-statements (json::value-array->elements s)))
    ((when erp) (mv t nil nil))
    (leo-this-branch (make-branch :test leo-condition
                                  :body leo-statements))
    ((mv erp remaining-branches last-else-stmts)
     (j2f-if-statement-tail n))
    ((when erp) (mv t nil nil)))
   (mv nil
       (cons leo-this-branch remaining-branches)
       last-else-stmts))))