Grammar-parser-input-decomposition
Input decomposition theorems for the parser of ABNF grammars.
If parsing succeeds,
the string at the leaves of the returned tree(s)
consists of the consumed natural numbers in the input.
That is,
appending the string at the leaves with the remaining input
yields the original input.
More precisely, it yields the original input
fixed according to nat-list-fix,
because the parsing functions fix their input;
an alternative formulation is to avoid nat-list-fix
but include the hypothesis that the input satisfies nat-listp.
The input decomposition theorem of parse-any
does not involve trees but makes an analogous statement:
concatenating the returned natural number with the remaining input
yields the original input.
The input decomposition proof of each parsing function uses,
as rewrite rules,
the input decomposition theorems of the parsing functions called by
the parsing function whose theorem is being proved.
The proofs also use the definition of tree->string,
which we enable just before these theorems and disable just after.
Subtopics
- Input-decomposition-of-parse-alt/conc/rep/elem/group/option
- Input decomposition 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.
- Input-decomposition-of-parse-case-insensitive-string
- Input decomposition theorem for
parse-case-insensitive-string.
- Input-decomposition-of-parse-*wsp/vchar
- Input decomposition theorem for parse-*wsp/vchar.
- Input-decomposition-of-parse-*digit-star-*digit
- Input decomposition theorem for parse-*digit-star-*digit.
- Input-decomposition-of-parse-*cwsp-cnl
- Input decomposition theorem for parse-*cwsp-cnl.
- Input-decomposition-of-parse-*-rule-/-*cwsp-cnl
- Input decomposition theorem for parse-*-rule-/-*cwsp-cnl.
- Input-decomposition-of-parse-*-in-either-range
- Input decomposition theorem for parse-*-in-either-range.
- Input-decomposition-of-parse-*-dot-1*hexdig
- Input decomposition theorem for parse-*-dot-1*hexdig.
- Input-decomposition-of-parse-*-dot-1*digit
- Input decomposition theorem for parse-*-dot-1*digit.
- Input-decomposition-of-parse-*-dot-1*bit
- Input decomposition theorem for parse-*-dot-1*bit.
- Input-decomposition-of-parse-*-alpha/digit/dash
- Input decomposition theorem for parse-*-alpha/digit/dash.
- Input-decomposition-of-parse-wsp/vchar
- Input decomposition theorem for parse-wsp/vchar.
- Input-decomposition-of-parse-rulename
- Input decomposition theorem for parse-rulename.
- Input-decomposition-of-parse-rulelist
- Input decomposition theorem for parse-rulelist.
- Input-decomposition-of-parse-rule-/-*cwsp-cnl
- Input decomposition theorem for parse-rule-/-*cwsp-cnl.
- Input-decomposition-of-parse-quoted-string
- Input decomposition theorem for parse-quoted-string.
- Input-decomposition-of-parse-prose-val
- Input decomposition theorem for parse-prose-val.
- Input-decomposition-of-parse-num-val
- Input decomposition theorem for parse-num-val.
- Input-decomposition-of-parse-in-range
- Input decomposition theorem for parse-in-range.
- Input-decomposition-of-parse-in-either-range
- Input decomposition theorem for parse-in-either-range.
- Input-decomposition-of-parse-ichar2
- Input decomposition theorem for parse-ichar2.
- Input-decomposition-of-parse-hex-val-rest
- Input decomposition theorem for parse-hex-val-rest.
- Input-decomposition-of-parse-hex-val
- Input decomposition theorem for parse-hex-val.
- Input-decomposition-of-parse-equal-/-equal-slash
- Input decomposition theorem for parse-equal-/-equal-slash.
- Input-decomposition-of-parse-elements
- Input decomposition theorem for parse-elements.
- Input-decomposition-of-parse-dot-1*hexdig
- Input decomposition theorem for parse-dot-1*hexdig.
- Input-decomposition-of-parse-dot-1*digit
- Input decomposition theorem for parse-dot-1*digit.
- Input-decomposition-of-parse-dot-1*bit
- Input decomposition theorem for parse-dot-1*bit.
- Input-decomposition-of-parse-defined-as
- Input decomposition theorem for parse-defined-as.
- Input-decomposition-of-parse-dec-val-rest
- Input decomposition theorem for parse-dec-val-rest.
- Input-decomposition-of-parse-dec-val
- Input decomposition theorem for parse-dec-val.
- Input-decomposition-of-parse-dash-1*hexdig
- Input decomposition theorem for parse-dash-1*hexdig.
- Input-decomposition-of-parse-dash-1*digit
- Input decomposition theorem for parse-dash-1*digit.
- Input-decomposition-of-parse-dash-1*bit
- Input decomposition theorem for parse-dash-1*bit.
- Input-decomposition-of-parse-comment
- Input decomposition theorem for parse-comment.
- Input-decomposition-of-parse-cnl-wsp
- Input decomposition theorem for parse-cnl-wsp.
- Input-decomposition-of-parse-char-val
- Input decomposition theorem for parse-char-val.
- Input-decomposition-of-parse-case-sensitive-string
- Input decomposition theorem for parse-case-sensitive-string.
- Input-decomposition-of-parse-bin/dec/hex-val
- Input decomposition theorem for parse-bin/dec/hex-val.
- Input-decomposition-of-parse-bin-val-rest
- Input decomposition theorem for parse-bin-val-rest.
- Input-decomposition-of-parse-bin-val
- Input decomposition theorem for parse-bin-val.
- Input-decomposition-of-parse-alpha/digit/dash
- Input decomposition theorem for parse-alpha/digit/dash.
- Input-decomposition-of-parse-1*hexdig
- Input decomposition theorem for parse-1*hexdig.
- Input-decomposition-of-parse-1*digit
- Input decomposition theorem for parse-1*digit.
- Input-decomposition-of-parse-1*cwsp
- Input decomposition theorem for parse-1*cwsp.
- Input-decomposition-of-parse-1*bit
- Input decomposition theorem for parse-1*bit.
- Input-decomposition-of-parse-1*-dot-1*hexdig
- Input decomposition theorem for parse-1*-dot-1*hexdig.
- Input-decomposition-of-parse-1*-dot-1*digit
- Input decomposition theorem for parse-1*-dot-1*digit.
- Input-decomposition-of-parse-1*-dot-1*bit
- Input decomposition theorem for parse-1*-dot-1*bit.
- Input-decomposition-of-parse-?%i
- Input decomposition theorem for parse-?%i.
- Input-decomposition-of-parse-?repeat
- Input decomposition theorem for parse-?repeat.
- Input-decomposition-of-parse-*hexdig
- Input decomposition theorem for parse-*hexdig.
- Input-decomposition-of-parse-*digit
- Input decomposition theorem for parse-*digit.
- Input-decomposition-of-parse-*cwsp
- Input decomposition theorem for parse-*cwsp.
- Input-decomposition-of-parse-*bit
- Input decomposition theorem for parse-*bit.
- Input-decomposition-of-parse-wsp
- Input decomposition theorem for parse-wsp.
- Input-decomposition-of-parse-vchar
- Input decomposition theorem for parse-vchar.
- Input-decomposition-of-parse-sp
- Input decomposition theorem for parse-sp.
- Input-decomposition-of-parse-rule
- Input decomposition theorem for parse-rule.
- Input-decomposition-of-parse-repeat
- Input decomposition theorem for parse-repeat.
- Input-decomposition-of-parse-lf
- Input decomposition theorem for parse-lf.
- Input-decomposition-of-parse-ichar
- Input decomposition theorem for parse-ichar.
- Input-decomposition-of-parse-htab
- Input decomposition theorem for parse-htab.
- Input-decomposition-of-parse-hexdig
- Input decomposition theorem for parse-hexdig.
- Input-decomposition-of-parse-exact
- Input decomposition theorem for parse-exact.
- Input-decomposition-of-parse-dquote
- Input decomposition theorem for parse-dquote.
- Input-decomposition-of-parse-digit
- Input decomposition theorem for parse-digit.
- Input-decomposition-of-parse-cwsp
- Input decomposition theorem for parse-cwsp.
- Input-decomposition-of-parse-crlf
- Input decomposition theorem for parse-crlf.
- Input-decomposition-of-parse-cr
- Input decomposition theorem for parse-cr.
- Input-decomposition-of-parse-cnl
- Input decomposition theorem for parse-cnl.
- Input-decomposition-of-parse-bit
- Input decomposition theorem for parse-bit.
- Input-decomposition-of-parse-any
- Input decomposition theorem for parse-any.
- Input-decomposition-of-parse-alpha
- Input decomposition theorem for parse-alpha.
