Flit DAG dumper for Twelf 1.4
Copyright (C) 2002 Roberto Virga. All rights reserved.
N.B. The following instructions assume the availability of the flit
binary program and related tools, as maintained in the Foundational
Proof-Carrying Code project at Princeton. (For further information, see
.)
To use:
The DAG dumper functions only inside twelf-sml, and it is not
currently accessible from twelf-server.
First you need to initialize the dumper, by typing:
Flit.init ;
where is the path (either absolute, or
relative to the current working directory) to the TCB symbol
table file generated using the files in logic/pcc/flit/untrusted.
After you have initialized the dumper by providing the symbol
table of the TCB as outlined above, there are two ways you
can use the dumper:
a) to dump a single symbol (together with all the other non-TCB
symbols it might depend):
Flit.dump ;
b) to dump all symbols used in a logic program:
Flit.setFlag ();
Twelf.Config.append (Twelf.Config.read );
Flit.dumpFlagged ;
will dump all symbols loaded since Flit.setFlag () was
issued, and in particular, all symbols introduced by
loading the Twelf configuration file .
All such symbols will have the "clause" bit set to 1
(the clause bit is the 10th bit of the first field of
a node, and can be retrieved by doing a logical and with
mask 512).