Deriving.Traversable

Deriving traversable instances using reflection
You can for instance define:
```
data Tree a = Leaf a | Node (Tree a) (Tree a)
treeFoldable : Traversable Tree
treeFoldable = %runElab derive
```

Reexports

import public Control.Monad.Either
import public Control.Monad.State
import public Data.List1
import public Data.Maybe
import public Data.Morphisms
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
NotAnApplication : TTImp -> Error
NotATraversable : TTImp -> Error
NotABitraversable : TTImp -> Error
NotTraversableInItsLastArg : TTImp -> Error
UnsupportedType : TTImp -> Error
NotAFiniteStructure : Error
NotAnUnconstrainedValue : Count -> Error
InvalidGoal : Error
ConfusingReturnType : Error
WhenCheckingConstructor : Name -> Error -> Error
WhenCheckingArg : TTImp -> Error -> Error

Hint:

Show Error

data IsTraversableIn : Name -> Name -> TTImp -> Type

  IsTraversableIn is parametrised by
  @ t  the name of the data type whose constructors are being analysed
  @ x  the name of the type variable that the traversable action will act on
  @ ty the type being analysed
  The inductive type delivers a proof that x can be traversed over in ty,
  assuming that t also is traversable.

Totality: total
Visibility: public export
Constructors:

TIVar : IsTraversableIn t x (IVar fc x)

  The type variable x occurs alone

TIRec : (0 _ : IsAppView ({_:4523}, t) {_:4524} f) -> IsTraversableIn t x arg -> IsTraversableIn t x (IApp fc f arg)

  There is a recursive subtree of type (t a1 ... an u) and u is Traversable 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))

TIDelayed : IsTraversableIn t x ty -> IsTraversableIn t x (IDelayed fc LLazy ty)

  The subterm is delayed (Lazy only, we can't traverse infinite structures)

TIBifold : IsFreeOf x sp -> HasImplementation Bitraversable sp -> IsTraversableIn t x arg1 -> Either (IsTraversableIn t x arg2) (IsFreeOf x arg2) -> IsTraversableIn t x (IApp fc1 (IApp fc2 sp arg1) arg2)

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

TIFold : IsFreeOf x sp -> HasImplementation Traversable sp -> IsTraversableIn t x arg -> IsTraversableIn t x (IApp fc sp arg)

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

TIFree : IsFreeOf x a -> IsTraversableIn t x a

  A type free of x is trivially Traversable in it

TypeView : Elaboration m => MonadError Error m => MonadState Parameters m => Name -> List (Name, Nat) -> Name -> TTImp -> Type

  When analysing the type of a constructor for the type family t,
  we hope to observe
    1. either that it is traversable in x
    2. or that it is free of x
  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 ty -> IsTraversableIn 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 ty)

  Hoping to observe that ty is traversable

Totality: total
Visibility: export

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

  Derive an implementation of Traversable for a type constructor.
  This can be used like so:
  ```
  data Tree a = Leaf a | Node (Tree a) (Tree a)
  treeTraversable : Traversable Tree
  treeTraversable = %runElab derive
  ```

Totality: total
Visibility: export