Macro to formalize the Solidity integer comparisons.
This macro takes, as required arguments,
the name of the function to define (which formalizes the comparison),
an indication of whether the comparison is signed or not,
and an untranslated term that defines the comparison on the core values.
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-comparison (name &key signedp operation (parents 'nil parents-suppliedp) (short 'nil short-suppliedp) (long 'nil long-suppliedp)) (cons 'make-event (cons (cons 'def-uint/int-comparison-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-comparison-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-comparison-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"))) (cons 'define (cons name (cons (cons (cons 'left (cons typep 'nil)) (cons (cons 'right (cons typep 'nil)) 'nil)) (cons ':guard (cons (cons '= (cons (cons type->size '(left)) (cons (cons type->size '(right)) 'nil))) (cons ':returns (cons '(result boolp) (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 'x (cons (cons type->value '(left)) 'nil)) (cons (cons 'y (cons (cons type->value '(right)) 'nil)) 'nil)) (cons (cons 'bool (cons operation 'nil)) 'nil))) '(:hooks (:fix) :no-function t)))))))))))))))