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

record SpecialisationParams : Type

Totality: total
Visibility: public export
Constructor: 

MkSpecParams : Bool -> SpecialisationParams

Projection: 

.eraseConNames : SpecialisationParams -> Bool

.eraseConNames : SpecialisationParams -> Bool

Totality: total
Visibility: public export

eraseConNames : SpecialisationParams -> Bool

Totality: total
Visibility: public export

SpecialisationDefaults : SpecialisationParams

Totality: total
Visibility: public 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

inNS : Monad m => Namespace -> NamespaceProvider m

Totality: total
Visibility: export

NoNS : Monad m => 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

0 snoc : All p prev -> p new -> All p (snoc prev new)

  Proof that Vect.All works over Vect.snoc

Totality: total
Visibility: export

fromListAll : (l : List t) -> {auto 0 _ : All p l} -> Subset (Vect (length l) t) (All p)

  List + List.All to Vect + Vect.All

Totality: total
Visibility: export

0 snoc : All p prev -> p new -> All p (snoc prev new)

  Proof that List.All works over List.snoc

Totality: total
Visibility: export

toListAll : (sl : SnocList Arg) -> (0 _ : All p sl) -> Subset (List Arg) (All p)

  SnocList + SnocList.All to List + List.All

Totality: total
Visibility: export

specialiseDataRaw : Monad m => NamespaceProvider m => CanUnify m => MonadLog m => MonadError SpecialisationError m => NamesInfoInTypes => SpecialisationParams => 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

normaliseTask : Elaboration m => List Arg -> TTImp -> m (TTImp, TTImp)

Totality: total
Visibility: export

specialiseDataArgs : Elaboration m => NamespaceProvider m => CanUnify m => MonadLog m => MonadError SpecialisationError m => NamesInfoInTypes => SpecialisationParams => Name -> List Arg -> TTImp -> m (TypeInfo, List Decl)

Totality: total
Visibility: export

specialiseDataLam : Monad m => Elaboration m => NamespaceProvider m => CanUnify m => MonadError SpecialisationError m => NamesInfoInTypes => SpecialisationParams => 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

specialiseDataLam'' : Elaboration m => NamespaceProvider m => CanUnify m => SpecialisationParams => 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:
  ```
  specialiseDataLam'' `{VF} $ \n => Fin n
  ```

Totality: total
Visibility: export

specialiseDataLam' : Elaboration m => NamespaceProvider m => CanUnify m => SpecialisationParams => 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 specialiseDataLam' `{VF} $ \n => Fin n
  ```

Totality: total
Visibility: export