		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-from-params

Generate certain pieces of information from the formal parameters of a function.

Signature
(simpadd0-gen-from-params params gin) → (mv okp args parargs arg-types arg-types-compst)
Arguments: params — Guard (c::param-declon-listp params).; gin — Guard (simpadd0-ginp gin).
Returns: okp — Type (booleanp okp).; args — Type (symbol-listp args).; parargs — Type (true-listp parargs).; arg-types — Type (true-listp arg-types).; arg-types-compst — Type (true-listp arg-types-compst).

The results of this function are used to generate theorems about function calls.

We generate the following:

A list args of symbols used as ACL2 variables that denote the C values passed as arguments to the function.
A list parargs of terms that denote the cons pairs that form the initial scope of the function. Each cons pair consists of the name of the parameter and the variable for the corresponding argument.
A list arg-types of terms that assert that each variable in args is a value of type int.
A list arg-types-compst of terms that assert that each parameter in params can be read from a computation state and its reading yields a value of type int.

These results are generated only if all the parameters have type int, which we check as we go through the parameters. This is because for now we only support theorem generation for functions whose parameters are all int; we will generalize this. The okp result says whether this is the case; if it is nil, the other results are nil too.

Definitions and Theorems

Function: simpadd0-gen-from-params

(defun simpadd0-gen-from-params (params gin)
 (declare (xargs :guard (and (c::param-declon-listp params)
                             (simpadd0-ginp gin))))
 (let ((__function__ 'simpadd0-gen-from-params))
  (declare (ignorable __function__))
  (b*
   (((when (endp params))
     (mv t nil nil nil nil))
    ((c::param-declon param) (car params))
    ((unless (c::tyspecseq-case param.tyspec :sint))
     (mv nil nil nil nil nil))
    ((unless (c::obj-declor-case param.declor :ident))
     (mv nil nil nil nil nil))
    (ident (c::obj-declor-ident->get param.declor))
    (par (c::ident->name ident))
    (arg (intern-in-package-of-symbol
              par (simpadd0-gin->const-new gin)))
    (pararg (cons 'cons
                  (cons (cons 'c::ident (cons par 'nil))
                        (cons arg 'nil))))
    (arg-type
     (cons
       'and
       (cons (cons 'c::valuep (cons arg 'nil))
             (cons (cons 'equal
                         (cons (cons 'c::value-kind (cons arg 'nil))
                               '(:sint)))
                   'nil))))
    (arg-type-compst
     (cons
      'b*
      (cons
       (cons
        (cons
         'var
         (cons
          (cons
               'mv-nth
               (cons '1
                     (cons (cons 'c$::ldm-ident
                                 (cons (cons 'ident (cons par 'nil))
                                       'nil))
                           'nil)))
          'nil))
        '((objdes (c::objdesign-of-var var compst))
          (val (c::read-object objdes compst))))
       '((and objdes (c::valuep val)
              (c::value-case val :sint))))))
    ((mv okp more-args more-parargs
         more-arg-types more-arg-types-compst)
     (simpadd0-gen-from-params (cdr params)
                               gin))
    ((unless okp) (mv nil nil nil nil nil)))
   (mv t (cons arg more-args)
       (cons pararg more-parargs)
       (cons arg-type more-arg-types)
       (cons arg-type-compst
             more-arg-types-compst)))))

Theorem: booleanp-of-simpadd0-gen-from-params.okp

(defthm booleanp-of-simpadd0-gen-from-params.okp
  (b* (((mv ?okp acl2::?args
            ?parargs ?arg-types ?arg-types-compst)
        (simpadd0-gen-from-params params gin)))
    (booleanp okp))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-simpadd0-gen-from-params.args

(defthm symbol-listp-of-simpadd0-gen-from-params.args
  (b* (((mv ?okp acl2::?args
            ?parargs ?arg-types ?arg-types-compst)
        (simpadd0-gen-from-params params gin)))
    (symbol-listp args))
  :rule-classes :rewrite)

Theorem: true-listp-of-simpadd0-gen-from-params.parargs

(defthm true-listp-of-simpadd0-gen-from-params.parargs
  (b* (((mv ?okp acl2::?args
            ?parargs ?arg-types ?arg-types-compst)
        (simpadd0-gen-from-params params gin)))
    (true-listp parargs))
  :rule-classes :rewrite)

Theorem: true-listp-of-simpadd0-gen-from-params.arg-types

(defthm true-listp-of-simpadd0-gen-from-params.arg-types
  (b* (((mv ?okp acl2::?args
            ?parargs ?arg-types ?arg-types-compst)
        (simpadd0-gen-from-params params gin)))
    (true-listp arg-types))
  :rule-classes :rewrite)

Theorem: true-listp-of-simpadd0-gen-from-params.arg-types-compst

(defthm true-listp-of-simpadd0-gen-from-params.arg-types-compst
  (b* (((mv ?okp acl2::?args
            ?parargs ?arg-types ?arg-types-compst)
        (simpadd0-gen-from-params params gin)))
    (true-listp arg-types-compst))
  :rule-classes :rewrite)

Theorem: len-of-simpadd0-gen-from-params.parargs

(defthm len-of-simpadd0-gen-from-params.parargs
  (b* (((mv ?okp acl2::?args
            ?parargs ?arg-types ?arg-types-compst)
        (simpadd0-gen-from-params params gin)))
    (equal (len parargs) (len args))))

Theorem: len-of-simpadd0-gen-from-params.arg-types

(defthm len-of-simpadd0-gen-from-params.arg-types
  (b* (((mv ?okp acl2::?args
            ?parargs ?arg-types ?arg-types-compst)
        (simpadd0-gen-from-params params gin)))
    (equal (len arg-types) (len args))))

Theorem: len-of-simpadd0-gen-from-params.arg-types-compst

(defthm len-of-simpadd0-gen-from-params.arg-types-compst
  (b* (((mv ?okp acl2::?args
            ?parargs ?arg-types ?arg-types-compst)
        (simpadd0-gen-from-params params gin)))
    (equal (len arg-types-compst)
           (len args))))