Importation is done before type checking

[francoisthire]

The current mechanism to import dependencies is done at runtime while type checking a term. Dependencies are imported on the fly.

This side-effect is convenient for prototyping, but has disadvantages. The main one being that the type checking and reduction produce both side-effects on the signature.

This raises several issues when Dedukti is used as a library via the modules in api folder.

To overcome this, a way is to always ensure that modules are imported before type checking. This PR is a first step towards this goal:

1. We ensure modules are imported before starting to type check thems
2. We keep the importations implicit. We could argue later on that the REQUIRE directive should be mandatory but I suspect this is a choice which will impact the standardisation of Dedukti so we make no commitment on it.

Performance-wise, this MR has one main downside: terms are processed twice instead now. I suspect this is not sensible since in practice we spend most of our time doing reductions. However, this could be avoided if we solve 2. I have no benchmark to sustain this point at the moment.

TODO:

• Clean up the code
• Add more tests
• Add an option like --no-implicit-import to get the benefit of 2. without the downside of computing the dependencies introduced in this MR. If a dependency is missing, the type checking will just fail.