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


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


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

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

dataIsTraversableIn : 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
TIVar : IsTraversableIntx (IVarfcx)
  The type variable x occurs alone
TIRec : (0_ : IsAppView ({_:4523}, t) {_:4524}f) ->IsTraversableIntxarg->IsTraversableIntx (IAppfcfarg)
  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 : IsTraversableIntxty->IsTraversableIntx (IDelayedfcLLazyty)
  The subterm is delayed (Lazy only, we can't traverse infinite structures)
TIBifold : IsFreeOfxsp->HasImplementationBitraversablesp->IsTraversableIntxarg1->Either (IsTraversableIntxarg2) (IsFreeOfxarg2) ->IsTraversableIntx (IAppfc1 (IAppfc2sparg1) arg2)
  There are nested subtrees somewhere inside a 3rd party type constructor
which satisfies the Bitraversable interface
TIFold : IsFreeOfxsp->HasImplementationTraversablesp->IsTraversableIntxarg->IsTraversableIntx (IAppfcsparg)
  There are nested subtrees somewhere inside a 3rd party type constructor
which satisfies the Traversable interface
TIFree : IsFreeOfxa->IsTraversableIntxa
  A type free of x is trivially Traversable 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 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 : {autoelab : Elaborationm} -> {autoerror : MonadErrorErrorm} -> {autocs : MonadStateParametersm} -> (t : Name) -> (ps : List (Name, Nat)) -> (x : Name) ->TypeViewty->IsTraversableIntxty
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 traversable

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