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

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

Definitions

data Error : 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:

Show Error

data Polarity : Type

Totality: total
Visibility: public export
Constructors:

Positive : Polarity
Negative : Polarity

not : Polarity -> Polarity

Totality: total
Visibility: public export

data IsFunctorialIn : 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 : IsFunctorialIn Positive t x (IVar fc x)

  The type variable x occurs alone

FIRec : (0 _ : IsAppView ({_:4466}, t) {_:4467} f) -> IsFunctorialIn pol t x arg -> IsFunctorialIn Positive t x (IApp fc f arg)

  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 : IsFunctorialIn pol t x ty -> IsFunctorialIn pol t x (IDelayed fc lr ty)

  The subterm is delayed (either Inf or Lazy)

FIBifun : IsFreeOf x sp -> HasImplementation Bifunctor sp -> IsFunctorialIn pol t x arg1 -> Either (IsFunctorialIn pol t x arg2) (IsFreeOf x arg2) -> IsFunctorialIn pol t x (IApp fc1 (IApp fc2 sp arg1) arg2)

  There are nested subtrees somewhere inside a 3rd party type constructor
  which satisfies the Bifunctor interface

FIFun : IsFreeOf x sp -> HasImplementation Functor sp -> IsFunctorialIn pol t x arg -> IsFunctorialIn pol t x (IApp fc sp arg)

  There are nested subtrees somewhere inside a 3rd party type constructor
  which satisfies the Functor interface

FIPi : IsFunctorialIn (not pol) t x a -> IsFunctorialIn pol t x b -> IsFunctorialIn pol t x (IPi fc rig pinfo nm a b)

  A pi type, with no negative occurrence of x in its domain

FIFree : IsFreeOf x a -> IsFunctorialIn pol t x a

  A type free of x is trivially Functorial in it

TypeView : Elaboration m => MonadError Error m => MonadState Parameters m => 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 : {auto elab : Elaboration m} -> {auto error : MonadError Error m} -> {auto cs : MonadState Parameters m} -> (t : Name) -> (ps : List (Name, Nat)) -> (x : Name) -> TypeView pol ty -> IsFunctorialIn pol t x ty

Totality: total
Visibility: export

typeView : {auto elab : Elaboration m} -> {auto error : MonadError Error m} -> {auto cs : MonadState Parameters m} -> (t : Name) -> (ps : List (Name, Nat)) -> (x : Name) -> (ty : TTImp) -> m (TypeView pol ty)

  Hoping to observe that ty is functorial

Totality: total
Visibility: export

derive : {default Private _ : Visibility} -> {default Total _ : TotalReq} -> {default [] _ : List Name} -> Elab (Functor f)

  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