More intelligent behavior for Implement missing fields

[sxhya]

Current behavior of Implement missing fields/coclauses quickfix is unsatisfactory because it ignores the mechanism of default fields, see pic. In this example all the fields of DecSet except decideEq and E can be omitted (because the other fields can be expressed through decideEq).

Recall that the mechanism of default fields is similar to that of Haskell and allows the user to implement only some class fields rather than all of them. The other fields are deduced via default-implementations.

To better illustrate how this mechanism works precisely let us look at the simplest nontrivial example from arend-lib: Arend's definition of a group. By definition, a group is a set E with a binary multiplication operation *, neutral element ide and the inverse operation inverse such that * is associative, ide is both right and left identity element and inverse is both the right and the left inverse, see Wikipedia article. Manually verifying everywhere these 5 axioms is tedious and awkward. However, it is quite obvious that instead of verifying all of inverse-left, ide-left, inverse-right, ide-right it is enough to verify either the first or the last two. In arend-lib this is spelled as the following implementation:

\class Group \extends CancelMonoid { -- the class inherits ide-left and ide-right
  | inverse : E -> E

  | inverse-left {x : E} : inverse x * x = ide
  | inverse-right {x : E}: x * inverse x = ide

  \default inverse-left {x} => -- ... Some expression using [inverse-right, ide-right]
  \default inverse-right {x} => -- ... Some expression using [inverse-left, ide-left]

  \default ide-left {x} => -- ... Some expression using [ide-right, inverse-right, inverse-left]
  \default ide-right {x} => -- ... Some expression using [ide-left, inverse-left, inverse-right]
 -- ...
}

So, basically, this means that if inverse-left and ide-left are implemented by the user then first inverse-right is deduced from the corresponding default field and consequently also so is ide-right (however implementing inverse-left together with ide-right would not be sufficient).

Thus, the following needs to be done.

1. Implement the algorithm computing all minimal sets of fields that need to be implemented for a given class (so that the other fields are implemented via their default implementations). This algorithm should have several parts:

• The algorithm looking through the definition of a class (and its ancestors!) and preparing the set of rules of the form $[f_1, ... f_n] \mapsto f_{n+1}$ based on it. Here $f_i$ are elements of the set $F$ of non-implemented fields of a given class. For example for Group there are 4 such rules:

[inverse-right, ide-right] -> inverse-left
[inverse-left, ide-left] -> inverse-right
[ide-right, inverse-right, inverse-left] -> ide-left
[ide-left, inverse-left, inverse-right] -> ide-right

• Implement the algorithm computing all minimal subsets $F_0\subseteq F$ from which all of $F$ can be deduced by successively adding right-hand-side of each applicable rule (a rule is applicable if all left-hand-side elements are already in $F_0$). You can solve this problem by constructing the graph whose vertices correspond to subsets of F and whose edges are calculated from these rules. The minimal (wrt to inclusion order) subsets connected with the vertex F are the answer.

2. After this algorithm is implemented the behavior of Implement missing fields fix should be modified:

If there is only one minimal subset $F_0$, the fix should add only fields from this minimal subset (like for DecSet above). If there are multiple minimal subsets, the question balloon implemented via HintAction should appear (similar to ArendImportHintAction, see the pic below).

The items in this baloon should correspond to the calculated minimal subsets of fields, the caption of each item is the list names of the fields to be implemented separated by comma.

The order in which the items in this list go is determined by the frequency of the user selecting this variant (variants used more often should be at the top) and some ad-hoc natural order on the list of fields (so that items in this menu would follow some consistent order). These frequency values should be stored in the user profile via PersistentStateComponent.

3. Test fixtures need to be properly modified and tests need to be added.