Mariari/list additions and refactorings

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

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);

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

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 :=

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

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;