git.iko.soy/Idris-dev
on master help sign in
More docstrings
1d867e5David Raymond Christiansen
libs/prelude/Prelude.idr+20−2
compare with master
unifiedsplit
@@ -439,26 +439,32 @@ uniformB64x2 x = prim__mkB64x2 x x
439
439
440---- some basic io
440---- some basic io
441
441
442+||| Output a string to stdout without a trailing newline
442partial
443partial
443putStr : String -> IO ()
444putStr : String -> IO ()
444putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
445putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
445
446
447+||| Output a string to stdout with a trailing newline
446partial
448partial
447putStrLn : String -> IO ()
449putStrLn : String -> IO ()
448putStrLn x = putStr (x ++ "\n")
450putStrLn x = putStr (x ++ "\n")
449
451
452+||| Output something showable to stdout, with a trailing newline
450partial
453partial
451print : Show a => a -> IO ()
454print : Show a => a -> IO ()
452print x = putStrLn (show x)
455print x = putStrLn (show x)
453
456
457+||| Read one line of input from stdin
454partial
458partial
455getLine : IO String
459getLine : IO String
456getLine = prim_fread prim__stdin
460getLine = prim_fread prim__stdin
457
461
462+||| Write a single character to stdout
458partial
463partial
459putChar : Char -> IO ()
464putChar : Char -> IO ()
460putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)
465putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)
461
466
467+||| Read a single character from stdin
462partial
468partial
463getChar : IO Char
469getChar : IO Char
464getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
470getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
@@ -468,21 +474,30 @@ getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
468abstract
474abstract
469data File = FHandle Ptr
475data File = FHandle Ptr
470
476
477+||| Standard input
471partial stdin : File
478partial stdin : File
472stdin = FHandle prim__stdin
479stdin = FHandle prim__stdin
473
480
481+||| Call the RTS's file opening function
474do_fopen : String -> String -> IO Ptr
482do_fopen : String -> String -> IO Ptr
475do_fopen f m
483do_fopen f m
476 = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
484 = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
477
485
486+||| Open a file
487+||| @ f the filename
488+||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
478−fopen : String -> String -> IO File
489+fopen : (f : String) -> (m : String) -> IO File
479fopen f m = do h <- do_fopen f m
490fopen f m = do h <- do_fopen f m
480 return (FHandle h)
491 return (FHandle h)
481
492
493+||| Modes for opening files
482data Mode = Read | Write | ReadWrite
494data Mode = Read | Write | ReadWrite
483
495
496+||| Open a file
497+||| @ f the filename
498+||| @ m the mode
484partial
499partial
485−openFile : String -> Mode -> IO File
500+openFile : (f : String) -> (m : Mode) -> IO File
486openFile f m = fopen f (modeStr m) where
501openFile f m = fopen f (modeStr m) where
487 modeStr Read = "r"
502 modeStr Read = "r"
488 modeStr Write = "w"
503 modeStr Write = "w"
@@ -567,15 +582,18 @@ nullPtr : Ptr -> IO Bool
567nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
582nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
568 return (ok /= 0)
583 return (ok /= 0)
569
584
585+||| Check if a supposed string was actually a null pointer
570partial
586partial
571nullStr : String -> IO Bool
587nullStr : String -> IO Bool
572nullStr p = do ok <- mkForeign (FFun "isNull" [FString] FInt) p
588nullStr p = do ok <- mkForeign (FFun "isNull" [FString] FInt) p
573 return (ok /= 0)
589 return (ok /= 0)
574
590
591+||| Pointer equality
575eqPtr : Ptr -> Ptr -> IO Bool
592eqPtr : Ptr -> Ptr -> IO Bool
576eqPtr x y = do eq <- mkForeign (FFun "idris_eqPtr" [FPtr, FPtr] FInt) x y
593eqPtr x y = do eq <- mkForeign (FFun "idris_eqPtr" [FPtr, FPtr] FInt) x y
577 return (eq /= 0)
594 return (eq /= 0)
578
595
596+||| Check whether a file handle is actually a null pointer
579partial
597partial
580validFile : File -> IO Bool
598validFile : File -> IO Bool
581validFile (FHandle h) = do x <- nullPtr h
599validFile (FHandle h) = do x <- nullPtr h