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.

Definitions

interface Elaborateable : Type -> Type

  Interface for named things that can be looked up by name using
  elaborator reflection.

Parameters: a
Constraints: Named a
Methods:

find_ : Elaboration m => Name -> m a

Implementation: 

Elaborateable TypeInfo

find_ : Elaborateable a => Elaboration m => Name -> m a

Totality: total
Visibility: public export

find : (0 a : Type) -> Elaborateable a => Elaboration m => Name -> m a

  Utility version of `find_` taking an explicit type argument.

Totality: total
Visibility: public export

funName : Named a => a -> String -> Name

  Generates the name of a function implementing some functionality
  for the given type.

Totality: total
Visibility: export

implName : Named a => a -> String -> Name

  Generates the name of an interface's implementation function

Totality: total
Visibility: export

record BoundArg : Nat -> (Arg -> Type) -> Type

  A single constructor argument, for which we have `n` bound
  variables on the left hand side of a pattern match clause, and
  which is refined by predicate `p`.

Totality: total
Visibility: public export
Constructor: 

BA : (arg : Arg) -> Vect n Name -> p arg -> BoundArg n p

Projections:

.arg : BoundArg n p -> Arg

.prf : ({rec:0} : BoundArg n p) -> p (arg {rec:0})

.vars : BoundArg n p -> Vect n Name

.arg : BoundArg n p -> Arg

Totality: total
Visibility: public export

arg : BoundArg n p -> Arg

Totality: total
Visibility: public export

.vars : BoundArg n p -> Vect n Name

Totality: total
Visibility: public export

vars : BoundArg n p -> Vect n Name

Totality: total
Visibility: public export

.prf : ({rec:0} : BoundArg n p) -> p (arg {rec:0})

Totality: total
Visibility: public export

prf : ({rec:0} : BoundArg n p) -> p (arg {rec:0})

Totality: total
Visibility: public export

split : Vect k (Vect (S n) a) -> (Vect k a, Vect k (Vect n a))

Totality: total
Visibility: public export

boundArgs : ((a : Arg) -> Maybe (p a)) -> Vect n Arg -> Vect k (Vect n Name) -> SnocList (BoundArg k p)

  Refine a list of constructor arguments with the given predicate
  and pair them with a number of bound variable names.

Totality: total
Visibility: export

data Explicit : Arg -> Type

Totality: total
Visibility: public export
Constructor: 

IsExplicit : Explicit (MkArg c ExplicitArg n t)

explicit : (a : Arg) -> Maybe (Explicit a)

Totality: total
Visibility: public export

data NamedArg : Arg -> Type

Totality: total
Visibility: public export
Constructor: 

IsNamed : NamedArg (MkArg c p (Just (UN (Basic n))) t)

named : (a : Arg) -> Maybe (NamedArg a)

Totality: total
Visibility: public export

argName : (a : Arg) -> {auto 0 _ : NamedArg a} -> Name

Totality: total
Visibility: public export

data Unerased : Arg -> Type

Totality: total
Visibility: public export
Constructors:

U1 : Unerased (MkArg M1 p n t)

UW : Unerased (MkArg MW p n t)

unerased : (a : Arg) -> Maybe (Unerased a)

Totality: total
Visibility: public export

data Erased : Arg -> Type

Totality: total
Visibility: public export
Constructor: 

IsErased : Erased (MkArg M0 p n t)

erased : (a : Arg) -> Maybe (Erased a)

Totality: total
Visibility: public export

0 Regular : Arg -> Type

Totality: total
Visibility: public export

regular : (a : Arg) -> Maybe (Regular a)

Totality: total
Visibility: public export

0 RegularNamed : Arg -> Type

Totality: total
Visibility: public export

regularNamed : (a : Arg) -> Maybe (RegularNamed a)

Totality: total
Visibility: public export

0 NamedExplicit : Arg -> Type

Totality: total
Visibility: public export

namedExplicit : (a : Arg) -> Maybe (NamedExplicit a)

Totality: total
Visibility: public export

toNamed : BoundArg n p -> Maybe (BoundArg n (\a => (NamedArg a, p a)))

Totality: total
Visibility: public export

failRecord : String -> Res a

Totality: total
Visibility: export

accumArgs : ((a : Arg) -> Maybe (p a)) -> (TTImp -> TTImp) -> (SnocList TTImp -> TTImp) -> (BoundArg 1 p -> TTImp) -> Con n vs -> Clause

  Generates a pattern clause for accumulating the arguments
  of a singled data constructor.
  
  This is used, for instance, to implement `showPrec`, when
  deriving `Show` implementations.
  
  @ p   : The predicate used to refine the constructor's arguments
  
  @ f   : Refining function.
  
  @ lhs : Adjusts the left-hand side of the clause.
          The argument corresponds to the constructor with
          all explicit arguments bound to variables named
          `x0`, `x1` etc.
  
  @ rhs : Adjusts the right-hand side of the clause.
          The `SnocList` contains the arguments, as transformed
          by `arg`.
  
  @ arg : Processes a single argument
  
  @ con : The constructor to process.

Totality: total
Visibility: export

accumArgs2 : ((a : Arg) -> Maybe (p a)) -> (TTImp -> TTImp -> TTImp) -> (SnocList TTImp -> TTImp) -> (BoundArg 2 p -> TTImp) -> Con n vs -> Clause

  Generates a pattern clause for accumulating the arguments
  of two equivalent data constructors.
  
  This is used, for instance, to implement `(==)`, when
  deriving `Eq` implementations.
  
  @ p   : The predicate used to refine the constructor's arguments
  
  @ f   : Refining function.
  
  @ lhs : Adjusts the left-hand side of the clause.
          The first argument corresponds to the constructor with
          all explicit arguments bound to variables named
          `x0`, `x1` etc., the second to the constructor
          with bound explicit arguments namd `y0`, `y1` etc.
  
  @ rhs : Adjusts the right-hand side of the clause.
          The `SnocList` contains the arguments, as transformed
          by `arg`.
  
  @ arg : Processes a single pair of arguments
  
  @ con : The constructor to process.

Totality: total
Visibility: export

mapArgs : ((a : Arg) -> Maybe (p a)) -> (TTImp -> TTImp) -> (BoundArg 1 p -> TTImp) -> Con n vs -> Clause

  Generates a pattern clause for mapping the arguments
  of a data constructors over a unary function.
  
  This is used, for instance, to implement `abs`, when
  deriving `Abs` implementations.
  
  @ p   : The predicate used to refine the constructor's arguments
  
  @ f   : Refining function.
  
  @ lhs : Adjusts the left-hand side of the clause.
          The argument corresponds to the constructor with
          all explicit arguments bound to variables named
          `x0`, `x1` etc.
  
  @ arg : Processes a single argument
  
  @ con : The constructor to process.

Totality: total
Visibility: export

mapArgs2 : ((a : Arg) -> Maybe (p a)) -> (TTImp -> TTImp -> TTImp) -> (BoundArg 2 p -> TTImp) -> Con n vs -> Clause

  Generates a pattern clause for mapping the arguments
  of two data constructors over a binary function.
  
  This is used, for instance, to implement `(+)`, when
  deriving `Num` implementations.
  
  @ p   : The predicate used to refine the constructor's arguments
  
  @ f   : Refining function.
  
  @ lhs : Adjusts the left-hand side of the clause.
          The first argument corresponds to the constructor with
          all explicit arguments bound to variables named
          `x0`, `x1` etc., the second to the constructor
          with bound explicit arguments namd `y0`, `y1` etc.
  
  @ arg : Processes a pair of arguments
  
  @ con : The constructor to process.

Totality: total
Visibility: export

injArgs : ((a : Arg) -> Maybe (p a)) -> (BoundArg 0 p -> TTImp) -> Con n vs -> TTImp

  Generates a pattern clause for creating and applying
  constructor arguments.
  
  This is used, for instance, to implement `fromInteger`, when
  deriving `Num` implementations for record types.
  
  @ p   : The predicate used to refine the constructor's arguments
  
  @ f   : Refining function.
  
  @ arg : Processes a single argument
  
  @ con : The constructor to process.

Totality: total
Visibility: export

record TopLevel : Type

  A top-level declaration plus its definition.

Totality: total
Visibility: public export
Constructor: 

TL : Decl -> Decl -> TopLevel

Projections:

.claim : TopLevel -> Decl

.defn : TopLevel -> Decl

.claim : TopLevel -> Decl

Totality: total
Visibility: public export

claim : TopLevel -> Decl

Totality: total
Visibility: public export

.defn : TopLevel -> Decl

Totality: total
Visibility: public export

defn : TopLevel -> Decl

Totality: total
Visibility: public export

implClaimVis : Visibility -> Name -> TTImp -> Decl

  Creates a function declaration with a `%hint` and `%inline`
  annotation.
  
  This is what you want if you use separate top-level function
  for the interface's implementation and the actual implementation
  just adds those functions to the interface constructor.

Totality: total
Visibility: public export

implClaim : Name -> TTImp -> Decl

  Creates a function declaration with a `%hint` and `%inline`
  annotation.
  
  This is what you want if you use separate top-level function
  for the interface's implementation and the actual implementation
  just adds those functions to the interface constructor.

Totality: total
Visibility: public export

implType : Name -> ParamTypeInfo -> TTImp

  Creates the function type for an interface implementation including
  the required implicit and auto-implicit arguments.
  
  For instance, if `Name` is `"Eq"` and the data type in question is
  `Either` with parameter names `a` and `b`, the `TTImp` returned
  corresponds to
  
  ```idris
  {0 a : _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b)`
  ```

Totality: total
Visibility: export

unAppAny : TTImp -> TTImp

  Extracts the innermost target of a function application.
  For instance, for `Foo @{bar} baz {n = 12}`, this will extract `Foo`.

Totality: total
Visibility: export

extractResult : TTImp -> Maybe (TTImp, Name)

  Tries to extract the result type from the current goal when
  deriving custom interface implementations.
  
  For instance, if the goal type is `Eq (Either a b)`, this
  returns a `TTImp` corresponding to `Either a b` plus the
  name of the data constructor `Either`.

Totality: total
Visibility: export

sequenceJoin : Applicative f => List (f (List a)) -> f (List a)

Totality: total
Visibility: export

record ParamInfo : Type

Totality: total
Visibility: public export
Constructor: 

PI : Name -> ((n : Nat) -> Maybe (Exists Nat (ParamPattern n))) -> List (List Name -> ParamTypeInfo -> Res (List TopLevel)) -> ParamInfo

Projections:

.goals : ParamInfo -> List (List Name -> ParamTypeInfo -> Res (List TopLevel))

.name : ParamInfo -> Name

.strategy : ParamInfo -> (n : Nat) -> Maybe (Exists Nat (ParamPattern n))

.name : ParamInfo -> Name

Totality: total
Visibility: public export

name : ParamInfo -> Name

Totality: total
Visibility: public export

.strategy : ParamInfo -> (n : Nat) -> Maybe (Exists Nat (ParamPattern n))

Totality: total
Visibility: public export

strategy : ParamInfo -> (n : Nat) -> Maybe (Exists Nat (ParamPattern n))

Totality: total
Visibility: public export

.goals : ParamInfo -> List (List Name -> ParamTypeInfo -> Res (List TopLevel))

Totality: total
Visibility: public export

goals : ParamInfo -> List (List Name -> ParamTypeInfo -> Res (List TopLevel))

Totality: total
Visibility: public export

deriveParam : Elaboration m => List ParamInfo -> m ()

Totality: total
Visibility: export

allParams : (n : Nat) -> Maybe (Exists Nat (ParamPattern n))

Totality: total
Visibility: export

allIndices : (n : Nat) -> Maybe (Exists Nat (ParamPattern n))

Totality: total
Visibility: export

match : ParamPattern m k -> (n : Nat) -> Maybe (Exists Nat (ParamPattern n))

Totality: total
Visibility: export

deriveMutual : Elaboration m => List Name -> List (List Name -> ParamTypeInfo -> Res (List TopLevel)) -> m ()

Totality: total
Visibility: export

derive : Elaboration m => Name -> List (List Name -> ParamTypeInfo -> Res (List TopLevel)) -> m ()

  Given a name of a parameterized data type plus a list of
  interface generation functions, 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

deriveIndexed : Elaboration m => Name -> List (List Name -> ParamTypeInfo -> Res (List TopLevel)) -> m ()

Totality: total
Visibility: export

derivePattern : Elaboration m => Name -> ParamPattern n k -> List (List Name -> ParamTypeInfo -> Res (List TopLevel)) -> m ()

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