0 | module Prelude.IO
  1 |
  2 | import Builtin
  3 | import PrimIO
  4 | import Prelude.Basics
  5 | import Prelude.Interfaces
  6 | import Prelude.Show
  7 |
  8 | %default total
  9 |
 10 | --------
 11 | -- IO --
 12 | --------
 13 |
 14 | public export
 15 | Functor IO where
 16 |   map f io = io_bind io $ io_pure . f
 17 |
 18 | %inline
 19 | public export
 20 | Applicative IO where
 21 |   pure x = io_pure x
 22 |   f <*> a
 23 |       = io_bind f (\f' =>
 24 |           io_bind a (\a' =>
 25 |             io_pure (f' a')))
 26 |
 27 | %inline
 28 | public export
 29 | Monad IO where
 30 |   b >>= k = io_bind b k
 31 |
 32 | public export
 33 | interface Monad io => HasIO io where
 34 |   constructor MkHasIO
 35 |   liftIO : IO a -> io a
 36 |
 37 | public export
 38 | interface Monad io => HasLinearIO io where
 39 |   constructor MkHasLinearIO
 40 |   liftIO1 : (1 _ : IO a) -> io a
 41 |
 42 | public export %inline
 43 | HasLinearIO IO where
 44 |   liftIO1 x = x
 45 |
 46 | public export %inline
 47 | HasLinearIO io => HasIO io where
 48 |   liftIO x = liftIO1 x
 49 |
 50 | export %inline
 51 | primIO : HasIO io => (fn : (1 x : %World) -> IORes a) -> io a
 52 | primIO op = liftIO (fromPrim op)
 53 |
 54 | export %inline
 55 | primIO1 : HasLinearIO io => (1 fn : (1 x : %World) -> IORes a) -> io a
 56 | primIO1 op = liftIO1 (fromPrim op)
 57 |
 58 | %extern
 59 | prim__onCollectAny : AnyPtr -> (AnyPtr -> PrimIO ()) -> PrimIO GCAnyPtr
 60 | %extern
 61 | prim__onCollect : Ptr t -> (Ptr t -> PrimIO ()) -> PrimIO (GCPtr t)
 62 |
 63 | export
 64 | onCollectAny : HasIO io => AnyPtr -> (AnyPtr -> IO ()) -> io GCAnyPtr
 65 | onCollectAny ptr c = primIO (prim__onCollectAny ptr (\x => toPrim (c x)))
 66 |
 67 | export
 68 | onCollect : HasIO io => Ptr t -> (Ptr t -> IO ()) -> io (GCPtr t)
 69 | onCollect ptr c = primIO (prim__onCollect ptr (\x => toPrim (c x)))
 70 |
 71 | %foreign "C:idris2_getString, libidris2_support, idris_support.h"
 72 |          "javascript:lambda:x=>x"
 73 | export
 74 | prim__getString : Ptr String -> String
 75 |
 76 | %foreign "C:putchar,libc 6"
 77 |          "node:lambda:x=>process.stdout.write(x)"
 78 |          "browser:lambda:x=>console.log(x)"
 79 | prim__putChar : Char -> (1 x : %World) -> IORes ()
 80 |
 81 | %foreign "C:getchar,libc 6"
 82 |          "node:support:getChar,support_system_file"
 83 | %extern prim__getChar : (1 x : %World) -> IORes Char
 84 |
 85 | %foreign "C:idris2_getStr, libidris2_support, idris_support.h"
 86 |          "node:support:getStr,support_system_file"
 87 | prim__getStr : PrimIO String
 88 |
 89 | %foreign "C:idris2_putStr, libidris2_support, idris_support.h"
 90 |          "node:lambda:x=>process.stdout.write(x)"
 91 |          "browser:lambda:x=>console.log(x)"
 92 | prim__putStr : String -> PrimIO ()
 93 |
 94 | ||| Output a string to stdout without a trailing newline.
 95 | %inline export
 96 | putStr : HasIO io => String -> io ()
 97 | putStr str = primIO (prim__putStr str)
 98 |
 99 | ||| Output a string to stdout with a trailing newline.
100 | export
101 | %inline putStrLn : HasIO io => String -> io ()
102 | putStrLn str = putStr (prim__strAppend str "\n")
103 |
104 | ||| Read one line of input from stdin, without the trailing newline.
105 | %inline export
106 | getLine : HasIO io => io String
107 | getLine = primIO prim__getStr
108 |
109 | ||| Write one single-byte character to stdout.
110 | %inline export
111 | putChar : HasIO io => Char -> io ()
112 | putChar c = primIO (prim__putChar c)
113 |
114 | ||| Write one multi-byte character to stdout, with a trailing newline.
115 | %inline export
116 | putCharLn : HasIO io => Char -> io ()
117 | putCharLn c = putStrLn (prim__cast_CharString c)
118 |
119 | ||| Read one single-byte character from stdin.
120 | %inline export
121 | getChar : HasIO io => io Char
122 | getChar = primIO prim__getChar
123 |
124 | %foreign "scheme:blodwen-thread"
125 |          "C:refc_fork"
126 | export
127 | prim__fork : (1 prog : PrimIO ()) -> PrimIO ThreadID
128 |
129 | export
130 | fork : (1 prog : IO ()) -> IO ThreadID
131 | fork act = fromPrim (prim__fork (toPrim act))
132 |
133 | %foreign "scheme:blodwen-thread-wait"
134 | export
135 | prim__threadWait : (1 threadID : ThreadID) -> PrimIO ()
136 |
137 | export
138 | threadWait : (1 threadID : ThreadID) -> IO ()
139 | threadWait threadID = fromPrim (prim__threadWait threadID)
140 |
141 | ||| Output something showable to stdout, without a trailing newline.
142 | %inline export
143 | print : HasIO io => Show a => a -> io ()
144 | print = putStr . show
145 |
146 | ||| Output something showable to stdout, with a trailing newline.
147 | %inline export
148 | printLn : HasIO io => Show a => a -> io ()
149 | printLn = putStrLn . show
150 |