@@ -439,26 +439,32 @@ uniformB64x2 x = prim__mkB64x2 x x
439439
440440---- some basic io
441441
442+||| Output a string to stdout without a trailing newline
442443partial
443444putStr : String -> IO ()
444445putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
445446
447+||| Output a string to stdout with a trailing newline
446448partial
447449putStrLn : String -> IO ()
448450putStrLn x = putStr (x ++ "\n")
449451
452+||| Output something showable to stdout, with a trailing newline
450453partial
451454print : Show a => a -> IO ()
452455print x = putStrLn (show x)
453456
457+||| Read one line of input from stdin
454458partial
455459getLine : IO String
456460getLine = prim_fread prim__stdin
457461
462+||| Write a single character to stdout
458463partial
459464putChar : Char -> IO ()
460465putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)
461466
467+||| Read a single character from stdin
462468partial
463469getChar : IO Char
464470getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
@@ -468,21 +474,30 @@ getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
468474abstract
469475data File = FHandle Ptr
470476
477+||| Standard input
471478partial stdin : File
472479stdin = FHandle prim__stdin
473480
481+||| Call the RTS's file opening function
474482do_fopen : String -> String -> IO Ptr
475483do_fopen f m
476484 = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
477485
478−fopen : String -> String -> IO File
486+||| Open a file
487+||| @ f the filename
488+||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
489+fopen : (f : String) -> (m : String) -> IO File
479490fopen f m = do h <- do_fopen f m
480491 return (FHandle h)
481492
493+||| Modes for opening files
482494data Mode = Read | Write | ReadWrite
483495
496+||| Open a file
497+||| @ f the filename
498+||| @ m the mode
484499partial
485−openFile : String -> Mode -> IO File
500+openFile : (f : String) -> (m : Mode) -> IO File
486501openFile f m = fopen f (modeStr m) where
487502 modeStr Read = "r"
488503 modeStr Write = "w"
@@ -567,15 +582,18 @@ nullPtr : Ptr -> IO Bool
567582nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
568583 return (ok /= 0)
569584
585+||| Check if a supposed string was actually a null pointer
570586partial
571587nullStr : String -> IO Bool
572588nullStr p = do ok <- mkForeign (FFun "isNull" [FString] FInt) p
573589 return (ok /= 0)
574590
591+||| Pointer equality
575592eqPtr : Ptr -> Ptr -> IO Bool
576593eqPtr x y = do eq <- mkForeign (FFun "idris_eqPtr" [FPtr, FPtr] FInt) x y
577594 return (eq /= 0)
578595
596+||| Check whether a file handle is actually a null pointer
579597partial
580598validFile : File -> IO Bool
581599validFile (FHandle h) = do x <- nullPtr h