Idris2Doc : 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


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


fromFoldMap : (0f : (Type->Type)) -> (Monoidb=> (a->b) ->fa->b) ->Foldablef
Totality: total
Visibility: public export
dataError : Type
  Possible errors for the functor-deriving machinery.

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

dataIsFoldableIn : 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
FIVar : IsFoldableIntx (IVarfcx)
  The type variable x occurs alone
FIRec : (0_ : IsAppView ({_:4781}, t) {_:4782}f) ->IsFoldableIntxarg->IsFoldableIntx (IAppfcfarg)
  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 : IsFoldableIntxty->IsFoldableIntx (IDelayedfcLLazyty)
  The subterm is delayed (Lazy only, we can't fold over infinite structures)
FIBifold : IsFreeOfxsp->HasImplementationBifoldablesp->IsFoldableIntxarg1->Either (IsFoldableIntxarg2) (IsFreeOfxarg2) ->IsFoldableIntx (IAppfc1 (IAppfc2sparg1) arg2)
  There are nested subtrees somewhere inside a 3rd party type constructor
which satisfies the Bifoldable interface
FIFold : IsFreeOfxsp->HasImplementationFoldablesp->IsFoldableIntxarg->IsFoldableIntx (IAppfcsparg)
  There are nested subtrees somewhere inside a 3rd party type constructor
which satisfies the Foldable interface
FIFree : IsFreeOfxa->IsFoldableIntxa
  A type free of x is trivially Foldable in it
TypeView : Elaborationm=>MonadErrorErrorm=>MonadStateParametersm=>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 : {autoelab : Elaborationm} -> {autoerror : MonadErrorErrorm} -> {autocs : MonadStateParametersm} -> (t : Name) -> (ps : List (Name, Nat)) -> (x : Name) ->TypeViewty->IsFoldableIntxty
Totality: total
Visibility: export
typeView : {autoelab : Elaborationm} -> {autoerror : MonadErrorErrorm} -> {autocs : MonadStateParametersm} -> (t : Name) -> (ps : List (Name, Nat)) -> (x : Name) -> (ty : TTImp) ->m (TypeViewty)
  Hoping to observe that ty is foldable

Totality: total
Visibility: export
derive : {defaultPrivate_ : Visibility} -> {defaultTotal_ : TotalReq} -> {default [] _ : ListName} ->Elab (Foldablef)
  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