The token file generated by the tokenizer includes the internal
representation of a given DATR theory. It contains all necessary
information for the inference engine required as input for
zdatrinf.
Note: The token file should never be modified manually.
The following specification is therefore mentioned for the sake of completeness
only.
The file is organized in three sections: the header information, the look-up tables for atoms, variables and nodes and the equation part.
The header consists of the `magic string' DATR-Token-file followed by the source name of the theory.
The three look-up tables are line-oriented and contain after the number of atoms/vars/nodes an enumeration number, the length of the item in bytes and the item itself.
The equation section contains for each node the node key as defined in the look-up table, the number of equations, and the list of left hand sides and right hand sides with each pair separated with a '=='.