Streamline tracking of dependencies

[Lysxia]

Previously, dependencies started as dep_set: IndexSet before being converted into the expansion_queue.

Now, that logic is gathered in a single DepGraphBuilder structure to directly build the final graph.
Thanks to that, update_graph is just a small loop now.

A further simplification is that expansion_queue now only contains unvisited vertices instead of edges,
since the edges are added to the graph immediately.

[xldenis]

A further simplification is that expansion_queue now only contains unvisited vertices instead of edges,
since the edges are added to the graph immediately.

that always felt like a failure when I had to move the expansion queue to track edges. I had originally wanted to get it working with just nodes, so I'm glad you've managed to fix the bugs that prevented that!

[jhjourdan]

Generally, this looks good to me.

However, I think we can fix #1299 along the way, and it might be very well the case that the fix would be a simplification of Creusot.

In #1299, I said that the problem was that Why3 was not compatible with that. I think I was wrong: in program code, we should consider the source program function just like any other function (ignoring the fact that it is recursive), and, in the names map, we do not associate the name of the source function with the generated body. Then, a recursive call (in a closure or not) will generate a stub for the source function, with the right specification, and therefore we will generate the right VCs. We translate a recursive function to a no recursive one, but who cares?

Should we do something similar for logic functions, to support polymorphic recursion, and even perhaps mutual recursion?

[Lysxia]

That does sound feasible! It would require tweaking the termination checker, so maybe #2006 should be merged before that happens.

[jhjourdan]

Are you trying to Lazy.force my review of #2006 ? 😉

I'll do that as soon as the deadline chain that I currently have comes at its end.