Algorithm for populating Trocq database for inductives

[Tvallejos]

description todo

[MysaaJava]

TODO

• rebase
• git mv std/algo/theories generic/inductives and change std/_CoqProject and hott/_CoqProject accordingly
• git mv std/algo/elpi elpi/inductives and update Elpi Accumulate accordingly
• git mv std/algo/tests tests/inductives and update tests/_CoqProject.{std,hott} accordingly
• Move most significant examples of std/algo/detailed to docs/inductive-generation, and write some documentation to docs/codebase.md about how the inductive generation works. Remove std/algo/detailed.
• rename Umap to Map4
• Remove coq.locate and {{ ... }} constructs from inside elpi code
• Remove dead code inside Rel40

Todo for myself, after merge:

• split utils.elpi content to adequates files if needed
• accumulate from inside elpi files directly
• Fold generic/Param_xxx into one file generic/Param_inductives.v Move check commands to tests/inductives/check_.....v
• Add a failing test with an inductive to Prop. For example with derive False which should generate False_sym when it doesn't. Check Zulip #Trocq users & devs > populating the Trocq database

Issues for later:

• There is a duplicated database with trocq.db, derive.param2.db and derive.xxx.db
• Can we clean all the databases derive.xxxx.db ?

[Tvallejos]

Hi @MysaaJava,
I'm using Trocq definitions in elpi files. Where should I register those definitions?

A few examples are Mapn.Has, eq_Mapn and eq

[MysaaJava]

I think you can add them to database.elpi.
You can add a predicate definition here, and accumulate on the clause.
You can see an example in Hierarchy.v which calls a predicate in generation/hierarchy.elpi

[Tvallejos]

I've been working on recovering the build for HoTT.
Inductives in HoTT are defined using universe polymorphism, so I need to extend the plugins to not assume global _ terms. In particular, almost all my derivations query derive.param2.db, which currently does not support universe polymorphism issue.

I minimized the dependencies to derive, but there are a couple more that will need such extension. For instance, discriminate and isK in derive.
I'm working on adding support for these plugins before continuing.