Grammar-parser-tree-matching
Tree matching theorems for the parser of ABNF grammars.
If parsing succeeds,
the returned tree(s) match(es) the syntactic entities being parsed.
For instance, if parse-alpha succeeds,
the returned tree matches ALPHA.
The tree matching proof of each parsing function uses, as rewrite rules,
the tree matching theorems of the parsing functions called by
the parsing function whose theorem is being proved.
The tree matching theorems use hypotheses of the form
(equal element ...) or (equal repetition ...),
where element and repetition are variables
that appear in the theorems' conclusions
as the second arguments of
tree-match-element-p and tree-list-match-repetition-p,
and where ... are constant terms
that evaluate to certain elements and repetitions.
The reason for not substituting these hypotheses in the conclusions
is so that these theorems can be used as rewrite rules
when proving the tree matching theorems for the calling parsing functions.
Consider, for example,
how the tree matching theorem tree-match-of-parse-alpha
is used in the proof of tree-match-of-parse-alpha/digit/dash:
the goal
(tree-match-element-p
... (!_ (/_ *alpha*) (/_ *digit*) (/_ "-")) ...)
simplifies (via the executable counterpart rules) to
(tree-match-element-p
... '(:group (((:repetition (:repeat 1 (:finite 1))
(:rulename (:rulename "alpha"))))
((:repetition (:repeat 1 (:finite 1))
(:rulename (:rulename "digit"))))
((:repetition (:repeat 1 (:finite 1))
(:char-val (:insensitive nil "-")))))) ...)
and then reduces to, among others, the subgoal
(tree-match-element-p
... '(:rulename (:rulename "alpha")) ...)
which would not match
(tree-match-element-p ... (element-rulename *alpha*) ...)
if that were the conclusion of tree-match-of-parse-alpha.
We could substitute the fully evaluated quoted constants
into the conclusions of the tree matching theorems
(e.g. '(:rulename (:rulename "alpha"))
in tree-match-of-parse-alpha),
but this would be slightly more inconvenient and less readable,
especially when the elements are not simple rule elements.
In the tree matching theorems for the mutually recursive parsing functions
(i.e. parse-alternation, parse-concatenation, etc.),
the extra variables element and repetition
in the (equal element ...) and (equal repetition ...) hypotheses
would lead to an unprovable induction structure
because the variables element and repetition
are the same in the induction hypotheses and conclusions,
but are equated to different constant terms.
Thus, we first prove by induction versions of the theorems
with the equalities substituted in the conclusions
(i.e., the tree-match-...-lemma and tree-list-match-...-lemma
theorems),
and then we prove the desired theorems, with the equality hypotheses.
The latter are used as rewrite rules in the tree matching proofs
for the parsing functions that call
the mutually recursive parsing functions.
The tree matching proofs also use the definitions of
tree->string,
tree-match-element-p,
tree-list-match-repetition-p,
tree-list-match-element-p,
and numrep-match-repeat-range-p.
We enable these definitions just before the tree matching theorems
and we disable them just after.
Since in some theorems
tree-match-element-p does not get expanded
in places where it should
(presumably due to ACL2's heuristics for expanding recursive functions),
we use explicit :expand hints in those theorems;
the potential looping due to the mutually recursive grammar rules
(for alternation, concatenation, etc.) does not happen,
presumably thanks to the firing of the tree matching rewrite rules
as soon as they apply.
There is no direct use of the definitions of
tree-list-list-match-alternation-p and
tree-list-list-match-concatenation-p
because the alternations and concatenations in these theorems
always have an explicit list structure and thus rewrite rules like
tree-list-list-match-alternation-p-of-cons-alternation suffice.
For some parsing functions that parse repetitions,
the tree matching theorems say that the returned trees match
not only the repetitions (via tree-list-match-repetition-p),
but also the repeated elements (via tree-list-match-element-p).
This is because subgoals involving tree-list-match-element-p
arise in the tree matching theorems
of the callers of such parsing functions.
Subtopics
- Tree-match-of-parse-alt/conc/rep/elem/group/option
- Tree matching theorems for
parse-alternation,
parse-concatenation,
parse-repetition,
parse-element,
parse-group,
parse-option,
parse-alt-rest,
parse-alt-rest-comp,
parse-conc-rest, and
parse-conc-rest-comp.
- Tree-list-match-of-parse-*-in-either-range
- Tree matching theorem for parse-*-in-either-range.
- Tree-match-of-parse-in-either-range
- Tree matching theorem for parse-in-either-range.
- Tree-list-match-of-parse-*-rule-/-*cwsp-cnl
- Tree matching theorem for parse-*-rule-/-*cwsp-cnl.
- Tree-match-of-parse-in-range
- Tree matching theorem for parse-in-range.
- Tree-match-of-parse-alpha/digit/dash
- Tree matching theorem for parse-alpha/digit/dash.
- Tree-match-of-parse-alpha
- Tree matching theorem for parse-alpha.
- Tree-list-match-of-parse-*-dot-1*hexdig
- Tree matching theorem for parse-*-dot-1*hexdig.
- Tree-match-of-parse-*digit-star-*digit
- Tree matching theorem for parse-*digit-star-*digit.
- Tree-match-of-parse-rule-/-*cwsp-cnl
- Tree matching theorem for parse-rule-/-*cwsp-cnl.
- Tree-match-of-parse-quoted-string
- Tree matching theorem for parse-quoted-string.
- Tree-match-of-parse-ichar2
- Tree matching theorem for parse-ichar2.
- Tree-match-of-parse-ichar
- Tree matching theorem for parse-ichar.
- Tree-match-of-parse-hex-val-rest
- Tree matching theorem for parse-hex-val-rest.
- Tree-match-of-parse-exact
- Tree matching theorem for parse-exact.
- Tree-match-of-parse-equal-/-equal-slash
- Tree matching theorem for parse-equal-/-equal-slash.
- Tree-match-of-parse-defined-as
- Tree matching theorem for parse-defined-as.
- Tree-match-of-parse-dec-val-rest
- Tree matching theorem for parse-dec-val-rest.
- Tree-match-of-parse-dash-1*hexdig
- Tree matching theorem for parse-dash-1*hexdig.
- Tree-match-of-parse-case-sensitive-string
- Tree matching theorem for parse-case-sensitive-string.
- Tree-match-of-parse-case-insensitive-string
- Tree matching theorem for parse-case-insensitive-string.
- Tree-match-of-parse-bin/dec/hex-val
- Tree matching theorem for parse-bin/dec/hex-val.
- Tree-match-of-parse-bin-val-rest
- Tree matching theorem for parse-bin-val-rest.
- Tree-list-match-of-parse-*hexdig
- Tree matching theorem for parse-*hexdig.
- Tree-list-match-of-parse-*digit
- Tree matching theorem for parse-*digit.
- Tree-list-match-of-parse-*cwsp
- Tree matching theorem for parse-*cwsp.
- Tree-list-match-of-parse-*bit
- Tree matching theorem for parse-*bit.
- Tree-list-match-of-parse-*-dot-1*digit
- Tree matching theorem for parse-*-dot-1*digit.
- Tree-list-match-of-parse-*-dot-1*bit
- Tree matching theorem for parse-*-dot-1*bit.
- Tree-list-match-of-parse-*-alpha/digit/dash
- Tree matching theorem for parse-*-alpha/digit/dash.
- Tree-list-match-of-parse-1*-dot-1*hexdig
- Tree matching theorem for parse-1*-dot-1*hexdig.
- Tree-list-match-of-parse-1*-dot-1*digit
- Tree matching theorem for parse-1*-dot-1*digit.
- Tree-list-match-of-parse-1*-dot-1*bit
- Tree matching theorem for parse-1*-dot-1*bit.
- Tree-match-of-parse-?%i
- Tree matching theorem for parse-?%i.
- Tree-match-of-parse-?repeat
- Tree matching theorem for parse-?repeat.
- Tree-match-of-parse-*cwsp-cnl
- Tree matching theorem for parse-*cwsp-cnl.
- Tree-match-of-parse-wsp/vchar
- Tree matching theorem for parse-wsp/vchar.
- Tree-match-of-parse-wsp
- Tree matching theorem for parse-wsp.
- Tree-match-of-parse-vchar
- Tree matching theorem for parse-vchar.
- Tree-match-of-parse-sp
- Tree matching theorem for parse-sp.
- Tree-match-of-parse-rulename
- Tree matching theorem for parse-rulename.
- Tree-match-of-parse-rulelist
- Tree matching theorem for parse-rulelist.
- Tree-match-of-parse-rule
- Tree matching theorem for parse-rule.
- Tree-match-of-parse-repeat
- Tree matching theorem for parse-repeat.
- Tree-match-of-parse-prose-val
- Tree matching theorem for parse-prose-val.
- Tree-match-of-parse-num-val
- Tree matching theorem for parse-num-val.
- Tree-match-of-parse-lf
- Tree matching theorem for parse-lf.
- Tree-match-of-parse-htab
- Tree matching theorem for parse-htab.
- Tree-match-of-parse-hexdig
- Tree matching theorem for parse-hexdig.
- Tree-match-of-parse-hex-val
- Tree matching theorem for parse-hex-val.
- Tree-match-of-parse-elements
- Tree matching theorem for parse-elements.
- Tree-match-of-parse-dquote
- Tree matching theorem for parse-dquote.
- Tree-match-of-parse-dot-1*hexdig
- Tree matching theorem for parse-dot-1*hexdig.
- Tree-match-of-parse-dot-1*digit
- Tree matching theorem for parse-dot-1*digit.
- Tree-match-of-parse-dot-1*bit
- Tree matching theorem for parse-dot-1*bit.
- Tree-match-of-parse-digit
- Tree matching theorem for parse-digit.
- Tree-match-of-parse-dec-val
- Tree matching theorem for parse-dec-val.
- Tree-match-of-parse-dash-1*digit
- Tree matching theorem for parse-dash-1*digit.
- Tree-match-of-parse-dash-1*bit
- Tree matching theorem for parse-dash-1*bit.
- Tree-match-of-parse-cwsp
- Tree matching theorem for parse-cwsp.
- Tree-match-of-parse-crlf
- Tree matching theorem for parse-crlf.
- Tree-match-of-parse-cr
- Tree matching theorem for parse-cr.
- Tree-match-of-parse-comment
- Tree matching theorem for parse-comment.
- Tree-match-of-parse-cnl-wsp
- Tree matching theorem for parse-cnl-wsp.
- Tree-match-of-parse-cnl
- Tree matching theorem for parse-cnl.
- Tree-match-of-parse-char-val
- Tree matching theorem for parse-char-val.
- Tree-match-of-parse-bit
- Tree matching theorem for parse-bit.
- Tree-match-of-parse-bin-val
- Tree matching theorem for parse-bin-val.
- Tree-list-match-of-parse-*wsp/vchar
- Tree matching theorem for parse-*wsp/vchar.
- Tree-list-match-of-parse-1*hexdig
- Tree matching theorem for parse-1*hexdig.
- Tree-list-match-of-parse-1*digit
- Tree matching theorem for parse-1*digit.
- Tree-list-match-of-parse-1*cwsp
- Tree matching theorem for parse-1*cwsp.
- Tree-list-match-of-parse-1*bit
- Tree matching theorem for parse-1*bit.