Reasoning trick. Alias for the type of the token returned by vl-match-some-token.
(vl-type-of-matched-token types tokens) → *
We added this when we disabled the functions vl-is-some-token? and vl-match-some-token to address the problem of reasoning about which kind of token was matched. We could prove, for instance, that
(implies (vl-is-some-token? types tokens) (member (mv-nth 1 (vl-match-some-token types)) types))
But it was difficult to get ACL2 to actually make use of this rule, because
the
Instead, we use this new alias so that we can rewrite
(equal (mv-nth 1 (vl-match-some-token types)) (vl-type-of-matched-tokens types tokens))
Function:
(defun vl-type-of-matched-token (types tokens) (declare (xargs :guard (and (true-listp types) (vl-tokenlist-p tokens)))) (let ((__function__ 'vl-type-of-matched-token)) (declare (ignorable __function__)) (b* ((tokens (vl-tokenlist-fix tokens))) (if (and (consp tokens) (member-eq (vl-token->type (car tokens)) types)) (vl-token->type (car tokens)) nil))))
Theorem:
(defthm vl-token->type-of-vl-match-some-token (equal (vl-token->type (mv-nth 1 (vl-match-some-token types))) (vl-type-of-matched-token types (vl-tokstream->tokens))))
Theorem:
(defthm vl-type-of-matched-token-when-atom-of-types (implies (atom types) (equal (vl-type-of-matched-token types tokens) nil)))
Theorem:
(defthm vl-type-of-matched-token-when-atom-of-tokens (implies (atom tokens) (equal (vl-type-of-matched-token types tokens) nil)))
Theorem:
(defthm vl-type-of-matched-token-of-vl-tokenlist-fix (equal (vl-type-of-matched-token types (vl-tokenlist-fix tokens)) (vl-type-of-matched-token types tokens)))