Language.Reflection.Derive

Utility types and functions for automatically deriving
interface instances. So far, this module does not provide
deriving functions for existing interfaces. See
Doc.Generic4 for examples, how this could be done
using the functionality provided here.

Reexports

Definitions

record DeriveUtil : Type

  Utility type for deriving interface implementations
  automatically. See implementations of `Eq'` and `Ord'`
  in Doc.Generic4 as examples, how this can be done.

Totality: total
Visibility: public export
Constructor: 

MkDeriveUtil : ParamTypeInfo -> TTImp -> List Name -> List TTImp -> DeriveUtil

Projections:

.appliedType : DeriveUtil -> TTImp

  Fully applied data type, i.e. `var "Either" .$ var "a" .$ var "b"`

.argTypesWithParams : DeriveUtil -> List TTImp

  Types of constructor arguments where at least one
  type parameter makes an appearance. These are the
  `tpe` fields of `ExplicitArg` where `hasParam`
  is set to true and `isRecursive` is set
  to false. See the documentation of `ExplicitArg`
  when this is the case

.paramNames : DeriveUtil -> List Name

  The names of type parameters

.typeInfo : DeriveUtil -> ParamTypeInfo

  The underlying type info containing the list and names
  of data constructors plus their arguments as well as
  the data type's name and type arguments.

.typeInfo : DeriveUtil -> ParamTypeInfo

  The underlying type info containing the list and names
  of data constructors plus their arguments as well as
  the data type's name and type arguments.

Totality: total
Visibility: public export

typeInfo : DeriveUtil -> ParamTypeInfo

  The underlying type info containing the list and names
  of data constructors plus their arguments as well as
  the data type's name and type arguments.

Totality: total
Visibility: public export

.appliedType : DeriveUtil -> TTImp

  Fully applied data type, i.e. `var "Either" .$ var "a" .$ var "b"`

Totality: total
Visibility: public export

appliedType : DeriveUtil -> TTImp

  Fully applied data type, i.e. `var "Either" .$ var "a" .$ var "b"`

Totality: total
Visibility: public export

.paramNames : DeriveUtil -> List Name

  The names of type parameters

Totality: total
Visibility: public export

paramNames : DeriveUtil -> List Name

  The names of type parameters

Totality: total
Visibility: public export

.argTypesWithParams : DeriveUtil -> List TTImp

  Types of constructor arguments where at least one
  type parameter makes an appearance. These are the
  `tpe` fields of `ExplicitArg` where `hasParam`
  is set to true and `isRecursive` is set
  to false. See the documentation of `ExplicitArg`
  when this is the case

Totality: total
Visibility: public export

argTypesWithParams : DeriveUtil -> List TTImp

  Types of constructor arguments where at least one
  type parameter makes an appearance. These are the
  `tpe` fields of `ExplicitArg` where `hasParam`
  is set to true and `isRecursive` is set
  to false. See the documentation of `ExplicitArg`
  when this is the case

Totality: total
Visibility: public export

genericUtil : ParamTypeInfo -> DeriveUtil

  Creates a deriving utility from information about
  a (possibly) parameterized type.

Totality: total
Visibility: export

implName : DeriveUtil -> String -> Name

  Generates the name of an interface's implementation function

Totality: total
Visibility: export

record InterfaceImpl : Type

  Syntax tree and additional info about the
  implementation function of an interface.
  
  With 'implementation function', we mean the following:
  When deriving an interface implementation, the elaborator
  creates a function returning the corresponding record value.
  Values of this record should provide both the full type
  and implementation of this function as `TTImp` values.
  
  ```idris exampel
  public export
  implEqEither : {0 a : _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b)
  implEqEither = ?impl
  ```

Totality: total
Visibility: public export
Constructor: 

MkInterfaceImpl : String -> Visibility -> List FnOpt -> TTImp -> TTImp -> InterfaceImpl

Projections:

.impl : InterfaceImpl -> TTImp

  Actual implementation of the implementation function.
  This will be the right hand side of the sole pattern clause
  in the function definition.
  
  As an example, assume there is a `genEq` function used
  as an implementation for `(==)` for data types with
  some kind of `Generic` instance (see the tutorial on
  Generics for more information about this). An implementation
  for interface `Eq` could then look like this:
  
  ```idirs example
  impl = var (singleCon "Eq") .$ `(genEq) .$ `(\a,b => not (a == b))
  ```

.interfaceName : InterfaceImpl -> String

  The interface's name, for instance "Eq" ord "Ord".
  This is used to generate the name of the
  implementation function.

.options : InterfaceImpl -> List FnOpt

  Visibility of the implementation function.

.type : InterfaceImpl -> TTImp

  Full type of the implementation function, including
  implicit arguments (type parameters), which have to be part
  of the `TTImp`.
  
  See also `implementationType`, a utility function to create this
  kind of function types for type classes with a single parameter
  of type `Type`.
  
  Example:
  
  ```idirs example
  `({0 a: _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b))
  ```

.visibility : InterfaceImpl -> Visibility

  Visibility of the implementation function.

.interfaceName : InterfaceImpl -> String

  The interface's name, for instance "Eq" ord "Ord".
  This is used to generate the name of the
  implementation function.

Totality: total
Visibility: public export

interfaceName : InterfaceImpl -> String

  The interface's name, for instance "Eq" ord "Ord".
  This is used to generate the name of the
  implementation function.

Totality: total
Visibility: public export

.visibility : InterfaceImpl -> Visibility

  Visibility of the implementation function.

Totality: total
Visibility: public export

visibility : InterfaceImpl -> Visibility

  Visibility of the implementation function.

Totality: total
Visibility: public export

.options : InterfaceImpl -> List FnOpt

  Visibility of the implementation function.

Totality: total
Visibility: public export

options : InterfaceImpl -> List FnOpt

  Visibility of the implementation function.

Totality: total
Visibility: public export

.impl : InterfaceImpl -> TTImp

  Actual implementation of the implementation function.
  This will be the right hand side of the sole pattern clause
  in the function definition.
  
  As an example, assume there is a `genEq` function used
  as an implementation for `(==)` for data types with
  some kind of `Generic` instance (see the tutorial on
  Generics for more information about this). An implementation
  for interface `Eq` could then look like this:
  
  ```idirs example
  impl = var (singleCon "Eq") .$ `(genEq) .$ `(\a,b => not (a == b))
  ```

Totality: total
Visibility: public export

impl : InterfaceImpl -> TTImp

  Actual implementation of the implementation function.
  This will be the right hand side of the sole pattern clause
  in the function definition.
  
  As an example, assume there is a `genEq` function used
  as an implementation for `(==)` for data types with
  some kind of `Generic` instance (see the tutorial on
  Generics for more information about this). An implementation
  for interface `Eq` could then look like this:
  
  ```idirs example
  impl = var (singleCon "Eq") .$ `(genEq) .$ `(\a,b => not (a == b))
  ```

Totality: total
Visibility: public export

.type : InterfaceImpl -> TTImp

  Full type of the implementation function, including
  implicit arguments (type parameters), which have to be part
  of the `TTImp`.
  
  See also `implementationType`, a utility function to create this
  kind of function types for type classes with a single parameter
  of type `Type`.
  
  Example:
  
  ```idirs example
  `({0 a: _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b))
  ```

Totality: total
Visibility: public export

type : InterfaceImpl -> TTImp

  Full type of the implementation function, including
  implicit arguments (type parameters), which have to be part
  of the `TTImp`.
  
  See also `implementationType`, a utility function to create this
  kind of function types for type classes with a single parameter
  of type `Type`.
  
  Example:
  
  ```idirs example
  `({0 a: _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b))
  ```

Totality: total
Visibility: public export

deriveDecls : Name -> List (DeriveUtil -> InterfaceImpl) -> Elab (List (Decl, Decl))

  Generates a list of pairs of declarations for the
  implementations of the interfaces specified.
  
  The first elements of the pairs are type declarations, while
  the second elements are the actual implementations.
  
  This separation of type declaration and implementation
  allows us to first declare all types before declaring
  the actual implementations. This is essential in the
  implementation of `deriveMutual`.

Totality: total
Visibility: export

derive : Name -> List (DeriveUtil -> InterfaceImpl) -> Elab ()

  Given a name of a data type plus a list of interfaces, tries
  to implement these interfaces automatically using
  elaborator reflection.
  
  Again, see Doc.Generic4 for a tutorial and examples how
  to use this.

Totality: total
Visibility: export

deriveMutual : List (Name, List (DeriveUtil -> InterfaceImpl)) -> Elab ()

  Allows the derivation of mutually dependant interface
  implementations by first defining type declarations before
  declaring implementations.
  
  Note: There is no need to call this from withi a `mutual` block.

Totality: total
Visibility: export

implementationType : TTImp -> DeriveUtil -> TTImp

  Given a `TTImp` representing an interface, generates
  the type of the implementation function with all type
  parameters applied and auto implicits specified.
  
  Example: Given the `DeriveUtil` info of `Either`, this
  will generate the following type for input ``(Eq)`:
  
  ```idris example
  {0 a : _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b)
  ```
  
  Note: This function is only to be used with single-parameter
  type classes, whose type parameters are of type `Type`.

Totality: total
Visibility: export

mkEq : (a -> a -> Bool) -> Eq a

  Like `mkEq'` but generates (/=) from the passed `eq` function.

Totality: total
Visibility: public export

mkOrd : Eq a => (a -> a -> Ordering) -> Ord a

  Creates an `Ord` value from the passed comparison function
  using default implementations based on `comp` for all
  other function.

Totality: total
Visibility: public export

mkShow : (a -> String) -> Show a

  Creates a `Show` value from the passed `show` functions.

Totality: total
Visibility: public export

mkShowPrec : (Prec -> a -> String) -> Show a

  Creates a `Show` value from the passed `showPrec` functions.

Totality: total
Visibility: public export

mkDecEq : ((x1 : a) -> (x2 : a) -> Dec (x1 = x2)) -> DecEq a

  Creates a `DecEq` value from the passed implementation function
  for `decEq`

Totality: total
Visibility: public export