From 6126fe1618efc0696de44905dc5d75cf1977ea21 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 1 Aug 2024 11:38:53 +0100
Subject: [PATCH] Update native and anoma bytes test to use stdlib

---
 juvix-stdlib                                  |  2 +-
 test/Anoma/Compilation/Positive.hs            | 13 ++++++-
 .../Anoma/Compilation/positive/test081.juvix  | 36 ++++++++++++++----
 tests/Compilation/positive/out/test078.out    |  3 ++
 tests/Compilation/positive/test078.juvix      | 38 +++++--------------
 5 files changed, 54 insertions(+), 38 deletions(-)

diff --git a/juvix-stdlib b/juvix-stdlib
index 297601a98d..d8eea7a203 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 297601a98dcace657aaff6e42945f1430647885b
+Subproject commit d8eea7a2038f93fa2f2100434742cd9773300b43
diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
index dc8c25ec9d..fea8d489cf 100644
--- a/test/Anoma/Compilation/Positive.hs
+++ b/test/Anoma/Compilation/Positive.hs
@@ -601,7 +601,16 @@ allTests =
         $(mkRelFile "test081.juvix")
         []
         $ checkOutput
-          [ [nock| 255 |],
-            [nock| 0 |]
+          [ [nock| 1 |],
+            [nock| 255 |],
+            [nock| 2 |],
+            [nock| true |],
+            [nock| true |],
+            [nock| false |],
+            [nock| 1 |],
+            [nock| 238 |],
+            [nock| 3 |],
+            [nock| 240 |],
+            [nock| [1 238 3 2 nil] |]
           ]
     ]
diff --git a/tests/Anoma/Compilation/positive/test081.juvix b/tests/Anoma/Compilation/positive/test081.juvix
index cb5f437ab6..a34823b9b3 100644
--- a/tests/Anoma/Compilation/positive/test081.juvix
+++ b/tests/Anoma/Compilation/positive/test081.juvix
@@ -1,13 +1,35 @@
 module test081;
 
-import Stdlib.Data.Nat open hiding {fromNat};
+import Stdlib.Prelude open;
 import Stdlib.Debug.Trace open;
-import Stdlib.Function open using {>->};
 
-builtin byte
-axiom Byte : Type;
+n1 : Byte := fromNat 1;
 
-builtin byte-from-nat
-axiom fromNat : Nat -> Byte;
+n2 : Byte := fromNat 0xff;
 
-main : Byte := trace (fromNat 0xff) >-> fromNat 0x100;
+n3 : Byte := fromNat 0x102;
+
+l1 : Byte := 1;
+
+l2 : Byte := 0xee;
+
+l3 : Byte := 0x103;
+
+xs : List Byte := [l1; l2; l3; 2];
+
+printByteLn : Byte -> IO := Show.show >> printStringLn;
+
+printListByteLn : List Byte -> IO := Show.show >> printStringLn;
+
+main : List Byte :=
+  trace n1
+    >-> trace n2
+    >-> trace n3
+    >-> trace (n1 == l1)
+    >-> trace (l1 == 0x101)
+    >-> trace (l2 == n2)
+    >-> trace (Byte.toNat l1)
+    >-> trace (Byte.toNat l2)
+    >-> trace (Byte.toNat l3)
+    >-> trace (Byte.toNat 0xf0)
+    >-> xs;
diff --git a/tests/Compilation/positive/out/test078.out b/tests/Compilation/positive/out/test078.out
index 586cfa0b6d..6224a0c855 100644
--- a/tests/Compilation/positive/out/test078.out
+++ b/tests/Compilation/positive/out/test078.out
@@ -1,6 +1,9 @@
 1
 255
 2
+true
+true
+false
 1
 238
 3
diff --git a/tests/Compilation/positive/test078.juvix b/tests/Compilation/positive/test078.juvix
index 81ab048a57..898160edb7 100644
--- a/tests/Compilation/positive/test078.juvix
+++ b/tests/Compilation/positive/test078.juvix
@@ -1,27 +1,6 @@
 module test078;
 
-import Stdlib.Data.Nat open hiding {fromNat};
-import Stdlib.Debug.Trace open;
-import Stdlib.Function open using {>->; >>};
-import Stdlib.Data.List open;
-import Stdlib.Trait.FromNatural open;
-import Stdlib.Trait.Functor open;
-import Stdlib.System.IO open;
-
-builtin byte
-axiom Byte : Type;
-
-builtin byte-from-nat
-axiom byteFromNat : Nat -> Byte;
-
-builtin byte-to-nat
-axiom toNat : Byte -> Nat;
-
-instance
-ByteFromNaturalI : FromNatural Byte :=
-  mkFromNatural@{
-    fromNat := byteFromNat
-  };
+import Stdlib.Prelude open;
 
 n1 : Byte := fromNat 1;
 
@@ -37,16 +16,19 @@ l3 : Byte := 0x103;
 
 xs : List Byte := [l1; l2; l3; 2];
 
-printByteLn : Byte -> IO := toNat >> printNatLn;
+printByteLn : Byte -> IO := Show.show >> printStringLn;
 
-printListByteLn : List Byte -> IO := map toNat >> Show.show >> printStringLn;
+printListByteLn : List Byte -> IO := Show.show >> printStringLn;
 
 main : IO :=
   printByteLn n1
     >>> printByteLn n2
     >>> printByteLn n3
-    >>> printNatLn (toNat l1)
-    >>> printNatLn (toNat l2)
-    >>> printNatLn (toNat l3)
-    >>> printNatLn (toNat 0xf0)
+    >>> printBoolLn (n1 == l1)
+    >>> printBoolLn (l1 == 0x101)
+    >>> printBoolLn (l2 == n2)
+    >>> printNatLn (Byte.toNat l1)
+    >>> printNatLn (Byte.toNat l2)
+    >>> printNatLn (Byte.toNat l3)
+    >>> printNatLn (Byte.toNat 0xf0)
     >>> printListByteLn xs;