Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rename ∘ to << and add >>, |> and <| functions #103

Merged
merged 9 commits into from
Jun 24, 2024
Merged
Show file tree
Hide file tree
Changes from 8 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Stdlib/Data/List/Base.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,7 @@ quickSort {A} {{Ord A}} : List A → List A :=
| nil := nil
| xs@(_ :: nil) := xs
| (x :: xs) :=
case partition (isGT Ord.cmp x) xs of
case partition (isGT << Ord.cmp x) xs of
l1, l2 := go l1 ++ x :: go l2;
in go;

Expand All @@ -219,7 +219,7 @@ syntax iterator concatMap {init := 0; range := 1};
--- Applies a function to every item on a ;List; and concatenates the result.
--- 𝒪(𝓃), where 𝓃 is the number of items in the resulting list.
concatMap {A B} (f : A -> List B) : List A -> List B :=
flatten map f;
flatten << map f;
Copy link
Contributor

@lukaszcz lukaszcz Jun 24, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since we have >>, I think it would be more readable to use it in most situations instead of << (the composition order of >> from left to right seems more intuitive: we first map, then flatten).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed - I will change this. Thanks

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done


--- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
transpose {A} : List (List A) -> List (List A)
Expand Down
2 changes: 1 addition & 1 deletion Stdlib/Data/String/Base.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,4 @@ concatStr : List String -> String := foldl (++str) "";

--- Joins a ;List; of ;String;s with "\n".
unlines : List String -> String :=
concatStr intersperse "\n";
concatStr << intersperse "\n";
26 changes: 19 additions & 7 deletions Stdlib/Function.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,17 @@ import Stdlib.Data.Fixity open;
import Stdlib.Data.Nat.Base open;
import Stdlib.Data.Pair.Base open;

syntax operator composition;
syntax operator << composition;

--- Function composition.
--- Function composition, passing results from the second function to the first.
{-# inline: 2 #-}
∘ {A B C} (f : B → C) (g : A → B) (x : A) : C := f (g x);
<< {A B C} (f : B → C) (g : A → B) (x : A) : C := f (g x);

syntax operator >> lcomposition;

--- Function composition, passing results from the first function to the second.
{-# inline: 2 #-}
>> {A B C} (f : A → B) (g : B → C) (x : A) : C := g (f x);

--- Always returns the first argument.
{-# inline: 1 #-}
Expand All @@ -21,11 +27,17 @@ id {A} (a : A) : A := a;
{-# inline: 1 #-}
flip {A B C} (f : A → B → C) (b : B) (a : A) : C := f a b;

syntax operator $ rapp;
syntax operator <| rapp;

--- Application operator with right associativity. Usually used as a syntactical
--- facility.
$ {A B} (f : A → B) (x : A) : B := f x;
<| {A B} (f : A → B) (x : A) : B := f x;

syntax operator |> lapp;

--- Application operator with left associativity. Usually used as a syntactical
--- facility.
|> {A B} (x : A) (f : A → B) : B := f x;

--- Applies a function n times.
iterate {A} : Nat -> (A -> A) -> A -> A
Expand All @@ -38,8 +50,8 @@ syntax operator on lapp;
on {A B C} (f : B → B → C) (g : A → B) (a b : A) : C :=
f (g a) (g b);

syntax operator >>> seq;
syntax operator >-> seq;

builtin seq
>>> : {A B : Type} → A → B → B
>-> : {A B : Type} → A → B → B
| x y := y;
4 changes: 2 additions & 2 deletions Stdlib/System/IO/Base.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,6 @@ import Stdlib.Data.Fixity open;
builtin IO
axiom IO : Type;

syntax operator >> seq;
syntax operator >>> seq;
builtin IO-sequence
axiom >> : IO → IO → IO;
axiom >>> : IO → IO → IO;
2 changes: 1 addition & 1 deletion Stdlib/System/IO/Bool.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -8,4 +8,4 @@ builtin bool-print
axiom printBool : Bool → IO;

printBoolLn (b : Bool) : IO :=
printBool b >> printString "\n";
printBool b >>> printString "\n";
3 changes: 2 additions & 1 deletion Stdlib/System/IO/Int.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,5 @@ import Stdlib.System.IO.String open;
builtin int-print
axiom printInt : Int → IO;

printIntLn (i : Int) : IO := printInt i >> printString "\n";
printIntLn (i : Int) : IO :=
printInt i >>> printString "\n";
3 changes: 2 additions & 1 deletion Stdlib/System/IO/Nat.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,5 @@ import Stdlib.System.IO.String open;
builtin nat-print
axiom printNat : Nat → IO;

printNatLn (n : Nat) : IO := printNat n >> printString "\n";
printNatLn (n : Nat) : IO :=
printNat n >>> printString "\n";
2 changes: 1 addition & 1 deletion Stdlib/System/IO/String.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,4 @@ builtin IO-readline
axiom readLn : (String → IO) → IO;

printStringLn (s : String) : IO :=
printString s >> printString "\n";
printString s >>> printString "\n";
2 changes: 1 addition & 1 deletion test/Package.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,5 @@ package : Package :=
; github
"anoma"
"juvix-quickcheck"
"b6ca4d4bd80d62b95e2d7e28e881c5b547643564"
"8068d58360d2adecba3674a31e031e7ad992e0e1"
]};
6 changes: 3 additions & 3 deletions test/juvix.lock.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -2,17 +2,17 @@
# Do not edit this file manually.

version: 2
checksum: c311ba35a484fb649358719f7720cf706aa8b13d8066bb0fe600ef0d7bc4ca2c
checksum: 5de68b52002fccbfacd5df82593d631368f3303203d03dc72f126e74a5997283
dependencies:
- path: ../
dependencies: []
- git:
name: anoma_juvix-quickcheck
ref: b6ca4d4bd80d62b95e2d7e28e881c5b547643564
ref: 8068d58360d2adecba3674a31e031e7ad992e0e1
url: https://github.com/anoma/juvix-quickcheck
dependencies:
- git:
name: anoma_juvix-stdlib
ref: 3f2c29880e749c7dd222011527a077b5f5050a95
ref: 290f67fc85b637ce4df886fc3cd1a5289b38db95
url: https://github.com/anoma/juvix-stdlib
dependencies: []
Loading