[ derive ] Impement multi-stage algorithm for calculation of ordering

[buzden]

No description provided.

[buzden]

Currently, we are choosing candidates of generation one by one, because the order matters: if we choose one of them, its generation can release more candidates, which can be more important than already existing candidates.

It seems to be important that we would take GADT status of their type arguments into account. This would require us to analyse

• for each candidate type (or for each type at all, if we precalculate this)

  • for each type argument

    • for each constructor decide whether it is

      • a single constructor's argument name (i.e. parametric);
      • contains only constructor's arguments and names of constructors/types (i.e. easily pattern-matchable);
      • other (i.e. including application of arbitrary functions, thus shouldn't be given).

Open question is to which f a belongs, where both f and a are constructor arguments. This is important once we support polymorphic types. Maybe the second class above should be reformulated as "application of names of constructors/types to constructor arguments or names of constructors/types".

[buzden]

The newly suggested algorithm can be described in the following way.

We consider a constructor and its arguments as a graph, nodes are arguments. Edges are of four sorts:

• weak (parametric) forward determination (dash lines);
• normal forward determination (normal lines);
• strong forward determination (thick lines);
• strong back determination (double lines).

Forward determination goes from argument b to argument a if type of argument b depends on argument a. Weak forward determination goes when a is used as a parameter (i.e. not as index) in a type of b (in current context). Normal forward determination goes when a is used as a type index in a type of b and only constructors applied to (constructors applied to)* con args are used in all index expressions. Strong forward determination is used if non-constructor functions are used in index expressions in type declaration of type of b. Semantically forward determination means that when we generated b, we can generate a along with it in a dependent pair, unless a is already generated, in which case it needs to be a given argument in generation of b. Strong forward determination means that this particular argument a cannot be used as given for b.

Strong back determination goes from argument a to argument b if argument a is used in a type of argument b inside a function application, like (b : S a `LT` c). Strong back determination means semantically that we need to generate a before b in case they are not generated by anything else.

You can consider an example of such a graph for the constructor NodeLT of type AllLT from the sorted-tree-naive example:

We consider also already generated or otherwise present arguments. We start with the fact that given arguments are already present.

---

We start a step with counting how many outgoing normal forward determination links go to already present (given or generated) arguments. The more the number, the higher the priority is assigned to this node. This priority also gets back along strong back determination, normal foward determination and strong forward determination edges (e.g. from #6 to #1 (x) in the example on the picture above) taking max with the current priority (0 by default).

After that we determine which edges to not have any incoming normal forward determination, strong forward determination or strong back determination edges. Among them we choose one with the highes priority and mark as generated all not yet generated nodes to which any forward detemination edge goes from the newly added. Then repeat the step until no not generated arguments left.