Idris2Doc : Deriving.Functor

Deriving.Functor

Deriving functor instances using reflection
You can for instance define:
```
data Tree a = Leaf a | Node (Tree a) (Tree a)
treeFunctor : Functor Tree
treeFunctor = %runElab derive
```

Reexports

importpublic Control.Monad.Either
importpublic Control.Monad.State
importpublic Data.Maybe
importpublic Decidable.Equality
importpublic Language.Reflection
importpublic Deriving.Common

Definitions

dataError : Type
  Possible errors for the functor-deriving machinery.

Totality: total
Visibility: public export
Constructors:
NotFreeOf : Name->TTImp->Error
NegativeOccurrence : Name->TTImp->Error
NotAnApplication : TTImp->Error
NotAFunctor : TTImp->Error
NotABifunctor : TTImp->Error
NotAFunctorInItsLastArg : TTImp->Error
UnsupportedType : TTImp->Error
InvalidGoal : Error
ConfusingReturnType : Error
WhenCheckingConstructor : Name->Error->Error
WhenCheckingArg : TTImp->Error->Error

Hint: 
ShowError
dataPolarity : Type
Totality: total
Visibility: public export
Constructors:
Positive : Polarity
Negative : Polarity
not : Polarity->Polarity
Totality: total
Visibility: public export
dataIsFunctorialIn : Polarity->Name->Name->TTImp->Type
  IsFunctorialIn is parametrised by
@ pol the polarity of the type being analysed. We start in positive polarity
where occurrences of x are allowed and negate the polarity every time
we step into the domain of a Pi type.
@ t the name of the data type whose constructors are being analysed
@ x the name of the type variable that the functioral action will change
@ ty the type being analysed
The inductive type delivers a proof that x occurs positively in ty,
assuming that t also is positive.

Totality: total
Visibility: public export
Constructors:
FIVar : IsFunctorialInPositivetx (IVarfcx)
  The type variable x occurs alone
FIRec : (0_ : IsAppView ({_:4466}, t) {_:4467}f) ->IsFunctorialInpoltxarg->IsFunctorialInPositivetx (IAppfcfarg)
  There is a recursive subtree of type (t a1 ... an u) and u is functorial in x.
We do not insist that u is exactly x so that we can deal with nested types
like the following:
data Full a = Leaf a | Node (Full (a, a))
data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))
FIDelayed : IsFunctorialInpoltxty->IsFunctorialInpoltx (IDelayedfclrty)
  The subterm is delayed (either Inf or Lazy)
FIBifun : IsFreeOfxsp->HasImplementationBifunctorsp->IsFunctorialInpoltxarg1->Either (IsFunctorialInpoltxarg2) (IsFreeOfxarg2) ->IsFunctorialInpoltx (IAppfc1 (IAppfc2sparg1) arg2)
  There are nested subtrees somewhere inside a 3rd party type constructor
which satisfies the Bifunctor interface
FIFun : IsFreeOfxsp->HasImplementationFunctorsp->IsFunctorialInpoltxarg->IsFunctorialInpoltx (IAppfcsparg)
  There are nested subtrees somewhere inside a 3rd party type constructor
which satisfies the Functor interface
FIPi : IsFunctorialIn (notpol) txa->IsFunctorialInpoltxb->IsFunctorialInpoltx (IPifcrigpinfonmab)
  A pi type, with no negative occurrence of x in its domain
FIFree : IsFreeOfxa->IsFunctorialInpoltxa
  A type free of x is trivially Functorial in it
TypeView : Elaborationm=>MonadErrorErrorm=>MonadStateParametersm=>Name->List (Name, Nat) ->Name->Polarity->TTImp->Type
  When analysing the type of a constructor for the type family t,
we hope to observe
1. either that it is functorial in x
2. or that it is free of x
If if it is not the case, we will use the `MonadError Error` constraint
to fail with an informative message.

Totality: total
Visibility: public export
fromTypeView : {autoelab : Elaborationm} -> {autoerror : MonadErrorErrorm} -> {autocs : MonadStateParametersm} -> (t : Name) -> (ps : List (Name, Nat)) -> (x : Name) ->TypeViewpolty->IsFunctorialInpoltxty
Totality: total
Visibility: export
typeView : {autoelab : Elaborationm} -> {autoerror : MonadErrorErrorm} -> {autocs : MonadStateParametersm} -> (t : Name) -> (ps : List (Name, Nat)) -> (x : Name) -> (ty : TTImp) ->m (TypeViewpolty)
  Hoping to observe that ty is functorial

Totality: total
Visibility: export
derive : {defaultPrivate_ : Visibility} -> {defaultTotal_ : TotalReq} -> {default [] _ : ListName} ->Elab (Functorf)
  Derive an implementation of Functor for a type constructor.
This can be used like so:
```
data Tree a = Leaf a | Node (Tree a) (Tree a)
treeFunctor : Functor Tree
treeFunctor = %runElab derive
```

Totality: total
Visibility: export