		Search-engine friendly clone of the ACL2 documentation.

Input-checking

Check-input-item

Check an input item.

Signature
(check-input-item initem intitle params env) → new-params
Arguments: initem — Guard (input-itemp initem).; intitle — Guard (input-titlep intitle).; params — Guard (funparam-listp params).; env — Guard (senvp env).
Returns: new-params — Type (funparam-list-resultp new-params).

We ensure that the type of the input expression matches the input type.

The params input to this ACL2 function consists of (the information in) all the input items that precede this input item in the input file. We use them to check that the name of this item is different from all the previous ones, and we extend the list of function parameters with the information from this input item; we use the current input title to determine the variable or constant sort. This way, as we go through all the items of the input file, we ensure that they have distinct names and we create a list of function parameters corresponding to them. The reason for this list of function parameters is that the items in an input file correspond to the inputs of the main function of the Leo program, and so in this way we can check the consistency of the input file with the main function.

Definitions and Theorems

Function: check-input-item

(defun check-input-item (initem intitle params env)
  (declare (xargs :guard (and (input-itemp initem)
                              (input-titlep intitle)
                              (funparam-listp params)
                              (senvp env))))
  (let ((__function__ 'check-input-item))
    (declare (ignorable __function__))
    (b* (((input-item initem) initem)
         ((okf &)
          (check-input-type initem.type env))
         ((okf type)
          (check-input-expression initem.value env))
         (intype (input-type->get initem.type))
         ((unless (equal type intype))
          (reserrf (list :input-item-mistype
                         :type initem.type
                         :expression type)))
         ((when (member-equal initem.name
                              (funparam-list->name-list params)))
          (reserrf (list :duplicate-input-name initem.name))))
      (cons (make-funparam :name initem.name
                           :type intype
                           :sort (input-title->sort intitle))
            (funparam-list-fix params)))))

Theorem: funparam-list-resultp-of-check-input-item

(defthm funparam-list-resultp-of-check-input-item
  (b* ((new-params (check-input-item initem intitle params env)))
    (funparam-list-resultp new-params))
  :rule-classes :rewrite)

Theorem: check-input-item-of-input-item-fix-initem

(defthm check-input-item-of-input-item-fix-initem
  (equal (check-input-item (input-item-fix initem)
                           intitle params env)
         (check-input-item initem intitle params env)))

Theorem: check-input-item-input-item-equiv-congruence-on-initem

(defthm check-input-item-input-item-equiv-congruence-on-initem
  (implies
       (input-item-equiv initem initem-equiv)
       (equal (check-input-item initem intitle params env)
              (check-input-item initem-equiv intitle params env)))
  :rule-classes :congruence)

Theorem: check-input-item-of-input-title-fix-intitle

(defthm check-input-item-of-input-title-fix-intitle
  (equal (check-input-item initem (input-title-fix intitle)
                           params env)
         (check-input-item initem intitle params env)))

Theorem: check-input-item-input-title-equiv-congruence-on-intitle

(defthm check-input-item-input-title-equiv-congruence-on-intitle
  (implies
       (input-title-equiv intitle intitle-equiv)
       (equal (check-input-item initem intitle params env)
              (check-input-item initem intitle-equiv params env)))
  :rule-classes :congruence)

Theorem: check-input-item-of-funparam-list-fix-params

(defthm check-input-item-of-funparam-list-fix-params
  (equal (check-input-item initem
                           intitle (funparam-list-fix params)
                           env)
         (check-input-item initem intitle params env)))

Theorem: check-input-item-funparam-list-equiv-congruence-on-params

(defthm check-input-item-funparam-list-equiv-congruence-on-params
  (implies
       (funparam-list-equiv params params-equiv)
       (equal (check-input-item initem intitle params env)
              (check-input-item initem intitle params-equiv env)))
  :rule-classes :congruence)

Theorem: check-input-item-of-senv-fix-env

(defthm check-input-item-of-senv-fix-env
  (equal (check-input-item initem intitle params (senv-fix env))
         (check-input-item initem intitle params env)))

Theorem: check-input-item-senv-equiv-congruence-on-env

(defthm check-input-item-senv-equiv-congruence-on-env
  (implies
       (senv-equiv env env-equiv)
       (equal (check-input-item initem intitle params env)
              (check-input-item initem intitle params env-equiv)))
  :rule-classes :congruence)