git.iko.soy/Idris-dev
on master help sign in
Add JS FFI description
2170b9aEdwin Brady
libs/prelude/IO.idr+36−7
compare with master
unifiedsplit
@@ -96,6 +96,13 @@ unsafePerformIO : IO' ffi a -> a
96unsafePerformIO (MkIO f) = unsafePerformPrimIO
96unsafePerformIO (MkIO f) = unsafePerformPrimIO
97 (prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_return b))
97 (prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_return b))
98
98
99+prim_fread : Ptr -> IO' l String
100+prim_fread h = MkIO (\w => prim_io_return (prim__readString (world w) h))
101+
102+prim_fwrite : Ptr -> String -> IO' l Int
103+prim_fwrite h s
104+ = MkIO (\w => prim_io_return (prim__writeString (world w) h s))
105+
99--------- The C FFI
106--------- The C FFI
100
107
101data Raw a = MkRaw a -- code generated can assume it's compiled just as 'a'
108data Raw a = MkRaw a -- code generated can assume it's compiled just as 'a'
@@ -141,13 +148,35 @@ fork (MkIO f) = MkIO (\w => prim_io_bind
141 (\ x => prim_io_return x)))
148 (\ x => prim_io_return x)))
142 (\x => prim_io_return x))
149 (\x => prim_io_return x))
143
150
144−prim_fread : Ptr -> IO String
145−prim_fread h = MkIO (\w => prim_io_return (prim__readString (world w) h))
146−
147−prim_fwrite : Ptr -> String -> IO Int
148−prim_fwrite h s
149− = MkIO (\w => prim_io_return (prim__writeString (world w) h s))
150−
151forceGC : IO ()
151forceGC : IO ()
152forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm
152forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm
153
153
154+--------- The Javascript/Node FFI
155+
156+
157+-- Supported JS foreign types
158+mutual
159+ data JsFn t = MkJsFn t
160+
161+ data JS_IntTypes : Type -> Type where
162+ JS_IntChar : JS_IntTypes Char
163+ JS_IntNative : JS_IntTypes Int
164+
165+ data JS_FnTypes : Type -> Type where
166+ JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
167+ JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
168+ JS_FnBase : JS_Types t -> JS_FnTypes t
169+
170+ data JS_Types : Type -> Type where
171+ JS_Str : JS_Types String
172+ JS_Float : JS_Types Float
173+ JS_Unit : JS_Types ()
174+ JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
175+ JS_IntT : JS_IntTypes i -> JS_Types i
176+
177+FFI_JS : FFI
178+FFI_JS = MkFFI JS_Types String
179+
180+JS_IO : Type -> Type
181+JS_IO = IO' FFI_JS
182+
libs/prelude/Prelude.idr+5−5
@@ -434,12 +434,12 @@ uniformB64x2 x = prim__mkB64x2 x x
434---- some basic io
434---- some basic io
435
435
436||| Output a string to stdout without a trailing newline
436||| Output a string to stdout without a trailing newline
437−putStr : String -> IO ()
437+putStr : String -> IO' l ()
438putStr x = do prim_fwrite prim__stdout x
438putStr x = do prim_fwrite prim__stdout x
439 return ()
439 return ()
440
440
441||| Output a string to stdout with a trailing newline
441||| Output a string to stdout with a trailing newline
442−putStrLn : String -> IO ()
442+putStrLn : String -> IO' l ()
443putStrLn x = putStr (x ++ "\n")
443putStrLn x = putStr (x ++ "\n")
444
444
445||| Output something showable to stdout, with a trailing newline
445||| Output something showable to stdout, with a trailing newline
@@ -449,7 +449,7 @@ print x = putStrLn (show x)
449
449
450||| Read one line of input from stdin
450||| Read one line of input from stdin
451partial
451partial
452−getLine : IO String
452+getLine : IO' l String
453getLine = prim_fread prim__stdin
453getLine = prim_fread prim__stdin
454
454
455||| Write a single character to stdout
455||| Write a single character to stdout
@@ -514,7 +514,7 @@ closeFile : File -> IO ()
514closeFile (FHandle h) = do_fclose h
514closeFile (FHandle h) = do_fclose h
515
515
516partial
516partial
517−do_fread : Ptr -> IO String
517+do_fread : Ptr -> IO' l String
518do_fread h = prim_fread h
518do_fread h = prim_fread h
519
519
520fgetc : File -> IO Char
520fgetc : File -> IO Char
@@ -547,7 +547,7 @@ pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
547-- prim__vm h
547-- prim__vm h
548
548
549partial
549partial
550−fread : File -> IO String
550+fread : File -> IO' l String
551fread (FHandle h) = do_fread h
551fread (FHandle h) = do_fread h
552
552
553partial
553partial