Check mappings

[agontard]

Related to issue #178.

Adds command "make check-mappings" to check the correctness of the mappings, printing errors for wrong mappings.
It is done by translating the theory_hol.lp, $(base)_types.lp and $(base)_terms.lp files by adapting the lambdapi export code (in file xmapcheck.ml) and uses both ocaml checks and calls to Rocq's typechecker.

It can automatically diagnose all the following at once :

• Ill-typed mappings (for both objects and definitional lemmas/axioms)
• An object being mapped but not it's definitionnal lemma (or the converse)
• An axiom not being mapped
• A mapping not being used (for example if a name changed or was written with a typo)

Notes:

• also adds an intermediary command "make get-check-mappings" that generates the rocq file without checking it, which could be removed.
• While it tries as much as possible to keep going after finding a mapping error, I know two ways it can prematurely stop:
  1. a mapping to an inexistant qualid (an inexistant ident is accepted as uconstr but it does not work for a qualid)
  2. an ill-typed/inexistant term appearing in a non-mapped definition.

[agontard]

with the latest commit, I fully removed rocq compile warnings (for example during vo).
I am not sure interesting warnings could come from the automatically translated files that would not have appeared in the mappings file.

[agontard]

I had to add a dependency to lambdapi as I use the parser.
CI therefore fails because it tries to build hol2dk before installing lambdapi.

[agontard]

@fblanqui fun fact: now that I check objects from all relevant files including theory_hol.lp, I found out that ∃ᵢ had a small error by having an untyped parameter t which was therefore wrongly assumed to be of type Set (Type') upon export.

This was not an actual problem as it is always mapped and thus not actually translated as is, but maybe it could have been an issue for translation to other proof systems.

[fblanqui]

Why do you see this as an error? Note there are other symbols for which the argument A or a has no explicit type given. The problem seems rather about t after your change in this PR, right?

[agontard]

Why do you see this as an error? Note there are other symbols for which the argument A or a has no explicit type given. The problem seems rather about t after your change in this PR, right?

I am not sure to understand. What I meant is that lampdapi export to stt-coq automatically assumes the type of untyped parameters to be Type', which is correct for all automatically generated files. theory_hol.lp is the only non-automatically generated file that is translated, and in this file I believe this t is the only untyped parameter (or at least the only one not of type Type'), which is indeed not a problem since this axiom is mapped and thus not translated.

in 6af45f1 I explicitly typed it, just in case, so that even if this axiom is unmapped, the proofs could compile.

[fblanqui]

Hi. I had a quick look at this PR and made a few comments. Could you please make the requested changes?

[agontard]

CI now succeeds