Predicate naming in constraint graph

[ecranceMERCE]

The add-dep-gref predicate below is in charge of adding information to the constraint graph about a constant, i.e., asserting that the output class ID of the constant must be assigned before the other classes IDs, because the output class determines them.

trocq/elpi/constraints/constraint-graph.elpi

Lines 77 to 86 in 95f083a

	pred add-dep-gref
	i:class-id, i:gref, i:term, i:term, i:gref, i:list class-id, i:constraint-graph,
	o:constraint-graph.
	add-dep-gref ID GR T Tm' GRR IDs (constraint-graph G) (constraint-graph G') :-
	% the classes C_i (IDs) are not really "higher" than the output class C (ID)
	% here, higher is a way to say that they must be instantiated later than the output class
	util.map.update ID (internal.add-higher-node (node.var (ct.gref GR T Tm' GRR) IDs)) G G1,
	std.fold IDs G1 (id\ g\ g'\
	util.map.update id (internal.add-lower-node (node.var (ct.gref _ _ _ _) [ID])) g g')
	G'.

For instance, in list : Type(α) -> Type(β), we must first know the value of β, and the instance of listR at level β registered in Trocq will give the required value for α in its type, e.g., in the following type we have class $(3,1)$ for the parameter:

listR31 : forall A A' (AR : Param31.Rel A A'), Param31.Rel (list A) (list A').

In this example, we will have an edge β --gref--> α in the graph, and in general an edge i --gref--> ID for each i in IDs, so that in the instantiation order computed after the goal traversal, ID comes before, and when it gets a value, we make sure all the IDs are equal to the classes found in the type of the registered witness for this constant at (now ground) level ID.

However, as the comment explains, constraints are added to the graph through predicates add-higher-node and add-lower-node, which suggests they are all ordering constraints, and the constraint-type Elpi type below is used to determine which of them are actual ordering constraints, and which are complex constraints:

trocq/elpi/constraints/constraint-graph.elpi

Lines 37 to 42 in 95f083a

	kind constraint-type type.
	type ct.pi constraint-type.
	type ct.arrow constraint-type.
	type ct.type constraint-type.
	type ct.gref gref -> term -> term -> gref -> constraint-type.
	type ct.geq constraint-type.

This graph contains both ordering constraints and complex constraints used to determine an instantiation order, thus having nothing to do with ordering. In other words, the edges have different meanings according to the annotation on them. Therefore, the naming for add-higher-node and add-lower-node is a bit confusing because it only makes sense for ordering constraints, but renaming them to add-later-node and add-earlier-node would make sense only for non-ordering constraints.