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.
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:
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.
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 classID
of the constant must be assigned before the other classesIDs
, because the output class determines them.https://github.com/coq-community/trocq/blob/95f083ad0b3bca87324437d835b5957b9bd6a6cd/elpi/constraints/constraint-graph.elpi#L77-L86
For instance, in
list : Type(α) -> Type(β)
, we must first know the value ofβ
, and the instance oflistR
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:In this example, we will have an edge
β --gref--> α
in the graph, and in general an edgei --gref--> ID
for eachi
inIDs
, so that in the instantiation order computed after the goal traversal,ID
comes before, and when it gets a value, we make sure all theIDs
are equal to the classes found in the type of the registered witness for this constant at (now ground) levelID
.However, as the comment explains, constraints are added to the graph through predicates
add-higher-node
andadd-lower-node
, which suggests they are all ordering constraints, and theconstraint-type
Elpi type below is used to determine which of them are actual ordering constraints, and which are complex constraints:https://github.com/coq-community/trocq/blob/95f083ad0b3bca87324437d835b5957b9bd6a6cd/elpi/constraints/constraint-graph.elpi#L37-L42
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
andadd-lower-node
is a bit confusing because it only makes sense for ordering constraints, but renaming them toadd-later-node
andadd-earlier-node
would make sense only for non-ordering constraints.