git.iko.soy/Idris-dev
on master help sign in
Merge pull request #989 from david-christiansen/docs
a706a7aEdwin Brady
libs/prelude/Decidable/Equality.idr+10−8
compare with master
unifiedsplit
@@ -12,6 +12,7 @@ import Prelude.Maybe
12-- Utility lemmas
12-- Utility lemmas
13--------------------------------------------------------------------------------
13--------------------------------------------------------------------------------
14
14
15+||| The negation of equality is symmetric (follows from symmetry of equality)
15total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
16total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
16negEqSym p h = p (sym h)
17negEqSym p h = p (sym h)
17
18
@@ -20,7 +21,9 @@ negEqSym p h = p (sym h)
20-- Decidable equality
21-- Decidable equality
21--------------------------------------------------------------------------------
22--------------------------------------------------------------------------------
22
23
24+||| Decision procedures for propositional equality
23class DecEq t where
25class DecEq t where
26+ ||| Decide whether two elements of `t` are propositionally equal
24 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
27 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
25
28
26--------------------------------------------------------------------------------
29--------------------------------------------------------------------------------
@@ -33,7 +36,6 @@ instance DecEq () where
33--------------------------------------------------------------------------------
36--------------------------------------------------------------------------------
34-- Booleans
37-- Booleans
35--------------------------------------------------------------------------------
38--------------------------------------------------------------------------------
36−
37total trueNotFalse : True = False -> _|_
39total trueNotFalse : True = False -> _|_
38trueNotFalse refl impossible
40trueNotFalse refl impossible
39
41
@@ -122,13 +124,13 @@ lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->
122lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl
124lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl
123
125
124instance (DecEq a, DecEq b) => DecEq (a, b) where
126instance (DecEq a, DecEq b) => DecEq (a, b) where
125− decEq (a, b) (a', b') with (decEq a a')
127+ decEq (a, b) (a', b') with (decEq a a')
126− decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
128+ decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
127− decEq (a, b) (a, b) | (Yes refl) | (Yes refl) = Yes refl
129+ 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)
130+ 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')
131+ 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)
132+ 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)
133+ decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
132
134
133
135
134--------------------------------------------------------------------------------
136--------------------------------------------------------------------------------
libs/prelude/Prelude.idr+20−2
@@ -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