		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Gen-from-params

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

Signature
(gen-from-params params gin) → (mv okp args parargs arg-types arg-types-compst vartys)
Arguments: params — Guard (c::param-declon-listp params).; gin — Guard (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).; vartys — Type (c::ident-type-mapp vartys).

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 calls 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.
A variable-type map corresponding to the parameters in the obvious way.

These results are generated only if all the parameters have certain types (see 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: gen-from-params

(defun gen-from-params (params gin)
 (declare (xargs :guard (and (c::param-declon-listp params)
                             (ginp gin))))
 (let ((__function__ 'gen-from-params))
  (declare (ignorable __function__))
  (b*
   (((when (endp params))
     (mv t nil nil nil nil nil))
    ((c::param-declon param) (car params))
    ((mv okp type)
     (tyspecseq-to-type param.tyspec))
    ((unless okp)
     (mv nil nil nil nil nil nil))
    ((unless (c::obj-declor-case param.declor :ident))
     (mv nil 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 (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 'c::compustate-has-var-with-type-p
               (cons (cons 'quote (cons ident 'nil))
                     (cons (cons 'quote (cons type 'nil))
                           '(compst)))))
    ((mv okp more-args parargs more-arg-types
         more-arg-types-compst more-vartys)
     (gen-from-params (cdr params) gin))
    ((unless okp)
     (mv nil nil nil nil nil nil))
    (parargs (cons 'omap::update
                   (cons (cons 'c::ident (cons par 'nil))
                         (cons arg (cons parargs 'nil)))))
    (vartys (omap::update ident type more-vartys)))
   (mv t (cons arg more-args)
       parargs (cons arg-type more-arg-types)
       (cons arg-type-compst more-arg-types-compst)
       vartys))))

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

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

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

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

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

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

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

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

Theorem: ident-type-mapp-of-gen-from-params.vartys

(defthm ident-type-mapp-of-gen-from-params.vartys
  (b* (((mv ?okp acl2::?args ?parargs
            ?arg-types ?arg-types-compst ?vartys)
        (gen-from-params params gin)))
    (c::ident-type-mapp vartys))
  :rule-classes :rewrite)

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

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

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

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