Deriving.DepTyCheck.Gen

Derivation interface for an end-point user

Reexports

Definitions

deriveGenExpr : DeriveBodyForType => TTImp -> Elab TTImp

Totality: total
Visibility: export

deriveGen : DeriveBodyForType => Elab a

  The entry-point function of automatic derivation of `Gen`'s.
  
  Consider, you have a `data X (a : A) (b : B n) (c : C) where ...` and
  you want a derived `Gen` for `X`.
  Say, you want to have `a` and `c` parameters of `X` to be set by the caller and the `b` parameter to be generated.
  For this your generator function should have a signature like `(a : A) -> (c : C) -> (n ** b : B n ** X a b c)`.
  So, you need to define a function with this signature, say, named as `genX` and
  to write `genX = deriveGen` as an implementation to make the body to be derived.
  
  Say, you want `n` to be set by the caller and, as the same time, to be an implicit argument.
  In this case, the signature of the main function to be derived,
  becomes `{n : _} -> (a : A) -> (c : C) -> (b : B n ** X a b c)`.
  But still, you can use this function `deriveGen` to derive a function with such signature.
  
  Say, you want your generator to be parameterized with some external `Gen`'s.
  Consider types `data Y where ...`, `data Z1 where ...` and `data Z2 (b : B n) where ...`.
  For this, `auto`-parameters can be listed with `=>`-syntax in the signature.
  
  For example, if you want to use `Gen Y` and `Gen`'s for `Z1` and `Z2` as external generators,
  you can define your function in the following way:
  
    ```idris
    genX : Gen Y => Gen Z1 => ({n : _} -> {b : B n} -> Gen (Z2 b)) => {n : _} -> (a : A) -> (c : C) -> Gen (b : B n ** X a b c)
    genX = deriveGen
    ```
  
  Consider also, that you may be asked for having the `Fuel` argument as the first argument in the signature
  due to (maybe, temporary) unability of `Gen`'s to manage infinite processes of values generation.
  So, the example from above will look like this:
  
    ```idris
    genX : Fuel -> (Fuel -> Gen Y) => (Fuel -> Gen Z1) => (Fuel -> {n : _} -> {b : B n} -> Gen (Z2 b)) =>
           {n : _} -> (a : A) -> (c : C) -> Gen (b : B n ** X a b c)
    genX = deriveGen
    ```
  
  

Totality: total
Visibility: export

deriveGenFor : DeriveBodyForType => (0 a : Type) -> Elab a

  Alternative entry-point function of automatic derivation of `Gen`'s.
  
  This function can be used precisely as the `deriveGen`.
  The only difference is that this function does not rely on somewhat fragile goal mechanism
  allowing the user to pass the desired type explicitly.
  
  Since Idris allows simple top-level definitions to not to contain type signature,
  one can use this derivation function as a one-liner without repetition of a desired type, e.g.
  
    ```idris
    genX = deriveGenFor $ Fuel -> (Fuel -> Gen Y) => (a : A) -> (c : C) -> Gen (b ** X a b c)
    ```

Totality: total
Visibility: export

deriveGenPrinter : {default True _ : Bool} -> {default True _ : Bool} -> DeriveBodyForType => (0 _ : Type) -> Elab ()

  Declares `main : IO Unit` function that prints derived generator for the given generator's signature
  
  Caution! When `logDerivation` is set to `True`, this function would change the global logging state
  and wouldn't turn it back.

Totality: total
Visibility: export

DefaultConstructorDerivator : DeriveBodyRhsForCon

Totality: total
Visibility: public export