From 61e7cd7ccf8511558b79d8d0eceb6fa782c10d6b Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 6 Nov 2024 18:23:35 +0100 Subject: [PATCH 01/12] add new modules to index.juvix --- index.juvix | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/index.juvix b/index.juvix index b5d09be2..7b307b9a 100644 --- a/index.juvix +++ b/index.juvix @@ -10,8 +10,18 @@ Compiler: http://github.com/anoma/juvix module index; import Stdlib.Prelude; -import Stdlib.Data.Nat.Ord; -import Stdlib.Data.Int.Ord; -import Stdlib.Data.String.Ord; +import Stdlib.Data.BinaryTree; +import Stdlib.Data.Set; +import Stdlib.Data.Map; +import Stdlib.Data.UnbalancedSet; +import Stdlib.Data.Queue; +import Stdlib.Data.Tree; + +import Stdlib.Cairo.Ec; import Stdlib.Cairo.Poseidon; +import Stdlib.Cairo.Pedersen; + +import Stdlib.Debug; + +import Stdlib.Extra.Gcd; From ed3a5f4c64b0132bfaae4e4a8d41d60e95be2c40 Mon Sep 17 00:00:00 2001 From: mariari Date: Thu, 7 Nov 2024 12:55:53 +0800 Subject: [PATCH 02/12] Add the last function --- Stdlib/Data/List/Base.juvix | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index bc8d0900..de956180 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -165,6 +165,10 @@ head {A} (defaultValue : A) (list : List A) : A := | x :: _ := x | nil := defaultValue; +--- 𝒪(𝓃). Grabs the last element of the given ;List;. +last {A} : A -> List A -> A + | default := reverse >> head default; + syntax iterator any {init := 0; range := 1}; --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate. From a567cf1722488a441dad94230e7aac7e53353e6e Mon Sep 17 00:00:00 2001 From: mariari Date: Thu, 7 Nov 2024 13:17:35 +0800 Subject: [PATCH 03/12] Add a maybe head function The naming on this is probably bad, I'd assume `head` would return Maybe, and you'd have a headDefault or something for a default head --- Stdlib/Data/List/Base.juvix | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index bc8d0900..589836ff 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -165,6 +165,11 @@ head {A} (defaultValue : A) (list : List A) : A := | x :: _ := x | nil := defaultValue; +--- 𝒪(1). Grabs the first element of a ;List; +headMaybe {A} : List A -> Maybe A + | (x :: _) := just x + | nil := nothing; + syntax iterator any {init := 0; range := 1}; --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate. From 386b38e483b4bc8d9d543fc4b8a16f2e66fdad12 Mon Sep 17 00:00:00 2001 From: mariari Date: Thu, 7 Nov 2024 15:18:59 +0800 Subject: [PATCH 04/12] Write the nth function --- Stdlib/Data/List/Base.juvix | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 589836ff..4ea06ecd 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -96,6 +96,10 @@ drop {A} : (elemsNum : Nat) -> (list : List A) -> List A | (suc n) (x :: xs) := drop n xs | _ xs := xs; +--- Take the nth value of a ;List; +nth {A} : Nat -> List A -> Maybe A + | n := drop n >> headMaybe; + --- 𝒪(𝓃). Returns a tuple where first element is the --- prefix of the given list of length prefixLength and second element is the --- remainder of the ;List;. From 4485bd7f9051c025cefbbe4c39f772273ba8b612 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 13:40:31 +0800 Subject: [PATCH 05/12] Losen the Constraints on the Partial Trait Partial trait relied upon import Stdlib.Data.String.Base open; which indirectly relies upon list, we loosen the restriction to just rely on the String type itself. This lets us move some functions around to the base module --- Stdlib/Debug/Fail.juvix | 2 +- Stdlib/Trait/Partial.juvix | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Stdlib/Debug/Fail.juvix b/Stdlib/Debug/Fail.juvix index 45a106e6..bfc03523 100644 --- a/Stdlib/Debug/Fail.juvix +++ b/Stdlib/Debug/Fail.juvix @@ -1,6 +1,6 @@ module Stdlib.Debug.Fail; -import Stdlib.Data.String.Base open; +import Juvix.Builtin.V1.String open; --- Exit the program with an error message. builtin fail diff --git a/Stdlib/Trait/Partial.juvix b/Stdlib/Trait/Partial.juvix index 1670c417..9b2e3449 100644 --- a/Stdlib/Trait/Partial.juvix +++ b/Stdlib/Trait/Partial.juvix @@ -1,6 +1,6 @@ module Stdlib.Trait.Partial; -import Stdlib.Data.String.Base open; +import Juvix.Builtin.V1.String open; import Stdlib.Debug.Fail as Debug; trait From dbc3a556409828176e900c2ef70d1fe60095b340 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 13:40:36 +0800 Subject: [PATCH 06/12] Move Phead to List Base --- Stdlib/Data/List.juvix | 5 ----- Stdlib/Data/List/Base.juvix | 6 ++++++ 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix index f62aa06d..0091378d 100644 --- a/Stdlib/Data/List.juvix +++ b/Stdlib/Data/List.juvix @@ -16,11 +16,6 @@ import Stdlib.Trait.Foldable open using { fromPolymorphicFoldable; }; ---- 𝒪(1). Partial function that returns the first element of a ;List;. -phead {A} {{Partial}} : List A -> A - | (x :: _) := x - | nil := fail "head: empty list"; - instance eqListI {A} {{Eq A}} : Eq (List A) := let diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index bc8d0900..425a850b 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -7,6 +7,7 @@ import Stdlib.Function open; import Stdlib.Data.Nat.Base open; import Stdlib.Data.Maybe.Base open; import Stdlib.Trait.Ord open; +import Stdlib.Trait.Partial open; import Stdlib.Data.Pair.Base open; --- 𝒪(𝓃). Returns ;true; if the given object elem is in the ;List;. @@ -165,6 +166,11 @@ head {A} (defaultValue : A) (list : List A) : A := | x :: _ := x | nil := defaultValue; +--- 𝒪(1). Partial function that returns the first element of a ;List;. +phead {A} {{Partial}} : List A -> A + | (x :: _) := x + | nil := fail "head: empty list"; + syntax iterator any {init := 0; range := 1}; --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate. From 8e3e16d77dffb7fbfe99cf96d35b7e89d84b3089 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 14:42:21 +0800 Subject: [PATCH 07/12] Add the cons function --- Stdlib/Data/List/Base.juvix | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 290aa4e2..4b44b2f3 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -139,6 +139,10 @@ syntax operator ++ cons; | nil ys := ys | (x :: xs) ys := x :: xs ++ ys; +--- 𝒪(1). Cons on an element onto a ;List;. +cons {A} : A -> List A -> List A + | x xs := x :: xs; + --- 𝒪(𝓃). Append an element. snoc {A} (list : List A) (elem : A) : List A := list ++ elem :: nil; From 5578ebaf315d114046a82b2788c907c05804ce4e Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 14:30:07 +0800 Subject: [PATCH 08/12] Add foldi to the standard library --- Stdlib/Trait/Foldable/Polymorphic.juvix | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/Stdlib/Trait/Foldable/Polymorphic.juvix b/Stdlib/Trait/Foldable/Polymorphic.juvix index 727dc740..00884575 100644 --- a/Stdlib/Trait/Foldable/Polymorphic.juvix +++ b/Stdlib/Trait/Foldable/Polymorphic.juvix @@ -1,6 +1,8 @@ module Stdlib.Trait.Foldable.Polymorphic; import Stdlib.Function open; +import Juvix.Builtin.V1.Nat.Base open; +import Stdlib.Data.Pair.Base open; --- A trait for combining elements into a single result, processing one element at a time. trait @@ -15,13 +17,28 @@ type Foldable (F : Type -> Type) := open Foldable public; +foldli + {F : Type -> Type} + {{Foldable F}} + {Elem Acc : Type} + (fun : Nat -> Acc -> Elem -> Acc) + (initialValue : Acc) + (container : F Elem) + : Acc := + let + g := λ{(index, acc) ele := suc index, fun index acc ele}; + in for (acc := zero, initialValue) (x in container) { + g acc x + } + |> snd; + --- Combine the elements of the type using the provided function starting with the element in the left-most position. {-# inline: true #-} foldl {F : Type -> Type} {{Foldable F}} {Elem Acc : Type} - (fun : Acc -> Elem -> Acc) + (fun : Acgc -> Elem -> Acc) (initialValue : Acc) (container : F Elem) : Acc := From 7fc552e28d10cff2258aef4d68d1da1cc9b7c017 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 14:54:59 +0800 Subject: [PATCH 09/12] Add unzip to the list standard library --- Stdlib/Data/List/Base.juvix | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 4b44b2f3..781ae5f5 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -231,6 +231,12 @@ zip {A B} : (list1 : List A) -> (list2 : List B) -> List (Pair A B) | _ nil := nil | (x :: xs) (y :: ys) := (x, y) :: zip xs ys; +--- 𝒪(n). Transforms a ;List; of ;Pair;s into a ;List; of the first componenet +--- and a ;List; of second component +unzip {A B} : List (Pair A B) -> Pair (List A) (List B) + -- TODO :: Optimize into a single pass + | xs := listMap fst xs, listMap snd xs; + --- 𝒪(𝓃 log 𝓃). Sorts a list of elements in ascending order using the MergeSort --- algorithm. mergeSort {A} {{Ord A}} (list : List A) : List A := From a4afe0f408ad355e760955e81e769bb9cee78674 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 15:15:46 +0800 Subject: [PATCH 10/12] Add group to list functionality --- Stdlib/Data/List/Base.juvix | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 781ae5f5..351d4359 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -285,3 +285,16 @@ transpose {A} : (listOfLists : List (List A)) -> List (List A) | nil := nil | (xs :: nil) := listMap λ{x := x :: nil} xs | (xs :: xss) := zipWith (::) xs (transpose xss); + +--- 𝒪(𝓃). Groups a ;List; given a predicate +group {A} : (break : A -> A -> Bool) -> List A -> List (List A) + | _ nil := nil + | break (x :: xs) := + let + go : List A -> List (List A) -> Pair A (List A) -> List (List A) + | nil acc _ := acc + | (x :: xs) acc (prev, prevs) := + if + | break prev x := go xs acc (x, prev :: prevs) + | else := go xs ((prev :: prevs) :: acc) (x, nil); + in go xs nil (x, nil); From efaa0d292be7273a55fa33a070cbc7d986ae0d11 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 15:31:13 +0800 Subject: [PATCH 11/12] Add the Count function to the standard library --- Stdlib/Data/List/Base.juvix | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 351d4359..4304d3ef 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -75,6 +75,10 @@ length {A} (list : List A) : Nat := suc acc }; +--- 𝒪(𝓃). Find the number of elements in a ;List;. that satisfy a given predicate. +count {A} : (A -> Bool) -> List A -> Nat + | predicate := filter predicate >> length; + --- 𝒪(𝓃). Returns the given ;List; in reverse order. {-# isabelle-function: {name: "rev"} #-} reverse {A} (list : List A) : List A := From 51d4d325b84b7134181f3fd238fa749587052cc3 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 15:38:02 +0800 Subject: [PATCH 12/12] Add the mapi function I'm unsure if we can add this to a trait or not --- Stdlib/Data/List/Base.juvix | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 4304d3ef..b52ad407 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -57,6 +57,16 @@ listMap {A B} (fun : A -> B) : (list : List A) -> List B | nil := nil | (h :: hs) := fun h :: listMap fun hs; +--- 𝒪(𝓃). Maps a function over each element of a ;List; with an index. +{-# specialize: [1] #-} +mapi {A B} : (fun : Nat -> A -> B) -> List A -> List B + | fun xs := + let + go : Nat -> List A -> List B + | _ nil := nil + | n (x :: xs) := fun n x :: go (suc n) xs; + in go zero xs; + syntax iterator filter {init := 0; range := 1}; --- 𝒪(𝓃). Filters a ;List; according to a given predicate, i.e.,