git.iko.soy/Idris-dev
on master help sign in
Add JS FFI description

It's not implemented yet though...

commit2170b9a3b4ba0178cdfc31e76398f3ec4f3d6394 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 19 Jan 2015, 12:38 (12 years ago) parentf6df58c
2 files changed+41−12
compare with master
unifiedsplit
libs/prelude/IO.idr+36−7 libs/prelude/Prelude.idr+5−5
libs/prelude/IO.idr+36−7
@@ -96,6 +96,13 @@ unsafePerformIO : IO' ffi a -> a
9696unsafePerformIO (MkIO f) = unsafePerformPrimIO
9797 (prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_return b))
9898
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+
99106--------- The C FFI
100107
101108data 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
141148 (\ x => prim_io_return x)))
142149 (\x => prim_io_return x))
143150
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−
151151forceGC : IO ()
152152forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm
153153
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
434434---- some basic io
435435
436436||| Output a string to stdout without a trailing newline
437−putStr : String -> IO ()
437+putStr : String -> IO' l ()
438438putStr x = do prim_fwrite prim__stdout x
439439 return ()
440440
441441||| Output a string to stdout with a trailing newline
442−putStrLn : String -> IO ()
442+putStrLn : String -> IO' l ()
443443putStrLn x = putStr (x ++ "\n")
444444
445445||| Output something showable to stdout, with a trailing newline
@@ -449,7 +449,7 @@ print x = putStrLn (show x)
449449
450450||| Read one line of input from stdin
451451partial
452−getLine : IO String
452+getLine : IO' l String
453453getLine = prim_fread prim__stdin
454454
455455||| Write a single character to stdout
@@ -514,7 +514,7 @@ closeFile : File -> IO ()
514514closeFile (FHandle h) = do_fclose h
515515
516516partial
517−do_fread : Ptr -> IO String
517+do_fread : Ptr -> IO' l String
518518do_fread h = prim_fread h
519519
520520fgetc : File -> IO Char
@@ -547,7 +547,7 @@ pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
547547-- prim__vm h
548548
549549partial
550−fread : File -> IO String
550+fread : File -> IO' l String
551551fread (FHandle h) = do_fread h
552552
553553partial