10 | ------------------------------------------
11 | --- Facilities for manual order tuning ---
12 | ------------------------------------------
16 | ||| A magic interface for tuning the order of generation in derived generators
17 | |||
18 | ||| This interface defines a function `isConstructor` which can be implemented only by calling a macro `itIsConstructor`.
19 | ||| If the argument of the implementation is not a name of a constructor, you will get a compilation error at this point.
20 | |||
21 | ||| `deriveFirst` function gets some information about given arguments in the current derivation task,
22 | ||| and returns constructor's arguments that must be generated first in the derived generator, in order.
23 | ||| If given arguments require some other arguments to be derived before them, these arguments would be generated appropriately.
24 | ||| Any repetitions, mentions of already given arguments and mentions of arguments that will be generated by arguments earlier in the list
25 | ||| will be simply ignored.
26 | |||
27 | ||| Constructor arguments can be given by their number or their name (using name literals).
28 | |||
29 | ||| Typical usage is the following:
30 | |||
31 | ||| ```idris
32 | ||| data X : Nat -> Nat -> Type where
33 | ||| X1 : (n, m : Nat) -> n `LT` m => X n m
34 | ||| X2 : X n n
35 | |||
36 | ||| GenOrderTuning "X".dataCon where
37 | ||| isConstructor = itIsConstructor
38 | ||| deriveFirst gt gc = [`{m}, 2] -- 2 is the `LT` argument
39 | ||| ```
47 | -------------------------------
48 | --- Tuning of probabilities ---
49 | -------------------------------