Match a source type to a target type.
(match-type expr source target ctxt) → (mv yes/no obligs)
This is used when an expression with a statically calculated type (this is the source type) is passed as argument to a function with a certain argument type (this is the target type), or when a similar situation occurs (see the static semantic functions that call this function). We need to make sure that the expression, besides its inferred source type, also has the target type. The expression is passed to this ACL2 function, for the purpose of generating the proof obligations (see below).
This is trivial when source and target types are the same. When the source type is a subtype of the target type, it is also easy. In other cases, a necessary condition for the expression to have also the target type is that the source and target type have a supremum type: if they do not, they are disjoint types, and we have a ``typical'' type error.
If source and destination types have a supremum, there are three possible situations. One is that the target type is the supremum: in this case the source type is a subtype, and this case has already been described above as easy. Another case is that the source type is the supremum, in which case the target type is a subtype: in this case, we generate proof obligations saying that the expression satisfies all the predicates that define the subtypes down to the target type. The third case is that the supremum differs from both source and target: in this case, we know that the expression readily has also the supremum as type (going up the hierarchy from the source type), but to reach the target type, we need to generate proof obligations with all the predicates encountered from the supremum to the target.
The three cases above can be unified into (i) calculating the supremum and (ii) collecting the proof obligations from supremum down to target. If the supremum is the same as the target, then there is no obligation. Otherwise, there is some obligation.
We collect the subtype restriction expressions at the same time as we calculate the supremum: we do so by climbing up from the target type, and otherwise doing the same as in supremum-type (which climbs up from its first type argument). We use the same approach to ensuring termination. Note that the restriction expressions are collected in reverse: we put in the correct order, from higher to lower, and we call make-subproof-obligations to produce the obligations.
Function:
(defun match-type-aux (expr source target defined-names tops) (declare (xargs :guard (and (expressionp expr) (typep source) (typep target) (identifier-listp defined-names) (toplevel-listp tops)))) (let ((__function__ 'match-type-aux)) (declare (ignorable __function__)) (b* ((defined-names (identifier-list-fix defined-names)) ((when (subtypep source target tops)) (mv t nil)) (tsub (get-type-subset target tops)) ((when (not tsub)) (mv nil nil)) (subst (omap::update (type-subset->variable tsub) (expression-fix expr) nil)) (restr (subst-expression subst (type-subset->restriction tsub))) (name (type-defined->name target)) ((unless (member-equal name defined-names)) (mv nil nil)) ((mv yes/no restrs) (match-type-aux expr source (type-subset->supertype tsub) (remove1-equal name defined-names) tops)) ((unless yes/no) (mv nil nil))) (mv t (cons restr restrs)))))
Theorem:
(defthm booleanp-of-match-type-aux.yes/no (b* (((mv ?yes/no ?restrs) (match-type-aux expr source target defined-names tops))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm expression-listp-of-match-type-aux.restrs (b* (((mv ?yes/no ?restrs) (match-type-aux expr source target defined-names tops))) (expression-listp restrs)) :rule-classes :rewrite)
Theorem:
(defthm match-type-aux-of-expression-fix-expr (equal (match-type-aux (expression-fix expr) source target defined-names tops) (match-type-aux expr source target defined-names tops)))
Theorem:
(defthm match-type-aux-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (match-type-aux expr source target defined-names tops) (match-type-aux expr-equiv source target defined-names tops))) :rule-classes :congruence)
Theorem:
(defthm match-type-aux-of-type-fix-source (equal (match-type-aux expr (type-fix source) target defined-names tops) (match-type-aux expr source target defined-names tops)))
Theorem:
(defthm match-type-aux-type-equiv-congruence-on-source (implies (type-equiv source source-equiv) (equal (match-type-aux expr source target defined-names tops) (match-type-aux expr source-equiv target defined-names tops))) :rule-classes :congruence)
Theorem:
(defthm match-type-aux-of-type-fix-target (equal (match-type-aux expr source (type-fix target) defined-names tops) (match-type-aux expr source target defined-names tops)))
Theorem:
(defthm match-type-aux-type-equiv-congruence-on-target (implies (type-equiv target target-equiv) (equal (match-type-aux expr source target defined-names tops) (match-type-aux expr source target-equiv defined-names tops))) :rule-classes :congruence)
Theorem:
(defthm match-type-aux-of-identifier-list-fix-defined-names (equal (match-type-aux expr source target (identifier-list-fix defined-names) tops) (match-type-aux expr source target defined-names tops)))
Theorem:
(defthm match-type-aux-identifier-list-equiv-congruence-on-defined-names (implies (identifier-list-equiv defined-names defined-names-equiv) (equal (match-type-aux expr source target defined-names tops) (match-type-aux expr source target defined-names-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm match-type-aux-of-toplevel-list-fix-tops (equal (match-type-aux expr source target defined-names (toplevel-list-fix tops)) (match-type-aux expr source target defined-names tops)))
Theorem:
(defthm match-type-aux-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (match-type-aux expr source target defined-names tops) (match-type-aux expr source target defined-names tops-equiv))) :rule-classes :congruence)
Function:
(defun match-type (expr source target ctxt) (declare (xargs :guard (and (expressionp expr) (typep source) (typep target) (contextp ctxt)))) (let ((__function__ 'match-type)) (declare (ignorable __function__)) (b* (((mv yes/no restrs) (match-type-aux expr source target (get-defined-type-names (context->tops ctxt)) (context->tops ctxt))) ((unless yes/no) (mv nil nil)) (obligs (make-subproof-obligations (context->obligation-vars ctxt) (context->obligation-hyps ctxt) (rev restrs) expr))) (mv t obligs))))
Theorem:
(defthm booleanp-of-match-type.yes/no (b* (((mv ?yes/no ?obligs) (match-type expr source target ctxt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm proof-obligation-listp-of-match-type.obligs (b* (((mv ?yes/no ?obligs) (match-type expr source target ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm match-type-of-expression-fix-expr (equal (match-type (expression-fix expr) source target ctxt) (match-type expr source target ctxt)))
Theorem:
(defthm match-type-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (match-type expr source target ctxt) (match-type expr-equiv source target ctxt))) :rule-classes :congruence)
Theorem:
(defthm match-type-of-type-fix-source (equal (match-type expr (type-fix source) target ctxt) (match-type expr source target ctxt)))
Theorem:
(defthm match-type-type-equiv-congruence-on-source (implies (type-equiv source source-equiv) (equal (match-type expr source target ctxt) (match-type expr source-equiv target ctxt))) :rule-classes :congruence)
Theorem:
(defthm match-type-of-type-fix-target (equal (match-type expr source (type-fix target) ctxt) (match-type expr source target ctxt)))
Theorem:
(defthm match-type-type-equiv-congruence-on-target (implies (type-equiv target target-equiv) (equal (match-type expr source target ctxt) (match-type expr source target-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm match-type-of-context-fix-ctxt (equal (match-type expr source target (context-fix ctxt)) (match-type expr source target ctxt)))
Theorem:
(defthm match-type-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (match-type expr source target ctxt) (match-type expr source target ctxt-equiv))) :rule-classes :congruence)