Match a list of source types to a list of target types.
(match-type-list exprs sources targets ctxt) → (mv yes/no obligs)
This lifts match-type to lists. The number of expressions and source types are the same, because the source types are the ones of the expressions. The number of target types must also be the same for this function to succeed. We accumulate the proof obligations and return all of them.
Function:
(defun match-type-list (exprs sources targets ctxt) (declare (xargs :guard (and (expression-listp exprs) (type-listp sources) (type-listp targets) (contextp ctxt)))) (declare (xargs :guard (= (len exprs) (len sources)))) (let ((__function__ 'match-type-list)) (declare (ignorable __function__)) (b* (((when (endp exprs)) (mv (endp targets) nil)) ((when (endp targets)) (mv nil nil)) ((mv okp obligs) (match-type (car exprs) (car sources) (car targets) ctxt)) ((unless okp) (mv nil nil)) ((mv okp more-obligs) (match-type-list (cdr exprs) (cdr sources) (cdr targets) ctxt)) ((unless okp) (mv nil nil))) (mv t (append obligs more-obligs)))))
Theorem:
(defthm booleanp-of-match-type-list.yes/no (b* (((mv ?yes/no ?obligs) (match-type-list exprs sources targets ctxt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm proof-obligation-listp-of-match-type-list.obligs (b* (((mv ?yes/no ?obligs) (match-type-list exprs sources targets ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm same-len-target-exprs-when-match-type-list (implies (mv-nth 0 (match-type-list exprs sources targets ctxt)) (equal (len targets) (len exprs))) :rule-classes :forward-chaining)
Theorem:
(defthm match-type-list-of-expression-list-fix-exprs (equal (match-type-list (expression-list-fix exprs) sources targets ctxt) (match-type-list exprs sources targets ctxt)))
Theorem:
(defthm match-type-list-expression-list-equiv-congruence-on-exprs (implies (expression-list-equiv exprs exprs-equiv) (equal (match-type-list exprs sources targets ctxt) (match-type-list exprs-equiv sources targets ctxt))) :rule-classes :congruence)
Theorem:
(defthm match-type-list-of-type-list-fix-sources (equal (match-type-list exprs (type-list-fix sources) targets ctxt) (match-type-list exprs sources targets ctxt)))
Theorem:
(defthm match-type-list-type-list-equiv-congruence-on-sources (implies (type-list-equiv sources sources-equiv) (equal (match-type-list exprs sources targets ctxt) (match-type-list exprs sources-equiv targets ctxt))) :rule-classes :congruence)
Theorem:
(defthm match-type-list-of-type-list-fix-targets (equal (match-type-list exprs sources (type-list-fix targets) ctxt) (match-type-list exprs sources targets ctxt)))
Theorem:
(defthm match-type-list-type-list-equiv-congruence-on-targets (implies (type-list-equiv targets targets-equiv) (equal (match-type-list exprs sources targets ctxt) (match-type-list exprs sources targets-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm match-type-list-of-context-fix-ctxt (equal (match-type-list exprs sources targets (context-fix ctxt)) (match-type-list exprs sources targets ctxt)))
Theorem:
(defthm match-type-list-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (match-type-list exprs sources targets ctxt) (match-type-list exprs sources targets ctxt-equiv))) :rule-classes :congruence)