Update native and anoma bytes test to use stdlib

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] |]
           ]
     ]

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;

tests/Compilation/positive/out/test078.out

@@ -1,6 +1,9 @@
 1
 255
 2
+true
+true
+false
 1
 238
 3

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;