Syntax-abstraction
An executable mapping from
the concrete syntax of ABNF to the abstract syntax of ABNF.
The ABNF abstract syntax is an abstraction of the concrete syntax.
That is, there is a mapping
from the parse trees obtained by parsing sequences of natural numbers
according to the rules of the concrete syntax of ABNF,
to the entities of the abstract syntax of ABNF.
The mapping abstracts away many of the details of the concrete syntax.
This abstraction mapping is defined by a collection of functions.
These functions explicitly check that the trees
satisfy certain expected conditions.
Eventually, these expected conditions
should be proved to follow from suitable guards.
Subtopics
- Abstract-repeat
- A repeat parse tree is abstracted to
its correspoding repetition range.
- Abstract-bin/dec/hex-val-rest-dot-p
- Discriminate
between a ("." 1*BIT)
and a ("-" 1*BIT) parse tree,
or between a ("." 1*DIGIT)
and a ("-" 1*DIGIT) parse tree,
or between a ("." 1*HEXDIG)
and a ("-" 1*HEXDIG) parse tree.
- Abstract-*digit-star-*digit
- A (*DIGIT "*" *DIGIT) parse tree is abstracted to
(i) the big-endian value of its first *DIGIT and
(ii) either the big-endian value of its second *DIGIT
(if non-empty)
or infinity
(if empty).
- Abstract-*-grouped-terminal
- A list of zero or more ( term1 / ... / termN ) parse trees,
where term1, ..., termN are
terminal numeric or character value notations
that all denote single natural numbers,
are abstracted to the list of its natural numbers.
- Abstract-case-insensitive-string
- A case-insensitive-string parse tree
is abstracted to its character string and to a boolean flag
saying whether the %i prefix is present or not.
- Abstract-grouped-terminals
- A ( term1 / ... / termN ) parse tree,
where term1, ..., termN are
terminal numeric or character value notations,
is generally abstracted to its list of natural numbers.
- Abstract-hexdig
- A HEXDIG parse tree is abstracted to its hexadecimal digit.
- Abstract-hex-val-rest
- A [ 1*("." 1*HEXDIG) / ("-" 1*HEXDIG) ] parse tree
is abstracted to
either the list of its big-endian values (for the first alternative)
or its single big-endian value (for the second alternative).
- Abstract-grouped-terminal
- A ( term1 / ... / termN ) parse tree,
where term1, ..., termN are
terminal numeric and character notations
that all denote single natural numbers,
is sometimes abstracted to its only natural number.
- Abstract-dec-val-rest
- A [ 1*("." 1*DIGIT) / ("-" 1*DIGIT) ] parse tree
is abstracted to
either the list of its big-endian values (for the first alternative)
or its single big-endian value (for the second alternative).
- Abstract-bin-val-rest
- A [ 1*("." 1*BIT) / ("-" 1*BIT) ] parse tree
is abstracted to
either the list of its big-endian values (for the first alternative)
or its single big-endian value (for the second alternative).
- Abstract-rulename
- A rulename parse tree is abstracted to
its corresponding rule name.
- Abstract-*hexdig
- A list of zero or more HEXDIG parse trees is abstracted to
the big-endian value of its hexadecimal digits.
- Abstract-*digit
- A list of zero or more DIGIT parse trees is abstracted to
the big-endian value of its decimal digits.
- Abstract-terminals
- A term parse tree,
where term is a terminal numeric or character value notation,
is generally abstracted to its list of natural numbers.
- Abstract-terminal
- A term parse tree,
where term is a terminal numeric or character value notation
that denotes a single natural number,
is sometimes abstracted to its only natural number.
- Abstract-rule-/-*cwsp-cnl
- A ( rule / (*c-wsp c-nl) ) parse tree is abstracted to
either its rule (for the first alternative)
or nothing (for the second alternative).
- Abstract-digit
- A DIGIT parse tree is abstracted to its decimal digit.
- Abstract-bin/dec/hex-val
- A (bin-val / dec-val / hex-val ) parse tree is abstracted to
its corresponding numeric value notation.
- Abstract-?repeat
- A [repeat] parse tree is abstracted to
its corresponding repetition range.
- Abstract-*bit
- A list of zero or more BIT parse trees is abstracted to
the big-endian value of its bits.
- Abstract-rule
- A rule parse tree is abstracted to its corresponding rule.
- Abstract-hex-val
- A hex-val parse tree is abstracted to
its corresponding numeric value notation.
- Abstract-dec-val
- A dec-val parse tree is abstracted to
its corresponding numeric value notation.
- Abstract-char-val
- A char-val parse tree is abstracted to
its corresponding character value notation.
- Abstract-bin-val
- A bin-val parse tree is abstracted to
its corresponding numeric value notation.
- Abstract-alpha/digit/dash
- A (ALPHA / DIGIT / "-") parse tree
is abstracted to its corresponding character.
- Abstract-*-rule-/-*cwsp-cnl
- A list of zero or more ( rule / (*c-wsp c-nl) ) parse trees
is abstracted to the list of its corresponding rules.
- Abstract-*-alpha/digit/dash
- A list of zero or more (ALPHA / DIGIT / "-") parse trees
is abstracted to its corresponding list of characters.
- Abstract-quoted-string
- A quoted-string parse tree is abstracted to
its character string.
- Abstract-prose-val
- A prose-val parse tree is abstracted to
its corresponding prose value notation.
- Abstract-defined-as
- A defined-as parse tree is abstracted to
the boolean indicating whether the rule is incremental or not.
- Abstract-case-sensitive-string
- A case-sensitive-string parse tree
is abstracted to its character string.
- Abstract-bit
- A BIT parse tree is abstracted to its bit.
- Abstract-*-dot-1*hexdig
- A list of zero or more ("." 1*HEXDIG) parse trees
is abstracted to the list of their corresponding big-endian values.
- Abstract-*-dot-1*digit
- A list of zero or more ("." 1*DIGIT) parse trees
is abstracted to the list of their corresponding big-endian values.
- Abstract-*-dot-1*bit
- A list of zero or more ("." 1*BIT) parse trees
is abstracted to the list of their corresponding big-endian values.
- Abstract-rulelist
- A rulelist parse tree is abstracted to
its corresponding list of rules.
- Abstract-num-val
- A num-val parse tree is abstracted to
its corresponding numeric value notation.
- Abstract-element
- An element parse tree is abstracted to
its corresponding element.
- Abstract-dot/dash-1*hexdig
- A ("." 1*HEXDIG) or ("-" 1*HEXDIG) parse tree
is abstracted to the big-endian value of its hexadecimal digits.
- Abstract-dot/dash-1*digit
- A ("." 1*DIGIT) or ("-" 1*DIGIT) parse tree
is abstracted to the big-endian value of its decimal digits.
- Abstract-elements
- An elements parse tree is abstracted to its alternation.
- Abstract-dot/dash-1*bit
- A ("." 1*BIT) or ("-" 1*BIT) parse tree
is abstracted to the big-endian value of its bits.
- Abstract-alpha
- An ALPHA parse tree is abstracted to its corresponding letter.
- Abstract-repetition
- A repetition parse tree is abstracted to
its corresponding repetition.
- Abstract-concatenation
- A concatenation parse tree is abstracted to
its corresponding concatenation.
- Abstract-conc-rest
- A list of zero or more
(1*c-wsp repetition) parse trees
is abstracted to the list of its repetitions
(i.e. a concatenation).
- Abstract-alternation
- An alternation parse tree is abstracted to
its corresponding alternation.
- Abstract-alt-rest
- A list of zero or more
(*c-wsp "/" *c-wsp concatenation) parse trees
is abstracted to the list of its concatenations
(i.e. an alternation).
- Abstract-group/option
- A group or option parse tree is abstracted to
its alternation inside the group or option.
- Abstract-fail
- Called when abstraction fails.
- Abstract-conc-rest-comp
- A (1*c-wsp repetition) parse tree
is abstracted to its repetition.
- Abstract-alt-rest-comp
- A (*c-wsp "/" *c-wsp concatenation) parse tree
is abstracted to its concatenation.
