git.iko.soy/Idris-dev
on master help sign in
Initial support for JS in new ffi
commit794852acf1912df91043d1193bc999311e866151 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 20 Jan 2015, 10:57 (12 years ago) parent39e4eb0
4 files changed+38−6
compare with master
unifiedsplit
libs/prelude/IO.idr+1 libs/prelude/Prelude.idr+18−4 src/IRTS/CodegenJavaScript.hs+18−1 test/basic007/test033.idr+1−1
libs/prelude/IO.idr+1
@@ -177,6 +177,7 @@ mutual
177177 data JS_Types : Type -> Type where
178178 JS_Str : JS_Types String
179179 JS_Float : JS_Types Float
180+ JS_Ptr : JS_Types Ptr
180181 JS_Unit : JS_Types ()
181182 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
182183 JS_IntT : JS_IntTypes i -> JS_Types i
libs/prelude/Prelude.idr+18−4
@@ -434,22 +434,22 @@ uniformB64x2 x = prim__mkB64x2 x x
434434---- some basic io
435435
436436||| Output a string to stdout without a trailing newline
437−putStr : String -> IO' l ()
437+putStr : String -> IO' ffi ()
438438putStr x = do prim_write x
439439 return ()
440440
441441||| Output a string to stdout with a trailing newline
442−putStrLn : String -> IO' l ()
442+putStrLn : String -> IO' ffi ()
443443putStrLn x = putStr (x ++ "\n")
444444
445445||| Output something showable to stdout, with a trailing newline
446446partial
447−print : Show a => a -> IO ()
447+print : Show a => a -> IO' ffi ()
448448print x = putStrLn (show x)
449449
450450||| Read one line of input from stdin
451451partial
452−getLine : IO' l String
452+getLine : IO' ffi String
453453getLine = prim_read
454454
455455||| Write a single character to stdout
@@ -592,6 +592,20 @@ nullStr : String -> IO Bool
592592nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p
593593 return (ok /= 0)
594594
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+
595609||| Pointer equality
596610eqPtr : Ptr -> Ptr -> IO Bool
597611eqPtr 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)
88import IRTS.Bytecode
99import IRTS.Lang
1010import IRTS.Simplified
11+import IRTS.Defunctionalise
1112import IRTS.CodegenCommon
1213import Idris.Core.TT
1314import IRTS.System
@@ -1328,7 +1329,8 @@ translateBC info bc
13281329 | NULL r <- bc = jsNULL info r
13291330 | CALL n <- bc = jsCALL info n
13301331 | TAILCALL n <- bc = jsTAILCALL info n
1331− | FOREIGNCALL r _ n a <- bc = error "jsFOREIGN info r n a"
1332+ | FOREIGNCALL r _ (DConst (Str n)) args
1333+ <- bc = jsFOREIGN info r n (map fcall args)
13321334 | TOPBASE n <- bc = jsTOPBASE info n
13331335 | BASETOP n <- bc = jsBASETOP info n
13341336 | STOREOLD <- bc = jsSTOREOLD info
@@ -1342,4 +1344,19 @@ translateBC info bc
13421344 | OP r o a <- bc = jsOP info r o a
13431345 | ERROR e <- bc = jsERROR info e
13441346 | 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")
13451362
test/basic007/test033.idr+1−1
@@ -1,4 +1,4 @@
11module Main
22
3−main : IO ()
3+main : JS_IO ()
44main = nullPtr null >>= print