Merge the containers library (#125)

* Depends on anoma/juvix#3087

Stdlib/Cairo/Pedersen.juvix

@@ -1,8 +1,7 @@
 module Stdlib.Cairo.Pedersen;
 
 import Stdlib.Data.Field open using {Field};
-import
-Stdlib.Cairo.Ec as Ec;
+import Stdlib.Cairo.Ec as Ec;
 
 module ConstantPoints;
   P0 : Ec.Point :=

Stdlib/Data/BinaryTree.juvix

@@ -0,0 +1,20 @@
+module Stdlib.Data.BinaryTree;
+
+import Stdlib.Data.Nat open;
+import Stdlib.Data.List open;
+
+type BinaryTree (A : Type) :=
+  | leaf : BinaryTree A
+  | node : BinaryTree A -> A -> BinaryTree A -> BinaryTree A;
+
+--- fold a tree in depth first order
+fold {A B} (f : A -> B -> B -> B) (acc : B) : BinaryTree A -> B :=
+  let
+    go (acc : B) : BinaryTree A -> B
+      | leaf := acc
+      | (node l a r) := f a (go acc l) (go acc r);
+  in go acc;
+
+length : {A : Type} -> BinaryTree A -> Nat := fold λ {_ l r := 1 + l + r} 0;
+
+to-list : {A : Type} -> BinaryTree A -> List A := fold λ {e ls rs := e :: ls ++ rs} nil;

Stdlib/Data/Map.juvix

@@ -0,0 +1,72 @@
+module Stdlib.Data.Map;
+
+import Stdlib.Data.Pair open;
+import Stdlib.Data.Maybe open;
+import Stdlib.Data.List open;
+import Stdlib.Data.Nat open;
+
+import Stdlib.Trait.Functor open;
+import Stdlib.Trait.Foldable open;
+import Stdlib.Trait.Ord open;
+
+import Stdlib.Function open;
+
+import Stdlib.Data.Set as Set;
+open Set using {Set};
+
+import Stdlib.Data.Set.AVL as AVL;
+open AVL using {AVLTree};
+
+import Stdlib.Data.BinaryTree as Tree;
+
+type Binding A B := binding A B;
+
+key {A B} : Binding A B -> A
+  | (binding a _) := a;
+
+value {A B} : Binding A B -> B
+  | (binding _ b) := b;
+
+toPair {A B} : Binding A B -> Pair A B
+  | (binding a b) := a, b;
+
+instance
+bindingKeyOrdering {A B} {{Ord A}} : Ord (Binding A B) :=
+  mkOrd λ {b1 b2 := Ord.cmp (key b1) (key b2)};
+
+type Map A B := mkMap (AVLTree (Binding A B));
+
+empty {A B} : Map A B := mkMap AVL.empty;
+
+{-# specialize: [1, f] #-}
+insertWith {A B} {{Ord A}} (f : B -> B -> B) (k : A) (v : B) : Map A B -> Map A B
+  | (mkMap s) :=
+    let
+      f' : Binding A B -> Binding A B -> Binding A B
+        | (binding a b1) (binding _ b2) := binding a (f b1 b2);
+    in mkMap (Set.insertWith f' (binding k v) s);
+
+insert {A B : Type} {{Ord A}} : A -> B -> Map A B -> Map A B := insertWith λ {old new := new};
+
+{-# specialize: [1] #-}
+lookup {A B} {{Ord A}} (k : A) : Map A B -> Maybe B
+  | (mkMap s) := map value (Set.lookupWith key k s);
+
+{-# specialize: [1, f] #-}
+fromListWith {A B} {{Ord A}} (f : B -> B -> B) (xs : List (Pair A B)) : Map A B :=
+  for (acc := empty) (k, v in xs)
+    insertWith f k v acc;
+
+fromList {A B} {{Ord A}} : List (Pair A B) -> Map A B := fromListWith λ {old new := new};
+
+toList {A B} : Map A B -> List (Pair A B)
+  | (mkMap s) := map (x in Set.toList s) toPair x;
+
+size {A B} : Map A B -> Nat
+  | (mkMap s) := Set.size s;
+
+delete {A B} {{Ord A}} (k : A) : Map A B -> Map A B
+  | m@(mkMap s) := Set.deleteWith key k s |> mkMap;
+
+instance
+eqMapI {A B} {{Eq A}} {{Eq B}} : Eq (Map A B) := mkEq (Eq.eq on toList);

Stdlib/Data/Maybe/Base.juvix

@@ -1,6 +1,7 @@
 module Stdlib.Data.Maybe.Base;
 
 import Juvix.Builtin.V1.Maybe open public;
+import Juvix.Builtin.V1.Bool open;
 
 --- Extracts the value from a ;Maybe; if present, else returns the given value.
 {-# inline: true #-}
@@ -14,3 +15,7 @@ fromMaybe {A} (a : A) : Maybe A → A
 maybe {A B} (b : B) (f : A → B) : Maybe A → B
   | nothing := b
   | (just a) := f a;
+
+isJust {A} : Maybe A -> Bool
+  | nothing := false
+  | (just _) := true;

Stdlib/Data/Queue.juvix

@@ -0,0 +1,3 @@
+module Stdlib.Data.Queue;
+
+import Stdlib.Data.Queue.Base open public;

Stdlib/Data/Queue/Base.juvix

@@ -0,0 +1,81 @@
+--- This module provides an implementation of a First-In, First-Out (FIFO)
+--- queue based on Okasaki's "Purely Functional Data Structures." Ch.3.
+---
+--- This Okasaki Queue version data structure ensures amortized constant-time
+--- performance for basic operations such as push, pop, and front.
+---
+--- The Okasaki Queue consists of two lists (front and back) to separate
+--- the concerns of adding and removing elements for ensuring efficient
+--- performance.
+module Stdlib.Data.Queue.Base;
+
+import Stdlib.Data.List open;
+import Stdlib.Data.Bool open;
+import Stdlib.Data.Maybe open;
+import Stdlib.Data.Pair open;
+import Stdlib.Data.Nat open;
+import Stdlib.Function open;
+import Stdlib.Trait.Foldable open;
+
+--- A first-in-first-out data structure
+type Queue (A : Type) := queue (List A) (List A);
+
+--- 𝒪(1). The empty ;Queue;.
+empty {A} : Queue A := queue nil nil;
+
+--- 𝒪(1). Returns ;true; when the ;Queue; has no elements.
+isEmpty {A} : Queue A -> Bool
+  | (queue nil nil) := true
+  | _ := false;
+
+--- 𝒪(1). Returns first element of the ;Queue;, if any.
+head {A} : Queue A -> Maybe A
+  | (queue nil _) := nothing
+  | (queue (x :: _) _) := just x;
+
+--- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty
+--  then returns ;nothing;.
+tail {A} : Queue A -> Maybe (Queue A)
+  | (queue nil _) := nothing
+  | (queue (_ :: front) back) := just (queue front back);
+
+--- 𝒪(n) worst-case, but 𝒪(1) amortized
+{-# inline: true #-}
+check {A} : Queue A -> Queue A
+  | (queue nil back) := queue (reverse back) nil
+  | q := q;
+
+--- 𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the
+--  rest of the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
+pop {A} : Queue A -> Maybe (Pair A (Queue A))
+  | (queue nil _) := nothing
+  | (queue (x :: front) back) := just (x, check (queue front back));
+
+--- 𝒪(1). Adds an element to the end of the ;Queue;.
+push {A} (x : A) : Queue A -> Queue A
+  | (queue front back) := check (queue front (x :: back));
+
+--- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
+pushMany {A} (xs : List A) (q : Queue A) : Queue A := for (acc := q) (x in xs) push x acc;
+
+--- 𝒪(n). Build a ;Queue; from a ;List;.
+fromList {A} (xs : List A) : Queue A := pushMany xs empty;
+
+--- toList: O(n). Returns a ;List; of the elements in the ;Queue;.
+--- The elements are in the same order as they appear in the ;Queue;
+--- (i.e. the first element of the ;Queue; is the first element of the ;List;).
+toList {A} : Queue A -> List A
+  | (queue front back) := front ++ reverse back;
+
+--- 𝒪(n). Returns the number of elements in the ;Queue;.
+size {A} : Queue A -> Nat
+  | (queue front back) := length front + length back;
+
+instance
+eqQueueI {A} {{Eq A}} : Eq (Queue A) := mkEq ((==) on toList);
+
+instance
+showQueueI {A} {{Show A}} : Show (Queue A) := mkShow (toList >> Show.show);
+
+instance
+ordQueueI {A} {{Ord A}} : Ord (Queue A) := mkOrd (Ord.cmp on toList);

Stdlib/Data/Result.juvix

@@ -2,9 +2,11 @@ module Stdlib.Data.Result;
 
 import Stdlib.Data.Result.Base open public;
 import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.String.Base open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Show open;
 import Stdlib.Trait open;
 
 {-# specialize: true, inline: case #-}
@@ -28,6 +30,14 @@ eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
       | _ _ := false
   };
 
+instance
+showResultI {A B} {{Show A}} {{Show B}} : Show (Result A B) :=
+  mkShow@{
+    show : Result A B -> String
+      | (error x) := "Error (" ++str Show.show x ++str ")"
+      | (ok x) := "Ok (" ++str Show.show x ++str ")"
+  };
+
 {-# specialize: true, inline: case #-}
 instance
 functorResultI {err} : Functor (Result err) :=

Stdlib/Data/Set.juvix

@@ -0,0 +1,11 @@
+module Stdlib.Data.Set;
+
+import Stdlib.Data.Set.AVL open public;
+import Stdlib.Trait.Eq as Eq open using {Eq};
+import Stdlib.Trait.Ord as Ord open using {Ord};
+
+syntax alias Set := AVLTree;
+
+eqSetI {A} {{Eq A}} : Eq (Set A) := eqAVLTreeI;
+
+ordSetI {A} {{Ord A}} : Ord (Set A) := ordAVLTreeI;