From 8f180ccfdac913dd3920c38b3b708c044b958765 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Thu, 24 Oct 2024 13:29:33 +0200
Subject: [PATCH] Improve Set and Map modules in the standard library (#3120)

* Updates the standard library to
https://github.com/anoma/juvix-stdlib/pull/130
* Also changes `null` to `isEmpty`, which required updating some tests

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
---
 examples/milestone/TicTacToe/Logic/GameState.juvix | 2 +-
 juvix-stdlib                                       | 2 +-
 tests/Anoma/Compilation/positive/test007.juvix     | 6 +++---
 tests/Casm/Compilation/positive/test007.juvix      | 4 ++--
 tests/Compilation/positive/test007.juvix           | 6 +++---
 tests/Rust/Compilation/positive/test007.juvix      | 4 ++--
 tests/smoke/Commands/dev/repl.smoke.yaml           | 4 ++--
 tests/smoke/Commands/repl.smoke.yaml               | 4 ++--
 8 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/examples/milestone/TicTacToe/Logic/GameState.juvix b/examples/milestone/TicTacToe/Logic/GameState.juvix
index 2547010256..6ec4c3b9f6 100644
--- a/examples/milestone/TicTacToe/Logic/GameState.juvix
+++ b/examples/milestone/TicTacToe/Logic/GameState.juvix
@@ -44,4 +44,4 @@ won (state : GameState) : Bool :=
 draw (state : GameState) : Bool :=
   let
     squares := Board.squares (GameState.board state);
-  in null (possibleMoves (flatten squares));
+  in isEmpty (possibleMoves (flatten squares));
diff --git a/juvix-stdlib b/juvix-stdlib
index e164aa1450..7c7162aca5 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit e164aa14503ff11dbcf0dc96bcd4cfa4d757b76d
+Subproject commit 7c7162aca573d116825857da272d83d0fc8afcf7
diff --git a/tests/Anoma/Compilation/positive/test007.juvix b/tests/Anoma/Compilation/positive/test007.juvix
index 6c68d86ecf..622b88deb6 100644
--- a/tests/Anoma/Compilation/positive/test007.juvix
+++ b/tests/Anoma/Compilation/positive/test007.juvix
@@ -14,13 +14,13 @@ map' {A B} (f : A → B) : List A → List B :=
 -- TODO: Restore when anoma backend supports strings
 -- terminating
 -- map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
---   if (null x) nil (f (phead x) :: map'' f (tail x));
+--   if (isEmpty x) nil (f (phead x) :: map'' f (tail x));
 
 lst : List Nat := 0 :: 1 :: nil;
 
 main : List Nat :=
-  trace (null lst)
-    >-> trace (null (nil {Nat}))
+  trace (isEmpty lst)
+    >-> trace (isEmpty (nil {Nat}))
     >-> trace (head 1 lst)
     >-> trace (tail lst)
     >-> trace (head 0 (tail lst))
diff --git a/tests/Casm/Compilation/positive/test007.juvix b/tests/Casm/Compilation/positive/test007.juvix
index b2c114dec7..4b1cbfdbc4 100644
--- a/tests/Casm/Compilation/positive/test007.juvix
+++ b/tests/Casm/Compilation/positive/test007.juvix
@@ -12,8 +12,8 @@ map' {A B} (f : A → B) : List A → List B :=
 lst : List Nat := 0 :: 1 :: nil;
 
 main : Nat :=
-  ite (null lst) 1 0
-    + ite (null (nil {Nat})) 1 0
+  ite (isEmpty lst) 1 0
+    + ite (isEmpty (nil {Nat})) 1 0
     + head 1 lst
     + head 0 (tail lst)
     + head 0 (tail (map ((+) 1) lst))
diff --git a/tests/Compilation/positive/test007.juvix b/tests/Compilation/positive/test007.juvix
index 054198abb3..844209d5af 100644
--- a/tests/Compilation/positive/test007.juvix
+++ b/tests/Compilation/positive/test007.juvix
@@ -11,7 +11,7 @@ map' {A B} (f : A → B) : List A → List B :=
 
 terminating
 map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
-  ite (null x) nil (f (phead x) :: map'' f (tail x));
+  ite (isEmpty x) nil (f (phead x) :: map'' f (tail x));
 
 lst : List Nat := 0 :: 1 :: nil;
 
@@ -24,8 +24,8 @@ printNatListLn (lst : List Nat) : IO :=
   printNatList lst >>> printString "\n";
 
 main : IO :=
-  printBoolLn (null lst)
-    >>> printBoolLn (null (nil {Nat}))
+  printBoolLn (isEmpty lst)
+    >>> printBoolLn (isEmpty (nil {Nat}))
     >>> printNatLn (head 1 lst)
     >>> printNatListLn (tail lst)
     >>> printNatLn (head 0 (tail lst))
diff --git a/tests/Rust/Compilation/positive/test007.juvix b/tests/Rust/Compilation/positive/test007.juvix
index b2c114dec7..4b1cbfdbc4 100644
--- a/tests/Rust/Compilation/positive/test007.juvix
+++ b/tests/Rust/Compilation/positive/test007.juvix
@@ -12,8 +12,8 @@ map' {A B} (f : A → B) : List A → List B :=
 lst : List Nat := 0 :: 1 :: nil;
 
 main : Nat :=
-  ite (null lst) 1 0
-    + ite (null (nil {Nat})) 1 0
+  ite (isEmpty lst) 1 0
+    + ite (isEmpty (nil {Nat})) 1 0
     + head 1 lst
     + head 0 (tail lst)
     + head 0 (tail (map ((+) 1) lst))
diff --git a/tests/smoke/Commands/dev/repl.smoke.yaml b/tests/smoke/Commands/dev/repl.smoke.yaml
index 6dec6075e2..f3522de189 100644
--- a/tests/smoke/Commands/dev/repl.smoke.yaml
+++ b/tests/smoke/Commands/dev/repl.smoke.yaml
@@ -68,14 +68,14 @@ tests:
           Stdlib.Prelude> \1
     exit-status: 0
 
-  - name: check-type-null
+  - name: check-type-isEmpty
     command:
       - juvix
       - dev
       - repl
     stdout:
       contains: "{A : Type} -> (list : List A) -> Bool"
-    stdin: ":type null"
+    stdin: ":type isEmpty"
     exit-status: 0
 
   - name: check-type-suc
diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml
index 014d019ee5..7afe2d5afb 100644
--- a/tests/smoke/Commands/repl.smoke.yaml
+++ b/tests/smoke/Commands/repl.smoke.yaml
@@ -151,13 +151,13 @@ tests:
           Stdlib.Prelude> \1
     exit-status: 0
 
-  - name: check-type-null
+  - name: check-type-isEmpty
     command:
       - juvix
       - repl
     stdout:
       contains: "{A : Type} -> (list : List A) -> Bool"
-    stdin: ":type null"
+    stdin: ":type isEmpty"
     exit-status: 0
 
   - name: check-type-suc