• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
      • Aleobft
      • Aleovm
      • Leo
        • Grammar
        • Early-version
          • Json2ast
            • Json2ast-mutual-recursion-expressions
              • J2f-function-call-expression-top
              • J2f-unary-expression
              • J2f-ternary-expression
              • J2f-function-call-expression
              • J2f-binop-expression
              • J2f-expression-list
              • J2f-expression
            • Json-fixtype-span-removal
            • Json2ast-mutual-recursion-statements
            • Json-value-is-span-object-p
            • Json-value-is-core-span-object-p
            • Json2ast-mutual-recursion-types
            • J2f-struct-declaration
            • J2f-console-statement
            • Jsonast-looks-like-function-definition-p
            • J2f-function-definition
            • J2f-assign-statement
            • Json-member-is-span-p
            • J2f-struct-declarations
            • J2f-let-or-const-statement
            • J2f-console-error
            • J2f-struct-members
            • J2f-return-statement
            • J2f-function-definitions
            • J2f-console-log
            • J2f-console-assert
            • Jsonast-looks-like-struct-declaration-p
            • J2f-funinputs
            • J2f-if-statement-tail
            • Jsonast-looks-like-file-p
            • J2f-iteration-statement
            • J2f-if-statement
            • J2f-block-statement
            • J2f-statements
            • J2f-statement
            • J2f-type
          • Testing
          • Definition
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Json2ast

Json2ast-mutual-recursion-expressions

Converts a Leo expression from JSON AST to fixtype AST.

Definitions and Theorems

Function: j2f-ternary-expression

(defun j2f-ternary-expression (json-ifelse-expression)
 (declare (xargs :guard (json::memberp json-ifelse-expression)))
 (let ((__function__ 'j2f-ternary-expression))
  (declare (ignorable __function__))
  (b*
   (((unless
          (and (json::memberp json-ifelse-expression)
               (equal "Ternary"
                      (json::member->name json-ifelse-expression))))
     (mv t *error-cond*))
    ((json::pattern (:object (:member "condition" test-expr)
                             (:member "if_true" then-expr)
                             (:member "if_false" else-expr)))
     (json::member->value json-ifelse-expression))
    ((unless json::match?)
     (mv t *error-cond*))
    ((mv erp-test leo-test)
     (j2f-expression test-expr))
    ((mv erp-then leo-then)
     (j2f-expression then-expr))
    ((mv erp-else leo-else)
     (j2f-expression else-expr))
    ((when (or erp-test erp-then erp-else))
     (mv t *error-cond*)))
   (mv nil
       (make-expression-cond :test leo-test
                             :then leo-then
                             :else leo-else)))))

Function: j2f-binop-expression

(defun j2f-binop-expression (json-binop-expression)
 (declare (xargs :guard (json::memberp json-binop-expression)))
 (let ((__function__ 'j2f-binop-expression))
  (declare (ignorable __function__))
  (b*
   (((unless
      (and
       (json::memberp json-binop-expression)
       (equal "Binary"
              (json::member->name json-binop-expression))
       (json::valuep (json::member->value json-binop-expression))
       (equal
        :object (json::value-kind
                     (json::member->value json-binop-expression)))))
     (mv t *error-binop*))
    ((json::pattern (:object (:member "left" left_operand)
                             (:member "right" right_operand)
                             (:member "op" (:string opname))))
     (json::member->value json-binop-expression))
    ((unless json::match?)
     (mv t *error-binop*))
    ((mv erp expression1)
     (j2f-expression left_operand))
    ((when erp) (mv t *error-binop*))
    ((mv erp expression2)
     (j2f-expression right_operand))
    ((when erp) (mv t *error-binop*)))
   (mv nil
       (make-expression-binary :op (j2f-binop-name-to-binop opname)
                               :arg1 expression1
                               :arg2 expression2)))))

Function: j2f-unary-expression

(defun j2f-unary-expression (json-unary-expression)
 (declare (xargs :guard (json::memberp json-unary-expression)))
 (let ((__function__ 'j2f-unary-expression))
  (declare (ignorable __function__))
  (b*
   (((unless
      (and
       (json::memberp json-unary-expression)
       (equal "Unary"
              (json::member->name json-unary-expression))
       (json::valuep (json::member->value json-unary-expression))
       (equal
        :object (json::value-kind
                     (json::member->value json-unary-expression)))))
     (mv t *error-unary-op*))
    ((json::pattern (:object (:member "receiver" operand)
                             (:member "op" (:string opname))))
     (json::member->value json-unary-expression))
    ((unless json::match?)
     (mv t *error-unary-op*))
    ((mv erp expression)
     (j2f-expression operand))
    ((when erp) (mv t *error-unary-op*)))
   (mv nil
       (make-expression-unary :op (j2f-unary-op-name-to-unop opname)
                              :arg expression)))))

Function: j2f-function-call-expression-top

(defun j2f-function-call-expression-top
       (ident-w-span json-array-of-arg-exprs)
 (declare
      (xargs :guard (and (stringp ident-w-span)
                         (json::valuep json-array-of-arg-exprs))))
 (let ((__function__ 'j2f-function-call-expression-top))
  (declare (ignorable __function__))
  (b*
   (((unless
       (and (stringp ident-w-span)
            (json::valuep json-array-of-arg-exprs)
            (eq :array (json::value-kind json-array-of-arg-exprs))))
     (mv t *error-expression*))
    (cleaned-id-value (extract-identifier-name ident-w-span))
    ((unless (identifier-string-p cleaned-id-value))
     (mv t *error-expression*))
    ((mv erp arg-exprs)
     (j2f-expression-list
          (json::value-array->elements json-array-of-arg-exprs)))
    ((when erp) (mv t *error-expression*)))
   (mv nil
       (make-expression-internal-call
            :fun (make-identifier :name cleaned-id-value)
            :args arg-exprs)))))

Function: j2f-function-call-expression

(defun j2f-function-call-expression (json-funcall-expression)
 (declare (xargs :guard (json::memberp json-funcall-expression)))
 (let ((__function__ 'j2f-function-call-expression))
  (declare (ignorable __function__))
  (b*
   (((unless
         (and (json::memberp json-funcall-expression)
              (equal "Call"
                     (json::member->name json-funcall-expression))))
     (mv t *error-expression*))
    ((json::pattern
      (:object
       (:member
            "function"
            (:object (:member "Identifier" (:string ident-w-span))))
       (:member "arguments" json-array-of-arg-exprs)))
     (json::member->value json-funcall-expression))
    ((when (and json::match? (stringp ident-w-span)
                (json::valuep json-array-of-arg-exprs)))
     (j2f-function-call-expression-top
          ident-w-span json-array-of-arg-exprs)))
   (mv t *error-expression*))))

Function: j2f-expression-list

(defun j2f-expression-list (json-expressions)
  (declare (xargs :guard (json::value-listp json-expressions)))
  (let ((__function__ 'j2f-expression-list))
    (declare (ignorable __function__))
    (b* (((when (endp json-expressions))
          (mv nil nil))
         ((mv first-erp first-expr)
          (j2f-expression (car json-expressions)))
         ((mv rest-erp rest-exprs)
          (j2f-expression-list (cdr json-expressions))))
      (mv (or first-erp rest-erp)
          (cons first-expr rest-exprs)))))

Function: j2f-expression

(defun j2f-expression (json-expression)
 (declare (xargs :guard (json::valuep json-expression)))
 (let ((__function__ 'j2f-expression))
  (declare (ignorable __function__))
  (if
   (equal :object (json::value-kind json-expression))
   (if
    (and (= 1
            (len (json::value-object->members json-expression)))
         (consp (json::value-object->members json-expression)))
    (let
      ((json-member
            (first (json::value-object->members json-expression))))
     (if (equal "Call" (json::member->name json-member))
         (j2f-function-call-expression json-member)
      (if (equal "Ternary"
                 (json::member->name json-member))
          (j2f-ternary-expression json-member)
       (if (equal "Binary"
                  (json::member->name json-member))
           (j2f-binop-expression json-member)
        (if (equal "Unary"
                   (json::member->name json-member))
            (j2f-unary-expression json-member)
         (if (equal "Literal"
                    (json::member->name json-member))
             (j2f-value-wrapper-expression json-member)
          (if (equal "value"
                     (json::member->name json-member))
              (j2f-value-expression json-member)
           (if (equal "Implicit"
                      (json::member->name json-member))
               (j2f-implicit-expression json-member)
            (if (equal "Expression"
                       (json::member->name json-member))
                (j2f-expression-expression json-member)
             (if (equal "Identifier"
                        (json::member->name json-member))
                 (j2f-var-or-self-expression json-member)
              (if (equal "Integer"
                         (json::member->name json-member))
                  (j2f-integer-literal-expression json-member)
               (if (equal "Boolean"
                          (json::member->name json-member))
                   (j2f-boolean-literal-expression json-member)
                (if (equal "Field"
                           (json::member->name json-member))
                    (j2f-field-literal-expression json-member)
                  (if (equal "Group"
                             (json::member->name json-member))
                      (j2f-group-literal-expression json-member)
                    (if (equal "Address"
                               (json::member->name json-member))
                        (j2f-address-literal-expression json-member)
                      (mv t *error-expression*))))))))))))))))
    (let
     ((json-members (json::value-object->members json-expression)))
     (if (and (< 1 (len json-members))
              (equal "identifier"
                     (json::member->name (first json-members))))
         (j2f-var-or-self-expression-2 (first json-members))
       (mv t *error-expression*))))
   (mv t *error-expression*))))

Subtopics

J2f-function-call-expression-top

J2f-unary-expression

J2f-ternary-expression

J2f-function-call-expression

J2f-binop-expression

J2f-expression-list

J2f-expression