on master help sign in
Support the RTS function idris_time in executor
b0e53f8David Raymond Christiansen
src/Idris/Core/Execute.hs+5
@@ -27,6 +27,7 @@ import Control.Monad hiding (forM)
27import Data.Maybe
27import Data.Maybe
28import Data.Bits
28import Data.Bits
29import Data.Traversable (forM)
29import Data.Traversable (forM)
30+import Data.Time.Clock.POSIX (getPOSIXTime)
30import qualified Data.Map as M
31import qualified Data.Map as M
31
32
32#ifdef IDRIS_FFI
33#ifdef IDRIS_FFI
@@ -252,6 +253,10 @@ execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
252 "The argument to idris_readStr should be a handle, but it was " ++
253 "The argument to idris_readStr should be a handle, but it was " ++
253 show handle ++
254 show handle ++
254 ". Are all cases covered?"
255 ". Are all cases covered?"
256+execApp env ctxt (EP _ fp _) (_:fn:rest)
257+ | fp == mkfprim,
258+ Just (FFun "idris_time" _ _) <- foreignFromTT fn
259+ = do execIO $ fmap (ioWrap . EConstant . I . round) getPOSIXTime
255execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
260execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
256 | fp == mkfprim,
261 | fp == mkfprim,
257 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
262 Just (FFun "fileOpen" _ _) <- foreignFromTT fn