Add pipeline operators (#3284)

* Add pipeline operators

* Fix tests

* Change fixity, add tests

* [ fix ] silence actual fixity

---------

Co-authored-by: itmuckel <18561536+itmuckel@users.noreply.github.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>

CHANGELOG_NEXT.md

@@ -114,6 +114,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 #### Prelude
 
+* Added pipeline operators `(|>)` and `(<|)`.
+
 #### Base
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.

libs/prelude/Prelude/Basics.idr

@@ -97,6 +97,26 @@ public export
 ($) : forall a, b . ((x : a) -> b x) -> (x : a) -> b x
 ($) f a = f a
 
+||| Pipeline style function application, useful for chaining
+||| functions into a series of transformations, reading top
+||| to bottom.
+|||
+||| ```idris example
+||| [[1], [2], [3]] |> join |> map (* 2)
+||| ```
+public export
+(|>) : a -> (a -> b) -> b
+a |> f = f a
+
+||| Backwards pipeline style function application, similar to $.
+|||
+||| ```idris example
+||| unpack <| "hello" ++ "world"
+||| ```
+public export
+(<|) : (a -> b) -> a -> b
+f <| a = f a
+
 -------------------
 -- PROOF HELPERS --
 -------------------

libs/prelude/Prelude/Ops.idr

@@ -25,6 +25,7 @@ export infixl 8 <+>
 
 -- Utility operators
 export infixr 9 ., .:
-export infixr 0 $
+export infixr 0 $, <|
+export infixl 0 |>
 
 export infixl 9 `div`, `mod`

src/Libraries/Data/PosMap.idr

@@ -10,6 +10,9 @@ import Core.FC
 
 import Data.List
 
+%hide Prelude.Ops.infixr.(<|)
+%hide Prelude.Ops.infixl.(|>)
+
 %default total
 
 export infixr 5 <|, <:

tests/idris2/misc/import009/Import.idr

@@ -2,6 +2,8 @@ module Import
 
 import Test
 
+%hide Prelude.Ops.infixl.(|>)
+
 (|>) : (s : HasComp x) => {0 a, b, c : x} -> a ~> b -> b ~> c -> a ~> c
 a |> b = comp s a b
 

tests/idris2/misc/import009/expected

@@ -2,13 +2,13 @@
 2/2: Building Import (Import.idr)
 Error: Unknown operator '~:>'
 
-Import:9:1--9:8
- 5 | (|>) : (s : HasComp x) => {0 a, b, c : x} -> a ~> b -> b ~> c -> a ~> c
- 6 | a |> b = comp s a b
- 7 | 
- 8 | (~:>) : Type -> Type -> Type
- 9 | a ~:> b = Pair a b
-     ^^^^^^^
+Import:11:1--11:8
+ 07 | (|>) : (s : HasComp x) => {0 a, b, c : x} -> a ~> b -> b ~> c -> a ~> c
+ 08 | a |> b = comp s a b
+ 09 | 
+ 10 | (~:>) : Type -> Type -> Type
+ 11 | a ~:> b = Pair a b
+      ^^^^^^^
 
 1/3: Building Prefix (Prefix.idr)
 Error: While processing right hand side of test. When unifying:

tests/idris2/operators/operators001/Test.idr

@@ -6,6 +6,8 @@ import Data.Vect
 private typebind infixr 0 =@
 private infixr 0 -@
 
+%hide Prelude.Ops.infixl.(|>)
+
 -- typebind infixr 1 =@@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
@@ -77,4 +79,3 @@ compose (a |> a') (b |> b') =
   (x : (y : a) @@ (a' y -> b)) |>
        (y : a' x.fst) @@
             b' (x.snd y)
-

tests/prelude/operators001/Test.idr

@@ -0,0 +1,8 @@
+
+testPipelineRight : Bool
+testPipelineRight =
+    ([[1], [2], [3]] |> join |> map (* 2)) == [2,4,6]
+
+testPipelineLeft : Bool
+testPipelineLeft =
+    (unpack <| "hello" ++ "world") == ['h', 'e', 'l', 'l', 'o', 'w', 'o', 'r', 'l', 'd']

tests/prelude/operators001/expected

@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)

tests/prelude/operators001/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+check Test.idr