@@ -25,6 +25,8 @@ import public Prelude.Pairs
2525import public Prelude.Stream
2626import public Prelude.Providers
2727import public Prelude.Show
28+import public Prelude.Interactive
29+import public Prelude.File
2830import public Decidable.Equality
2931import public Language.Reflection
3032import public Language.Reflection.Errors
@@ -43,9 +45,6 @@ decAsBool (No _) = False
4345instance Functor PrimIO where
4446 map f io = prim_io_bind io (prim_io_return . f)
4547
46−instance Functor (IO' ffi) where
47− map f io = io_bind io (\b => io_return (f b))
48−
4948instance Functor Maybe where
5049 map f (Just x) = Just (f x)
5150 map f Nothing = Nothing
@@ -61,12 +60,6 @@ instance Applicative PrimIO where
6160
6261 am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
6362
64−instance Applicative (IO' ffi) where
65− pure x = io_return x
66− f <*> a = io_bind f (\f' =>
67− io_bind a (\a' =>
68− io_return (f' a')))
69−
7063instance Applicative Maybe where
7164 pure = Just
7265
@@ -103,9 +96,6 @@ instance Alternative List where
10396instance Monad PrimIO where
10497 b >>= k = prim_io_bind b k
10598
106−instance Monad (IO' ffi) where
107− b >>= k = io_bind b k
108−
10999instance Monad Maybe where
110100 Nothing >>= k = Nothing
111101 (Just x) >>= k = k x
@@ -229,183 +219,6 @@ curry f a b = f (a, b)
229219uncurry : (a -> b -> c) -> (a, b) -> c
230220uncurry f (a, b) = f a b
231221
232−---- some basic io
233−
234−||| Output a string to stdout without a trailing newline
235−putStr : String -> IO' ffi ()
236−putStr x = do prim_write x
237− return ()
238−
239−||| Output a string to stdout with a trailing newline
240−putStrLn : String -> IO' ffi ()
241−putStrLn x = putStr (x ++ "\n")
242−
243−||| Output something showable to stdout, without a trailing newline
244−partial
245−print : Show a => a -> IO' ffi ()
246−print x = putStr (show x)
247−
248−||| Output something showable to stdout, with a trailing newline
249−partial
250−printLn : Show a => a -> IO' ffi ()
251−printLn x = putStrLn (show x)
252−
253−||| Read one line of input from stdin, without the trailing newline
254−partial
255−getLine : IO' ffi String
256−getLine = do x <- prim_read
257− return (reverse (trimNL (reverse x)))
258− where trimNL : String -> String
259− trimNL str with (strM str)
260− trimNL "" | StrNil = ""
261− trimNL (strCons '\n' xs) | StrCons _ _ = xs
262− trimNL (strCons x xs) | StrCons _ _ = strCons x xs
263−
264−||| Write a single character to stdout
265−partial
266−putChar : Char -> IO ()
267−putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)
268−
269−||| Write a singel character to stdout, with a trailing newline
270−partial
271−putCharLn : Char -> IO ()
272−putCharLn c = putStrLn (singleton c)
273−
274−||| Read a single character from stdin
275−partial
276−getChar : IO Char
277−getChar = map cast $ foreign FFI_C "getchar" (IO Int)
278−
279−---- some basic file handling
280−
281−||| A file handle
282−abstract
283−data File = FHandle Ptr
284−
285−||| Standard input
286−stdin : File
287−stdin = FHandle prim__stdin
288−
289−||| Standard output
290−stdout : File
291−stdout = FHandle prim__stdout
292−
293−||| Standard output
294−stderr : File
295−stderr = FHandle prim__stderr
296−
297−||| Call the RTS's file opening function
298−do_fopen : String -> String -> IO Ptr
299−do_fopen f m
300− = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
301−
302−||| Open a file
303−||| @ f the filename
304−||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
305−fopen : (f : String) -> (m : String) -> IO File
306−fopen f m = do h <- do_fopen f m
307− return (FHandle h)
308−
309−||| Modes for opening files
310−data Mode = Read | Write | ReadWrite
311−
312−||| Open a file
313−||| @ f the filename
314−||| @ m the mode
315−partial
316−openFile : (f : String) -> (m : Mode) -> IO File
317−openFile f m = fopen f (modeStr m) where
318− modeStr Read = "r"
319− modeStr Write = "w"
320− modeStr ReadWrite = "r+"
321−
322−partial
323−do_fclose : Ptr -> IO ()
324−do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
325−
326−partial
327−closeFile : File -> IO ()
328−closeFile (FHandle h) = do_fclose h
329−
330−partial
331−do_fread : Ptr -> IO' l String
332−do_fread h = prim_fread h
333−
334−fgetc : File -> IO Char
335−fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))
336−
337−fgetc' : File -> IO (Maybe Char)
338−fgetc' (FHandle h)
339− = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h
340− if (x < 0) then return Nothing
341− else return (Just (cast x))
342−
343−fflush : File -> IO ()
344−fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
345−
346−do_popen : String -> String -> IO Ptr
347−do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
348−
349−popen : String -> Mode -> IO File
350−popen f m = do ptr <- do_popen f (modeStr m)
351− return (FHandle ptr)
352− where
353− modeStr Read = "r"
354− modeStr Write = "w"
355− modeStr ReadWrite = "r+"
356−
357−pclose : File -> IO ()
358−pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
359−
360−-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
361−-- prim__vm h
362−
363−partial
364−fread : File -> IO' l String
365−fread (FHandle h) = do_fread h
366−
367−partial
368−do_fwrite : Ptr -> String -> IO ()
369−do_fwrite h s = do prim_fwrite h s
370− return ()
371−
372−partial
373−fwrite : File -> String -> IO ()
374−fwrite (FHandle h) s = do_fwrite h s
375−
376−partial
377−do_feof : Ptr -> IO Int
378−do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
379−
380−||| Check if a file handle has reached the end
381−feof : File -> IO Bool
382−feof (FHandle h) = do eof <- do_feof h
383− return (not (eof == 0))
384−
385−partial
386−do_ferror : Ptr -> IO Int
387−do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
388−
389−ferror : File -> IO Bool
390−ferror (FHandle h) = do err <- do_ferror h
391− return (not (err == 0))
392−
393−fpoll : File -> IO Bool
394−fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
395− return (p > 0)
396−
397−||| Check if a foreign pointer is null
398−partial
399−nullPtr : Ptr -> IO Bool
400−nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p
401− return (ok /= 0)
402−
403−||| Check if a supposed string was actually a null pointer
404−partial
405−nullStr : String -> IO Bool
406−nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p
407− return (ok /= 0)
408−
409222namespace JSNull
410223 ||| Check if a foreign pointer is null
411224 partial
@@ -425,12 +238,6 @@ eqPtr : Ptr -> Ptr -> IO Bool
425238eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y
426239 return (eq /= 0)
427240
428−||| Check whether a file handle is actually a null pointer
429−partial
430−validFile : File -> IO Bool
431−validFile (FHandle h) = do x <- nullPtr h
432− return (not x)
433−
434241||| Loop while some test is true
435242|||
436243||| @ test the condition of the loop
@@ -442,22 +249,6 @@ while t b = do v <- t
442249 while t b
443250 else return ()
444251
445−||| Read the contents of a file into a string
446−partial -- no error checking!
447−readFile : String -> IO String
448−readFile fn = do h <- openFile fn Read
449− c <- readFile' h ""
450− closeFile h
451− return c
452− where
453− partial
454− readFile' : File -> String -> IO String
455− readFile' h contents =
456− do x <- feof h
457− if not x then do l <- fread h
458− readFile' h (contents ++ l)
459− else return contents
460−
461252------- Some error rewriting
462253
463254%language ErrorReflection