RefC Integer Support (#1480)

* Add utility functions to treat All as a heterogeneous container
* Distinguish RefC Int and Bits types
* Change RefC Integers to be arbitrary precision
* Add RefC Bits maths operations
* Make RefC div and mod Euclidean
* Add RefC bit-ops tests
* Add RefC integer comparison tests
* Add RefC IntN support

libs/base/Data/List/Quantifiers.idr

@@ -74,6 +74,21 @@ namespace All
   mapProperty f [] = []
   mapProperty f (p::pl) = f p :: mapProperty f pl
 
+  ||| Modify the property given a pointwise interface function
+  public export
+  imapProperty : (0 i : Type -> Type)
+              -> (f : {0 a : Type} -> i a => p a -> q a)
+              -> {0 types : List Type}
+              -> All i types => All p types -> All q types
+  imapProperty i f @{[]} [] = []
+  imapProperty i f @{ix :: ixs} (x :: xs) = f @{ix} x :: imapProperty i f @{ixs} xs
+
+  ||| Forget property source for a homogeneous collection of properties
+  public export
+  forget : All (const type) types -> List type
+  forget [] = []
+  forget (x :: xs) = x :: forget xs
+
   ||| Given a decision procedure for a property, decide whether all elements of
   ||| a list satisfy it.
   |||
@@ -97,6 +112,20 @@ namespace All
   zipPropertyWith f (px :: pxs) (qx :: qxs)
     = f px qx :: zipPropertyWith f pxs qxs
 
+  export
+  All Show (map p xs) => Show (All p xs) where
+    show pxs = "[" ++ show' "" pxs ++ "]"
+      where
+        show' : String -> All Show (map p xs') => All p xs' -> String
+        show' acc @{[]} [] = acc
+        show' acc @{[_]} [px] = acc ++ show px
+        show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
+
+  ||| A heterogeneous list of arbitrary types
+  public export
+  HList : List Type -> Type
+  HList = All id
+
 ------------------------------------------------------------------------
 -- Relationship between all and any
 

nix/package.nix

@@ -2,6 +2,7 @@
 , lib
 , chez
 , clang
+, gmp
 , fetchFromGitHub
 , makeWrapper
 , idris2-version
@@ -19,7 +20,7 @@ stdenv.mkDerivation rec {
 
   strictDeps = true;
   nativeBuildInputs = [ makeWrapper clang chez ];
-  buildInputs = [ chez ];
+  buildInputs = [ chez gmp ];
 
   prePatch = ''
     patchShebangs --build tests

src/Compiler/RefC/CC.idr

@@ -62,7 +62,7 @@ compileCFile {asShared} objectFile outFile =
                        "-lidris2_refc " ++
                        "-L" ++ fullprefix_dir dirs "refc " ++
                        clibdirs (lib_dirs dirs) ++
-                       "-lm"
+                       "-lgmp -lm"
 
      log "compiler.refc.cc" 10 runcc
      0 <- coreLift $ system runcc

src/Compiler/RefC/RefC.idr

@@ -98,22 +98,30 @@ where
 
 
 cConstant : Constant -> String
-cConstant (I x) = "(Value*)makeInt32("++ show x ++")"
+cConstant (I x) = "(Value*)makeInt64("++ show x ++")"
-cConstant (BI x) = "(Value*)makeInt64("++ show x ++")"
+cConstant (I8 x) = "(Value*)makeInt8("++ show x ++")"
+cConstant (I16 x) = "(Value*)makeInt16("++ show x ++")"
+cConstant (I32 x) = "(Value*)makeInt32("++ show x ++")"
+cConstant (I64 x) = "(Value*)makeInt64("++ show x ++")"
+cConstant (BI x) = "(Value*)makeIntegerLiteral(\""++ show x ++"\")"
 cConstant (Db x) = "(Value*)makeDouble("++ show x ++")"
 cConstant (Ch x) = "(Value*)makeChar("++ escapeChar x ++")"
 cConstant (Str x) = "(Value*)makeString("++ cStringQuoted x ++")"
 cConstant WorldVal = "(Value*)makeWorld()"
-cConstant IntType = "i32"
+cConstant IntType = "Int64"
-cConstant IntegerType = "i64"
+cConstant Int8Type = "Int8"
+cConstant Int16Type = "Int16"
+cConstant Int32Type = "Int32"
+cConstant Int64Type = "Int64"
+cConstant IntegerType = "Integer"
 cConstant StringType = "string"
 cConstant CharType = "char"
 cConstant DoubleType = "double"
 cConstant WorldType = "f32"
-cConstant (B8 x)   = "(Value*)makeInt8("++ show x ++")"
+cConstant (B8 x)   = "(Value*)makeBits8("++ show x ++")"
-cConstant (B16 x)  = "(Value*)makeInt16("++ show x ++")"
+cConstant (B16 x)  = "(Value*)makeBits16("++ show x ++")"
-cConstant (B32 x)  = "(Value*)makeInt32("++ show x ++")"
+cConstant (B32 x)  = "(Value*)makeBits32("++ show x ++")"
-cConstant (B64 x)  = "(Value*)makeInt64("++ show x ++")"
+cConstant (B64 x)  = "(Value*)makeBits64("++ show x ++")"
 cConstant Bits8Type = "Bits8"
 cConstant Bits16Type = "Bits16"
 cConstant Bits32Type = "Bits32"
@@ -123,6 +131,10 @@ cConstant n = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw constant in C
 
 extractConstant : Constant -> String
 extractConstant (I x) = show x
+extractConstant (I8 x) = show x
+extractConstant (I16 x) = show x
+extractConstant (I32 x) = show x
+extractConstant (I64 x) = show x
 extractConstant (BI x) = show x
 extractConstant (Db x) = show x
 extractConstant (Ch x) = show x
@@ -400,6 +412,10 @@ integer_switch [] = True
 integer_switch (MkAConstAlt c _  :: _) =
     case c of
         (I x) => True
+        (I8 x) => True
+        (I16 x) => True
+        (I32 x) => True
+        (I64 x) => True
         (BI x) => True
         (Ch x) => True
         _ => False
@@ -408,6 +424,10 @@ const2Integer : Constant -> Integer -> Integer
 const2Integer c i =
     case c of
         (I x) => cast x
+        (I8 x) => x
+        (I16 x) => x
+        (I32 x) => x
+        (I64 x) => x
         (BI x) => x
         (Ch x) => cast x
         (B8 x) => cast x
@@ -764,11 +784,15 @@ emitFDef funcName ((varType, varName, varCFType) :: xs) = do
 
 extractValue : (cfType:CFType) -> (varName:String) -> String
 extractValue CFUnit          varName = "void"
-extractValue CFInt           varName = "((Value_Int32*)" ++ varName ++ ")->i32"
+extractValue CFInt           varName = "((Value_Int64*)" ++ varName ++ ")->i64"
-extractValue CFUnsigned8     varName = "((Value_Int8*)" ++ varName ++ ")->i8"
+extractValue CFInt8          varName = "((Value_Int8*)" ++ varName ++ ")->i8"
-extractValue CFUnsigned16    varName = "((Value_Int16*)" ++ varName ++ ")->i16"
+extractValue CFInt16         varName = "((Value_Int16*)" ++ varName ++ ")->i16"
-extractValue CFUnsigned32    varName = "((Value_Int32*)" ++ varName ++ ")->i32"
+extractValue CFInt32         varName = "((Value_Int32*)" ++ varName ++ ")->i32"
-extractValue CFUnsigned64    varName = "((Value_Int64*)" ++ varName ++ ")->i64"
+extractValue CFInt64         varName = "((Value_Int64*)" ++ varName ++ ")->i64"
+extractValue CFUnsigned8     varName = "((Value_Bits8*)" ++ varName ++ ")->ui8"
+extractValue CFUnsigned16    varName = "((Value_Bits16*)" ++ varName ++ ")->ui16"
+extractValue CFUnsigned32    varName = "((Value_Bits32*)" ++ varName ++ ")->ui32"
+extractValue CFUnsigned64    varName = "((Value_Bits64*)" ++ varName ++ ")->ui64"
 extractValue CFString        varName = "((Value_String*)" ++ varName ++ ")->str"
 extractValue CFDouble        varName = "((Value_Double*)" ++ varName ++ ")->d"
 extractValue CFChar          varName = "((Value_Char*)" ++ varName ++ ")->c"
@@ -785,11 +809,15 @@ extractValue n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw FFI type
 
 packCFType : (cfType:CFType) -> (varName:String) -> String
 packCFType CFUnit          varName = "NULL"
-packCFType CFInt           varName = "makeInt32(" ++ varName ++ ")"
+packCFType CFInt           varName = "makeInt64(" ++ varName ++ ")"
-packCFType CFUnsigned64    varName = "makeInt64(" ++ varName ++ ")"
+packCFType CFInt8          varName = "makeInt8(" ++ varName ++ ")"
-packCFType CFUnsigned32    varName = "makeInt32(" ++ varName ++ ")"
+packCFType CFInt16         varName = "makeInt16(" ++ varName ++ ")"
-packCFType CFUnsigned16    varName = "makeInt16(" ++ varName ++ ")"
+packCFType CFInt32         varName = "makeInt32(" ++ varName ++ ")"
-packCFType CFUnsigned8     varName = "makeInt8(" ++ varName ++ ")"
+packCFType CFInt64         varName = "makeInt64(" ++ varName ++ ")"
+packCFType CFUnsigned64    varName = "makeBits64(" ++ varName ++ ")"
+packCFType CFUnsigned32    varName = "makeBits32(" ++ varName ++ ")"
+packCFType CFUnsigned16    varName = "makeBits16(" ++ varName ++ ")"
+packCFType CFUnsigned8     varName = "makeBits8(" ++ varName ++ ")"
 packCFType CFString        varName = "makeString(" ++ varName ++ ")"
 packCFType CFDouble        varName = "makeDouble(" ++ varName ++ ")"
 packCFType CFChar          varName = "makeChar(" ++ varName ++ ")"

support/refc/casts.h

@@ -3,31 +3,66 @@
 
 #include "cBackend.h"
 #include <stdio.h>
+#include <gmp.h>
 
-Value *cast_i32_to_Bits8(Value *);
+Value *cast_Int8_to_Bits8(Value *);
-Value *cast_i32_to_Bits16(Value *);
+Value *cast_Int8_to_Bits16(Value *);
-Value *cast_i32_to_Bits32(Value *);
+Value *cast_Int8_to_Bits32(Value *);
-Value *cast_i32_to_Bits64(Value *);
+Value *cast_Int8_to_Bits64(Value *);
-Value *cast_i32_to_i64(Value *);
+Value *cast_Int8_to_Int16(Value *);
-Value *cast_i32_to_double(Value *);
+Value *cast_Int8_to_Int32(Value *);
-Value *cast_i32_to_char(Value *);
+Value *cast_Int8_to_Int64(Value *);
-Value *cast_i32_to_string(Value *);
+Value *cast_Int8_to_Integer(Value *);
+Value *cast_Int8_to_double(Value *);
+Value *cast_Int8_to_char(Value *);
+Value *cast_Int8_to_string(Value *);
 
-Value *cast_i64_to_Bits8(Value *);
+Value *cast_Int16_to_Bits8(Value *);
-Value *cast_i64_to_Bits16(Value *);
+Value *cast_Int16_to_Bits16(Value *);
-Value *cast_i64_to_Bits32(Value *);
+Value *cast_Int16_to_Bits32(Value *);
-Value *cast_i64_to_Bits64(Value *);
+Value *cast_Int16_to_Bits64(Value *);
-Value *cast_i64_to_i32(Value *);
+Value *cast_Int16_to_Int8(Value *);
-Value *cast_i64_to_double(Value *);
+Value *cast_Int16_to_Int32(Value *);
-Value *cast_i64_to_char(Value *);
+Value *cast_Int16_to_Int64(Value *);
-Value *cast_i64_to_string(Value *);
+Value *cast_Int16_to_Integer(Value *);
+Value *cast_Int16_to_double(Value *);
+Value *cast_Int16_to_char(Value *);
+Value *cast_Int16_to_string(Value *);
+
+Value *cast_Int32_to_Bits8(Value *);
+Value *cast_Int32_to_Bits16(Value *);
+Value *cast_Int32_to_Bits32(Value *);
+Value *cast_Int32_to_Bits64(Value *);
+Value *cast_Int32_to_Int8(Value *);
+Value *cast_Int32_to_Int16(Value *);
+Value *cast_Int32_to_Int64(Value *);
+Value *cast_Int32_to_Integer(Value *);
+Value *cast_Int32_to_double(Value *);
+Value *cast_Int32_to_char(Value *);
+Value *cast_Int32_to_string(Value *);
+
+Value *cast_Int64_to_Bits8(Value *);
+Value *cast_Int64_to_Bits16(Value *);
+Value *cast_Int64_to_Bits32(Value *);
+Value *cast_Int64_to_Bits64(Value *);
+Value *cast_Int64_to_Int8(Value *);
+Value *cast_Int64_to_Int16(Value *);
+Value *cast_Int64_to_Int32(Value *);
+Value *cast_Int64_to_Int64(Value *);
+Value *cast_Int64_to_Integer(Value *);
+Value *cast_Int64_to_double(Value *);
+Value *cast_Int64_to_char(Value *);
+Value *cast_Int64_to_string(Value *);
 
 Value *cast_double_to_Bits8(Value *);
 Value *cast_double_to_Bits16(Value *);
 Value *cast_double_to_Bits32(Value *);
 Value *cast_double_to_Bits64(Value *);
-Value *cast_double_to_i32(Value *);
+Value *cast_double_to_Int8(Value *);
-Value *cast_double_to_i64(Value *);
+Value *cast_double_to_Int16(Value *);
+Value *cast_double_to_Int32(Value *);
+Value *cast_double_to_Int64(Value *);
+Value *cast_double_to_Integer(Value *);
 Value *cast_double_to_char(Value *);
 Value *cast_double_to_string(Value *);
 
@@ -35,8 +70,11 @@ Value *cast_char_to_Bits8(Value *);
 Value *cast_char_to_Bits16(Value *);
 Value *cast_char_to_Bits32(Value *);
 Value *cast_char_to_Bits64(Value *);
-Value *cast_char_to_i32(Value *);
+Value *cast_char_to_Int8(Value *);
-Value *cast_char_to_i64(Value *);
+Value *cast_char_to_Int16(Value *);
+Value *cast_char_to_Int32(Value *);
+Value *cast_char_to_Int64(Value *);
+Value *cast_char_to_Integer(Value *);
 Value *cast_char_to_double(Value *);
 Value *cast_char_to_string(Value *);
 
@@ -44,42 +82,72 @@ Value *cast_string_to_Bits8(Value *);
 Value *cast_string_to_Bits16(Value *);
 Value *cast_string_to_Bits32(Value *);
 Value *cast_string_to_Bits64(Value *);
-Value *cast_string_to_i32(Value *);
+Value *cast_string_to_Int8(Value *);
-Value *cast_string_to_i64(Value *);
+Value *cast_string_to_Int16(Value *);
+Value *cast_string_to_Int32(Value *);
+Value *cast_string_to_Int64(Value *);
+Value *cast_string_to_Integer(Value *);
 Value *cast_string_to_double(Value *);
 Value *cast_string_to_char(Value *);
 
 Value *cast_Bits8_to_Bits16(Value *input);
 Value *cast_Bits8_to_Bits32(Value *input);
 Value *cast_Bits8_to_Bits64(Value *input);
-Value *cast_Bits8_to_i32(Value *input);
+Value *cast_Bits8_to_Int8(Value *input);
-Value *cast_Bits8_to_i64(Value *input);
+Value *cast_Bits8_to_Int16(Value *input);
+Value *cast_Bits8_to_Int32(Value *input);
+Value *cast_Bits8_to_Int64(Value *input);
+Value *cast_Bits8_to_Integer(Value *input);
 Value *cast_Bits8_to_double(Value *input);
 Value *cast_Bits8_to_char(Value *input);
 Value *cast_Bits8_to_string(Value *input);
+
 Value *cast_Bits16_to_Bits8(Value *input);
 Value *cast_Bits16_to_Bits32(Value *input);
 Value *cast_Bits16_to_Bits64(Value *input);
-Value *cast_Bits16_to_i32(Value *input);
+Value *cast_Bits16_to_Int8(Value *input);
-Value *cast_Bits16_to_i64(Value *input);
+Value *cast_Bits16_to_Int16(Value *input);
+Value *cast_Bits16_to_Int32(Value *input);
+Value *cast_Bits16_to_Int64(Value *input);
+Value *cast_Bits16_to_Integer(Value *input);
 Value *cast_Bits16_to_double(Value *input);
 Value *cast_Bits16_to_char(Value *input);
 Value *cast_Bits16_to_string(Value *input);
+
 Value *cast_Bits32_to_Bits8(Value *input);
 Value *cast_Bits32_to_Bits16(Value *input);
 Value *cast_Bits32_to_Bits64(Value *input);
-Value *cast_Bits32_to_i32(Value *input);
+Value *cast_Bits32_to_Int8(Value *input);
-Value *cast_Bits32_to_i64(Value *input);
+Value *cast_Bits32_to_Int16(Value *input);
+Value *cast_Bits32_to_Int32(Value *input);
+Value *cast_Bits32_to_Int64(Value *input);
+Value *cast_Bits32_to_Integer(Value *input);
 Value *cast_Bits32_to_double(Value *input);
 Value *cast_Bits32_to_char(Value *input);
 Value *cast_Bits32_to_string(Value *input);
+
 Value *cast_Bits64_to_Bits8(Value *input);
 Value *cast_Bits64_to_Bits16(Value *input);
 Value *cast_Bits64_to_Bits32(Value *input);
-Value *cast_Bits64_to_i32(Value *input);
+Value *cast_Bits64_to_Int8(Value *input);
-Value *cast_Bits64_to_i64(Value *input);
+Value *cast_Bits64_to_Int16(Value *input);
+Value *cast_Bits64_to_Int32(Value *input);
+Value *cast_Bits64_to_Int64(Value *input);
+Value *cast_Bits64_to_Integer(Value *input);
 Value *cast_Bits64_to_double(Value *input);
 Value *cast_Bits64_to_char(Value *input);
 Value *cast_Bits64_to_string(Value *input);
 
+Value *cast_Integer_to_Bits8(Value *input);
+Value *cast_Integer_to_Bits16(Value *input);
+Value *cast_Integer_to_Bits32(Value *input);
+Value *cast_Integer_to_Bits64(Value *input);
+Value *cast_Integer_to_Int8(Value *input);
+Value *cast_Integer_to_Int16(Value *input);
+Value *cast_Integer_to_Int32(Value *input);
+Value *cast_Integer_to_Int64(Value *input);
+Value *cast_Integer_to_double(Value *input);
+Value *cast_Integer_to_char(Value *input);
+Value *cast_Integer_to_string(Value *input);
+
 #endif

support/refc/clock.c

@@ -10,13 +10,13 @@ Value *clockTimeMonotonic()
 
 Value *clockTimeUtc()
 {
-    return (Value *)makeInt64(time(NULL) * NSEC_PER_SEC);
+    return (Value *)makeBits64(time(NULL) * NSEC_PER_SEC);
 }
 
 Value *clockTimeProcess()
 {
     uint64_t time_ns = clock() / CLOCKS_PER_NSEC;
-    return (Value *)makeInt64(time_ns);
+    return (Value *)makeBits64(time_ns);
 }
 
 Value *clockTimeThread()
@@ -41,12 +41,12 @@ int clockValid(Value *clock)
 
 uint64_t clockSecond(Value *clock)
 {
-    uint64_t totalNano = ((Value_Int64 *)clock)->i64;
+    uint64_t totalNano = ((Value_Bits64 *)clock)->ui64;
     return totalNano / NSEC_PER_SEC;
 }
 
 uint64_t clockNanosecond(Value *clock)
 {
-    uint64_t totalNano = ((Value_Int64 *)clock)->i64;
+    uint64_t totalNano = ((Value_Bits64 *)clock)->ui64;
     return totalNano % NSEC_PER_SEC;
 }

support/refc/datatypes.h

@@ -5,19 +5,25 @@
 #include <string.h>
 #include <pthread.h>
 #include <stdint.h>
+#include <gmp.h>
 
 #define NO_TAG 0
-#define INT8_TAG 1
+#define BITS8_TAG 1
-#define INT16_TAG 2
+#define BITS16_TAG 2
-#define INT32_TAG 3
+#define BITS32_TAG 3
-#define INT64_TAG 4
+#define BITS64_TAG 4
-#define DOUBLE_TAG 5
+#define INT8_TAG 5
-#define CHAR_TAG 6
+#define INT16_TAG 6
-#define STRING_TAG 7
+#define INT32_TAG 7
+#define INT64_TAG 8
+#define INTEGER_TAG 9
+#define DOUBLE_TAG 10
+#define CHAR_TAG 11
+#define STRING_TAG 12
 
-#define CLOSURE_TAG 10
+#define CLOSURE_TAG 15
-#define ARGLIST_TAG 11
+#define ARGLIST_TAG 16
-#define CONSTRUCTOR_TAG 12
+#define CONSTRUCTOR_TAG 17
 
 #define IOREF_TAG 20
 #define ARRAY_TAG 21
@@ -46,13 +52,37 @@ typedef struct
 typedef struct
 {
     Value_header header;
-    uint8_t i8;
+    uint8_t ui8;
+} Value_Bits8;
+
+typedef struct
+{
+    Value_header header;
+    uint16_t ui16;
+} Value_Bits16;
+
+typedef struct
+{
+    Value_header header;
+    uint32_t ui32;
+} Value_Bits32;
+
+typedef struct
+{
+    Value_header header;
+    uint64_t ui64;
+} Value_Bits64;
+
+typedef struct
+{
+    Value_header header;
+    int8_t i8;
 } Value_Int8;
 
 typedef struct
 {
     Value_header header;
-    uint16_t i16;
+    int16_t i16;
 } Value_Int16;
 
 typedef struct
@@ -67,6 +97,12 @@ typedef struct
     int64_t i64;
 } Value_Int64;
 
+typedef struct
+{
+    Value_header header;
+    mpz_t i;
+} Value_Integer;
+
 typedef struct
 {
     Value_header header;

support/refc/mathFunctions.h

@@ -2,90 +2,203 @@
 #define __MATH_FUNCTIONS_H__
 #include "cBackend.h"
 #include <math.h>
+#include <gmp.h>
 
 double unpackDouble(Value *d);
 Value *believe_me(Value *, Value *, Value *);
 
 /* add */
-Value *add_i32(Value *x, Value *y);
+Value *add_Bits8(Value *x, Value *y);
-Value *add_i64(Value *x, Value *y);
+Value *add_Bits16(Value *x, Value *y);
+Value *add_Bits32(Value *x, Value *y);
+Value *add_Bits64(Value *x, Value *y);
+Value *add_Int8(Value *x, Value *y);
+Value *add_Int16(Value *x, Value *y);
+Value *add_Int32(Value *x, Value *y);
+Value *add_Int64(Value *x, Value *y);
+Value *add_Integer(Value *x, Value *y);
 Value *add_double(Value *x, Value *y);
 
 /* sub */
-Value *sub_i32(Value *x, Value *y);
+Value *sub_Bits8(Value *x, Value *y);
-Value *sub_i64(Value *x, Value *y);
+Value *sub_Bits16(Value *x, Value *y);
+Value *sub_Bits32(Value *x, Value *y);
+Value *sub_Bits64(Value *x, Value *y);
+Value *sub_Int8(Value *x, Value *y);
+Value *sub_Int16(Value *x, Value *y);
+Value *sub_Int32(Value *x, Value *y);
+Value *sub_Int64(Value *x, Value *y);
+Value *sub_Integer(Value *x, Value *y);
 Value *sub_double(Value *x, Value *y);
 
 /* negate */
-Value *negate_i32(Value *x);
+Value *negate_Bits8(Value *x);
-Value *negate_i64(Value *x);
+Value *negate_Bits16(Value *x);
+Value *negate_Bits32(Value *x);
+Value *negate_Bits64(Value *x);
+Value *negate_Int8(Value *x);
+Value *negate_Int16(Value *x);
+Value *negate_Int32(Value *x);
+Value *negate_Int64(Value *x);
+Value *negate_Integer(Value *x);
 Value *negate_double(Value *x);
 
 /* mul */
-Value *mul_i32(Value *x, Value *y);
+Value *mul_Bits8(Value *x, Value *y);
-Value *mul_i64(Value *x, Value *y);
+Value *mul_Bits16(Value *x, Value *y);
+Value *mul_Bits32(Value *x, Value *y);
+Value *mul_Bits64(Value *x, Value *y);
+Value *mul_Int8(Value *x, Value *y);
+Value *mul_Int16(Value *x, Value *y);
+Value *mul_Int32(Value *x, Value *y);
+Value *mul_Int64(Value *x, Value *y);
+Value *mul_Integer(Value *x, Value *y);
 Value *mul_double(Value *x, Value *y);
 
 /* div */
-Value *div_i32(Value *x, Value *y);
+Value *div_Bits8(Value *x, Value *y);
-Value *div_i64(Value *x, Value *y);
+Value *div_Bits16(Value *x, Value *y);
+Value *div_Bits32(Value *x, Value *y);
+Value *div_Bits64(Value *x, Value *y);
+Value *div_Int8(Value *x, Value *y);
+Value *div_Int16(Value *x, Value *y);
+Value *div_Int32(Value *x, Value *y);
+Value *div_Int64(Value *x, Value *y);
+Value *div_Integer(Value *x, Value *y);
 Value *div_double(Value *x, Value *y);
 
 /* mod */
-Value *mod_i32(Value *x, Value *y);
+Value *mod_Bits8(Value *x, Value *y);
-Value *mod_i64(Value *x, Value *y);
+Value *mod_Bits16(Value *x, Value *y);
+Value *mod_Bits32(Value *x, Value *y);
+Value *mod_Bits64(Value *x, Value *y);
+Value *mod_Int8(Value *x, Value *y);
+Value *mod_Int16(Value *x, Value *y);
+Value *mod_Int32(Value *x, Value *y);
+Value *mod_Int64(Value *x, Value *y);
+Value *mod_Integer(Value *x, Value *y);
 
 /* shiftl */
-Value *shiftl_i32(Value *x, Value *y);
+Value *shiftl_Bits8(Value *x, Value *y);
-Value *shiftl_i64(Value *x, Value *y);
+Value *shiftl_Bits16(Value *x, Value *y);
+Value *shiftl_Bits32(Value *x, Value *y);
+Value *shiftl_Bits64(Value *x, Value *y);
+Value *shiftl_Int8(Value *x, Value *y);
+Value *shiftl_Int16(Value *x, Value *y);
+Value *shiftl_Int32(Value *x, Value *y);
+Value *shiftl_Int64(Value *x, Value *y);
+Value *shiftl_Integer(Value *x, Value *y);
 
 /* shiftr */
-Value *shiftr_i32(Value *x, Value *y);
+Value *shiftr_Bits8(Value *x, Value *y);
-Value *shiftr_i64(Value *x, Value *y);
+Value *shiftr_Bits16(Value *x, Value *y);
+Value *shiftr_Bits32(Value *x, Value *y);
+Value *shiftr_Bits64(Value *x, Value *y);
+Value *shiftr_Int8(Value *x, Value *y);
+Value *shiftr_Int16(Value *x, Value *y);
+Value *shiftr_Int32(Value *x, Value *y);
+Value *shiftr_Int64(Value *x, Value *y);
+Value *shiftr_Integer(Value *x, Value *y);
 
 /* and */
-Value *and_i32(Value *x, Value *y);
+Value *and_Bits8(Value *x, Value *y);
-Value *and_i64(Value *x, Value *y);
+Value *and_Bits16(Value *x, Value *y);
+Value *and_Bits32(Value *x, Value *y);
+Value *and_Bits64(Value *x, Value *y);
+Value *and_Int8(Value *x, Value *y);
+Value *and_Int16(Value *x, Value *y);
+Value *and_Int32(Value *x, Value *y);
+Value *and_Int64(Value *x, Value *y);
+Value *and_Integer(Value *x, Value *y);
 
 /* or */
-Value *or_i32(Value *x, Value *y);
+Value *or_Bits8(Value *x, Value *y);
-Value *or_i64(Value *x, Value *y);
+Value *or_Bits16(Value *x, Value *y);
+Value *or_Bits32(Value *x, Value *y);
+Value *or_Bits64(Value *x, Value *y);
+Value *or_Int8(Value *x, Value *y);
+Value *or_Int16(Value *x, Value *y);
+Value *or_Int32(Value *x, Value *y);
+Value *or_Int64(Value *x, Value *y);
+Value *or_Integer(Value *x, Value *y);
 
 /* xor */
-Value *xor_i32(Value *x, Value *y);
+Value *xor_Bits8(Value *x, Value *y);
-Value *xor_i64(Value *x, Value *y);
+Value *xor_Bits16(Value *x, Value *y);
+Value *xor_Bits32(Value *x, Value *y);
+Value *xor_Bits64(Value *x, Value *y);
+Value *xor_Int8(Value *x, Value *y);
+Value *xor_Int16(Value *x, Value *y);
+Value *xor_Int32(Value *x, Value *y);
+Value *xor_Int64(Value *x, Value *y);
+Value *xor_Integer(Value *x, Value *y);
 
 /* lt */
-Value *lt_i32(Value *x, Value *y);
+Value *lt_Bits8(Value *x, Value *y);
-Value *lt_i64(Value *x, Value *y);
+Value *lt_Bits16(Value *x, Value *y);
+Value *lt_Bits32(Value *x, Value *y);
+Value *lt_Bits64(Value *x, Value *y);
+Value *lt_Int8(Value *x, Value *y);
+Value *lt_Int16(Value *x, Value *y);
+Value *lt_Int32(Value *x, Value *y);
+Value *lt_Int64(Value *x, Value *y);
+Value *lt_Integer(Value *x, Value *y);
 Value *lt_double(Value *x, Value *y);
 Value *lt_char(Value *x, Value *y);
 Value *lt_string(Value *x, Value *y);
 
 /* gt */
-Value *gt_i32(Value *x, Value *y);
+Value *gt_Bits8(Value *x, Value *y);
-Value *gt_i64(Value *x, Value *y);
+Value *gt_Bits16(Value *x, Value *y);
+Value *gt_Bits32(Value *x, Value *y);
+Value *gt_Bits64(Value *x, Value *y);
+Value *gt_Int8(Value *x, Value *y);
+Value *gt_Int16(Value *x, Value *y);
+Value *gt_Int32(Value *x, Value *y);
+Value *gt_Int64(Value *x, Value *y);
+Value *gt_Integer(Value *x, Value *y);
 Value *gt_double(Value *x, Value *y);
 Value *gt_char(Value *x, Value *y);
 Value *gt_string(Value *x, Value *y);
 
 /* eq */
-Value *eq_i32(Value *x, Value *y);
+Value *eq_Bits8(Value *x, Value *y);
-Value *eq_i64(Value *x, Value *y);
+Value *eq_Bits16(Value *x, Value *y);
+Value *eq_Bits32(Value *x, Value *y);
+Value *eq_Bits64(Value *x, Value *y);
+Value *eq_Int8(Value *x, Value *y);
+Value *eq_Int16(Value *x, Value *y);
+Value *eq_Int32(Value *x, Value *y);
+Value *eq_Int64(Value *x, Value *y);
+Value *eq_Integer(Value *x, Value *y);
 Value *eq_double(Value *x, Value *y);
 Value *eq_char(Value *x, Value *y);
 Value *eq_string(Value *x, Value *y);
 
 /* lte */
-Value *lte_i32(Value *x, Value *y);
+Value *lte_Bits8(Value *x, Value *y);
-Value *lte_i64(Value *x, Value *y);
+Value *lte_Bits16(Value *x, Value *y);
+Value *lte_Bits32(Value *x, Value *y);
+Value *lte_Bits64(Value *x, Value *y);
+Value *lte_Int8(Value *x, Value *y);
+Value *lte_Int16(Value *x, Value *y);
+Value *lte_Int32(Value *x, Value *y);
+Value *lte_Int64(Value *x, Value *y);
+Value *lte_Integer(Value *x, Value *y);
 Value *lte_double(Value *x, Value *y);
 Value *lte_char(Value *x, Value *y);
 Value *lte_string(Value *x, Value *y);
 
 /* gte */
-Value *gte_i32(Value *x, Value *y);
+Value *gte_Bits8(Value *x, Value *y);
-Value *gte_i64(Value *x, Value *y);
+Value *gte_Bits16(Value *x, Value *y);
+Value *gte_Bits32(Value *x, Value *y);
+Value *gte_Bits64(Value *x, Value *y);
+Value *gte_Int8(Value *x, Value *y);
+Value *gte_Int16(Value *x, Value *y);
+Value *gte_Int32(Value *x, Value *y);
+Value *gte_Int64(Value *x, Value *y);
+Value *gte_Integer(Value *x, Value *y);
 Value *gte_double(Value *x, Value *y);
 Value *gte_char(Value *x, Value *y);
 Value *gte_string(Value *x, Value *y);

support/refc/memoryManagement.c

@@ -62,6 +62,38 @@ Value_Char *makeChar(char c)
     return retVal;
 }
 
+Value_Bits8 *makeBits8(uint8_t i)
+{
+    Value_Bits8 *retVal = (Value_Bits8 *)newValue();
+    retVal->header.tag = BITS8_TAG;
+    retVal->ui8 = i;
+    return retVal;
+}
+
+Value_Bits16 *makeBits16(uint16_t i)
+{
+    Value_Bits16 *retVal = (Value_Bits16 *)newValue();
+    retVal->header.tag = BITS16_TAG;
+    retVal->ui16 = i;
+    return retVal;
+}
+
+Value_Bits32 *makeBits32(uint32_t i)
+{
+    Value_Bits32 *retVal = (Value_Bits32 *)newValue();
+    retVal->header.tag = BITS32_TAG;
+    retVal->ui32 = i;
+    return retVal;
+}
+
+Value_Bits64 *makeBits64(uint64_t i)
+{
+    Value_Bits64 *retVal = (Value_Bits64 *)newValue();
+    retVal->header.tag = BITS64_TAG;
+    retVal->ui64 = i;
+    return retVal;
+}
+
 Value_Int8 *makeInt8(int8_t i)
 {
     Value_Int8 *retVal = (Value_Int8 *)newValue();
@@ -94,6 +126,26 @@ Value_Int64 *makeInt64(int64_t i)
     return retVal;
 }
 
+Value_Int8 *makeBool(int p)
+{
+    return makeInt8(p ? 1 : 0);
+}
+
+Value_Integer *makeInteger()
+{
+    Value_Integer *retVal = (Value_Integer *)newValue();
+    retVal->header.tag = INTEGER_TAG;
+    mpz_init(retVal->i);
+    return retVal;
+}
+
+Value_Integer *makeIntegerLiteral(char *i)
+{
+    Value_Integer *retVal = makeInteger();
+    mpz_set_str(retVal->i, i, 10);
+    return retVal;
+}
+
 Value_String *makeEmptyString(size_t l)
 {
     Value_String *retVal = (Value_String *)newValue();
@@ -180,12 +232,21 @@ void removeReference(Value *elem)
     {
         switch (elem->header.tag)
         {
+        case BITS8_TAG:
+        case BITS16_TAG:
+        case BITS32_TAG:
+        case BITS64_TAG:
+        case INT8_TAG:
+        case INT16_TAG:
         case INT32_TAG:
-            /* nothing to delete, added for sake of completeness */
-            break;
         case INT64_TAG:
             /* nothing to delete, added for sake of completeness */
             break;
+        case INTEGER_TAG:
+        {
+            mpz_clear(((Value_Integer *)elem)->i);
+            break;
+        }
         case DOUBLE_TAG:
             /* nothing to delete, added for sake of completeness */
             break;

support/refc/memoryManagement.h

@@ -14,10 +14,17 @@ Value_Closure *makeClosureFromArglist(fun_ptr_t f, Value_Arglist *);
 
 Value_Double *makeDouble(double d);
 Value_Char *makeChar(char d);
+Value_Bits8 *makeBits8(uint8_t i);
+Value_Bits16 *makeBits16(uint16_t i);
+Value_Bits32 *makeBits32(uint32_t i);
+Value_Bits64 *makeBits64(uint64_t i);
 Value_Int8 *makeInt8(int8_t i);
 Value_Int16 *makeInt16(int16_t i);
 Value_Int32 *makeInt32(int32_t i);
 Value_Int64 *makeInt64(int64_t i);
+Value_Int8 *makeBool(int p);
+Value_Integer *makeInteger();
+Value_Integer *makeIntegerLiteral(char *i);
 Value_String *makeEmptyString(size_t l);
 Value_String *makeString(char *);
 

support/refc/prim.c

@@ -123,14 +123,14 @@ Value *newArray(Value *erased, Value *_length, Value *v, Value *_word)
 Value *arrayGet(Value *erased, Value *_array, Value *_index, Value *_word)
 {
     Value_Array *a = (Value_Array *)_array;
-    return newReference(a->arr[((Value_Int32 *)_index)->i32]);
+    return newReference(a->arr[((Value_Int64 *)_index)->i64]);
 }
 
 Value *arraySet(Value *erased, Value *_array, Value *_index, Value *v, Value *_word)
 {
     Value_Array *a = (Value_Array *)_array;
-    removeReference(a->arr[((Value_Int32 *)_index)->i32]);
+    removeReference(a->arr[((Value_Int64 *)_index)->i64]);
-    a->arr[((Value_Int32 *)_index)->i32] = newReference(v);
+    a->arr[((Value_Int64 *)_index)->i64] = newReference(v);
     return NULL;
 }
 
@@ -252,10 +252,10 @@ Value *System_Concurrency_Raw_prim__conditionWaitTimeout(Value *_condition, Valu
 {
     Value_Condition *cond = (Value_Condition *)_condition;
     Value_Mutex *mutex = (Value_Mutex *)_mutex;
-    Value_Int32 *timeout = (Value_Int32 *)_timeout;
+    Value_Int64 *timeout = (Value_Int64 *)_timeout;
     struct timespec t;
-    t.tv_sec = timeout->i32 / 1000000;
+    t.tv_sec = timeout->i64 / 1000000;
-    t.tv_nsec = timeout->i32 % 1000000;
+    t.tv_nsec = timeout->i64 % 1000000;
     if (pthread_cond_timedwait(cond->cond, mutex->mutex, &t))
     {
         fprintf(stderr, "Error in pthread_cond_timedwait\n");

support/refc/runtime.c

@@ -73,14 +73,29 @@ Value *tailcall_apply_closure(Value *_clos, Value *arg)
 
 int extractInt(Value *v)
 {
-  if (v->header.tag == INT64_TAG)
+  if (v->header.tag == INTEGER_TAG)
   {
-    return (int)((Value_Int64 *)v)->i64;
+    return (int)mpz_get_si(((Value_Integer *)v)->i);
+  }
+
+  if (v->header.tag == INT8_TAG)
+  {
+    return (int)((Value_Int8 *)v)->i8;
+  }
+
+  if (v->header.tag == INT16_TAG)
+  {
+    return (int)((Value_Int16 *)v)->i16;
   }
 
   if (v->header.tag == INT32_TAG)
   {
-    return ((Value_Int32 *)v)->i32;
+    return (int)((Value_Int32 *)v)->i32;
+  }
+
+  if (v->header.tag == INT64_TAG)
+  {
+    return (int)((Value_Int64 *)v)->i64;
   }
 
   if (v->header.tag == DOUBLE_TAG)

support/refc/stringOps.c

@@ -3,7 +3,7 @@
 Value *stringLength(Value *s)
 {
     int length = strlen(((Value_String *)s)->str);
-    return (Value *)makeInt32(length);
+    return (Value *)makeInt64(length);
 }
 
 Value *head(Value *str)
@@ -54,16 +54,9 @@ Value *reverse(Value *str)
 
 Value *strIndex(Value *str, Value *i)
 {
-    Value_Char *c;
+    char *s = ((Value_String *)str)->str;
-    switch (i->header.tag)
+    int idx = ((Value_Int64 *)i)->i64;
-    {
+    return (Value *)makeChar(s[idx]);
-    case INT64_TAG:
-        c = makeChar(((Value_String *)str)->str[((Value_Int64 *)i)->i64]);
-        return (Value *)c;
-    default:
-        c = makeChar(((Value_String *)str)->str[((Value_Int32 *)i)->i32]);
-        return (Value *)c;
-    }
 }
 
 Value *strCons(Value *c, Value *str)

tests/Main.idr

@@ -213,7 +213,7 @@ chezTests = MkTestPool "Chez backend" [Chez]
 refcTests : TestPool
 refcTests = MkTestPool "Reference counting C backend" [C]
     [ "refc001" , "refc002"
-    , "strings", "doubles"
+    , "strings", "integers", "doubles"
     , "buffer", "clock", "args"
     ]
 

tests/refc/integers/IntBits.idr

@@ -0,0 +1,94 @@
+module IntBits
+
+import IntCasts
+import IntEqOrd
+import IntNum
+
+import Data.Bits
+import Data.DPair
+
+-- This file to be deleted once these interfaces are added to base
+
+public export %inline
+Bits Int8 where
+  Index       = Subset Nat (`LT` 8)
+  (.&.)       = prim__and_Int8
+  (.|.)       = prim__or_Int8
+  xor         = prim__xor_Int8
+  bit         = (1 `shiftL`)
+  zeroBits    = 0
+  testBit x i = (x .&. bit i) /= 0
+  shiftR x    = prim__shr_Int8 x . cast . fst
+  shiftL x    = prim__shl_Int8 x . cast . fst
+  complement  = xor (-1)
+  oneBits     = -1
+
+public export %inline
+Bits Int16 where
+  Index       = Subset Nat (`LT` 16)
+  (.&.)       = prim__and_Int16
+  (.|.)       = prim__or_Int16
+  xor         = prim__xor_Int16
+  bit         = (1 `shiftL`)
+  zeroBits    = 0
+  testBit x i = (x .&. bit i) /= 0
+  shiftR x    = prim__shr_Int16 x . cast . fst
+  shiftL x    = prim__shl_Int16 x . cast . fst
+  complement  = xor (-1)
+  oneBits     = -1
+
+public export %inline
+Bits Int32 where
+  Index       = Subset Nat (`LT` 32)
+  (.&.)       = prim__and_Int32
+  (.|.)       = prim__or_Int32
+  xor         = prim__xor_Int32
+  bit         = (1 `shiftL`)
+  zeroBits    = 0
+  testBit x i = (x .&. bit i) /= 0
+  shiftR x    = prim__shr_Int32 x . cast . fst
+  shiftL x    = prim__shl_Int32 x . cast . fst
+  complement  = xor (-1)
+  oneBits     = -1
+
+public export %inline
+Bits Int64 where
+  Index       = Subset Nat (`LT` 64)
+  (.&.)       = prim__and_Int64
+  (.|.)       = prim__or_Int64
+  xor         = prim__xor_Int64
+  bit         = (1 `shiftL`)
+  zeroBits    = 0
+  testBit x i = (x .&. bit i) /= 0
+  shiftR x    = prim__shr_Int64 x . cast . fst
+  shiftL x    = prim__shl_Int64 x . cast . fst
+  complement  = xor (-1)
+  oneBits     = -1
+
+public export %inline
+Bits Bits64 where
+  Index       = Subset Nat (`LT` 64)
+  (.&.)       = prim__and_Bits64
+  (.|.)       = prim__or_Bits64
+  xor         = prim__xor_Bits64
+  bit         = (1 `shiftL`)
+  zeroBits    = 0
+  testBit x i = (x .&. bit i) /= 0
+  shiftR x    = prim__shr_Bits64 x . fromInteger . cast . fst
+  shiftL x    = prim__shl_Bits64 x . fromInteger . cast . fst
+  complement  = xor 0xffffffffffffffff
+  oneBits     = 0xffffffffffffffff
+
+public export %inline
+Bits Integer where
+  Index       = Nat
+  (.&.)       = prim__and_Integer
+  (.|.)       = prim__or_Integer
+  xor         = prim__xor_Integer
+  bit         = (1 `shiftL`)
+  zeroBits    = 0
+  testBit x i = (x .&. bit i) /= 0
+  shiftR x    = prim__shr_Integer x . cast
+  shiftL x    = prim__shl_Integer x . cast
+  complement  = xor (-1)
+  oneBits     = (-1)

tests/refc/integers/IntCasts.idr

@@ -0,0 +1,383 @@
+module IntCasts
+
+import IntNum
+
+-- This file to be deleted once these interfaces are added to prelude
+
+-- To String
+
+export
+Cast Int8 String where
+  cast = prim__cast_Int8String
+
+export
+Cast Int16 String where
+  cast = prim__cast_Int16String
+
+export
+Cast Int32 String where
+  cast = prim__cast_Int32String
+
+export
+Cast Int64 String where
+  cast = prim__cast_Int64String
+
+-- To Integer
+
+export
+Cast Int8 Integer where
+  cast = prim__cast_Int8Integer
+
+export
+Cast Int16 Integer where
+  cast = prim__cast_Int16Integer
+
+export
+Cast Int32 Integer where
+  cast = prim__cast_Int32Integer
+
+export
+Cast Int64 Integer where
+  cast = prim__cast_Int64Integer
+
+-- To Int
+
+export
+Cast Int8 Int where
+  cast = prim__cast_Int8Int
+
+export
+Cast Int16 Int where
+  cast = prim__cast_Int16Int
+
+export
+Cast Int32 Int where
+  cast = prim__cast_Int32Int
+
+export
+Cast Int64 Int where
+  cast = prim__cast_Int64Int
+
+-- To Int8
+
+export
+Cast Int Int8 where
+  cast = prim__cast_IntInt8
+
+export
+Cast Int16 Int8 where
+  cast = prim__cast_Int16Int8
+
+export
+Cast Int32 Int8 where
+  cast = prim__cast_Int32Int8
+
+export
+Cast Int64 Int8 where
+  cast = prim__cast_Int64Int8
+
+export
+Cast Integer Int8 where
+  cast = prim__cast_IntegerInt8
+
+export
+Cast Char Int8 where
+  cast = prim__cast_CharInt8
+
+export
+Cast Double Int8 where
+  cast = prim__cast_DoubleInt8
+
+export
+Cast String Int8 where
+  cast = prim__cast_StringInt8
+
+export
+Cast Nat Int8 where
+  cast = fromInteger . natToInteger
+
+export
+Cast Bits8 Int8 where
+  cast = prim__cast_Bits8Int8
+
+export
+Cast Bits16 Int8 where
+  cast = prim__cast_Bits16Int8
+
+export
+Cast Bits32 Int8 where
+  cast = prim__cast_Bits32Int8
+
+export
+Cast Bits64 Int8 where
+  cast = prim__cast_Bits64Int8
+
+-- To Int16
+
+export
+Cast Int Int16 where
+  cast = prim__cast_IntInt16
+
+export
+Cast Int8 Int16 where
+  cast = prim__cast_Int8Int16
+
+export
+Cast Int32 Int16 where
+  cast = prim__cast_Int32Int16
+
+export
+Cast Int64 Int16 where
+  cast = prim__cast_Int64Int16
+
+export
+Cast Integer Int16 where
+  cast = prim__cast_IntegerInt16
+
+export
+Cast Char Int16 where
+  cast = prim__cast_CharInt16
+
+export
+Cast Double Int16 where
+  cast = prim__cast_DoubleInt16
+
+export
+Cast String Int16 where
+  cast = prim__cast_StringInt16
+
+export
+Cast Nat Int16 where
+  cast = fromInteger . natToInteger
+
+export
+Cast Bits8 Int16 where
+  cast = prim__cast_Bits8Int16
+
+export
+Cast Bits16 Int16 where
+  cast = prim__cast_Bits16Int16
+
+export
+Cast Bits32 Int16 where
+  cast = prim__cast_Bits32Int16
+
+export
+Cast Bits64 Int16 where
+  cast = prim__cast_Bits64Int16
+
+-- To Int32
+
+export
+Cast Int Int32 where
+  cast = prim__cast_IntInt32
+
+export
+Cast Int8 Int32 where
+  cast = prim__cast_Int8Int32
+
+export
+Cast Int16 Int32 where
+  cast = prim__cast_Int16Int32
+
+export
+Cast Int64 Int32 where
+  cast = prim__cast_Int64Int32
+
+export
+Cast Integer Int32 where
+  cast = prim__cast_IntegerInt32
+
+export
+Cast Char Int32 where
+  cast = prim__cast_CharInt32
+
+export
+Cast Double Int32 where
+  cast = prim__cast_DoubleInt32
+
+export
+Cast String Int32 where
+  cast = prim__cast_StringInt32
+
+export
+Cast Nat Int32 where
+  cast = fromInteger . natToInteger
+
+export
+Cast Bits8 Int32 where
+  cast = prim__cast_Bits8Int32
+
+export
+Cast Bits16 Int32 where
+  cast = prim__cast_Bits16Int32
+
+export
+Cast Bits32 Int32 where
+  cast = prim__cast_Bits32Int32
+
+export
+Cast Bits64 Int32 where
+  cast = prim__cast_Bits64Int32
+
+-- To Int64
+
+export
+Cast Int Int64 where
+  cast = prim__cast_IntInt64
+
+export
+Cast Int8 Int64 where
+  cast = prim__cast_Int8Int64
+
+export
+Cast Int16 Int64 where
+  cast = prim__cast_Int16Int64
+
+export
+Cast Int32 Int64 where
+  cast = prim__cast_Int32Int64
+
+export
+Cast Integer Int64 where
+  cast = prim__cast_IntegerInt64
+
+export
+Cast Char Int64 where
+  cast = prim__cast_CharInt64
+
+export
+Cast Double Int64 where
+  cast = prim__cast_DoubleInt64
+
+export
+Cast String Int64 where
+  cast = prim__cast_StringInt64
+
+export
+Cast Nat Int64 where
+  cast = fromInteger . natToInteger
+
+export
+Cast Bits8 Int64 where
+  cast = prim__cast_Bits8Int64
+
+export
+Cast Bits16 Int64 where
+  cast = prim__cast_Bits16Int64
+
+export
+Cast Bits32 Int64 where
+  cast = prim__cast_Bits32Int64
+
+export
+Cast Bits64 Int64 where
+  cast = prim__cast_Bits64Int64
+
+-- To Char
+
+export
+Cast Int8 Char where
+  cast = prim__cast_Int8Char
+
+export
+Cast Int16 Char where
+  cast = prim__cast_Int16Char
+
+export
+Cast Int32 Char where
+  cast = prim__cast_Int32Char
+
+export
+Cast Int64 Char where
+  cast = prim__cast_Int64Char
+
+-- To Double
+
+export
+Cast Int8 Double where
+  cast = prim__cast_Int8Double
+
+export
+Cast Int16 Double where
+  cast = prim__cast_Int16Double
+
+export
+Cast Int32 Double where
+  cast = prim__cast_Int32Double
+
+export
+Cast Int64 Double where
+  cast = prim__cast_Int64Double
+
+-- To Bits8
+
+export
+Cast Int8 Bits8 where
+  cast = prim__cast_Int8Bits8
+
+export
+Cast Int16 Bits8 where
+  cast = prim__cast_Int16Bits8
+
+export
+Cast Int32 Bits8 where
+  cast = prim__cast_Int32Bits8
+
+export
+Cast Int64 Bits8 where
+  cast = prim__cast_Int64Bits8
+
+-- To Bits16
+
+export
+Cast Int8 Bits16 where
+  cast = prim__cast_Int8Bits16
+
+export
+Cast Int16 Bits16 where
+  cast = prim__cast_Int16Bits16
+
+export
+Cast Int32 Bits16 where
+  cast = prim__cast_Int32Bits16
+
+export
+Cast Int64 Bits16 where
+  cast = prim__cast_Int64Bits16
+
+-- To Bits32
+
+export
+Cast Int8 Bits32 where
+  cast = prim__cast_Int8Bits32
+
+export
+Cast Int16 Bits32 where
+  cast = prim__cast_Int16Bits32
+
+export
+Cast Int32 Bits32 where
+  cast = prim__cast_Int32Bits32
+
+export
+Cast Int64 Bits32 where
+  cast = prim__cast_Int64Bits32
+
+-- To Bits64
+
+export
+Cast Int8 Bits64 where
+  cast = prim__cast_Int8Bits64
+
+export
+Cast Int16 Bits64 where
+  cast = prim__cast_Int16Bits64
+
+export
+Cast Int32 Bits64 where
+  cast = prim__cast_Int32Bits64
+
+export
+Cast Int64 Bits64 where
+  cast = prim__cast_Int64Bits64

tests/refc/integers/IntEqOrd.idr

@@ -0,0 +1,53 @@
+module IntEqOrd
+
+public export
+Eq Int8 where
+  x == y = intToBool (prim__eq_Int8 x y)
+
+public export
+Eq Int16 where
+  x == y = intToBool (prim__eq_Int16 x y)
+
+public export
+Eq Int32 where
+  x == y = intToBool (prim__eq_Int32 x y)
+
+public export
+Eq Int64 where
+  x == y = intToBool (prim__eq_Int64 x y)
+
+public export
+Ord Int8 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Int8 x y)
+  (<=) x y = intToBool (prim__lte_Int8 x y)
+  (>) x y = intToBool (prim__gt_Int8 x y)
+  (>=) x y = intToBool (prim__gte_Int8 x y)
+
+public export
+Ord Int16 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Int16 x y)
+  (<=) x y = intToBool (prim__lte_Int16 x y)
+  (>) x y = intToBool (prim__gt_Int16 x y)
+  (>=) x y = intToBool (prim__gte_Int16 x y)
+
+public export
+Ord Int32 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Int32 x y)
+  (<=) x y = intToBool (prim__lte_Int32 x y)
+  (>) x y = intToBool (prim__gt_Int32 x y)
+  (>=) x y = intToBool (prim__gte_Int32 x y)
+
+public export
+Ord Int64 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Int64 x y)
+  (<=) x y = intToBool (prim__lte_Int64 x y)
+  (>) x y = intToBool (prim__gt_Int64 x y)
+  (>=) x y = intToBool (prim__gte_Int64 x y)

tests/refc/integers/IntNum.idr

@@ -0,0 +1,193 @@
+module IntNum
+
+import IntEqOrd
+
+-- This file to be deleted once these interfaces are added to prelude
+
+-- Int8
+
+%inline
+public export
+Num Int8 where
+  (+) = prim__add_Int8
+  (*) = prim__mul_Int8
+  fromInteger = prim__cast_IntegerInt8
+
+public export
+Neg Int8 where
+  negate x = prim__sub_Int8 0 x
+  (-) = prim__sub_Int8
+
+public export
+Abs Int8 where
+  abs x = if x < 0 then -x else x
+
+public export
+Integral Int8 where
+  div x y
+      = case y == 0 of
+             False => prim__div_Int8 x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Int8 x y
+
+-- Int16
+
+%inline
+public export
+Num Int16 where
+  (+) = prim__add_Int16
+  (*) = prim__mul_Int16
+  fromInteger = prim__cast_IntegerInt16
+
+public export
+Neg Int16 where
+  negate x = prim__sub_Int16 0 x
+  (-) = prim__sub_Int16
+
+public export
+Abs Int16 where
+  abs x = if x < 0 then -x else x
+
+public export
+Integral Int16 where
+  div x y
+      = case y == 0 of
+             False => prim__div_Int16 x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Int16 x y
+
+-- Int32
+
+%inline
+public export
+Num Int32 where
+  (+) = prim__add_Int32
+  (*) = prim__mul_Int32
+  fromInteger = prim__cast_IntegerInt32
+
+public export
+Neg Int32 where
+  negate x = prim__sub_Int32 0 x
+  (-) = prim__sub_Int32
+
+public export
+Abs Int32 where
+  abs x = if x < 0 then -x else x
+
+public export
+Integral Int32 where
+  div x y
+      = case y == 0 of
+             False => prim__div_Int32 x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Int32 x y
+
+-- Int64
+
+%inline
+public export
+Num Int64 where
+  (+) = prim__add_Int64
+  (*) = prim__mul_Int64
+  fromInteger = prim__cast_IntegerInt64
+
+public export
+Neg Int64 where
+  negate x = prim__sub_Int64 0 x
+  (-) = prim__sub_Int64
+
+public export
+Abs Int64 where
+  abs x = if x < 0 then -x else x
+
+public export
+Integral Int64 where
+  div x y
+      = case y == 0 of
+             False => prim__div_Int64 x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Int64 x y
+
+-- Bits8
+
+public export
+Neg Bits8 where
+  negate x = prim__sub_Bits8 0 x
+  (-) = prim__sub_Bits8
+
+public export
+Abs Bits8 where
+  abs = id
+
+public export
+Integral Bits8 where
+  div x y
+      = case y == 0 of
+             False => prim__div_Bits8 x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Bits8 x y
+
+-- Bits16
+
+public export
+Neg Bits16 where
+  negate x = prim__sub_Bits16 0 x
+  (-) = prim__sub_Bits16
+
+public export
+Abs Bits16 where
+  abs = id
+
+public export
+Integral Bits16 where
+  div x y
+      = case y == 0 of
+             False => prim__div_Bits16 x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Bits16 x y
+
+-- Bits32
+
+public export
+Neg Bits32 where
+  negate x = prim__sub_Bits32 0 x
+  (-) = prim__sub_Bits32
+
+public export
+Abs Bits32 where
+  abs = id
+
+public export
+Integral Bits32 where
+  div x y
+      = case y == 0 of
+             False => prim__div_Bits32 x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Bits32 x y
+
+-- Bits64
+
+public export
+Neg Bits64 where
+  negate x = prim__sub_Bits64 0 x
+  (-) = prim__sub_Bits64
+
+public export
+Abs Bits64 where
+  abs = id
+
+public export
+Integral Bits64 where
+  div x y
+      = case y == 0 of
+             False => prim__div_Bits64 x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Bits64 x y

tests/refc/integers/IntShow.idr

@@ -0,0 +1,26 @@
+module IntShow
+
+-- This file to be deleted once these interfaces are added to prelude
+
+firstCharIs : (Char -> Bool) -> String -> Bool
+firstCharIs p "" = False
+firstCharIs p str = p (assert_total (prim__strHead str))
+
+primNumShow : (a -> String) -> Prec -> a -> String
+primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str
+
+export
+Show Int8 where
+  showPrec = primNumShow prim__cast_Int8String
+
+export
+Show Int16 where
+  showPrec = primNumShow prim__cast_Int16String
+
+export
+Show Int32 where
+  showPrec = primNumShow prim__cast_Int32String
+
+export
+Show Int64 where
+  showPrec = primNumShow prim__cast_Int64String

tests/refc/integers/TestIntegers.idr

@@ -0,0 +1,155 @@
+module TestIntegers
+
+import IntBits
+import IntCasts
+import IntEqOrd
+import IntNum
+import IntShow
+
+import Data.Bits
+import Data.List.Quantifiers
+
+put : Show a => a -> IO ()
+put = putStrLn . show
+
+castAllTo : (to : Type)
+         -> {0 types : List Type}
+         -> All (flip Cast to) types => HList types -> List to
+castAllTo to = forget . imapProperty (flip Cast to) (cast {to})
+
+interface Num a => Bits a => SomeBits a where
+    one : Index {a}
+
+SomeBits Bits8 where
+    one = fromNat 1
+
+SomeBits Bits16 where
+    one = fromNat 1
+
+SomeBits Bits32 where
+    one = fromNat 1
+
+SomeBits Bits64 where
+    one = fromNat 1
+
+SomeBits Int8 where
+    one = fromNat 1
+
+SomeBits Int16 where
+    one = fromNat 1
+
+SomeBits Int32 where
+    one = fromNat 1
+
+SomeBits Int64 where
+    one = fromNat 1
+
+SomeBits Int where
+    one = fromNat 1
+
+SomeBits Integer where
+    one = 1
+
+interface Num a => Ord a => NumOrd a where
+
+Num a => Ord a => NumOrd a where
+
+main : IO ()
+main = do
+    let ints = the (HList _) [
+        the Bits8 0, -- Bits8 min
+        the Bits8 50,
+        the Bits8 255, -- Bits8 max
+        the Bits16 0, -- Bits16 min
+        the Bits16 10000,
+        the Bits16 65535, -- Bits16 max
+        the Bits32 0, -- Bits32 min
+        the Bits32 1000000000,
+        the Bits32 4294967295, -- Bits32 max
+        the Bits64 0, -- Bits64 min
+        the Bits64 5000000000000000000,
+        the Bits64 18446744073709551615, -- Bits64 max
+        the Int8 $ -128, -- Int8 min
+        the Int8 50,
+        the Int8 127, -- Int8 max
+        the Int16 $ -32768, -- Int16 min
+        the Int16 10000,
+        the Int16 32767, -- Int16 max
+        the Int32 $ -2147483648, -- Int32 min
+        the Int32 500000000,
+        the Int32 2147483647, -- Int32 max
+        the Int64 $ -9223372036854775808, -- Int64 min
+        the Int64 1000000000000000000,
+        the Int64 9223372036854775807, -- Int64 max
+        the Int $ -9223372036854775808, -- Int min
+        the Int 1000000000000000000,
+        the Int 9223372036854775807, -- Int max
+        the Integer $ -9223372036854775809, -- Int min - 1
+        the Integer 0,
+        the Integer 9223372036854775808 -- Int max + 1
+    ]
+
+    putStrLn "Cast to String:"
+    put ints
+
+    putStrLn "Cast to Bits8:"
+    put $ castAllTo Bits8 ints
+
+    putStrLn "Cast to Bits16:"
+    put $ castAllTo Bits16 ints
+
+    putStrLn "Cast to Bits32:"
+    put $ castAllTo Bits32 ints
+
+    putStrLn "Cast to Bits64:"
+    put $ castAllTo Bits64 ints
+
+    putStrLn "Cast to Int:"
+    put $ castAllTo Int ints
+
+    putStrLn "Cast to Integer:"
+    put $ castAllTo Integer ints
+
+    putStrLn "Add:"
+    put $ imapProperty Num (+ 1) ints
+
+    putStrLn "Subtract:"
+    put $ imapProperty Neg (flip (-) 1) ints
+
+    putStrLn "Negate:"
+    put $ imapProperty Neg negate ints
+
+    putStrLn "Multiply:"
+    put $ imapProperty Num (* 2) ints
+
+    putStrLn "Divide:"
+    put $ imapProperty Integral (`div` 3) ints
+    put $ imapProperty Integral (`div` -3) ints
+
+    putStrLn "Mod:"
+    put $ imapProperty Integral (`mod` 17) ints
+    put $ imapProperty Integral (`mod` -17) ints
+
+    putStrLn "Division Euclidean:"
+    put $ imapProperty Integral (\x => (x `div` 19) * 19 + (x `mod` 19)) ints
+    put $ imapProperty Integral (\x => (x `div` -19) * -19 + (x `mod` -19)) ints
+
+    putStrLn "Shift:"
+    put $ imapProperty SomeBits (`shiftL` one) ints
+    put $ imapProperty SomeBits (`shiftR` one) ints
+
+    putStrLn "Bit Ops:"
+    put $ imapProperty SomeBits (.&. 0xAA) ints
+    put $ imapProperty SomeBits (.|. 0xAA) ints
+    put $ imapProperty SomeBits (`xor` 0xAA) ints
+
+    putStrLn "Comparisons:"
+    put $ imapProperty NumOrd (< 0) ints
+    put $ imapProperty NumOrd (< 1) ints
+    put $ imapProperty NumOrd (> 0) ints
+    put $ imapProperty NumOrd (> 1) ints
+    put $ imapProperty NumOrd (== 0) ints
+    put $ imapProperty NumOrd (<= 0) ints
+    put $ imapProperty NumOrd (<= 1) ints
+    put $ imapProperty NumOrd (>= 0) ints
+    put $ imapProperty NumOrd (>= 1) ints

tests/refc/integers/expected

@@ -0,0 +1,48 @@
+Cast to String:
+[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775809, 0, 9223372036854775808]
+Cast to Bits8:
+[0, 50, 255, 0, 16, 255, 0, 0, 255, 0, 0, 255, 128, 50, 127, 0, 16, 255, 0, 0, 255, 0, 0, 255, 0, 0, 255, 255, 0, 0]
+Cast to Bits16:
+[0, 50, 255, 0, 10000, 65535, 0, 51712, 65535, 0, 0, 65535, 65408, 50, 127, 32768, 10000, 32767, 0, 25856, 65535, 0, 0, 65535, 0, 0, 65535, 65535, 0, 0]
+Cast to Bits32:
+[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 1156841472, 4294967295, 4294967168, 50, 127, 4294934528, 10000, 32767, 2147483648, 500000000, 2147483647, 0, 2808348672, 4294967295, 0, 2808348672, 4294967295, 4294967295, 0, 0]
+Cast to Bits64:
+[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, 18446744073709551488, 50, 127, 18446744073709518848, 10000, 32767, 18446744071562067968, 500000000, 2147483647, 9223372036854775808, 1000000000000000000, 9223372036854775807, 9223372036854775808, 1000000000000000000, 9223372036854775807, 9223372036854775807, 0, 9223372036854775808]
+Cast to Int:
+[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, -1, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775808, 1000000000000000000, 9223372036854775807, 9223372036854775807, 0, -9223372036854775808]
+Cast to Integer:
+[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775809, 0, 9223372036854775808]
+Add:
+[1, 51, 0, 1, 10001, 0, 1, 1000000001, 0, 1, 5000000000000000001, 0, -127, 51, -128, -32767, 10001, -32768, -2147483647, 500000001, -2147483648, -9223372036854775807, 1000000000000000001, -9223372036854775808, -9223372036854775807, 1000000000000000001, -9223372036854775808, -9223372036854775808, 1, 9223372036854775809]
+Subtract:
+[255, 49, 254, 65535, 9999, 65534, 4294967295, 999999999, 4294967294, 18446744073709551615, 4999999999999999999, 18446744073709551614, 127, 49, 126, 32767, 9999, 32766, 2147483647, 499999999, 2147483646, 9223372036854775807, 999999999999999999, 9223372036854775806, 9223372036854775807, 999999999999999999, 9223372036854775806, -9223372036854775810, -1, 9223372036854775807]
+Negate:
+[0, 206, 1, 0, 55536, 1, 0, 3294967296, 1, 0, 13446744073709551616, 1, -128, -50, -127, -32768, -10000, -32767, -2147483648, -500000000, -2147483647, -9223372036854775808, -1000000000000000000, -9223372036854775807, -9223372036854775808, -1000000000000000000, -9223372036854775807, 9223372036854775809, 0, -9223372036854775808]
+Multiply:
+[0, 100, 254, 0, 20000, 65534, 0, 2000000000, 4294967294, 0, 10000000000000000000, 18446744073709551614, 0, 100, -2, 0, 20000, -2, 0, 1000000000, -2, 0, 2000000000000000000, -2, 0, 2000000000000000000, -2, -18446744073709551618, 0, 18446744073709551616]
+Divide:
+[0, 16, 85, 0, 3333, 21845, 0, 333333333, 1431655765, 0, 1666666666666666666, 6148914691236517205, -43, 16, 42, -10923, 3333, 10922, -715827883, 166666666, 715827882, -3074457345618258603, 333333333333333333, 3074457345618258602, -3074457345618258603, 333333333333333333, 3074457345618258602, -3074457345618258603, 0, 3074457345618258602]
+[0, 0, 1, 0, 0, 1, 0, 0, 1, 0, 0, 1, 43, -16, -42, 10923, -3333, -10922, 715827883, -166666666, -715827882, 3074457345618258603, -333333333333333333, -3074457345618258602, 3074457345618258603, -333333333333333333, -3074457345618258602, 3074457345618258603, 0, -3074457345618258602]
+Mod:
+[0, 16, 0, 0, 4, 0, 0, 7, 0, 0, 7, 0, 8, 16, 8, 8, 4, 8, 8, 12, 8, 8, 15, 8, 8, 15, 8, 7, 0, 9]
+[0, 50, 16, 0, 10000, 16, 0, 1000000000, 16, 0, 5000000000000000000, 16, 8, 16, 8, 8, 4, 8, 8, 12, 8, 8, 15, 8, 8, 15, 8, 7, 0, 9]
+Division Euclidean:
+[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775809, 0, 9223372036854775808]
+[0, 50, 255, 0, 10000, 65535, 0, 1000000000, 4294967295, 0, 5000000000000000000, 18446744073709551615, -128, 50, 127, -32768, 10000, 32767, -2147483648, 500000000, 2147483647, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775808, 1000000000000000000, 9223372036854775807, -9223372036854775809, 0, 9223372036854775808]
+Shift:
+[0, 100, 254, 0, 20000, 65534, 0, 2000000000, 4294967294, 0, 10000000000000000000, 18446744073709551614, 0, 100, -2, 0, 20000, -2, 0, 1000000000, -2, 0, 2000000000000000000, -2, 0, 2000000000000000000, -2, -18446744073709551618, 0, 18446744073709551616]
+[0, 25, 127, 0, 5000, 32767, 0, 500000000, 2147483647, 0, 2500000000000000000, 9223372036854775807, -64, 25, 63, -16384, 5000, 16383, -1073741824, 250000000, 1073741823, -4611686018427387904, 500000000000000000, 4611686018427387903, -4611686018427387904, 500000000000000000, 4611686018427387903, -4611686018427387905, 0, 4611686018427387904]
+Bit Ops:
+[0, 34, 170, 0, 0, 170, 0, 0, 170, 0, 0, 170, -128, 34, 42, 0, 0, 170, 0, 0, 170, 0, 0, 170, 0, 0, 170, 170, 0, 0]
+[170, 186, 255, 170, 10170, 65535, 170, 1000000170, 4294967295, 170, 5000000000000000170, 18446744073709551615, -86, -70, -1, -32598, 10170, 32767, -2147483478, 500000170, 2147483647, -9223372036854775638, 1000000000000000170, 9223372036854775807, -9223372036854775638, 1000000000000000170, 9223372036854775807, -9223372036854775809, 170, 9223372036854775978]
+[170, 152, 85, 170, 10170, 65365, 170, 1000000170, 4294967125, 170, 5000000000000000170, 18446744073709551445, 42, -104, -43, -32598, 10170, 32597, -2147483478, 500000170, 2147483477, -9223372036854775638, 1000000000000000170, 9223372036854775637, -9223372036854775638, 1000000000000000170, 9223372036854775637, -9223372036854775979, 170, 9223372036854775978]
+Comparisons:
+[False, False, False, False, False, False, False, False, False, False, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False]
+[True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, True, False]
+[False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, False, True]
+[False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, False, True]
+[True, False, False, True, False, False, True, False, False, True, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, True, False]
+[True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, True, False]
+[True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, False, False, True, True, False]
+[True, True, True, True, True, True, True, True, True, True, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True]
+[False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, True, True, False, False, True]

tests/refc/integers/run

@@ -0,0 +1,4 @@
+$1 --no-banner --no-color --console-width 0 --cg refc -o refc_integers TestIntegers.idr > /dev/null
+./build/exec/refc_integers
+
+rm -rf build