794852a · Idris-dev · git.iko.soy

libs/prelude/IO.idr+1

compare with master

unifiedsplit

@@ -177,6 +177,7 @@ mutual

177 data JS_Types : Type -> Type where

178 JS_Str : JS_Types String

179 JS_Float : JS_Types Float

180+ JS_Ptr : JS_Types Ptr

180 JS_Unit : JS_Types ()

181 JS_Unit : JS_Types ()

181 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)

182 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)

182 JS_IntT : JS_IntTypes i -> JS_Types i

183 JS_IntT : JS_IntTypes i -> JS_Types i

libs/prelude/Prelude.idr+18−4

@@ -434,22 +434,22 @@ uniformB64x2 x = prim__mkB64x2 x x

434---- some basic io

435

436||| Output a string to stdout without a trailing newline

437−putStr : String -> IO' l ()

437+putStr : String -> IO' ffi ()

438putStr x = do prim_write x

439 return ()

440

441||| Output a string to stdout with a trailing newline

442−putStrLn : String -> IO' l ()

442+putStrLn : String -> IO' ffi ()

443putStrLn x = putStr (x ++ "\n")

444

445||| Output something showable to stdout, with a trailing newline

446partial

447−print : Show a => a -> IO ()

447+print : Show a => a -> IO' ffi ()

448print x = putStrLn (show x)

449

450||| Read one line of input from stdin

451partial

452−getLine : IO' l String

452+getLine : IO' ffi String

453getLine = prim_read

454

455||| Write a single character to stdout

@@ -592,6 +592,20 @@ nullStr : String -> IO Bool

592nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p

593 return (ok /= 0)

594

595+namespace JSNull

596+ ||| Check if a foreign pointer is null

597+ partial

598+ nullPtr : Ptr -> JS_IO Bool

599+ nullPtr p = do ok <- foreign FFI_JS "isNull" (Ptr -> JS_IO Int) p

600+ return (ok /= 0)

601+

602+ ||| Check if a supposed string was actually a null pointer

603+ partial

604+ nullStr : String -> JS_IO Bool

605+ nullStr p = do ok <- foreign FFI_JS "isNull" (String -> JS_IO Int) p

606+ return (ok /= 0)

607+

608+

595||| Pointer equality

609||| Pointer equality

596eqPtr : Ptr -> Ptr -> IO Bool

610eqPtr : Ptr -> Ptr -> IO Bool

597eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y

611eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y

src/IRTS/CodegenJavaScript.hs+18−1

@@ -8,6 +8,7 @@ import Idris.AbsSyntax hiding (TypeCase)

8import IRTS.Bytecode

9import IRTS.Lang

10import IRTS.Simplified

11+import IRTS.Defunctionalise

11import IRTS.CodegenCommon

12import IRTS.CodegenCommon

12import Idris.Core.TT

13import Idris.Core.TT

13import IRTS.System

14import IRTS.System

@@ -1328,7 +1329,8 @@ translateBC info bc

1328 | NULL r <- bc = jsNULL info r

1329 | NULL r <- bc = jsNULL info r

1329 | CALL n <- bc = jsCALL info n

1330 | CALL n <- bc = jsCALL info n

1330 | TAILCALL n <- bc = jsTAILCALL info n

1331 | TAILCALL n <- bc = jsTAILCALL info n

1332+ | FOREIGNCALL r _ (DConst (Str n)) args

1331− | FOREIGNCALL r _ n a <- bc = error "jsFOREIGN info r n a"

1333+ <- bc = jsFOREIGN info r n (map fcall args)

1332 | TOPBASE n <- bc = jsTOPBASE info n

1334 | TOPBASE n <- bc = jsTOPBASE info n

1333 | BASETOP n <- bc = jsBASETOP info n

1335 | BASETOP n <- bc = jsBASETOP info n

1334 | STOREOLD <- bc = jsSTOREOLD info

1336 | STOREOLD <- bc = jsSTOREOLD info

@@ -1342,4 +1344,19 @@ translateBC info bc

1342 | OP r o a <- bc = jsOP info r o a

1344 | OP r o a <- bc = jsOP info r o a

1343 | ERROR e <- bc = jsERROR info e

1345 | ERROR e <- bc = jsERROR info e

1344 | otherwise = JSRaw $ "//" ++ show bc

1346 | otherwise = JSRaw $ "//" ++ show bc

1347+ where fcall (t, arg) = (toFType t, arg)

1348+

1349+toAType (FCon i)

1350+ | i == sUN "JS_IntChar" = ATInt ITChar

1351+ | i == sUN "JS_IntNative" = ATInt ITNative

1352+toAType t = error (show t ++ " not defined in toAType")

1353+

1354+toFType (FCon c)

1355+ | c == sUN "JS_Str" = FString

1356+ | c == sUN "JS_Float" = FArith ATFloat

1357+ | c == sUN "JS_Ptr" = FPtr

1358+ | c == sUN "JS_Unit" = FUnit

1359+toFType (FApp c [_,ity])

1360+ | c == sUN "JS_IntT" = FArith (toAType ity)

1361+toFType t = error (show t ++ " not yet defined in toFType")

1345

1362

test/basic007/test033.idr+1−1

@@ -1,4 +1,4 @@

1module Main

2

3−main : IO ()

3+main : JS_IO ()

4main = nullPtr null >>= print