
   0 | module Data.Uniplate
   1 | 
   2 | import Data.Vect
   3 | import Data.List1
   4 | 
   5 | %default total
   6 | 
   7 | infixl 3 |*
   8 | infixl 3 |+
   9 | infixl 3 ||+
  10 | infixl 3 |-
  11 | 
  12 | ||| How the children of a given node are represented
  13 | public export
  14 | data Repr : Type where
  15 |     RZero : Repr
  16 |     ROne : Repr
  17 |     RTwo : Repr -> Repr -> Repr
  18 | 
  19 | %name Repr repr
  20 | 
  21 | ||| The children of a node
  22 | public export
  23 | data Children : Repr -> Type -> Type where
  24 |     Zero : Children RZero a
  25 |     One : a -> Children ROne a
  26 |     Two : Children l a -> Children r a -> Children (RTwo l r) a
  27 | 
  28 | public export
  29 | Functor (Children repr) where
  30 |     map f Zero = Zero
  31 |     map f (One x) = One (f x)
  32 |     map f (Two x y) = Two (map f x) (map f y)
  33 | 
  34 | public export
  35 | Foldable (Children repr) where
  36 |     foldr f z Zero = z
  37 |     foldr f z (One x) = f x z
  38 |     foldr f z (Two x y) = foldr f (foldr f z y) x
  39 | 
  40 |     foldl f z Zero = z
  41 |     foldl f z (One x) = f z x
  42 |     foldl f z (Two x y) = foldl f (foldl f z x) y
  43 | 
  44 |     null Zero = True
  45 |     null _ = False
  46 | 
  47 |     foldlM f z Zero = pure z
  48 |     foldlM f z (One x) = f z x
  49 |     foldlM f z (Two x y) = foldlM f z x >>= (\z => foldlM f z y)
  50 | 
  51 |     toList cs = toListOnto cs []
  52 |       where
  53 |         toListOnto : forall repr. Children repr ty -> List ty -> List ty
  54 |         toListOnto Zero acc = acc
  55 |         toListOnto (One x) acc = x :: acc
  56 |         toListOnto (Two x y) acc = toListOnto x $ toListOnto y acc
  57 | 
  58 |     foldMap f Zero = neutral
  59 |     foldMap f (One x) = f x
  60 |     foldMap f (Two x y) = foldMap f x <+> foldMap f y
  61 | 
  62 | public export
  63 | Traversable (Children repr) where
  64 |     traverse f Zero = pure Zero
  65 |     traverse f (One x) = One <$> f x
  66 |     traverse f (Two x y) = Two <$> traverse f x <*> traverse f y
  67 | 
  68 | public export
  69 | record Plate (from : Type) (to : Type) where
  70 |     constructor MkPlate
  71 |     {0 repr : Repr}
  72 |     cs : Children repr to
  73 |     gen : Children repr to -> from
  74 | 
  75 | public export
  76 | interface Uniplate ty where
  77 |     ||| Get the direct children of a node
  78 |     ||| and a way to rebuild that node with modified children
  79 |     uniplate : (x : ty) -> Plate ty ty
  80 | 
  81 |     descend : (ty -> ty) -> ty -> ty
  82 |     descend f x =
  83 |         let MkPlate cs gen = uniplate x
  84 |          in gen (map f cs)
  85 | 
  86 |     descendM : Applicative m => (ty -> m ty) -> ty -> m ty
  87 |     descendM f x =
  88 |         let MkPlate cs gen = uniplate x
  89 |          in gen <$> traverse f cs
  90 | 
  91 | public export
  92 | interface Uniplate to => Biplate from to where
  93 |     biplate : (x : from) -> Plate from to
  94 | 
  95 |     bidescend : (to -> to) -> from -> from
  96 |     bidescend f x =
  97 |         let MkPlate cs gen = biplate x
  98 |          in gen (map f cs)
  99 | 
 100 |     bidescendM : Applicative m => (to -> m to) -> from -> m from
 101 |     bidescendM f x =
 102 |         let MkPlate cs gen = biplate x
 103 |          in gen <$> traverse f cs
 104 | 
 105 | compose : Biplate t a => Children r t -> Plate (Children r t) a
 106 | compose Zero = MkPlate Zero (\Zero => Zero)
 107 | compose (One x) =
 108 |     let MkPlate cs gen = biplate x
 109 |      in MkPlate cs (\cs => One (gen cs))
 110 | compose (Two x y) =
 111 |     let MkPlate xs genx = compose x
 112 |         MkPlate ys geny = compose y
 113 |      in MkPlate (Two xs ys) (\(Two xs ys) => Two (genx xs) (geny ys))
 114 | 
 115 | public export
 116 | [Compose] Biplate outer inner => Biplate inner to => Biplate outer to where
 117 |     biplate x =
 118 |         let MkPlate os geno = biplate {to = inner} x
 119 |             MkPlate is geni = compose os
 120 |          in MkPlate is (\is => geno (geni is))
 121 | 
 122 |     bidescend f x =
 123 |         let MkPlate cs gen = biplate @{Compose {outer, inner, to}} x
 124 |          in gen (f <$> cs)
 125 |     bidescendM f x =
 126 |         let MkPlate cs gen = biplate @{Compose {outer, inner, to}} x
 127 |          in gen <$> traverse f cs
 128 | 
 129 | public export
 130 | children : Uniplate ty => ty -> List ty
 131 | children x = toList $ cs $ uniplate x
 132 | 
 133 | ||| Start a new plate, not containing the target
 134 | public export
 135 | plate : from -> Plate from to
 136 | plate x = MkPlate { cs = Zero, gen = \Zero => x}
 137 | 
 138 | ||| The value to the right is the target
 139 | public export
 140 | (|*) : Plate (to -> from) to -> to -> Plate from to
 141 | MkPlate cs gen |* x = MkPlate (Two cs (One x)) (\(Two cs (One x)) => gen cs x)
 142 | 
 143 | ||| The value to the right contains the target
 144 | ||| Note: due to https://github.com/idris-lang/Idris2/issues/2737,
 145 | ||| you may need to use `assert_total`.
 146 | public export %tcinline
 147 | (|+) :
 148 |     Biplate item to =>
 149 |     Plate (item -> from) to ->
 150 |     item ->
 151 |     Plate from to
 152 | MkPlate ls lgen |+ x =
 153 |     let MkPlate rs rgen = biplate x
 154 |      in MkPlate (Two ls rs) (\(Two ls rs) => lgen ls (rgen rs))
 155 | 
 156 | ||| The value to the right contains the target 2 'layers' down
 157 | ||| This is equivalent to `|+` using the `Compose` implementation of `Biplate`
 158 | public export %tcinline
 159 | (||+) :
 160 |     forall f.
 161 |     Biplate (f inner) inner =>
 162 |     Biplate inner to =>
 163 |     Plate (f inner -> from) to ->
 164 |     f inner ->
 165 |     Plate from to
 166 | p ||+ x = (|+) @{Compose {outer = f inner, inner, to}} p x
 167 | 
 168 | ||| The value to the right does not contain the target
 169 | public export
 170 | (|-) : Plate (item -> from) to -> item -> Plate from to
 171 | MkPlate cs gen |- x = MkPlate cs (\cs => gen cs x)
 172 | 
 173 | ||| Fused form of `plate f |* x`
 174 | ||| This replaces an `RTwo RZero ROne` with `ROne`
 175 | public export
 176 | plateStar : (to -> from) -> to -> Plate from to
 177 | plateStar f x = MkPlate (One x) (\(One x) => f x)
 178 | 
 179 | ||| Fused form of `plate f |+ x`
 180 | ||| Note: due to https://github.com/idris-lang/Idris2/issues/2737,
 181 | ||| you may need to use `assert_total`.
 182 | public export %tcinline
 183 | platePlus : Biplate item to => (item -> from) -> (x : item) -> Plate from to
 184 | platePlus f x =
 185 |     let MkPlate cs gen = biplate x
 186 |      in MkPlate cs (\cs => f (gen cs))
 187 | 
 188 | ||| Create a plate by providing a mapping to or from another type
 189 | ||| i.e. a profunctor on `Plate`
 190 | public export
 191 | plateVia : Biplate s to => (f : s -> t) -> (g : t -> s) -> t -> Plate t to
 192 | plateVia f g x =
 193 |     let MkPlate cs gen = biplate $ g x
 194 |      in MkPlate cs (\cs => f (gen cs))
 195 | 
 196 | ||| Get all children of a node, including the node itself
 197 | ||| and non-direct descendents.
 198 | public export
 199 | universe : Uniplate ty => ty -> List ty
 200 | universe x = x :: assert_total (foldMap universe (uniplate x).cs)
 201 | 
 202 | ||| Apply a function to each sub-node, then to the node itself
 203 | public export
 204 | transform : Uniplate ty => (ty -> ty) -> ty -> ty
 205 | transform f = f . assert_total (descend (transform f))
 206 | 
 207 | ||| Apply a monadic function to each sub-node, then to the node itself
 208 | public export
 209 | transformM : Uniplate ty => Monad m => (ty -> m ty) -> ty -> m ty
 210 | transformM f = assert_total (descendM (transformM f)) >=> f
 211 | 
 212 | ||| Get all children of a node, including non-direct descendents.
 213 | public export
 214 | biuniverse : Biplate from to => from -> List to
 215 | biuniverse x = foldMap universe (biplate x).cs
 216 | 
 217 | ||| Apply a function to each sub-node of the target type
 218 | public export
 219 | bitransform : Biplate from to => (to -> to) -> from -> from
 220 | bitransform f = bidescend (transform f)
 221 | 
 222 | ||| Apply a monadic function to each sub-node of the target type
 223 | public export
 224 | bitransformM : Biplate from to => Monad m => (to -> m to) -> from -> m from
 225 | bitransformM f = bidescendM (transformM f)
 226 | 
 227 | ||| Find the fixed point of a function applied to every sub-node of a node
 228 | ||| This ensures there is nowhere in the node that can have the function applied
 229 | ||| ie forall f, x. all (isNothing . f) (universe (fixpoint f x)) = True
 230 | |||
 231 | ||| You can use `fixAdd` to combine 2 functions
 232 | ||| Note: it is up to the user to confirm that this is total
 233 | ||| Especially when using `fixAdd`, as there may be subtle conflicts between operations
 234 | public export covering %inline
 235 | fixpoint : Uniplate ty => (ty -> Maybe ty) -> ty -> ty
 236 | fixpoint f = transform fix
 237 |   where
 238 |     fix : ty -> ty
 239 |     fix x = maybe x (fixpoint f) (f x)
 240 | 
 241 | ||| Combine 2 functions that return `Maybe`
 242 | ||| prefering the first one, if both would return `Just`
 243 | public export
 244 | fixAdd : (a -> Maybe b) -> (a -> Maybe b) -> (a -> Maybe b)
 245 | fixAdd f g x = f x <|> g x
 246 | 
 247 | ||| Perform a fold on a node and it's sub-nodes
 248 | ||| This is a paramorphism
 249 | public export
 250 | para : Uniplate ty => (ty -> List r -> r) -> ty -> r
 251 | para f x = f x $ assert_total $ map (para f) $ children x
 252 | 
 253 | -- Instances
 254 | 
 255 | public export
 256 | [Id] Uniplate a where
 257 |     uniplate x = plateStar id x
 258 | 
 259 | public export
 260 | [FromUni] Uniplate a => Biplate a a where
 261 |     biplate = uniplate
 262 | 
 263 | public export
 264 | Uniplate (List a) where
 265 |     uniplate [] = plate []
 266 |     uniplate (x :: xs) = plateStar (x ::) xs
 267 | 
 268 | public export
 269 | Biplate (List a) a using Id where
 270 |     biplate [] = plate []
 271 |     biplate (x :: xs) = assert_total $ plateStar (::) x |+ xs
 272 | 
 273 | public export
 274 | Biplate (Maybe a) a using Id where
 275 |     biplate Nothing = plate Nothing
 276 |     biplate (Just x) = plateStar Just x
 277 | 
 278 | public export
 279 | Uniplate (SnocList a) where
 280 |     uniplate [<] = plate [<]
 281 |     uniplate (xs :< x) = plateStar (:< x) xs
 282 | 
 283 | public export
 284 | Biplate (SnocList a) a using Id where
 285 |     biplate [<] = plate [<]
 286 |     biplate (xs :< x) = assert_total $ platePlus (:<) xs |* x
 287 | 
 288 | public export
 289 | Biplate (Vect len a) a using Id where
 290 |     biplate [] = plate []
 291 |     biplate (x :: xs) = plateStar (::) x |+ xs 
 292 | 
 293 | public export
 294 | Biplate (List1 a) a using Id where
 295 |     biplate (x ::: xs) = plateStar (:::) x |+ xs
 296 | 
 297 | public export
 298 | Biplate String Char using Id where
 299 |     biplate str = plateVia pack unpack str
 300 |