git.iko.soy/Idris-dev
on master help sign in
Merge pull request #989 from david-christiansen/docs

Docs

commita706a7ac6ba1bcba48bda628984eecbc3dc99b55 authorEdwin Brady <edwin.brady@gmail.com> dateFri 21 Mar 2014, 18:55 (13 years ago) parent3cef6091d867e5
2 files changed+30−10
compare with master
unifiedsplit
libs/prelude/Decidable/Equality.idr+10−8 libs/prelude/Prelude.idr+20−2
libs/prelude/Decidable/Equality.idr+10−8
@@ -12,6 +12,7 @@ import Prelude.Maybe
1212-- Utility lemmas
1313--------------------------------------------------------------------------------
1414
15+||| The negation of equality is symmetric (follows from symmetry of equality)
1516total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
1617negEqSym p h = p (sym h)
1718
@@ -20,7 +21,9 @@ negEqSym p h = p (sym h)
2021-- Decidable equality
2122--------------------------------------------------------------------------------
2223
24+||| Decision procedures for propositional equality
2325class DecEq t where
26+ ||| Decide whether two elements of `t` are propositionally equal
2427 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
2528
2629--------------------------------------------------------------------------------
@@ -33,7 +36,6 @@ instance DecEq () where
3336--------------------------------------------------------------------------------
3437-- Booleans
3538--------------------------------------------------------------------------------
36−
3739total trueNotFalse : True = False -> _|_
3840trueNotFalse refl impossible
3941
@@ -122,13 +124,13 @@ lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->
122124lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl
123125
124126instance (DecEq a, DecEq b) => DecEq (a, b) where
125− decEq (a, b) (a', b') with (decEq a a')
126− decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
127− decEq (a, b) (a, b) | (Yes refl) | (Yes refl) = Yes refl
128− decEq (a, b) (a, b') | (Yes refl) | (No p) = No (\eq => lemma_snd_neq refl p eq)
129− decEq (a, b) (a', b') | (No p) with (decEq b b')
130− decEq (a, b) (a', b) | (No p) | (Yes refl) = No (\eq => lemma_fst_neq_snd_eq p refl eq)
131− decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
127+ decEq (a, b) (a', b') with (decEq a a')
128+ decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
129+ decEq (a, b) (a, b) | (Yes refl) | (Yes refl) = Yes refl
130+ decEq (a, b) (a, b') | (Yes refl) | (No p) = No (\eq => lemma_snd_neq refl p eq)
131+ decEq (a, b) (a', b') | (No p) with (decEq b b')
132+ decEq (a, b) (a', b) | (No p) | (Yes refl) = No (\eq => lemma_fst_neq_snd_eq p refl eq)
133+ decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
132134
133135
134136--------------------------------------------------------------------------------
libs/prelude/Prelude.idr+20−2
@@ -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