Virtual positions for generated symbols

[fblanqui]

The sym type has two fields:

• sym_pos, the position of the symbol name in the user source file;
• sym_decl_pos, the position of the symbol command in the user source file.

Problems:

• To print symbol and rule declarations in a valid order in commands exporting signatures (e.g. dk.ml), the sym_decl_pos of generated symbols (axioms, inductive type constructors and recursors) are shifted by some integer. Hence, they do not actually correspond to actual positions in the user source file. This is a problem because 1) Indexing.index_sym should provide a valid position, and 2) using shifted positions is not sufficient to handle inductive inductive types (see Fix dk export on indind and file.with.dot #820).
• For axioms, sym_decl_pos is using sym_pos instead of the position of the symbol command in which the axiom is generated.

Remarks:

• For a user-defined symbol s, s.sym_pos refers to the position of the symbol name in the user source file while s.sym_decl_pos refers to the position of the whole symbol command. These two positions are actual positions in the user source file.
• For a string literal symbol s, both s.sym_pos and s.sym_decl_pos refer to the position of the first occurrence of that string in the required user source files. They are actual positions.
• For an axiom symbol s generated while declaring a symbol t in a user source file, s.sym_pos refers to t.sym_pos (this would be better to take t.sym_decl_pos) and s.sym_decl_pos is a virtual position that generally occurs before t.sym_pos and t.sym_decl_pos, although this is not guaranteed (this should be fixed).
• For a generated symbol s that is an inductive type, constructor or recursor, s.sym_pos refers to the position of the inductive command in the user source file, and s.sym_decl_pos is a virtual position occurring after s.sym_pos.

TODO:

• use valid sym_decl_pos only (remove shift)
• order symbol declarations of inductive types according to their dependencies
• fix NOTE in term.ml, and sym_decl_pos comments in command.ml