Macro to formalize a Solidity integer binary operation.
This macro takes, as required arguments,
the name of the function to define (which formalizes the operation),
an indication of whether the operation is signed or not,
and an untranslated term that defines the operation on the core value.
This term must have
This macro also takes an optional argument to impose the additional guard restriction that the right operand is not zero; this is used for the division and modulo operations.
This macro also takes optional arguments for XDOC documentation: parents, short string, and long string. The latter may be forms, e.g. involving XDOC constructors.
Macro:
(defmacro def-uint/int-binary-op (name &key signedp operation nonzerop (parents 'nil parents-suppliedp) (short 'nil short-suppliedp) (long 'nil long-suppliedp)) (cons 'make-event (cons (cons 'def-uint/int-binary-op-fn (cons (cons 'quote (cons name 'nil)) (cons (cons 'quote (cons signedp 'nil)) (cons (cons 'quote (cons operation 'nil)) (cons (cons 'quote (cons nonzerop 'nil)) (cons (cons 'quote (cons parents 'nil)) (cons parents-suppliedp (cons short (cons short-suppliedp (cons long (cons long-suppliedp 'nil))))))))))) 'nil)))
Function:
(defun def-uint/int-binary-op-fn (name signedp operation nonzerop parents parents-suppliedp short short-suppliedp long long-suppliedp) (declare (xargs :guard (and (symbolp name) (booleanp signedp) (booleanp nonzerop) (symbol-listp parents) (booleanp parents-suppliedp) (booleanp short-suppliedp) (booleanp long-suppliedp)))) (let ((__function__ 'def-uint/int-binary-op-fn)) (declare (ignorable __function__)) (b* ((type (if signedp 'int 'uint)) (typep (add-suffix type "P")) (type->size (add-suffix type "->SIZE")) (type->value (add-suffix type "->VALUE")) (make-type (packn-pos (list "MAKE-" type) type)) (guard? (and nonzerop (cons 'not (cons (cons 'equal (cons (cons type->value '(right-operand)) '(0))) 'nil))))) (cons 'define (cons name (cons (cons (cons 'left-operand (cons typep 'nil)) (cons (cons 'right-operand (cons typep 'nil)) 'nil)) (append (and guard? (list :guard guard?)) (cons ':returns (cons (cons 'result (cons typep 'nil)) (append (and parents-suppliedp (list :parents parents)) (append (and short-suppliedp (list :short short)) (append (and long-suppliedp (list :long long)) (cons (cons 'b* (cons (cons (cons 'size (cons (cons type->size '(left-operand)) 'nil)) (cons (cons 'x (cons (cons type->value '(left-operand)) 'nil)) (cons (cons 'y (cons (cons type->value '(right-operand)) 'nil)) 'nil))) (cons (cons make-type (cons ':size (cons (cons type->size '(left-operand)) (cons ':value (cons operation 'nil))))) 'nil))) '(:hooks (:fix) :no-function t))))))))))))))