C type and argument derived from a guard conjunct, if any.
(atc-check-guard-conjunct conjunct prec-tags prec-objs) → (mv type defobj-pred arg)
This is used to determine the types of the formal parameters of functions from the conjuncts used in the guard, as explained in the user documentation.
The conjunct must have the form
If the recognizer does not have any of the above forms,
we return
As explained in the user documentation, we also allow the conjuncts to be wrapped with mbt. To handle these, we preliminarily conditionally unwrap the conjuncts.
Function:
(defun atc-check-guard-conjunct (conjunct prec-tags prec-objs) (declare (xargs :guard (and (pseudo-termp conjunct) (atc-string-taginfo-alistp prec-tags) (atc-string-objinfo-alistp prec-objs)))) (let ((__function__ 'atc-check-guard-conjunct)) (declare (ignorable __function__)) (b* ((conjunct (b* (((mv mbtp arg) (check-mbt-call conjunct)) ((when mbtp) arg)) conjunct)) ((when (or (variablep conjunct) (fquotep conjunct) (flambda-applicationp conjunct))) (mv nil nil nil)) (fn (ffn-symb conjunct)) (arg (fargn conjunct 1)) ((mv okp pointerp recog arg) (if (eq fn 'star) (if (or (variablep arg) (fquotep arg) (flambda-applicationp arg)) (mv nil nil nil nil) (mv t t (ffn-symb arg) (fargn arg 1))) (mv t nil fn arg))) ((when (not okp)) (mv nil nil nil)) ((unless (symbolp arg)) (mv nil nil nil)) ((mv type defobj-pred) (b* (((when (eq recog 'scharp)) (mv (type-schar) nil)) ((when (eq recog 'ucharp)) (mv (type-uchar) nil)) ((when (eq recog 'sshortp)) (mv (type-sshort) nil)) ((when (eq recog 'ushortp)) (mv (type-ushort) nil)) ((when (eq recog 'sintp)) (mv (type-sint) nil)) ((when (eq recog 'uintp)) (mv (type-uint) nil)) ((when (eq recog 'slongp)) (mv (type-slong) nil)) ((when (eq recog 'ulongp)) (mv (type-ulong) nil)) ((when (eq recog 'sllongp)) (mv (type-sllong) nil)) ((when (eq recog 'ullongp)) (mv (type-ullong) nil)) ((when (eq recog 'schar-arrayp)) (mv (type-array (type-schar) nil) nil)) ((when (eq recog 'uchar-arrayp)) (mv (type-array (type-uchar) nil) nil)) ((when (eq recog 'sshort-arrayp)) (mv (type-array (type-sshort) nil) nil)) ((when (eq recog 'ushort-arrayp)) (mv (type-array (type-ushort) nil) nil)) ((when (eq recog 'sint-arrayp)) (mv (type-array (type-sint) nil) nil)) ((when (eq recog 'uint-arrayp)) (mv (type-array (type-uint) nil) nil)) ((when (eq recog 'slong-arrayp)) (mv (type-array (type-slong) nil) nil)) ((when (eq recog 'ulong-arrayp)) (mv (type-array (type-ulong) nil) nil)) ((when (eq recog 'sllong-arrayp)) (mv (type-array (type-sllong) nil) nil)) ((when (eq recog 'ullong-arrayp)) (mv (type-array (type-ullong) nil) nil)) ((mv okp struct/object tag/name p) (atc-check-symbol-3part recog)) ((unless (and okp (equal (symbol-name p) "P"))) (mv nil nil)) ((when (equal (symbol-name struct/object) "STRUCT")) (b* ((tag (symbol-name tag/name)) (info (cdr (assoc-equal tag prec-tags))) ((unless info) (mv nil nil)) ((unless (atc-tag-infop info)) (raise "Internal error: malformed ATC-TAG-INFO ~x0." info) (mv nil nil)) (info (atc-tag-info->defstruct info)) ((unless (eq recog (defstruct-info->recognizer info))) (mv nil nil)) ((when (and (defstruct-info->flexiblep info) (not pointerp))) (mv nil nil))) (mv (type-struct (defstruct-info->tag info)) nil))) ((when (equal (symbol-name struct/object) "OBJECT")) (b* ((name (symbol-name tag/name)) (info (cdr (assoc-equal name prec-objs))) ((unless info) (mv nil nil)) ((unless (atc-obj-infop info)) (raise "Internal error: malformed ATC-OBJ-INFO ~x0." info) (mv nil nil)) (info (atc-obj-info->defobject info)) ((unless (eq recog (defobject-info->recognizer info))) (mv nil nil))) (mv (defobject-info->type info) (defobject-info->recognizer info))))) (mv nil nil))) ((unless type) (mv nil nil nil)) ((when (and pointerp (type-case type :array))) (mv nil nil nil)) (type (if pointerp (type-pointer type) type))) (mv type defobj-pred arg))))
Theorem:
(defthm type-optionp-of-atc-check-guard-conjunct.type (b* (((mv ?type ?defobj-pred ?arg) (atc-check-guard-conjunct conjunct prec-tags prec-objs))) (type-optionp type)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-check-guard-conjunct.defobj-pred (b* (((mv ?type ?defobj-pred ?arg) (atc-check-guard-conjunct conjunct prec-tags prec-objs))) (symbolp defobj-pred)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-check-guard-conjunct.arg (b* (((mv ?type ?defobj-pred ?arg) (atc-check-guard-conjunct conjunct prec-tags prec-objs))) (symbolp arg)) :rule-classes :rewrite)