I'm using a tool called Ox, which is an extension to Yacc which lets you declare attributes of the yacc productions and write attribute equations (in C/C++). But the particular attribute grammar, parser/evaluator is really irrelevant.
The key idea is, to translate from language L1 to language L2, we write a grammar and attribute equations for L1. And we write a noweb "skeleton" for L2. In my case L1 is VHDL and L2 is Larch. So my L2 skeleton could look like:
<L2 skeleton>= --| Larch <theory name> : trait <includes> <shorthands> introduces <function declarations> asserts <assertions> implies <implications> --| end Larch
Now, to translate an instance I of L1 into L2, I parse I and evaluate its attributes. Then I traverse the parse tree and ask each node to write its translation. So for example if the node is a declaration of a VHDL signal x of subtype S based on type T, it might write
<function declarations>= x : -> Signal[T] <assertions> x_constraints: ...some assertion about the subtype of x ....
If the node is a VHDL type definition of an array type, ty which is an array indexed by color of component type foo, it might write:
<includes>= includes ArrayTheory(Color, Foo)
<function declarations>+= ty : -> TypeCon
<assertions>= ty: ty = array_type_con(color,foo)
and so on.
Now all I have to do is set the output stream to be the one I get
from popen("notangle") so that everything get piped through notangle,
and I have the root node of the grammar start out by writing the
skeleton.
The point is, in language L1, declarations may be distrubuted here and there and in L2 they may all have to be gathered together (as in Larch). Or the declaration in L1 may correspond to several things in L2 (an include of some theory, a declaration, and an assertion). Without notangle, I would have to have synthesized attributes to gather up all the pieces of information for the various parts of the translation, or I would have to build up tables or something, just to get the information into the right place in the translation. With notangle, I let notangle take care of reordering things and I just implement a ``translate yourself'' method for each kind of node.
If I then want to translate into PVS instead of Larch (and I do) I just write a PVS skeleton.nw, and change my ``translate yourself'' methods and the same basic system now translates into PVS.
Of course, we also use noweb for our attribute equations themselves and for the C++ code too.
For the attribute equations, we start with a yacc grammar:
<original grammar>= root: A B A: D | E F B: X Y
and then we make (automatically) a skeleton that adds attribute equations:
<revised grammar>=
root: A B
@{ <root: A B> @}
A: D
@{ <A: D> @}
| E F
@{ <A: E F> @}
B: X Y
@{ <B: X Y> @}
<root: A B>=
<A: D>=
<A: E F>=
<B: X Y>=
So this adds a module for each production and defines it to be empty. The name of the module is the production itself. Now, when we want to add equations to some production, it is easy. And we can group the equations into ``layers'' so that we can include certain attributes and their defining equations in some tools based on the grammar and not include them in other tools that don't need them.