Deriving.SpecialiseData

Reexports

Definitions

data SpecialisationError : Type

  Specialisation error

Totality: total
Visibility: export
Constructors:

TaskTypeExtractionError : SpecialisationError

  Failed to extract polymorphic type name from task

UnusedVarError : SpecialisationError

  Unused variable

PartialSpecError : SpecialisationError

  Partial specification

InternalError : String -> SpecialisationError

  Internal error

UnnamedArgInLambdaError : SpecialisationError

  Lambda has unnamed arguments

UnnamedArgInPolyTyError : Name -> SpecialisationError

  Polymorphic type has unnamed arguments

MissingTypeInfoError : Name -> SpecialisationError

  Failed to get TypeInfo
  
  Can occur either due to trying to specialise a non-type invocation
  or due to not having the necessary TypeInfo in the NamesInfoInTypes instance

Hint: 

Show SpecialisationError

showSE : Show SpecialisationError

Totality: total
Visibility: export

interface NamespaceProvider : (Type -> Type) -> Type

Parameters: m
Constructor: 

MkNSProvider

Methods:

provideNS : m Namespace

Implementation: 

Monad m => MonadTrans t => NamespaceProvider m => NamespaceProvider (t m)

provideNS : NamespaceProvider m => m Namespace

Totality: total
Visibility: public export

CurrentNS : Elaboration m => NamespaceProvider m

Totality: total
Visibility: export

inNS : Monad m => Namespace -> NamespaceProvider m

Totality: total
Visibility: export

.apply : (ti : TypeInfo) -> {auto 0 _ : AllTyArgsNamed ti} -> (Name -> TTImp) -> SortedMap Name TTImp -> TTImp

  Returns a full application of the given type constructor
  with argument values sourced from `argValues`
  or generated with `fallback` if not present

Totality: total
Visibility: export

.apply : (con : Con) -> {auto 0 _ : ConArgsNamed con} -> (Name -> TTImp) -> SortedMap Name TTImp -> TTImp

  Returns a full application of the given constructor
  with argument values sourced from `argValues`
  or generated with `fallback` if not present

Totality: total
Visibility: export

interface TaskLambda : Type -> Type

  Valid task lambda interface
  
  Auto-implemented by any Type or any function that returns Type.

Parameters: t
Implementations:

TaskLambda Type

TaskLambda b => TaskLambda (a -> b)

TaskLambda b => TaskLambda (a => b)

TaskLambda b => TaskLambda b

TaskLambda b => TaskLambda ((0 _ : a) -> b)

TaskLambda b => TaskLambda ({auto 0 _ : a} -> b)

TaskLambda b => TaskLambda b

specialiseDataRaw : Monad m => NamespaceProvider m => CanUnify m => MonadLog m => MonadError SpecialisationError m => NamesInfoInTypes => Name -> TTImp -> TTImp -> m (TypeInfo, List Decl)

  Perform a specialisation for a given type name, kind and content expressions
  
  In order to generate a specialised type declaration equivalent to the following type alias:
  ```
  VF : Nat -> Type
  VF n = Fin n
  ```
  ...you may use this function as follows:
  ```
  specialiseDataRaw `{VF} `(Nat -> Type) `(\n => Fin n)
  ```

Totality: total
Visibility: export

specialiseData : TaskLambda taskT => Monad m => Elaboration m => NamespaceProvider m => CanUnify m => MonadError SpecialisationError m => NamesInfoInTypes => Name -> (0 _ : taskT) -> m (TypeInfo, List Decl)

  Perform a specialisation for a given type name and content lambda
  
  In order to generate a specialised type declaration equivalent to the following type alias:
  ```
  VF : Nat -> Type
  VF n = Fin n
  ```
  ...you may use this function as follows:
  ```
  specialiseData `{VF} $ \n => Fin n
  ```

Totality: total
Visibility: export

specialiseData'' : Elaboration m => NamespaceProvider m => CanUnify m => TaskLambda taskT => Name -> (0 _ : taskT) -> m (List Decl)

  Perform a specialisation for a given type name and content lambda,
  returning a list of declarations and failing on error
  
  In order to generate a specialised type declaration equivalent to the following type alias:
  ```
  VF : Nat -> Type
  VF n = Fin n
  ```
  ...you may use this function as follows:
  ```
  specialiseData'' `{VF} $ \n => Fin n
  ```

Totality: total
Visibility: export

specialiseData' : Elaboration m => NamespaceProvider m => CanUnify m => TaskLambda taskT => Name -> (0 _ : taskT) -> m ()

  Perform a specialisation for a given type name and content lambda,
  declaring the results and failing on error
  
  In order to declare a specialised type declaration equivalent to the following type alias:
  ```
  VF : Nat -> Type
  VF n = Fin n
  ```
  ...you may use this function as follows:
  ```
  %runElab specialiseData' `{VF} $ \n => Fin n
  ```

Totality: total
Visibility: export