Fix 'time' to return Integer rather than Int

This way, the time in seconds actually fits...
This commit is contained in:
Edwin Brady 2015-07-01 13:56:57 +01:00
parent 4f8d10f863
commit dc277394ee
4 changed files with 11 additions and 7 deletions

View File

@ -73,8 +73,9 @@ exit : Int -> IO ()
exit code = foreign FFI_C "exit" (Int -> IO ()) code
||| Get the Unix time
time : IO Int
time = foreign FFI_C "idris_time" (IO Int)
time : IO Integer
time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
return t
usleep : Int -> IO ()
usleep i = foreign FFI_C "usleep" (Int -> IO ()) i

View File

@ -9,7 +9,7 @@ import Control.IOExcept
data System : Effect where
Args : sig System (List String)
Time : sig System Int
Time : sig System Integer
GetEnv : String -> sig System (Maybe String)
CSystem : String -> sig System Int
@ -33,7 +33,7 @@ SYSTEM = MkEff () System
getArgs : Eff (List String) [SYSTEM]
getArgs = call Args
time : Eff Int [SYSTEM]
time : Eff Integer [SYSTEM]
time = call Time
getEnv : String -> Eff (Maybe String) [SYSTEM]

View File

@ -1,5 +1,6 @@
#include "idris_stdfgn.h"
#include "idris_rts.h"
#include "idris_gmp.h"
#include "idris_gc.h"
#include <sys/select.h>
#include <fcntl.h>
@ -80,9 +81,9 @@ char* getEnvPair(int i) {
return *(environ + i);
}
int idris_time() {
VAL idris_time() {
time_t t = time(NULL);
return (int)t;
return MKBIGI(t);
}
void idris_forceGC(void* vm) {

View File

@ -1,6 +1,8 @@
#ifndef _IDRISSTDFGN_H
#define _IDRISSTDFGN_H
#include "idris_rts.h"
// A collection of useful standard functions to be used by the prelude.
void putStr(char* str);
@ -22,7 +24,7 @@ void* idris_stdin();
char* getEnvPair(int i);
int idris_time();
VAL idris_time();
void idris_forceGC();