		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-component-expression

Check if a multi-valued component expression is statically well-formed.

Signature
(check-component-expression multi multi-result index) → result
Arguments: multi — Guard (expressionp multi).; multi-result — Guard (type-resultp multi-result).; index — Guard (natp index).
Returns: result — Type (type-resultp result).

The expression must be a multi-valued one, i.e. have at least two types. The index must be below the number of types. The type corresponding to the index is the type of the expression.

Definitions and Theorems

Function: check-component-expression

(defun check-component-expression (multi multi-result index)
 (declare (xargs :guard (and (expressionp multi)
                             (type-resultp multi-result)
                             (natp index))))
 (let ((__function__ 'check-component-expression))
  (declare (ignorable __function__))
  (type-result-case
   multi-result
   :err (type-result-err multi-result.info)
   :ok
   (cond
    ((< (len multi-result.types) 2)
     (type-result-err
      (list
           :non-multi-component-expression (expression-fix multi))))
    ((>= (nfix index)
         (len multi-result.types))
     (type-result-err (list :multi-component-out-of-range
                            (expression-fix multi)
                            (nfix index))))
    (t (make-type-result-ok
            :types (list (nth (nfix index) multi-result.types))
            :obligations multi-result.obligations))))))

Theorem: type-resultp-of-check-component-expression

(defthm type-resultp-of-check-component-expression
  (b*
    ((result (check-component-expression multi multi-result index)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: check-component-expression-of-expression-fix-multi

(defthm check-component-expression-of-expression-fix-multi
  (equal (check-component-expression (expression-fix multi)
                                     multi-result index)
         (check-component-expression multi multi-result index)))

Theorem: check-component-expression-expression-equiv-congruence-on-multi

(defthm
    check-component-expression-expression-equiv-congruence-on-multi
 (implies
  (expression-equiv multi multi-equiv)
  (equal
       (check-component-expression multi multi-result index)
       (check-component-expression multi-equiv multi-result index)))
 :rule-classes :congruence)

Theorem: check-component-expression-of-type-result-fix-multi-result

(defthm check-component-expression-of-type-result-fix-multi-result
 (equal
    (check-component-expression multi (type-result-fix multi-result)
                                index)
    (check-component-expression multi multi-result index)))

Theorem: check-component-expression-type-result-equiv-congruence-on-multi-result

(defthm
 check-component-expression-type-result-equiv-congruence-on-multi-result
 (implies
  (type-result-equiv multi-result multi-result-equiv)
  (equal
       (check-component-expression multi multi-result index)
       (check-component-expression multi multi-result-equiv index)))
 :rule-classes :congruence)

Theorem: check-component-expression-of-nfix-index

(defthm check-component-expression-of-nfix-index
 (equal (check-component-expression multi multi-result (nfix index))
        (check-component-expression multi multi-result index)))

Theorem: check-component-expression-nat-equiv-congruence-on-index

(defthm check-component-expression-nat-equiv-congruence-on-index
 (implies
  (nat-equiv index index-equiv)
  (equal
       (check-component-expression multi multi-result index)
       (check-component-expression multi multi-result index-equiv)))
 :rule-classes :congruence)