		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-check-guard-conjunct

C type and argument derived from a guard conjunct, if any.

Signature
(atc-check-guard-conjunct conjunct prec-tags prec-objs) → (mv type defobj-pred arg)
Arguments: conjunct — Guard (pseudo-termp conjunct).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).
Returns: type — Type (type-optionp type).; defobj-pred — Type (symbolp defobj-pred).; arg — Type (symbolp 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 (recognizer var) or (star (recognizer var)), where recognizer is a recognizer of a C type and var is a variable. If the recognizer is a known one for integer array types, the star wrapper is disallowed, and the integer array type is readily determined. If the recognizer is a known one for integer types, the star wrapper may be present or not, and distinguishes between the integer type and the pointer type to the integer type. Otherwise, there are two possibilities. One is that the recognizer is the one of a defstruct, of the form struct-<tag>-p: in this case, the type is the structure type or a pointer type to it, depending on the absence or presence of the star wrapper. The other possibility is that the recognizer is the one of a defobject, of the form object-<name>-p: in this case, the star wrapper is disallowed, and the type is the one of the object. In this last case, we also return the object-<name>-p name; in all other cases, this result is nil.

If the recognizer does not have any of the above forms, we return nil as all results. If the argument is not a variable, we also return nil as all results.

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.

Definitions and Theorems

Function: atc-check-guard-conjunct

(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: type-optionp-of-atc-check-guard-conjunct.type

(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: symbolp-of-atc-check-guard-conjunct.defobj-pred

(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: symbolp-of-atc-check-guard-conjunct.arg

(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)