Macro to formalize a Solidity integer unary 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 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-unary-op (name &key signedp operation (parents 'nil parents-suppliedp) (short 'nil short-suppliedp) (long 'nil long-suppliedp)) (cons 'make-event (cons (cons 'def-uint/int-unary-op-fn (cons (cons 'quote (cons name 'nil)) (cons (cons 'quote (cons signedp 'nil)) (cons (cons 'quote (cons operation '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-unary-op-fn (name signedp operation parents parents-suppliedp short short-suppliedp long long-suppliedp) (declare (xargs :guard (and (symbolp name) (booleanp signedp) (symbol-listp parents) (booleanp parents-suppliedp) (booleanp short-suppliedp) (booleanp long-suppliedp)))) (let ((__function__ 'def-uint/int-unary-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))) (cons 'define (cons name (cons (cons (cons 'operand (cons typep 'nil)) 'nil) (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 '(operand)) 'nil)) (cons (cons 'x (cons (cons type->value '(operand)) 'nil)) 'nil)) (cons (cons make-type (cons ':size (cons (cons type->size '(operand)) (cons ':value (cons operation 'nil))))) 'nil))) '(:hooks (:fix) :no-function t)))))))))))))