Deriving.Foldable

Deriving foldable instances using reflection
You can for instance define:
```
data Tree a = Leaf a | Node (Tree a) (Tree a)
treeFoldable : Foldable 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

fromFoldMap : (0 f : (Type -> Type)) -> (Monoid b => (a -> b) -> f a -> b) -> Foldable f

Totality: total
Visibility: public export

data Error : Type

  Possible errors for the functor-deriving machinery.

Totality: total
Visibility: public export
Constructors:

NotFreeOf : Name -> TTImp -> Error
NotAnApplication : TTImp -> Error
NotAFoldable : TTImp -> Error
NotABifoldable : TTImp -> Error
NotFoldableInItsLastArg : 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 IsFoldableIn : Name -> Name -> TTImp -> Type

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

Totality: total
Visibility: public export
Constructors:

FIVar : IsFoldableIn t x (IVar fc x)

  The type variable x occurs alone

FIRec : (0 _ : IsAppView ({_:4781}, t) {_:4782} f) -> IsFoldableIn t x arg -> IsFoldableIn t x (IApp fc f arg)

  There is a recursive subtree of type (t a1 ... an u) and u is Foldable 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 : IsFoldableIn t x ty -> IsFoldableIn t x (IDelayed fc LLazy ty)

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

FIBifold : IsFreeOf x sp -> HasImplementation Bifoldable sp -> IsFoldableIn t x arg1 -> Either (IsFoldableIn t x arg2) (IsFreeOf x arg2) -> IsFoldableIn t x (IApp fc1 (IApp fc2 sp arg1) arg2)

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

FIFold : IsFreeOf x sp -> HasImplementation Foldable sp -> IsFoldableIn t x arg -> IsFoldableIn t x (IApp fc sp arg)

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

FIFree : IsFreeOf x a -> IsFoldableIn t x a

  A type free of x is trivially Foldable 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 foldable 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 -> IsFoldableIn 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 foldable

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export