8c28352 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some Prelude reorganisation

8c28352Edwin Brady11 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -26,6 +26,7 @@ New in 0.9.19:

26 variable used in the right hand side of the case.

27* Some improvements in interactive editing, particularly in lifting out

28 definitions and proof search.

29+* Moved System.Interactive, along with getArgs to the Prelude.

30New in 0.9.18:

31New in 0.9.18:

31--------------

32--------------

idris.cabal−3

@@ -390,9 +390,6 @@ Extra-source-files:

390 test/delab001/expected

391 test/delab001/input

392

393− test/disambig001/run

394− test/disambig001/*.idr

395− test/disambig001/expected

396 test/disambig002/run

393 test/disambig002/run

397 test/disambig002/*.idr

394 test/disambig002/*.idr

398 test/disambig002/expected

395 test/disambig002/expected

libs/base/System.idr−16

@@ -4,22 +4,6 @@ module System

4%default partial

5%access public

7−||| Get the command-line arguments that the program was called with.

8−getArgs : IO (List String)

9−getArgs = do n <- numArgs

10− ga' [] 0 n

11− where

12− numArgs : IO Int

13− numArgs = foreign FFI_C "idris_numArgs" (IO Int)

14−

15− getArg : Int -> IO String

16− getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x

17−

18− ga' : List String -> Int -> Int -> IO (List String)

19− ga' acc i n = if (i == n) then (return $ reverse acc) else

20− do arg <- getArg i

21− ga' (arg :: acc) (i+1) n

22−

23||| Retrieves an value from the environment, if the given key is present,

7||| Retrieves an value from the environment, if the given key is present,

24||| otherwise it returns Nothing.

8||| otherwise it returns Nothing.

25getEnv : String -> IO (Maybe String)

9getEnv : String -> IO (Maybe String)

libs/base/base.ipkg+1−1

@@ -5,7 +5,7 @@ modules = System,

6 Debug.Error, Debug.Trace,

8− System.Info, System.Interactive,

8+ System.Info,

10 Language.Reflection.Utils,

libs/prelude/Prelude.idr+2−211

@@ -25,6 +25,8 @@ import public Prelude.Pairs

25import public Prelude.Stream

26import public Prelude.Providers

27import public Prelude.Show

28+import public Prelude.Interactive

29+import public Prelude.File

28import public Decidable.Equality

30import public Decidable.Equality

29import public Language.Reflection

31import public Language.Reflection

30import public Language.Reflection.Errors

32import public Language.Reflection.Errors

@@ -43,9 +45,6 @@ decAsBool (No _) = False

43instance Functor PrimIO where

45instance Functor PrimIO where

44 map f io = prim_io_bind io (prim_io_return . f)

46 map f io = prim_io_bind io (prim_io_return . f)

46−instance Functor (IO' ffi) where

47− map f io = io_bind io (\b => io_return (f b))

48−

49instance Functor Maybe where

48instance Functor Maybe where

50 map f (Just x) = Just (f x)

49 map f (Just x) = Just (f x)

51 map f Nothing = Nothing

50 map f Nothing = Nothing

@@ -61,12 +60,6 @@ instance Applicative PrimIO where

62 am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

61 am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

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−

70instance Applicative Maybe where

63instance Applicative Maybe where

71 pure = Just

64 pure = Just

@@ -103,9 +96,6 @@ instance Alternative List where

103instance Monad PrimIO where

96instance Monad PrimIO where

104 b >>= k = prim_io_bind b k

97 b >>= k = prim_io_bind b k

105

106−instance Monad (IO' ffi) where

107− b >>= k = io_bind b k

108−

109instance Monad Maybe where

99instance Monad Maybe where

110 Nothing >>= k = Nothing

100 Nothing >>= k = Nothing

111 (Just x) >>= k = k x

101 (Just x) >>= k = k x

@@ -229,183 +219,6 @@ curry f a b = f (a, b)

229uncurry : (a -> b -> c) -> (a, b) -> c

219uncurry : (a -> b -> c) -> (a, b) -> c

230uncurry f (a, b) = f a b

220uncurry f (a, b) = f a b

231

221

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−

409namespace JSNull

222namespace JSNull

410 ||| Check if a foreign pointer is null

223 ||| Check if a foreign pointer is null

411 partial

224 partial

@@ -425,12 +238,6 @@ eqPtr : Ptr -> Ptr -> IO Bool

425eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y

238eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y

426 return (eq /= 0)

239 return (eq /= 0)

427

240

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−

434||| Loop while some test is true

241||| Loop while some test is true

435|||

242|||

436||| @ test the condition of the loop

243||| @ test the condition of the loop

@@ -442,22 +249,6 @@ while t b = do v <- t

442 while t b

249 while t b

443 else return ()

250 else return ()

444

251

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−

461------- Some error rewriting

252------- Some error rewriting

462

253

463%language ErrorReflection

254%language ErrorReflection

libs/prelude/Prelude/File.idrnew file+156

@@ -0,0 +1,156 @@

1+module Prelude.File

3+import Builtins

4+import Prelude.List

5+import Prelude.Maybe

6+import Prelude.Monad

7+import Prelude.Chars

8+import Prelude.Strings

9+import Prelude.Cast

10+import Prelude.Bool

11+import Prelude.Basics

12+import Prelude.Classes

13+import Prelude.Monad

14+import IO

15+

16+%access public

17+

18+||| A file handle

19+abstract

20+data File = FHandle Ptr

21+

22+||| Standard input

23+stdin : File

24+stdin = FHandle prim__stdin

25+

26+||| Standard output

27+stdout : File

28+stdout = FHandle prim__stdout

29+

30+||| Standard output

31+stderr : File

32+stderr = FHandle prim__stderr

33+

34+||| Call the RTS's file opening function

35+do_fopen : String -> String -> IO Ptr

36+do_fopen f m

37+ = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

38+

39+||| Open a file

40+||| @ f the filename

41+||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)

42+fopen : (f : String) -> (m : String) -> IO File

43+fopen f m = do h <- do_fopen f m

44+ return (FHandle h)

45+

46+||| Check whether a file handle is actually a null pointer

47+partial

48+validFile : File -> IO Bool

49+validFile (FHandle h) = do x <- nullPtr h

50+ return (not x)

51+

52+||| Modes for opening files

53+data Mode = Read | Write | ReadWrite

54+

55+||| Open a file

56+||| @ f the filename

57+||| @ m the mode

58+partial

59+openFile : (f : String) -> (m : Mode) -> IO File

60+openFile f m = fopen f (modeStr m) where

61+ modeStr Read = "r"

62+ modeStr Write = "w"

63+ modeStr ReadWrite = "r+"

64+

65+partial

66+do_fclose : Ptr -> IO ()

67+do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h

68+

69+partial

70+closeFile : File -> IO ()

71+closeFile (FHandle h) = do_fclose h

72+

73+partial

74+do_fread : Ptr -> IO' l String

75+do_fread h = prim_fread h

76+

77+fgetc : File -> IO Char

78+fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))

79+

80+fgetc' : File -> IO (Maybe Char)

81+fgetc' (FHandle h)

82+ = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h

83+ if (x < 0) then return Nothing

84+ else return (Just (cast x))

85+

86+fflush : File -> IO ()

87+fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

88+

89+do_popen : String -> String -> IO Ptr

90+do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m

91+

92+popen : String -> Mode -> IO File

93+popen f m = do ptr <- do_popen f (modeStr m)

94+ return (FHandle ptr)

95+ where

96+ modeStr Read = "r"

97+ modeStr Write = "w"

98+ modeStr ReadWrite = "r+"

99+

100+pclose : File -> IO ()

101+pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h

102+

103+-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))

104+-- prim__vm h

105+

106+partial

107+fread : File -> IO' l String

108+fread (FHandle h) = do_fread h

109+

110+partial

111+do_fwrite : Ptr -> String -> IO ()

112+do_fwrite h s = do prim_fwrite h s

113+ return ()

114+

115+partial

116+fwrite : File -> String -> IO ()

117+fwrite (FHandle h) s = do_fwrite h s

118+

119+partial

120+do_feof : Ptr -> IO Int

121+do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h

122+

123+||| Check if a file handle has reached the end

124+feof : File -> IO Bool

125+feof (FHandle h) = do eof <- do_feof h

126+ return (not (eof == 0))

127+

128+partial

129+do_ferror : Ptr -> IO Int

130+do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h

131+

132+ferror : File -> IO Bool

133+ferror (FHandle h) = do err <- do_ferror h

134+ return (not (err == 0))

135+

136+fpoll : File -> IO Bool

137+fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

138+ return (p > 0)

139+

140+||| Read the contents of a file into a string

141+partial -- no error checking!

142+readFile : String -> IO String

143+readFile fn = do h <- openFile fn Read

144+ c <- readFile' h ""

145+ closeFile h

146+ return c

147+ where

148+ partial

149+ readFile' : File -> String -> IO String

150+ readFile' h contents =

151+ do x <- feof h

152+ if not x then do l <- fread h

153+ readFile' h (contents ++ l)

154+ else return contents

155+

156+

libs/base/System/Interactive.idr → libs/prelude/Prelude/Interactive.idrrenamed+79−9

@@ -4,13 +4,83 @@

4||| the easy creation of interactive programs without needing to teach IO

5||| or Effects first, but they also capture some common patterns of interactive

6||| programming.

7−module System.Interactive

7+module Prelude.Interactive

9−{-

9+import Builtins

10−When the interfaces and names are stable, these are intended for the Prelude.

10+import Prelude.List

11−-}

11+import Prelude.File

12+import Prelude.Bool

13+import Prelude.Classes

14+import Prelude.Strings

15+import Prelude.Chars

16+import Prelude.Show

17+import Prelude.Cast

18+import Prelude.Maybe

19+import Prelude.Functor

20+import Prelude.Monad

21+import IO

22+

23+%access public

24+

25+---- some basic io

26+

27+||| Output a string to stdout without a trailing newline

28+putStr : String -> IO' ffi ()

29+putStr x = do prim_write x

30+ return ()

31+

32+||| Output a string to stdout with a trailing newline

33+putStrLn : String -> IO' ffi ()

34+putStrLn x = putStr (x ++ "\n")

35+

36+||| Output something showable to stdout, without a trailing newline

37+print : Show a => a -> IO' ffi ()

38+print x = putStr (show x)

39+

40+||| Output something showable to stdout, with a trailing newline

41+printLn : Show a => a -> IO' ffi ()

42+printLn x = putStrLn (show x)

43+

44+||| Read one line of input from stdin, without the trailing newline

45+getLine : IO' ffi String

46+getLine = do x <- prim_read

47+ return (reverse (trimNL (reverse x)))

48+ where trimNL : String -> String

49+ trimNL str with (strM str)

50+ trimNL "" | StrNil = ""

51+ trimNL (strCons '\n' xs) | StrCons _ _ = xs

52+ trimNL (strCons x xs) | StrCons _ _ = strCons x xs

53+

54+||| Write a single character to stdout

55+putChar : Char -> IO ()

56+putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)

57+

58+||| Write a singel character to stdout, with a trailing newline

59+putCharLn : Char -> IO ()

60+putCharLn c = putStrLn (singleton c)

61+

62+||| Read a single character from stdin

63+getChar : IO Char

64+getChar = map cast $ foreign FFI_C "getchar" (IO Int)

65+

66+||| Get the command-line arguments that the program was called with.

67+partial

68+getArgs : IO (List String)

69+getArgs = do n <- numArgs

70+ ga' [] 0 n

71+ where

72+ numArgs : IO Int

73+ numArgs = foreign FFI_C "idris_numArgs" (IO Int)

74+

75+ getArg : Int -> IO String

76+ getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x

77+

78+ partial

79+ ga' : List String -> Int -> Int -> IO (List String)

80+ ga' acc i n = if (i == n) then (return $ reverse acc) else

81+ do arg <- getArg i

82+ ga' (arg :: acc) (i+1) n

13−import System

15||| Process input from an open file handle, while maintaining a state.

85||| Process input from an open file handle, while maintaining a state.

16||| @ state the input state

86||| @ state the input state

@@ -18,7 +88,7 @@ import System

18||| output and a new state

88||| output and a new state

19||| @ onEOF the function to run on reaching end of file, returning a String

89||| @ onEOF the function to run on reaching end of file, returning a String

20||| to output

90||| to output

21−public partial

91+partial

22processHandle : File ->

92processHandle : File ->

23 (state : a) ->

93 (state : a) ->

24 (onRead : a -> String -> (String, a)) ->

94 (onRead : a -> String -> (String, a)) ->

@@ -38,7 +108,7 @@ processHandle h acc onRead onEOF

38||| output and a new state

108||| output and a new state

39||| @ onEOI the function to run on reaching end of input, returning a String

109||| @ onEOI the function to run on reaching end of input, returning a String

40||| to output

110||| to output

41−public partial

111+partial

42processStdin : (state : a) ->

112processStdin : (state : a) ->

43 (onRead : a -> String -> (String, a)) ->

113 (onRead : a -> String -> (String, a)) ->

44 (onEOI : a -> String) -> IO ()

114 (onEOI : a -> String) -> IO ()

@@ -49,7 +119,7 @@ processStdin = processHandle stdin

49||| @ prompt the prompt to show

119||| @ prompt the prompt to show

50||| @ onInput the function to run on reading input, returning a String to

120||| @ onInput the function to run on reading input, returning a String to

51||| output and a new state. Returns Nothing if the repl should exit

121||| output and a new state. Returns Nothing if the repl should exit

52−public partial

122+partial

53replWith : (state : a) -> (prompt : String) ->

123replWith : (state : a) -> (prompt : String) ->

54 (onInput : a -> String -> Maybe (String, a)) -> IO a

124 (onInput : a -> String -> Maybe (String, a)) -> IO a

55replWith acc prompt fn

125replWith acc prompt fn

@@ -64,7 +134,7 @@ replWith acc prompt fn

64||| @ prompt the prompt to show

134||| @ prompt the prompt to show

65||| @ onInput the function to run on reading input, returning a String to

135||| @ onInput the function to run on reading input, returning a String to

66||| output

136||| output

67−public partial

137+partial

68repl : (prompt : String) ->

138repl : (prompt : String) ->

69 (onInput : String -> String) -> IO ()

139 (onInput : String -> String) -> IO ()

70repl prompt fn

140repl prompt fn

libs/prelude/Prelude/Monad.idr+19−1

@@ -3,9 +3,10 @@ module Prelude.Monad

3-- Monads and Functors

5import Builtins

6−import Prelude.List

6+import Prelude.Functor

7import Prelude.Applicative

8import Prelude.Basics

9+import IO

10%access public

11%access public

@@ -22,3 +23,20 @@ flatten a = a >>= id

22||| define `return` and `pure` differently!

23||| define `return` and `pure` differently!

23return : Monad m => a -> m a

24return : Monad m => a -> m a

24return = pure

25return = pure

26+

27+-- Annoyingly, these need to be here, so that we can use them in other

28+-- Prelude modules other than the top level.

29+

30+instance Functor (IO' ffi) where

31+ map f io = io_bind io (\b => io_return (f b))

32+

33+instance Applicative (IO' ffi) where

34+ pure x = io_return x

35+ f <*> a = io_bind f (\f' =>

36+ io_bind a (\a' =>

37+ io_return (f' a')))

38+

39+

40+instance Monad (IO' ffi) where

41+ b >>= k = io_bind b k

42+

libs/prelude/Prelude/Strings.idr+15

@@ -1,6 +1,7 @@

1module Prelude.Strings

3import Builtins

4+import IO

5import Prelude.Algebra

6import Prelude.Algebra

6import Prelude.Basics

7import Prelude.Basics

@@ -13,6 +14,7 @@ import Prelude.Foldable

13import Prelude.Functor

14import Prelude.Functor

14import Prelude.List

15import Prelude.List

15import Prelude.Nat

16import Prelude.Nat

17+import Prelude.Monad

16import Decidable.Equality

18import Decidable.Equality

18partial

20partial

@@ -347,3 +349,16 @@ isSuffixOf a b = isSuffixOf (unpack a) (unpack b)

347

349

348isInfixOf : String -> String -> Bool

350isInfixOf : String -> String -> Bool

349isInfixOf a b = isInfixOf (unpack a) (unpack b)

351isInfixOf a b = isInfixOf (unpack a) (unpack b)

352+

353+||| Check if a foreign pointer is null

354+partial

355+nullPtr : Ptr -> IO Bool

356+nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p

357+ return (ok /= 0)

358+

359+||| Check if a supposed string was actually a null pointer

360+partial

361+nullStr : String -> IO Bool

362+nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p

363+ return (ok /= 0)

364+

libs/prelude/prelude.ipkg+1

@@ -9,6 +9,7 @@ modules = Builtins, Prelude, IO,

9 Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,

12+ Prelude.Interactive, Prelude.File,

13 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

14 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

test/disambig001/disambig001.idrdeleted−12

@@ -1,12 +0,0 @@

1−module Main

2−

3−import Prelude.Monad

4−

5−import System

6−import Effect.System

7−

8−main : IO ()

9−main = do

10− args <- System.getArgs

11− putStrLn (concat (drop 1 args))

12−

test/disambig001/expecteddeleted−1

@@ -1 +0,0 @@

1−foobar

test/disambig001/rundeleted−4

@@ -1,4 +0,0 @@

1−#!/usr/bin/env bash

2−idris $@ disambig001.idr -p effects -o disambig001

3−./disambig001 foo bar

4−rm -f disambig001 *.ibc

test/docs003/expected+1−1

@@ -11,11 +11,11 @@ Methods:

11 The function is Total

12Instances:

13 Functor List

14+ Functor (IO' ffi)

14 Functor Stream

15 Functor Stream

15 Functor Provider

16 Functor Provider

16 Functor Binder

17 Functor Binder

17 Functor PrimIO

18 Functor PrimIO

18− Functor (IO' ffi)

19 Functor Maybe

20 Functor (Either e)