Write Ints as 64 bit

Since they might be... This is especially likely for module hashes, and
if we don't get it right, the Racket runtime might fail to write the
buffer. This makes the code buildable with the Racket back end.

INSTALL.md

@@ -13,6 +13,13 @@ do this with `brew install coreutils`.
 
 If you have an existing Idris 2, go to step 1b. Otherwise, read on...
 
+Make sure that:
+
+* `$PREFIX/bin` is in your `PATH`
+* `$PREFIX/lib` is in your `LD_LIBRARY_PATH` (so that the system knows where
+  to look for library support code)
+
+
 1a: Installing without an existing Idris 2
 ------------------------------------------
 

idris2.ipkg

@@ -143,6 +143,7 @@ modules =
     Yaffle.Main,
     Yaffle.REPL
 
+-- opts = "--codegen racket"
 depends = contrib, network
 
 sourcedir = "src"

src/Core/Binary.idr

@@ -28,7 +28,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 26
+ttcVersion = 27
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Utils/Binary.idr

@@ -159,20 +159,20 @@ export
 TTC Int where
   toBuf b val
     = do chunk <- get Bin
-         if avail chunk >= 4
+         if avail chunk >= 8
             then
               do coreLift $ setInt (buf chunk) (loc chunk) val
-                 put Bin (appended 4 chunk)
-            else do chunk' <- extendBinary 4 chunk
+                 put Bin (appended 8 chunk)
+            else do chunk' <- extendBinary 8 chunk
                     coreLift $ setInt (buf chunk') (loc chunk') val
-                    put Bin (appended 4 chunk')
+                    put Bin (appended 8 chunk')
 
   fromBuf b
     = do chunk <- get Bin
-         if toRead chunk >= 4
+         if toRead chunk >= 8
             then
               do val <- coreLift $ getInt (buf chunk) (loc chunk)
-                 put Bin (incLoc 4 chunk)
+                 put Bin (incLoc 8 chunk)
                  pure val
               else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk))))
 

support/chez/support.ss

@@ -97,9 +97,15 @@
   (bytevector-u8-ref buf loc))
 
 (define (blodwen-buffer-setint buf loc val)
-  (bytevector-s32-set! buf loc val (native-endianness)))
+  (bytevector-s64-set! buf loc val (native-endianness)))
 
 (define (blodwen-buffer-getint buf loc)
+  (bytevector-s64-ref buf loc (native-endianness)))
+
+(define (blodwen-buffer-setint32 buf loc val)
+  (bytevector-s32-set! buf loc val (native-endianness)))
+
+(define (blodwen-buffer-getint32 buf loc)
   (bytevector-s32-ref buf loc (native-endianness)))
 
 (define (blodwen-buffer-setdouble buf loc val)

support/racket/support.rkt

@@ -85,9 +85,15 @@
   (bytevector-u8-ref buf loc))
 
 (define (blodwen-buffer-setint buf loc val)
-  (bytevector-s32-set! buf loc val (native-endianness)))
+  (bytevector-s64-set! buf loc val (native-endianness)))
 
 (define (blodwen-buffer-getint buf loc)
+  (bytevector-s64-ref buf loc (native-endianness)))
+
+(define (blodwen-buffer-setint32 buf loc val)
+  (bytevector-s32-set! buf loc val (native-endianness)))
+
+(define (blodwen-buffer-getint32 buf loc)
   (bytevector-s32-ref buf loc (native-endianness)))
 
 (define (blodwen-buffer-setdouble buf loc val)