• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
        • Syntax-for-tools
        • Atc
        • Language
        • Representation
        • Transformation-tools
          • Simpadd0
          • Deftrans
            • Deftrans-defn-expr
            • Deftrans-core
            • Deftrans-defn-type-spec
            • Deftrans-defn-stmt
            • Deftrans-defn-dirdeclor
            • Deftrans-defn-dirabsdeclor
            • Deftrans-defn-structdecl
            • Deftrans-defn-member-designor
            • Deftrans-defn-fundef
            • Deftrans-defn-decl-spec
            • Deftrans-parse-keywords
            • Deftrans-defn-param-declor
            • Deftrans-defn-spec/qual
            • Deftrans-defn-initdeclor
            • Deftrans-defn-genassoc
            • Deftrans-defn-decl
            • Deftrans-defn-block-item
            • Deftrans-defn-align-spec
            • Deftrans-mk-names
            • Deftrans-defn-structdeclor-list
            • Deftrans-defn-structdeclor
            • Deftrans-defn-structdecl-list
            • Deftrans-defn-spec/qual-list
            • Deftrans-defn-param-declon-list
            • Deftrans-defn-param-declon
            • Deftrans-defn-label
            • Deftrans-defn-initer
            • Deftrans-defn-initdeclor-list
            • Deftrans-defn-genassoc-list
            • Deftrans-defn-extdecl-list
            • Deftrans-defn-extdecl
            • Deftrans-defn-desiniter-list
            • Deftrans-defn-desiniter
            • Deftrans-defn-designor-list
            • Deftrans-defn-decl-spec-list
            • Deftrans-defn-block-item-list
            • Deftrans-defn
            • Deftrans-defn-tyname
            • Deftrans-defn-strunispec
            • Deftrans-defn-statassert
            • Deftrans-defn-initer-option
            • Deftrans-defn-ident-list
            • Deftrans-defn-expr-list
            • Deftrans-defn-enumspec
            • Deftrans-defn-enumer-list
            • Deftrans-defn-enumer
            • Deftrans-defn-dirabsdeclor-option
            • Deftrans-defn-designor
            • Deftrans-defn-declor-option
            • Deftrans-defn-declor
            • Deftrans-defn-decl-list
            • Deftrans-defn-const-expr-option
            • Deftrans-defn-const-expr
            • Deftrans-defn-absdeclor-option
            • Deftrans-defn-absdeclor
            • Deftrans-defn-transunit
            • Deftrans-defn-expr-option
            • Deftrans-cases
            • Deftrans-mk-names0
            • Deftrans-defn-ident
            • Deftrans-defn-const
            • Take-pairs
            • Deftrans-macro
            • Deftrans-get-args
          • Splitgso
          • Constant-propagation
          • Split-fn
          • Copy-fn
          • Specialize
          • Split-all-gso
          • Rename
          • Utilities
        • Insertion-sort
        • Pack
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Deftrans

Deftrans-defn-expr

Signature

(deftrans-defn-expr names bodies extra-args extra-args-names) 
  → 
*

Arguments

names — Guard (alistp names).

bodies — Guard (alistp bodies).

extra-args — Guard (true-listp extra-args).

extra-args-names — Guard (true-listp extra-args-names).

Definitions and Theorems

Function: deftrans-defn-expr

(defun deftrans-defn-expr (names bodies extra-args extra-args-names)
 (declare (xargs :guard (and (alistp names)
                             (alistp bodies)
                             (true-listp extra-args)
                             (true-listp extra-args-names))))
 (let ((__function__ 'deftrans-defn-expr))
  (declare (ignorable __function__))
  (deftrans-defn
   'expr
   names bodies '((expr exprp))
   extra-args
   (cons
    'expr-case
    (cons
     'expr
     (cons
      ':ident
      (cons
       (cons 'make-expr-ident
             (cons ':ident
                   (cons (cons (cdr (assoc-eq 'ident names))
                               (cons 'expr.ident extra-args-names))
                         '(:info expr.info))))
       (cons
        ':const
        (cons
         '(expr-fix expr)
         (cons
          ':string
          (cons
           '(expr-fix expr)
           (cons
            ':paren
            (cons
             (cons 'expr-paren
                   (cons (cons (cdr (assoc-eq 'expr names))
                               (cons 'expr.inner extra-args-names))
                         'nil))
             (cons
              ':gensel
              (cons
               (cons
                'make-expr-gensel
                (cons
                 ':control
                 (cons
                  (cons (cdr (assoc-eq 'expr names))
                        (cons 'expr.control extra-args-names))
                  (cons
                   ':assocs
                   (cons (cons (cdr (assoc-eq 'genassoc-list names))
                               (cons 'expr.assocs extra-args-names))
                         'nil)))))
               (cons
                ':arrsub
                (cons
                 (cons
                  'make-expr-arrsub
                  (cons
                   ':arg1
                   (cons
                    (cons (cdr (assoc-eq 'expr names))
                          (cons 'expr.arg1 extra-args-names))
                    (cons
                     ':arg2
                     (cons (cons (cdr (assoc-eq 'expr names))
                                 (cons 'expr.arg2 extra-args-names))
                           'nil)))))
                 (cons
                  ':funcall
                  (cons
                   (cons
                    'make-expr-funcall
                    (cons
                     ':fun
                     (cons
                      (cons (cdr (assoc-eq 'expr names))
                            (cons 'expr.fun extra-args-names))
                      (cons
                       ':args
                       (cons
                           (cons (cdr (assoc-eq 'expr-list names))
                                 (cons 'expr.args extra-args-names))
                           'nil)))))
                   (cons
                    ':member
                    (cons
                     (cons
                      'make-expr-member
                      (cons
                       ':arg
                       (cons
                            (cons (cdr (assoc-eq 'expr names))
                                  (cons 'expr.arg extra-args-names))
                            '(:name expr.name))))
                     (cons
                      ':memberp
                      (cons
                       (cons
                        'make-expr-memberp
                        (cons
                         ':arg
                         (cons
                            (cons (cdr (assoc-eq 'expr names))
                                  (cons 'expr.arg extra-args-names))
                            '(:name expr.name))))
                       (cons
                        ':complit
                        (cons
                         (cons
                          'make-expr-complit
                          (cons
                           ':type
                           (cons
                            (cons
                                 (cdr (assoc-eq 'tyname names))
                                 (cons 'expr.type extra-args-names))
                            (cons
                             ':elems
                             (cons
                              (cons
                               (cdr
                                   (assoc-eq 'desiniter-list names))
                               (cons 'expr.elems extra-args-names))
                              '(:final-comma expr.final-comma))))))
                         (cons
                          ':unary
                          (cons
                           (cons
                            'make-expr-unary
                            (cons
                             ':op
                             (cons
                              'expr.op
                              (cons
                               ':arg
                               (cons
                                (cons
                                  (cdr (assoc-eq 'expr names))
                                  (cons 'expr.arg extra-args-names))
                                '(:info expr.info))))))
                           (cons
                            ':sizeof
                            (cons
                             (cons
                              'expr-sizeof
                              (cons
                               (cons
                                 (cdr (assoc-eq 'tyname names))
                                 (cons 'expr.type extra-args-names))
                               'nil))
                             (cons
                              ':sizeof-ambig
                              (cons
                               '(prog2$
                                     (raise "Misusage error: ~x0."
                                            (expr-fix expr))
                                     (expr-fix expr))
                               (cons
                                ':alignof
                                (cons
                                 (cons
                                  'make-expr-alignof
                                  (cons
                                   ':type
                                   (cons
                                    (cons
                                      (cdr (assoc-eq 'tyname names))
                                      (cons 'expr.type
                                            extra-args-names))
                                    '(:uscores expr.uscores))))
                                 (cons
                                  ':cast
                                  (cons
                                   (cons
                                    'make-expr-cast
                                    (cons
                                     ':type
                                     (cons
                                      (cons
                                       (cdr
                                           (assoc-eq 'tyname names))
                                       (cons 'expr.type
                                             extra-args-names))
                                      (cons
                                       ':arg
                                       (cons
                                        (cons
                                         (cdr
                                             (assoc-eq 'expr names))
                                         (cons 'expr.arg
                                               extra-args-names))
                                        'nil)))))
                                   (cons
                                    ':binary
                                    (cons
                                     (cons
                                      'make-expr-binary
                                      (cons
                                       ':op
                                       (cons
                                        'expr.op
                                        (cons
                                         ':arg1
                                         (cons
                                          (cons
                                           (cdr
                                             (assoc-eq 'expr names))
                                           (cons 'expr.arg1
                                                 extra-args-names))
                                          (cons
                                           ':arg2
                                           (cons
                                            (cons
                                             (cdr (assoc-eq 'expr
                                                            names))
                                             (cons
                                                  'expr.arg2
                                                  extra-args-names))
                                            '(:info
                                                  expr.info))))))))
                                     (cons
                                      ':cond
                                      (cons
                                       (cons
                                        'make-expr-cond
                                        (cons
                                         ':test
                                         (cons
                                          (cons
                                           (cdr
                                             (assoc-eq 'expr names))
                                           (cons 'expr.test
                                                 extra-args-names))
                                          (cons
                                           ':then
                                           (cons
                                            (cons
                                             (cdr
                                              (assoc-eq 'expr-option
                                                        names))
                                             (cons
                                                  'expr.then
                                                  extra-args-names))
                                            (cons
                                             ':else
                                             (cons
                                              (cons
                                               (cdr
                                                   (assoc-eq 'expr
                                                             names))
                                               (cons
                                                  'expr.else
                                                  extra-args-names))
                                              'nil)))))))
                                       (cons
                                        ':comma
                                        (cons
                                         (cons
                                          'make-expr-comma
                                          (cons
                                           ':first
                                           (cons
                                            (cons
                                             (cdr (assoc-eq 'expr
                                                            names))
                                             (cons
                                                  'expr.first
                                                  extra-args-names))
                                            (cons
                                             ':next
                                             (cons
                                              (cons
                                               (cdr
                                                   (assoc-eq 'expr
                                                             names))
                                               (cons
                                                  'expr.next
                                                  extra-args-names))
                                              'nil)))))
                                         (cons
                                          ':cast/call-ambig
                                          (cons
                                           '(prog2$
                                             (raise
                                              "Misusage error: ~x0."
                                              (expr-fix expr))
                                             (expr-fix expr))
                                           (cons
                                            ':cast/mul-ambig
                                            (cons
                                             '(prog2$
                                               (raise
                                                "Misusage error: ~x0."
                                                (expr-fix expr))
                                               (expr-fix expr))
                                             (cons
                                              ':cast/add-ambig
                                              (cons
                                               '(prog2$
                                                 (raise
                                                  "Misusage error: ~x0."
                                                  (expr-fix expr))
                                                 (expr-fix expr))
                                               (cons
                                                ':cast/sub-ambig
                                                (cons
                                                 '(prog2$
                                                   (raise
                                                    "Misusage error: ~x0."
                                                    (expr-fix expr))
                                                   (expr-fix expr))
                                                 (cons
                                                  ':cast/and-ambig
                                                  (cons
                                                   '(prog2$
                                                     (raise
                                                      "Misusage error: ~x0."
                                                      (expr-fix
                                                           expr))
                                                     (expr-fix
                                                          expr))
                                                   (cons
                                                    ':stmt
                                                    (cons
                                                     (cons
                                                      'expr-stmt
                                                      (cons
                                                       (cons
                                                        (cdr
                                                         (assoc-eq
                                                          'block-item-list
                                                          names))
                                                        (cons
                                                         'expr.items
                                                         extra-args-names))
                                                       'nil))
                                                     (cons
                                                      ':tycompat
                                                      (cons
                                                       (cons
                                                        'make-expr-tycompat
                                                        (cons
                                                         ':type1
                                                         (cons
                                                          (cons
                                                           (cdr
                                                            (assoc-eq
                                                             'tyname
                                                             names))
                                                           (cons
                                                            'expr.type1
                                                            extra-args-names))
                                                          (cons
                                                           ':type2
                                                           (cons
                                                            (cons
                                                             (cdr
                                                              (assoc-eq
                                                               'tyname
                                                               names))
                                                             (cons
                                                              'expr.type2
                                                              extra-args-names))
                                                            'nil)))))
                                                       (cons
                                                        ':offsetof
                                                        (cons
                                                         (cons
                                                          'make-expr-offsetof
                                                          (cons
                                                           ':type
                                                           (cons
                                                            (cons
                                                             (cdr
                                                              (assoc-eq
                                                               'tyname
                                                               names))
                                                             (cons
                                                              'expr.type
                                                              extra-args-names))
                                                            (cons
                                                             ':member
                                                             (cons
                                                              (cons
                                                               (cdr
                                                                (assoc-eq
                                                                 'member-designor
                                                                 names))
                                                               (cons
                                                                'expr.member
                                                                extra-args-names))
                                                              'nil)))))
                                                         (cons
                                                          ':va-arg
                                                          (cons
                                                           (cons
                                                            'make-expr-va-arg
                                                            (cons
                                                             ':list
                                                             (cons
                                                              (cons
                                                               (cdr
                                                                (assoc-eq
                                                                 'expr
                                                                 names))
                                                               (cons
                                                                'expr.list
                                                                extra-args-names))
                                                              (cons
                                                               ':type
                                                               (cons
                                                                (cons
                                                                 (cdr
                                                                  (assoc-eq
                                                                   'tyname
                                                                   names))
                                                                 (cons
                                                                  'expr.type
                                                                  extra-args-names))
                                                                'nil)))))
                                                           (cons
                                                            ':extension
                                                            (cons
                                                             (cons
                                                              'expr-extension
                                                              (cons
                                                               (cons
                                                                (cdr
                                                                 (assoc-eq
                                                                  'expr
                                                                  names))
                                                                (cons
                                                                 'expr.expr
                                                                 extra-args-names))
                                                               'nil))
                                                             'nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   '(:returns (new-expr exprp)
              :measure (expr-count expr)))))