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..b52ad407 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;. @@ -56,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., @@ -74,6 +85,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 := @@ -96,6 +111,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;. @@ -134,6 +153,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; @@ -165,6 +188,20 @@ 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; + +--- 𝒪(𝓃). Grabs the last element of the given ;List;. +last {A} : A -> List A -> A + | default := reverse >> head default; + +--- 𝒪(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. @@ -208,6 +245,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 := @@ -256,3 +299,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); 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/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 := 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 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;