		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-loop-call

Check if a term may represent a C loop.

Signature
(atc-check-loop-call term var-term-alist prec-fns) → (mv yes/no fn args in-types affect loop limit)
Arguments: term — Guard (pseudo-termp term).; var-term-alist — Guard (symbol-pseudoterm-alistp var-term-alist).; prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; args — Type (pseudo-term-listp args).; in-types — Type (type-listp in-types).; affect — Type (symbol-listp affect).; loop — Type (stmtp loop).; limit — Type (pseudo-termp limit).

We check whether this is a call of a function that has been previously processed (i.e. it is in the prec-fns alist) and is recursive (indicated by the presence of the loop statement in its information). If the checks succeed, we return the function symbol, its arguments, the argument types, the variables affected by the loop, the associated loop statement, and the limit sufficient to execute the function call.

The limit retrieved from the function table refers to the formal parameters. We must instantiate it to the actual parameters in order to obtain an appropriate limit for the call, but we also need to substitute all the bindings in order to obtain the real arguments of the call from the point of view of the top level of where this call term occurs.

Definitions and Theorems

Function: atc-check-loop-call

(defun atc-check-loop-call (term var-term-alist prec-fns)
  (declare
       (xargs :guard (and (pseudo-termp term)
                          (symbol-pseudoterm-alistp var-term-alist)
                          (atc-symbol-fninfo-alistp prec-fns))))
  (let ((__function__ 'atc-check-loop-call))
    (declare (ignorable __function__))
    (b* (((acl2::fun (no))
          (mv nil nil nil nil nil (irr-stmt) nil))
         ((unless (pseudo-term-case term :fncall))
          (no))
         ((pseudo-term-fncall term) term)
         (fn+info (assoc-eq term.fn
                            (atc-symbol-fninfo-alist-fix prec-fns)))
         ((unless (consp fn+info)) (no))
         (info (cdr fn+info))
         (loop (atc-fn-info->loop? info))
         ((unless (stmtp loop)) (no))
         (in-types (atc-fn-info->in-types info))
         (affect (atc-fn-info->affect info))
         (limit (atc-fn-info->limit info))
         (limit (fty-fsublis-var var-term-alist limit)))
      (mv t term.fn
          term.args in-types affect loop limit))))

Theorem: booleanp-of-atc-check-loop-call.yes/no

(defthm booleanp-of-atc-check-loop-call.yes/no
  (b* (((mv ?yes/no ?fn acl2::?args ?in-types
            ?affect common-lisp::?loop ?limit)
        (atc-check-loop-call term var-term-alist prec-fns)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-loop-call.fn

(defthm symbolp-of-atc-check-loop-call.fn
  (b* (((mv ?yes/no ?fn acl2::?args ?in-types
            ?affect common-lisp::?loop ?limit)
        (atc-check-loop-call term var-term-alist prec-fns)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-atc-check-loop-call.args

(defthm pseudo-term-listp-of-atc-check-loop-call.args
  (b* (((mv ?yes/no ?fn acl2::?args ?in-types
            ?affect common-lisp::?loop ?limit)
        (atc-check-loop-call term var-term-alist prec-fns)))
    (pseudo-term-listp args))
  :rule-classes :rewrite)

Theorem: type-listp-of-atc-check-loop-call.in-types

(defthm type-listp-of-atc-check-loop-call.in-types
  (b* (((mv ?yes/no ?fn acl2::?args ?in-types
            ?affect common-lisp::?loop ?limit)
        (atc-check-loop-call term var-term-alist prec-fns)))
    (type-listp in-types))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-check-loop-call.affect

(defthm symbol-listp-of-atc-check-loop-call.affect
  (b* (((mv ?yes/no ?fn acl2::?args ?in-types
            ?affect common-lisp::?loop ?limit)
        (atc-check-loop-call term var-term-alist prec-fns)))
    (symbol-listp affect))
  :rule-classes :rewrite)

Theorem: stmtp-of-atc-check-loop-call.loop

(defthm stmtp-of-atc-check-loop-call.loop
  (b* (((mv ?yes/no ?fn acl2::?args ?in-types
            ?affect common-lisp::?loop ?limit)
        (atc-check-loop-call term var-term-alist prec-fns)))
    (stmtp loop))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-loop-call.limit

(defthm pseudo-termp-of-atc-check-loop-call.limit
  (b* (((mv ?yes/no ?fn acl2::?args ?in-types
            ?affect common-lisp::?loop ?limit)
        (atc-check-loop-call term var-term-alist prec-fns)))
    (pseudo-termp limit))
  :rule-classes :rewrite)