Mapping-to-language-definition
Mapping from the tool-oriented syntax to the language definition.
As mentioned in syntax-for-tools,
we plan to provide formal connections between
the tool-oriented abstract syntax
and the formal language definition in c::language.
Towards that goal, we provide a partial mapping
from the tool-oriented abstract syntax
to the abstract syntax of the formal language definition.
This mapping is partial because currently the latter
only covers a subset of C.
The proper way to relate the two abstract syntaxes would be
in terms of the file sets that they reduce to in concrete syntax.
The current mapping between the abstract syntaxes
is like a ``shortcut''.
The functions that map
from the tool-oriented abstract syntax
to the language definition abstract syntax
all start with ldm, for `language definition mapping'.
We use error-value tuples when we encounter constructs that do not map
(due to the language definition abstract syntax being a subset).
So the mapping functions can be used also to check whether
the syntax is within the subset of the language definition.
We accompany these mapping functions with theorems showing that
the functions always succeed (i.e. never return errors)
on constructs in the subset of C with formal dynamic semantics,
as characterized by the formalized-subset.
Recall that the subset of C with formal dynamic semantics
is a strict subset of the subset of C
over which the mapping functions succeed.
Some mapping functions have no accompanying theorems,
because the constructs they operate on are never
in the subset of C with formal dynamic semantics.
Subtopics
- Ldm-type-spec-list
- Map a list of type specifiers to
a type specifier sequence in the language definition.
- Ldm-stmts/blocks
- Map statements and blocks to
statements and blocks in the language definition.
- Ldm-exprs
- Map expressions to expressions in the language definition.
- Ldm-declor-obj
- Map a declarator to
an object declarator in the language definition.
- Ldm-absdeclor-obj
- Map an abstract declarator to
an abstract object declarator in the language definition.
- Ldm-dirdeclor-obj
- Map a direct declarator to
an object declarator in the language definition.
- Ldm-declor-fun
- Map a declarator to
a function declarator in the language definition.
- Ldm-dirdeclor-fun
- Map a direct declarator to
a function declarator in the language definition.
- Ldm-decl-tag
- Map a declaration to
a tag declaration in the language definition.
- Ldm-decl-obj
- Map a declaration to
an object declaration in the language definition.
- Ldm-transunit-ensemble
- Map a translation unit ensemble to the language definition.
- Ldm-structdecl
- Map a structure declaration to
a structure declaration in the language definition.
- Ldm-dirabsdeclor-obj
- Map a direct abstract declarator to
an abstract object declarator in the language definition.
- Ldm-decl-fun
- Map a declaration to
a function declaration in the language definition.
- Ldm-extdecl
- Map an external declaration to
an external declaration in the language definition.
- Ldm-fundef
- Map a function definition to the language definition.
- Ldm-param-declor
- Map a parameter declarator to
an object declarator in the language definition.
- Ldm-param-declon
- Map a parameter declaration to
a parameter declaration in the language definition.
- Ldm-structdecl-list
- Map a list of structure declarations to
a list of structure declarations in the language definition.
- Ldm-stor-spec-list
- Map a list of storage class specifiers to
a storage class specifier sequence in the language definition.
- Ldm-param-declon-list
- Map a list of parameter declarations to
a list of parameter declarations in the language definition.
- Ldm-transunit
- Map a translation unit to the language definition.
- Ldm-desiniter
- Map an initializer with optional designations
to an initializer expression in the language definition.
- Ldm-tyname
- Map a type name to a type name in the language definition.
- Ldm-isuffix-option
- Map an optional integer suffix
to an integer constant length in the language definition
and to an unsigned flag.
- Ldm-expr-option
- Map an optional expression to
an optional expression in the language definition.
- Ldm-desiniter-list
- Map a list of initializers with optional designations to
a list of initializer expressions in the language definition.
- Ldm-dec/oct/hex-const
- Map a decimal, octal, or hexadecimal constant
to a value
and to an integer constant base in the language definition.
- Ldm-isuffix
- Map an integer suffix
to an integer constant length in the language definition
and to an unsigned flag.
- Ldm-ident
- Map an identiifer to an identifier in the language definition.
- Ldm-extdecl-list
- Map a list of external declarations to the language definition.
- Ldm-binop
- Map a binary operator to
a binary operator in the language definition.
- Ldm-initer
- Map an initializer to
an initializer in the language definition.
- Ldm-const
- Map a constant to
a constant in the language definition.
- Ldm-enumer-list
- Map a list of enumerators to
a list of identifiers in the language definition.
- Ldm-enumer
- Map an enumerator to
an identifier in the language definition.
- Ldm-label
- Map a label to a label in the language definition.
- Ldm-lsuffix
- Map a length suffix to an integer constant length
in the language definition.
- Ldm-iconst
- Map an integer constant to
an integer constant in the language definition.
- Ldm-expr
- Map an expression to an expression in the language definition.
- Ldm-expr-list
- Map a list of expressions to
a list of expressions in the language definition.
- Ldm-block-item-list
- Map a list of block items to
a list of block items in the language definition.
- Ldm-stmt
- Map a statement to a statement in the language definition.
- Ldm-block-item
- Map a block item to a block item in the language definition.
