		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Match-to-target

Match the type(s) of an expression to some optional target type(s).

Signature
(match-to-target expr source target ctxt) → result
Arguments: expr — Guard (expressionp expr).; source — Guard (type-listp source).; target — Guard (type-listp target).; ctxt — Guard (contextp ctxt).
Returns: result — Type (type-resultp result).

When we check the static semantics constraints for an expression, we normally calculate a (list of) type(s) for the expression (one if the expression is single-valued, more if multi-valued), and then we may or may not have a (list of) target type(s) that the expression must match. This ACL2 function performs this matching.

The target input is nil if there are no required target types. In this case, the matching succeeds and we return the type(s) of the expression.

Otherwise, we ensure that source and target types are the same in number and match element-wise. This may generate some proof obligations. If these checks succeed, we return the target type(s).

Definitions and Theorems

Function: match-to-target

(defun match-to-target (expr source target ctxt)
 (declare (xargs :guard (and (expressionp expr)
                             (type-listp source)
                             (type-listp target)
                             (contextp ctxt))))
 (let ((__function__ 'match-to-target))
  (declare (ignorable __function__))
  (if (atom target)
      (make-type-result-ok :types source
                           :obligations nil)
   (if (/= (len target) (len source))
       (type-result-err (list :type-mismatch-in-number
                              (type-list-fix source)
                              (type-list-fix target)))
    (b* ((exprs (decompose-expression expr (len target)))
         ((mv okp obligs)
          (match-type-list exprs source target ctxt)))
      (if okp (make-type-result-ok :types target
                                   :obligations obligs)
        (type-result-err (list :type-mismatch (type-list-fix source)
                               (type-list-fix target)))))))))

Theorem: type-resultp-of-match-to-target

(defthm type-resultp-of-match-to-target
  (b* ((result (match-to-target expr source target ctxt)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: match-to-target-of-expression-fix-expr

(defthm match-to-target-of-expression-fix-expr
  (equal (match-to-target (expression-fix expr)
                          source target ctxt)
         (match-to-target expr source target ctxt)))

Theorem: match-to-target-expression-equiv-congruence-on-expr

(defthm match-to-target-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (match-to-target expr source target ctxt)
                  (match-to-target expr-equiv source target ctxt)))
  :rule-classes :congruence)

Theorem: match-to-target-of-type-list-fix-source

(defthm match-to-target-of-type-list-fix-source
  (equal (match-to-target expr (type-list-fix source)
                          target ctxt)
         (match-to-target expr source target ctxt)))

Theorem: match-to-target-type-list-equiv-congruence-on-source

(defthm match-to-target-type-list-equiv-congruence-on-source
  (implies (type-list-equiv source source-equiv)
           (equal (match-to-target expr source target ctxt)
                  (match-to-target expr source-equiv target ctxt)))
  :rule-classes :congruence)

Theorem: match-to-target-of-type-list-fix-target

(defthm match-to-target-of-type-list-fix-target
  (equal (match-to-target expr source (type-list-fix target)
                          ctxt)
         (match-to-target expr source target ctxt)))

Theorem: match-to-target-type-list-equiv-congruence-on-target

(defthm match-to-target-type-list-equiv-congruence-on-target
  (implies (type-list-equiv target target-equiv)
           (equal (match-to-target expr source target ctxt)
                  (match-to-target expr source target-equiv ctxt)))
  :rule-classes :congruence)

Theorem: match-to-target-of-context-fix-ctxt

(defthm match-to-target-of-context-fix-ctxt
  (equal (match-to-target expr source target (context-fix ctxt))
         (match-to-target expr source target ctxt)))

Theorem: match-to-target-context-equiv-congruence-on-ctxt

(defthm match-to-target-context-equiv-congruence-on-ctxt
  (implies (context-equiv ctxt ctxt-equiv)
           (equal (match-to-target expr source target ctxt)
                  (match-to-target expr source target ctxt-equiv)))
  :rule-classes :congruence)