		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 — A term.; 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 term parargs that is a nest of omap::update that denotes the initial scope of the function. Each omap::update call adds the name of the parameter as key and the variable for the corresponding argument as value.
A list arg-types of terms that assert that each variable in args is a value of the appropriate type.
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 the appropriate type.

These results are generated only if all the parameters have certain types (see simpadd0-tyspecseq-to-type), which we check as we go through the parameters. 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))
    ((mv okp type)
     (simpadd0-tyspecseq-to-type param.tyspec))
    ((unless okp) (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)))
    (arg-type
     (cons
      'and
      (cons
          (cons 'c::valuep (cons arg 'nil))
          (cons (cons 'equal
                      (cons (cons 'c::type-of-value (cons arg 'nil))
                            (cons (cons 'quote (cons type 'nil))
                                  'nil)))
                'nil))))
    (arg-type-compst
     (cons
      'b*
      (cons
       (cons
        (cons
         'var
         (cons
          (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-ident
                                 (cons (cons 'ident (cons par 'nil))
                                       'nil))
                           'nil)))
          'nil))
        '((objdes (c::objdesign-of-var var compst))
          (val (c::read-object objdes compst))))
       (cons
        (cons
         'and
         (cons
          'objdes
          (cons
              '(c::valuep val)
              (cons (cons 'equal
                          (cons '(c::type-of-value val)
                                (cons (cons 'quote (cons type 'nil))
                                      'nil)))
                    'nil))))
        'nil))))
    ((mv okp more-args parargs
         more-arg-types more-arg-types-compst)
     (simpadd0-gen-from-params (cdr params)
                               gin))
    ((unless okp) (mv nil nil nil nil nil))
    (parargs (cons 'omap::update
                   (cons (cons 'c::ident (cons par 'nil))
                         (cons arg (cons parargs 'nil))))))
   (mv t (cons arg more-args)
       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.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.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))))