Idris2Doc : Data.Uniplate

Data.Uniplate

(source)
Definitions
data Repr : Type
  How the children of a given node are represented

  Totality: total
  Visibility: public export
  Constructors:
  
RZero : Repr
  
ROne : Repr
  
RTwo : Repr -> Repr -> Repr

  Hints:
  
Foldable (Children repr)
  
Functor (Children repr)
  
Traversable (Children repr)
data Children : Repr -> Type -> Type
  The children of a node

  Totality: total
  Visibility: public export
  Constructors:
  
Zero : Children RZero a
  
One : a -> Children ROne a
  
Two : Children l a -> Children r a -> Children (RTwo l r) a

  Hints:
  
Foldable (Children repr)
  
Functor (Children repr)
  
Traversable (Children repr)
record Plate : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkPlate : Children repr to -> (Children repr to -> from) -> Plate from to

  Projections:
  
.cs : ({rec:0} : Plate from to) -> Children (repr {rec:0}) to
  
.gen : ({rec:0} : Plate from to) -> Children (repr {rec:0}) to -> from
  
0 .repr : Plate from to -> Repr
0 .repr : Plate from to -> Repr
  Totality: total
  Visibility: public export
0 repr : Plate from to -> Repr
  Totality: total
  Visibility: public export
.cs : ({rec:0} : Plate from to) -> Children (repr {rec:0}) to
  Totality: total
  Visibility: public export
cs : ({rec:0} : Plate from to) -> Children (repr {rec:0}) to
  Totality: total
  Visibility: public export
.gen : ({rec:0} : Plate from to) -> Children (repr {rec:0}) to -> from
  Totality: total
  Visibility: public export
gen : ({rec:0} : Plate from to) -> Children (repr {rec:0}) to -> from
  Totality: total
  Visibility: public export
interface Uniplate : Type -> Type
  Parameters: ty
Methods:
  
uniplate : ty -> Plate ty ty
  Get the direct children of a node
  and a way to rebuild that node with modified children
  
descend : (ty -> ty) -> ty -> ty
  
descendM : Applicative m => (ty -> m ty) -> ty -> m ty

Implementations:
  
Uniplate (List a)
  
Uniplate (SnocList a)
uniplate : Uniplate ty => ty -> Plate ty ty
  Get the direct children of a node
  and a way to rebuild that node with modified children

  Totality: total
  Visibility: public export
descend : Uniplate ty => (ty -> ty) -> ty -> ty
  Totality: total
  Visibility: public export
descendM : Uniplate ty => Applicative m => (ty -> m ty) -> ty -> m ty
  Totality: total
  Visibility: public export
interface Biplate : Type -> Type -> Type
  Parameters: from, to
Constraints: Uniplate to
Methods:
  
biplate : from -> Plate from to
  
bidescend : (to -> to) -> from -> from
  
bidescendM : Applicative m => (to -> m to) -> from -> m from

Implementations:
  
Biplate (List a) a
  
Biplate (Maybe a) a
  
Biplate (SnocList a) a
  
Biplate (Vect len a) a
  
Biplate (List1 a) a
  
Biplate String Char
biplate : Biplate from to => from -> Plate from to
  Totality: total
  Visibility: public export
bidescend : Biplate from to => (to -> to) -> from -> from
  Totality: total
  Visibility: public export
bidescendM : Biplate from to => Applicative m => (to -> m to) -> from -> m from
  Totality: total
  Visibility: public export
children : Uniplate ty => ty -> List ty
  Totality: total
  Visibility: public export
plate : from -> Plate from to
  Start a new plate, not containing the target

  Totality: total
  Visibility: public export
(|*) : Plate (to -> from) to -> to -> Plate from to
  The value to the right is the target

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
(|+) : Biplate item to => Plate (item -> from) to -> item -> Plate from to
  The value to the right contains the target
  Note: due to https://github.com/idris-lang/Idris2/issues/2737,
  you may need to use `assert_total`.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
(||+) : {0 f : Type -> Type} -> Biplate (f inner) inner => Biplate inner to => Plate (f inner -> from) to -> f inner -> Plate from to
  The value to the right contains the target 2 'layers' down
  This is equivalent to `|+` using the `Compose` implementation of `Biplate`

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
(|-) : Plate (item -> from) to -> item -> Plate from to
  The value to the right does not contain the target

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
plateStar : (to -> from) -> to -> Plate from to
  Fused form of `plate f |* x`
  This replaces an `RTwo RZero ROne` with `ROne`

  Totality: total
  Visibility: public export
platePlus : Biplate item to => (item -> from) -> item -> Plate from to
  Fused form of `plate f |+ x`
  Note: due to https://github.com/idris-lang/Idris2/issues/2737,
  you may need to use `assert_total`.

  Totality: total
  Visibility: public export
plateVia : Biplate s to => (s -> t) -> (t -> s) -> t -> Plate t to
  Create a plate by providing a mapping to or from another type
  i.e. a profunctor on `Plate`

  Totality: total
  Visibility: public export
universe : Uniplate ty => ty -> List ty
  Get all children of a node, including the node itself
  and non-direct descendents.

  Totality: total
  Visibility: public export
transform : Uniplate ty => (ty -> ty) -> ty -> ty
  Apply a function to each sub-node, then to the node itself

  Totality: total
  Visibility: public export
transformM : Uniplate ty => Monad m => (ty -> m ty) -> ty -> m ty
  Apply a monadic function to each sub-node, then to the node itself

  Totality: total
  Visibility: public export
biuniverse : Biplate from to => from -> List to
  Get all children of a node, including non-direct descendents.

  Totality: total
  Visibility: public export
bitransform : Biplate from to => (to -> to) -> from -> from
  Apply a function to each sub-node of the target type

  Totality: total
  Visibility: public export
bitransformM : Biplate from to => Monad m => (to -> m to) -> from -> m from
  Apply a monadic function to each sub-node of the target type

  Totality: total
  Visibility: public export
fixpoint : Uniplate ty => (ty -> Maybe ty) -> ty -> ty
  Find the fixed point of a function applied to every sub-node of a node
  This ensures there is nowhere in the node that can have the function applied
  ie forall f, x. all (isNothing . f) (universe (fixpoint f x)) = True
  
  You can use `fixAdd` to combine 2 functions
  Note: it is up to the user to confirm that this is total
  Especially when using `fixAdd`, as there may be subtle conflicts between operations

  Visibility: public export
fixAdd : (a -> Maybe b) -> (a -> Maybe b) -> a -> Maybe b
  Combine 2 functions that return `Maybe`
  prefering the first one, if both would return `Just`

  Totality: total
  Visibility: public export
para : Uniplate ty => (ty -> List r -> r) -> ty -> r
  Perform a fold on a node and it's sub-nodes
  This is a paramorphism

  Totality: total
  Visibility: public export