Add some useful functions

Stdlib/Data/Int.juvix

@@ -89,3 +89,8 @@ mod (ofNat m) (negSuc n) := ofNat (Nat.mod m (suc n));
 mod (negSuc m) (ofNat n) := negNat (Nat.mod (suc m) n);
 mod (negSuc m) (negSuc n) :=
   negNat (Nat.mod (suc m) (suc n));
+
+--- Absolute value
+abs : Int -> Nat;
+abs (ofNat n) := n;
+abs (negSuc n) := suc n;

Stdlib/Data/List.juvix

@@ -1,6 +1,7 @@
 module Stdlib.Data.List;
 
 open import Stdlib.Data.Bool;
+open import Stdlib.Data.Maybe;
 open import Stdlib.Function;
 open import Stdlib.Data.Nat;
 open import Stdlib.Data.Ord;
@@ -223,3 +224,15 @@ quickSort {A} cmp :=
     go (x :: xs) :=
       qsHelper x (both go (partition (isGT ∘ cmp x) xs));
   in go;
+
+--- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.
+catMaybes : {A : Type} -> List (Maybe A) -> List A;
+catMaybes nil := nil;
+catMaybes (just h :: hs) := h :: catMaybes hs;
+catMaybes (nothing :: hs) := catMaybes hs;
+
+--- 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 : Type} -> (A -> List B) -> List A -> List B;
+concatMap f := flatten ∘ map f;

Stdlib/Data/Nat.juvix

@@ -1,6 +1,6 @@
 module Stdlib.Data.Nat;
 
-open import Stdlib.Data.String;
+open import Stdlib.Data.String.Base;
 open import Stdlib.Data.Bool;
 
 --- Inductive natural numbers. I.e. whole non-negative numbers.

Stdlib/Data/String.juvix

@@ -1,10 +1,13 @@
 module Stdlib.Data.String;
 
---- Primitive representation of a sequence of characters.
-builtin string
-axiom String : Type;
+open import Stdlib.Data.String.Base public;
+open import Stdlib.Data.List;
 
 --- Concatenation of two ;String;s.
 infixr 5 ++str;
 builtin string-concat
 axiom ++str : String -> String -> String;
+
+unlines : List String -> String;
+unlines nil := "";
+unlines (x :: xs) := x ++str "\n" ++str unlines xs;

Stdlib/Data/String/Base.juvix

@@ -0,0 +1,5 @@
+module Stdlib.Data.String.Base;
+
+--- Primitive representation of a sequence of characters.
+builtin string
+axiom String : Type;

Stdlib/Debug/Fail.juvix

@@ -1,6 +1,6 @@
 module Stdlib.Debug.Fail;
 
-open import Stdlib.Data.String;
+open import Stdlib.Data.String.Base;
 
 --- Primitive that exits the program with an error message.
 builtin fail

test/Makefile

@@ -3,10 +3,8 @@ all: test
 
 deps/quickcheck:
 	@mkdir -p deps/
-	@git clone https://github.com/anoma/juvix-quickcheck.git deps/quickcheck
-	@git -C deps/quickcheck checkout 2a23d8ed14d171fecf95892da401ddd37f96d40a
-	@mkdir -p deps/quickcheck/deps/stdlib
-	@rsync -av ../* deps/quickcheck/deps/stdlib --exclude "test"
+	@git clone --branch use-abs-stdlib https://github.com/anoma/juvix-quickcheck.git deps/quickcheck
+	$(MAKE) -C deps/quickcheck deps
 
 build/Test: $(shell find ../ -name "*.juvix") $(wildcard deps/**/*.juvix) Test.juvix deps/quickcheck
 	@mkdir -p build