Deriving.Show

Deriving show instances using reflection
You can for instance define:
```
data Tree a = Leaf a | Node (Tree a) (Tree a)
treeShow : Show a => Show (Tree a)
treeShow = %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

fromShowPrec : (Prec -> ty -> String) -> Show ty

Totality: total
Visibility: public export

data Error : Type

  Possible errors for the functor-deriving machinery.

Totality: total
Visibility: public export
Constructors:

NotAShowable : Name -> 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 IsShowable : Name -> TTImp -> Type

Totality: total
Visibility: public export
Constructors:

ISDelayed : IsShowable t ty -> IsShowable t (IDelayed fc LLazy ty)

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

ISRec : (0 _ : IsAppView ({_:4388}, t) {_:4389} ty) -> IsShowable t ty

  There is a recursive subtree of type (t a1 ... an)

ISShowN : (0 _ : IsAppView ({_:4416}, tcon) args ty) -> HasType tcon tconty -> IsProvable (ShowN tconty tcon) -> IsShowableArgs t tconty (args <>> []) -> IsShowable t ty

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

ISParam : IsShowable t ty

  Or we could be referring to one of the parameters

ISPrim : (ty : PrimType) -> IsShowable t (IPrimVal fc (PrT ty))

  A primitive type is trivially Showable

typeView : Elaboration m => MonadError Error m => MonadState Parameters m => (t : Name) -> List (Name, Nat) -> (ty : TTImp) -> m (IsShowable t ty)

  Hoping to observe that ty can be shown

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export