From 8067c79e14347cef9a38fd45fbb7ada3c32f5dce Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 20 Jun 2024 12:08:08 +0100 Subject: [PATCH 1/9] Replace \times with << --- Stdlib/Function.juvix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix index 8e10b5ad..7331de4e 100644 --- a/Stdlib/Function.juvix +++ b/Stdlib/Function.juvix @@ -4,11 +4,11 @@ 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. {-# 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); --- Always returns the first argument. {-# inline: 1 #-} From 34a6bb0ee9e81f5771dbdf85f5e8f298f4e182b9 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 20 Jun 2024 12:08:31 +0100 Subject: [PATCH 2/9] Add >> function to complement << composition --- Stdlib/Function.juvix | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix index 7331de4e..ee324e93 100644 --- a/Stdlib/Function.juvix +++ b/Stdlib/Function.juvix @@ -6,10 +6,16 @@ import Stdlib.Data.Pair.Base open; 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); +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 #-} const {A B} (a : A) (_ : B) : A := a; From 39452801a3290ef2d8d965f23d6fb439873da57e Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 20 Jun 2024 12:09:10 +0100 Subject: [PATCH 3/9] Add |> application function --- Stdlib/Function.juvix | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix index ee324e93..8ef0dda5 100644 --- a/Stdlib/Function.juvix +++ b/Stdlib/Function.juvix @@ -32,6 +32,11 @@ syntax operator $ rapp; --- Application operator with right associativity. Usually used as a syntactical --- facility. $ {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 From 826f67e7b35d7990b57d23c5cd3208a911f55925 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 20 Jun 2024 12:09:42 +0100 Subject: [PATCH 4/9] Rename $ to <| to complement the |> function --- Stdlib/Function.juvix | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix index 8ef0dda5..097a268e 100644 --- a/Stdlib/Function.juvix +++ b/Stdlib/Function.juvix @@ -27,11 +27,12 @@ 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 From 7c008fb0ae9780b873c23531aa9523c2931bd686 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 21 Jun 2024 15:44:39 +0100 Subject: [PATCH 5/9] Fix usages of composition --- Stdlib/Data/List/Base.juvix | 4 ++-- Stdlib/Data/String/Base.juvix | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 94b45e6d..53715310 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -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; @@ -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; --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix. transpose {A} : List (List A) -> List (List A) diff --git a/Stdlib/Data/String/Base.juvix b/Stdlib/Data/String/Base.juvix index 91b3493d..74a8d7ee 100644 --- a/Stdlib/Data/String/Base.juvix +++ b/Stdlib/Data/String/Base.juvix @@ -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"; From 4fb6c9cdd300afd2560fc64dfdf7a62ad0e2ebad Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 21 Jun 2024 16:01:59 +0100 Subject: [PATCH 6/9] Rename >>> to >-> --- Stdlib/Function.juvix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix index 097a268e..21d7fe9d 100644 --- a/Stdlib/Function.juvix +++ b/Stdlib/Function.juvix @@ -50,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; From 290f67fc85b637ce4df886fc3cd1a5289b38db95 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 21 Jun 2024 16:02:17 +0100 Subject: [PATCH 7/9] Rename >> : IO -> IO -> IO to >>> --- Stdlib/System/IO/Base.juvix | 4 ++-- Stdlib/System/IO/Bool.juvix | 2 +- Stdlib/System/IO/Int.juvix | 3 ++- Stdlib/System/IO/Nat.juvix | 3 ++- Stdlib/System/IO/String.juvix | 2 +- 5 files changed, 8 insertions(+), 6 deletions(-) diff --git a/Stdlib/System/IO/Base.juvix b/Stdlib/System/IO/Base.juvix index bb04458e..67722245 100644 --- a/Stdlib/System/IO/Base.juvix +++ b/Stdlib/System/IO/Base.juvix @@ -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; diff --git a/Stdlib/System/IO/Bool.juvix b/Stdlib/System/IO/Bool.juvix index 0fd5a9bb..da364e69 100644 --- a/Stdlib/System/IO/Bool.juvix +++ b/Stdlib/System/IO/Bool.juvix @@ -8,4 +8,4 @@ builtin bool-print axiom printBool : Bool → IO; printBoolLn (b : Bool) : IO := - printBool b >> printString "\n"; + printBool b >>> printString "\n"; diff --git a/Stdlib/System/IO/Int.juvix b/Stdlib/System/IO/Int.juvix index ed5ea299..6c89adcd 100644 --- a/Stdlib/System/IO/Int.juvix +++ b/Stdlib/System/IO/Int.juvix @@ -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"; diff --git a/Stdlib/System/IO/Nat.juvix b/Stdlib/System/IO/Nat.juvix index 8322fd4f..99c54fef 100644 --- a/Stdlib/System/IO/Nat.juvix +++ b/Stdlib/System/IO/Nat.juvix @@ -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"; diff --git a/Stdlib/System/IO/String.juvix b/Stdlib/System/IO/String.juvix index a949f18c..511e7036 100644 --- a/Stdlib/System/IO/String.juvix +++ b/Stdlib/System/IO/String.juvix @@ -10,4 +10,4 @@ builtin IO-readline axiom readLn : (String → IO) → IO; printStringLn (s : String) : IO := - printString s >> printString "\n"; + printString s >>> printString "\n"; From 542cbf90378cf8bc007ce418c45e7ba11d114da2 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 21 Jun 2024 16:31:28 +0100 Subject: [PATCH 8/9] Update quickcheck reference --- test/Package.juvix | 2 +- test/juvix.lock.yaml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/test/Package.juvix b/test/Package.juvix index 0d3b98b4..b8c2c39d 100644 --- a/test/Package.juvix +++ b/test/Package.juvix @@ -9,5 +9,5 @@ package : Package := ; github "anoma" "juvix-quickcheck" - "b6ca4d4bd80d62b95e2d7e28e881c5b547643564" + "8068d58360d2adecba3674a31e031e7ad992e0e1" ]}; diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml index 3b894ddf..cff529ff 100644 --- a/test/juvix.lock.yaml +++ b/test/juvix.lock.yaml @@ -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: [] From fc47159ed4853e923a5accbfed4412e67ad58f4a Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Mon, 24 Jun 2024 17:24:33 +0100 Subject: [PATCH 9/9] Replace usages of << with >> --- Stdlib/Data/List/Base.juvix | 4 ++-- Stdlib/Data/String/Base.juvix | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 53715310..53aa4bf4 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -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 (Ord.cmp x >> isGT) xs of l1, l2 := go l1 ++ x :: go l2; in go; @@ -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; + map f >> flatten; --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix. transpose {A} : List (List A) -> List (List A) diff --git a/Stdlib/Data/String/Base.juvix b/Stdlib/Data/String/Base.juvix index 74a8d7ee..82a2660e 100644 --- a/Stdlib/Data/String/Base.juvix +++ b/Stdlib/Data/String/Base.juvix @@ -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"; + intersperse "\n" >> concatStr;