3.6 Formalism Inclusion

Typol   users will found in formalism inclusion an easy way to design ``environments''   without polluting the abstract syntax of their object language, nor duplicating some parts of its abstract syntax.

Suppose that we have defined a formalism containing some identifiers and integers:

abstract syntax of L is
...
id : string -> Id;
int : integer -> Int;
...
end L;

When writing a dynamic semantics for this language, we may want to describe the memory as a pair of identifiers and integer values, where these identifiers and values belong to L:

abstract syntax of L_env is

memory : Pair * -> Mem;
pair : Id::L # Int::L -> Pair;

end L_env;

The notation ``P::L'' indicates that P is a phylum belonging to the formalism L.

Formalism   inclusion can also be used together with type inclusion:

Exp::L < Expression;

Formalism inclusion can be used to define languages which share some parts of their syntax with an other formalism. This is the case for example for Lex and Yacc in which the action part of a rule is a C statement.

Typed Names