bf8dbc9 · Idris-dev · git.iko.soy

CHANGELOG+6−1

compare with master

unifiedsplit

@@ -23,6 +23,7 @@ New in 0.9.17:

23 an extra argument of type TTName. This allows more understandable

24 dynamic errors in DSL code and more readable code generation results.

25* DSL notation can now be applied with $

26+<<<<<<< HEAD

26* Added FFI_Export type which allows Idris functions to be exportoed and

27* Added FFI_Export type which allows Idris functions to be exportoed and

27 called from foreign code

28 called from foreign code

28* Instances can now have documentation strings.

29* Instances can now have documentation strings.

@@ -32,7 +33,11 @@ New in 0.9.17:

32* New REPL command ":core TM" that shows the elaborated form of TM along with

33* New REPL command ":core TM" that shows the elaborated form of TM along with

33 its elaborated type using the syntax of TT. IDE mode has a corresponding

34 its elaborated type using the syntax of TT. IDE mode has a corresponding

34 command :elaborate-term for serialized terms.

35 command :elaborate-term for serialized terms.

35−

36+* Effectful and IO function names for sending data to STDOUT have been

37+ aligned, semantically.

38+ + `print` is now for putting showable things to STDOUT.

39+ + `printLn` is for putting showable things to STDOUT with a new line

40+ + `putCharLn` for putting a single character to STDOUT, with a new line.

36

41

37New in 0.9.16:

42New in 0.9.16:

38--------------

43--------------

benchmarks/quasigroups/Main.idr+2−2

@@ -14,11 +14,11 @@ main = do

14 Left err => putStrLn err

15 Right (_ ** (board ** legal)) => do

16 putStrLn "Got board:"

17− print board

17+ printLn board

18 putStrLn "Solving..."

19 case fillBoard board legal of

20 Nothing => putStrLn "No solution found"

21 Just (solved ** _) => do

22 putStrLn "Solution found:"

23− print solved

23+ printLn solved

24 [self] => putStrLn ("Usage: " ++ self ++ " <board file>")

benchmarks/trivial/sortvec.idr+2−3

@@ -13,7 +13,7 @@ vsort [] = []

13vsort (x :: xs) = insert x (vsort xs)

14

15mkSortVec : (n : Nat) -> Eff m [RND] (Vect n Int)

16−mkSortVec Z = return []

16+mkSortVec Z = return []

17mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))

18

19main : IO ()

@@ -21,5 +21,4 @@ main = do (_ :: arg :: _) <- getArgs

21-- let arg = "2000"

22 let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))

23 putStrLn "Made vector"

24− print (vsort vec)

24+ printLn (vsort vec)

25−

contribs/lib/SQLite3/testunit.idr+14−14

@@ -7,12 +7,12 @@ testexpr = do db <- open_db "somedb.db"

7 let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (OR (AND (MkCond (Equals (VCol "data")(VStr "data0"))) (MkCond (Equals (VCol "num")(VInt 1))) ) (MkCond (Equals (VCol "num")(VInt 2))))))

8 let x = (fst sql) -- get the string

9 let list = (snd sql) -- list of vals

10− liftIO(print x) -- use liftIO to turn this into DB type

10+ liftIO(printLn x) -- use liftIO to turn this into DB type

11 stmt <- (prepare_db db x) -- prepare the statement

12 bindMulti stmt list -- bind the values in the list

13 exec_db_v2 stmt -- execute the prepared query

14 res <- toList_v1 db -- toList_v1 to get the result

15− liftIO(print res) -- print the result

15+ liftIO(printLn res) -- print the result

16 finalize_db stmt -- Statment pointer must be finalized in the end

17 close_db db -- close the datbase

18 return ()

@@ -22,7 +22,7 @@ testupdate = do db <- open_db "somedb.db"

22 let sql = (evalSQL [] (UPDATE (TBL ["tbl1"]) (WHERE (SET (MkCond (Equals(VCol "data") (VStr "data600"))) ) (MkCond (Equals (VCol "num") (VInt 2))) ) ))

23 let x = (fst sql)

24 let list = (snd sql)

25− liftIO(print x)

25+ liftIO(printLn x)

26 stmt <- (prepare_db db x)

27 bindMulti stmt list

28 exec_db_v2 stmt

@@ -35,7 +35,7 @@ testInsert = do db <- open_db "somedb.db"

35 let sql = (evalSQL [] (INSERT (TBL ["tbl1"]) [(VInt 3),(VStr "ham")]))

36 let x = (fst sql)

37 let list = (snd sql)

38− liftIO(print x)

38+ liftIO(printLn x)

39 stmt <- (prepare_db db x)

40 bindMulti stmt list

41 exec_db_v2 stmt

@@ -48,12 +48,12 @@ testNull = do db <- open_db "somedb.db"

48 let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (MkCond (MkNULL (VCol "data")))))

49 let x = (fst sql)

50 let list = (snd sql)

51− liftIO(print x)

51+ liftIO(printLn x)

52 stmt <- (prepare_db db x)

53 bindMulti stmt list

54 exec_db_v2 stmt

55 res <- toList_v1 db

56− liftIO(print res)

56+ liftIO(printLn res)

57 finalize_db stmt

58 close_db db

59 return ()

@@ -64,7 +64,7 @@ testInsertWithCond = do db <- open_db "somedb.db"

64 let sql = (evalSQL [] (INSERTC (TBL ["tbl1"]) [(VCol "data"),(VCol "num")] [(VInt 30),(VStr "inserthere")]))

65 let x = (fst sql)

66 let list = (snd sql)

67− liftIO(print x)

67+ liftIO(printLn x)

68 stmt <- (prepare_db db x)

69 bindMulti stmt list

70 exec_db_v2 stmt

@@ -78,12 +78,12 @@ testNestedSel1 = do db <- open_db "somedb.db"

78 let sql = (evalSQL [] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"]) (MkCond (MkGT (VCol "num")(VInt 2))))Empty))

79 let x = (fst sql)

80 let list = (snd sql)

81− liftIO(print x)

81+ liftIO(printLn x)

82 stmt <- (prepare_db db x)

83 bindMulti stmt list

84 exec_db_v2 stmt

85 res <- toList_v1 db

86− liftIO(print res)

86+ liftIO(printLn res)

87 finalize_db stmt

88 close_db db

89 return ()

@@ -94,7 +94,7 @@ testCreateTable = do db <- open_db "somedb.db"

94 let sql = (evalSQL [] (CREATE (TBL ["mynewtbl"]) [ ((VCol "col"),(CInt "int"),(None)) ] ) )

95 let x = (fst sql)

96 let list = (snd sql)

97− liftIO(print x)

97+ liftIO(printLn x)

98 stmt <- (prepare_db db x)

99 bindMulti stmt list

100 exec_db_v2 stmt

@@ -108,12 +108,12 @@ testMultiTable = do db <- open_db "somedb.db"

108 let sql = (evalSQL [] ((SELECT ALL )(TBL ["mytable","tbl1"]) (Empty) ) )

109 let x = (fst sql)

110 let list = (snd sql)

111− liftIO(print x)

111+ liftIO(printLn x)

112 stmt <- (prepare_db db x)

113 bindMulti stmt list

114 exec_db_v2 stmt

115 res <- toList_v1 db

116− liftIO(print res)

116+ liftIO(printLn res)

117 finalize_db stmt

118 close_db db

119 return ()

@@ -123,12 +123,12 @@ testSelAll = do db <- open_db "somedb.db"

123 let sql = (evalSQL [] ((SELECT ALL )(TBL ["tbl1"]) (Empty) ) )

124 let x = (fst sql)

125 let list = (snd sql)

126− liftIO(print x)

126+ liftIO(printLn x)

127 stmt <- (prepare_db db x)

128 bindMulti stmt list

129 exec_db_v2 stmt

130 res <- toList_v1 db

131− liftIO(print res)

131+ liftIO(printLn res)

132 finalize_db stmt

133 close_db db

134 return ()

libs/base/Data/Heap.idr+3−3

@@ -182,8 +182,8 @@ isEmptySizeZeroNodeAbsurd = proof {

182 does seem to work correctly!

183main : IO ()

184main = do

185− _ <- print $ main.sort [10, 3, 7, 2, 9, 1, 8, 0, 6, 4, 5]

185+ _ <- printLn $ main.sort [10, 3, 7, 2, 9, 1, 8, 0, 6, 4, 5]

186− _ <- print $ main.sort ["orange", "apple", "pear", "lime", "durian"]

186+ _ <- printLn $ main.sort ["orange", "apple", "pear", "lime", "durian"]

187− _ <- print $ main.sort [("jim", 19, "cs"), ("alice", 20, "english"), ("bob", 50, "engineering")]

187+ _ <- printLn $ main.sort [("jim", 19, "cs"), ("alice", 20, "english"), ("bob", 50, "engineering")]

188 return ()

189-}

libs/effects/Effect/Exception.idr+3−4

@@ -4,7 +4,7 @@ import Effects

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

8 Raise : a -> { () } Exception a b

9

10instance Handler (Exception a) Maybe where

@@ -14,7 +14,7 @@ instance Handler (Exception a) List where

14 handle _ (Raise e) k = []

15

16instance Show a => Handler (Exception a) IO where

17− handle _ (Raise e) k = do print e

17+ handle _ (Raise e) k = do printLn e

18 believe_me (exit 1)

19

20instance Handler (Exception a) (IOExcept a) where

@@ -26,7 +26,7 @@ instance Handler (Exception a) (Either a) where

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

29−raise : a -> { [EXCEPTION a ] } Eff b

29+raise : a -> { [EXCEPTION a ] } Eff b

30raise err = call $ Raise err

31

32

@@ -39,4 +39,3 @@ raise err = call $ Raise err

39

40-- possibly add a 'handle' to the Eff language so that an alternative

41-- handler can be introduced mid interpretation?

42−

libs/effects/Effect/StdIO.idr+7−3

@@ -42,13 +42,17 @@ STDIO = MkEff () StdIO

42putStr : String -> { [STDIO] } Eff ()

43putStr s = call $ PutStr s

44

45+||| Write a string to standard output, terminating with a newline.

46+putStrLn : String -> { [STDIO] } Eff ()

47+putStrLn s = putStr (s ++ "\n")

48+

45||| Write a character to standard output.

49||| Write a character to standard output.

46putChar : Char -> { [STDIO] } Eff ()

50putChar : Char -> { [STDIO] } Eff ()

47putChar c = call $ PutCh c

51putChar c = call $ PutCh c

48

52

49−||| Write a string to standard output, terminating with a newline.

53+||| Write a character to standard output, terminating with a newline.

50−putStrLn : String -> { [STDIO] } Eff ()

54+putCharLn : Char -> { [STDIO] } Eff ()

51−putStrLn s = putStr (s ++ "\n")

55+putCharLn c = putStrLn (singleton c)

52

56

53||| Read a string from standard input.

57||| Read a string from standard input.

54getStr : { [STDIO] } Eff String

58getStr : { [STDIO] } Eff String

libs/oldeffects/Effect/Exception.idr+3−4

@@ -4,7 +4,7 @@ import Effects

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

8 Raise : a -> { () } Exception a b

9

10instance Handler (Exception a) Maybe where

@@ -14,7 +14,7 @@ instance Handler (Exception a) List where

14 handle _ (Raise e) k = []

15

16instance Show a => Handler (Exception a) IO where

17− handle _ (Raise e) k = do print e

17+ handle _ (Raise e) k = do printLn e

18 believe_me (exit 1)

19

20instance Handler (Exception a) (IOExcept a) where

@@ -26,7 +26,7 @@ instance Handler (Exception a) (Either a) where

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

29−raise : a -> { [EXCEPTION a ] } Eff m b

29+raise : a -> { [EXCEPTION a ] } Eff m b

30raise err = call $ Raise err

31

32

@@ -39,4 +39,3 @@ raise err = call $ Raise err

39

40-- possibly add a 'handle' to the Eff language so that an alternative

41-- handler can be introduced mid interpretation?

42−

libs/prelude/Prelude.idr+15−5

@@ -442,20 +442,30 @@ putStr x = do prim_write x

442putStrLn : String -> IO' ffi ()

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

444

445−||| Output something showable to stdout, with a trailing newline

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

446partial

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

448+print x = putStr (show x)

449+

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

451+partial

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

448−print x = putStrLn (show x)

453+printLn x = putStrLn (show x)

449

454

450||| Read one line of input from stdin

455||| Read one line of input from stdin

451partial

456partial

452getLine : IO' ffi String

457getLine : IO' ffi String

453−getLine = prim_read

458+getLine = prim_read

454

459

455||| Write a single character to stdout

460||| Write a single character to stdout

456partial

461partial

457putChar : Char -> IO ()

462putChar : Char -> IO ()

458−putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)

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

464+

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

466+partial

467+putCharLn : Char -> IO ()

468+putCharLn c = putStrLn (singleton c)

459

469

460||| Read a single character from stdin

470||| Read a single character from stdin

461partial

471partial

@@ -484,7 +494,7 @@ stderr = FHandle prim__stderr

484do_fopen : String -> String -> IO Ptr

494do_fopen : String -> String -> IO Ptr

485do_fopen f m

495do_fopen f m

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

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

487−

497+

488||| Open a file

498||| Open a file

489||| @ f the filename

499||| @ f the filename

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

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

samples/binary.idr+1−2

@@ -41,7 +41,7 @@ adc (numx # bx) (numy # by) carry

41main : IO ()

42main = do let n1 = zero # b1 # b0 # b1 # b0

43 let n2 = zero # b1 # b1 # b1 # b0

44− print (adc n1 n2 b0)

44+ printLn (adc n1 n2 b0)

45

46

47

@@ -92,4 +92,3 @@ main.adc_lemma_1 = proof {

92 rewrite sym (plusZeroRightNeutral c) ;

93 trivial;

94}

95−

samples/interp-alt.idr+2−2

@@ -77,5 +77,5 @@ testFac : Int

77testFac = interp [] eFac 4

78

79main : IO ()

80−main = do print test

80+main = do printLn test

81− print testFac

81+ printLn testFac

samples/interp.idr+1−2

@@ -88,5 +88,4 @@ testFac : Int

88testFac = interp [] eFac 4

89

90main : IO ()

91−main = print testFac

91+main = printLn testFac

92−

samples/javaffi.idr+1−1

@@ -9,4 +9,4 @@ binom n k = mkForeign (FFun "IntMath.binomial" [FInt, FInt] FInt) n k

9main : IO ()

10main = do print "The number of possibilities in lotto is 49 choose 6:"

11 res <- binom 49 6

12− print res

12+ printLn res

test/basic002/test006.idr+1−1

@@ -18,7 +18,7 @@ natToBin k with (parity k)

18 natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

19

20main : IO ()

21−main = do print (natToBin 42)

21+main = do printLn (natToBin 42)

22

23---------- Proofs ----------

24

test/basic003/test027.idr+3−3

@@ -19,7 +19,7 @@ using (Ord a, Num n)

19 mprod (x :: xs) = x * mprod xs

20

21main : IO ()

22−main = do print $ isort [1,5,3,5,1,9,8]

22+main = do printLn $ isort [1,5,3,5,1,9,8]

23− print $ msum [1..10]

23+ printLn $ msum [1..10]

24− print $ mprod [1..10]

24+ printLn $ mprod [1..10]

25

test/basic004/test016.idr+1−1

@@ -13,5 +13,5 @@ take (S n) (x :: xs) = x :: take n xs

13take n [] = []

14

15main : IO ()

16−main = do print (take 10 (Main.countFrom 10))

16+main = do printLn (take 10 (Main.countFrom 10))

17

test/basic005/test019.lidr+1−1

@@ -14,5 +14,5 @@

14> | False = ifFalse x

15

16> main : IO ()

17−> main = print (test ((S 4) ==) 5 Oh)

17+> main = printLn (test ((S 4) ==) 5 Oh)

18

test/basic006/test020.idr+2−2

@@ -21,7 +21,7 @@ test : Integer -> String

21test x = "Number " ++ x

22

23main : IO ()

24−main = do print (foo [1,2,3])

24+main = do printLn (foo [1,2,3])

25− print (test 42)

25+ printLn (test 42)

26

27

test/basic006/test020a.idr+1−1

@@ -16,5 +16,5 @@ foo : Vect n a -> List a

16foo xs = reverse xs

17

18main : IO ()

19−main = print (foo [1,2,3])

19+main = printLn (foo [1,2,3])

20

test/basic007/test033.idr+1−1

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

1module Main

2

3main : IO ()

4−main = nullPtr null >>= print

4+main = nullPtr null >>= printLn

test/basic011/basic011.idr+10−10

@@ -3,14 +3,14 @@ module Main

3import Data.Hash

4

5main : IO ()

6−main = do print $ hash (the Bits8 3)

6+main = do printLn $ hash (the Bits8 3)

7− print $ hash (the (List Bits8) [3])

7+ printLn $ hash (the (List Bits8) [3])

8− print $ hash "hello world"

8+ printLn $ hash "hello world"

9− print $ hash 'a'

9+ printLn $ hash 'a'

10− print $ hash (the Bits8 3)

10+ printLn $ hash (the Bits8 3)

11− print $ hash (the Bits16 3)

11+ printLn $ hash (the Bits16 3)

12− print $ hash (the Bits32 3)

12+ printLn $ hash (the Bits32 3)

13− print $ hash (the Bits64 3)

13+ printLn $ hash (the Bits64 3)

14− print $ hash (the Int 3)

14+ printLn $ hash (the Int 3)

15− print $ hash (the Integer 3)

15+ printLn $ hash (the Integer 3)

16

test/basic012/basic012.idr+4−4

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

1import Data.Vect

2import Control.Monad.State

3import Control.Monad.Identity

4−

4+

5VThing : Type

6VThing = {n : Nat} -> Vect n Int -> Int

7

@@ -31,7 +31,7 @@ testfoo3 xs = foo 42 xs (bar 10)

31AnyST : Type -> Type -> Type

32AnyST s a = {m : _} -> Monad m => StateT s m a

33

34−foost: AnyST Int ()

34+foost : AnyST Int ()

35foost = do x <- get

36 put x

37

@@ -52,11 +52,11 @@ tupleId f (a, b) = (f a, f b)

52

53AppendType : Type

54AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55−

55+

56append : AppendType

57append [] ys = ys

58append (x :: xs) ys = x :: append xs ys

59

60main : IO ()

61main = do putStrLn (baz 42)

62− print (append [1,2,3] [4,5,6])

62+ printLn (append [1,2,3] [4,5,6])

test/dsl001/test001.idr+2−2

@@ -96,8 +96,8 @@ testEnv : Int -> Env [TyInt,TyInt]

96testEnv x = [x,x]

97

98main : IO ()

99−main = do { print testFac

99+main = do { printLn testFac

100− print test }

100+ printLn test }

101

102

103

test/effects002/test025.idr+1−1

@@ -30,6 +30,6 @@ testMemory = do Src :- allocate 5

30

31main : IO ()

32main = ioe_run (runInit [Dst := (), Src := ()] testMemory)

33− (\err => print err) (\ok => print ok)

33+ (\err => printLn err) (\ok => printLn ok)

34

35

test/io002/test008.idr+1−1

@@ -22,7 +22,7 @@ main = do (a, b) <- ioVals

22 let x = "bar"

23 putStrLn (show (getVal x 7 testlist))

24 let ((y, z) :: _) = testlist

25− print z

25+ printLn z

26 case lookup x testlist of

27 Just v => putStrLn (show v)

28 Nothing => putStrLn "Not there!"

test/io003/test018a.idr+1−1

@@ -27,7 +27,7 @@ mainProc = do mainID <- myID

27

28repeatIO : Int -> IO ()

29repeatIO 0 = return ()

30−repeatIO n = do print n

30+repeatIO n = do printLn n

31 run mainProc

32 repeatIO (n - 1)

33

test/primitives001/test005.idr+6−6

@@ -7,9 +7,9 @@ tlist : List Int

7tlist = [1, 2, 3, 4, 5]

8

9main : IO ()

10−main = do print (abs (-8))

10+main = do printLn (abs (-8))

11− print (abs (S Z))

11+ printLn (abs (S Z))

12− print (span isAlpha tstr)

12+ printLn (span isAlpha tstr)

13− print (break isDigit tstr)

13+ printLn (break isDigit tstr)

14− print (span (\x => x < 3) tlist)

14+ printLn (span (\x => x < 3) tlist)

15− print (break (\x => x > 2) tlist)

15+ printLn (break (\x => x > 2) tlist)

test/proof003/test015.idr+3−3

@@ -72,10 +72,10 @@ readNum = do putStr "Enter a number:"

72

73main : IO ()

74main = do let Just bin1 = natToBin 8 42

75− print bin1

75+ printLn bin1

76 let Just bin2 = natToBin 8 89

77− print bin2

77+ printLn bin2

78− print (adc bin1 bin2 b0)

78+ printLn (adc bin1 bin2 b0)

79

80

81

test/records001/test011.idr+5−5

@@ -20,9 +20,9 @@ person = MkPerson "Fred" 30

20main : IO ()

21main = do let x = record { name = "foo",

22 more_things = reverse ["a","b"] } testFoo

23− print $ name x

23+ printLn $ name x

24− print $ name person

24+ printLn $ name person

25− print $ things x

25+ printLn $ things x

26− print $ more_things x

26+ printLn $ more_things x

27− print $ age (record { age = 25 } person)

27+ printLn $ age (record { age = 25 } person)

28

test/records003/records003.idr+6−6

@@ -38,10 +38,10 @@ test : Meeting 2015

38test = next_year idm_gbg

39

40main : IO ()

41−main = do print (record { event->organiser->name } test)

41+main = do printLn (record { event->organiser->name } test)

42− print (record { event->organiser->age } test)

42+ printLn (record { event->organiser->age } test)

43− print (record { event->organiser->age } idm_gbg)

43+ printLn (record { event->organiser->age } idm_gbg)

44− print (record { organiser->age } test)

44+ printLn (record { organiser->age } test)

45− print (record { organiser->age } idm_gbg)

45+ printLn (record { organiser->age } idm_gbg)

46− print (record { year } idm_gbg)

46+ printLn (record { year } idm_gbg)

47

test/reg002/reg012.idr+1−1

@@ -30,4 +30,4 @@ swap (x :: Nil) = x :: Nil

30swap (x :: y :: xs) = (y :: x :: (swap xs))

31

32main : IO ()

33−main = print (swap [1,2,3,4,5])

33+main = printLn (swap [1,2,3,4,5])

test/reg004/reg004.idr+1−1

@@ -13,4 +13,4 @@ h True = r2 where

13 r2 = r

14

15main : IO ()

16−main = do print (h True); print (h False)

16+main = do printLn (h True); printLn (h False)

test/reg013/reg013.idr+3−3

@@ -2,7 +2,7 @@ module Main

2

3main : IO ()

4main = do

5− print $ prim_lenString "hallo"

5+ printLn $ prim_lenString "hallo"

6− print $ prim_lenString "1"

6+ printLn $ prim_lenString "1"

7− print $ prim_lenString ""

7+ printLn $ prim_lenString ""

8

test/reg016/reg016.idr+6−6

@@ -1,11 +1,11 @@

1module Main

2

3main : IO ()

4−main = do print $ the Integer 429496729500000000000000

4+main = do printLn $ the Integer 429496729500000000000000

5−-- print $ the Integer 4294967296

5+-- printLn $ the Integer 4294967296

6−-- print $ the Integer 4294967297

6+-- printLn $ the Integer 4294967297

7−-- print $ the Int 4294967295

7+-- printLn $ the Int 4294967295

8−-- print $ the Int 4294967296

8+-- printLn $ the Int 4294967296

9−-- print $ the Int 4294967297

9+-- printLn $ the Int 4294967297

10

11

test/reg017/reg017.idr+1−1

@@ -10,4 +10,4 @@ foo : { t : Type } ->

10foo {t} a {prfA = p} b c {prfBC} = b

11

12main : IO ()

13−main = print $ foo 3 4 4

13+main = printLn $ foo 3 4 4

test/reg018/reg018d.idr+1−1

@@ -12,4 +12,4 @@ pull {n=S _} (FS n) (x :: xs) =

12 (v, x::vs)

13

14main : IO ()

15−main = print (pull FZ [0, 1, 2])

15+main = printLn (pull FZ [0, 1, 2])

test/reg027/reg027.idr+1−1

@@ -27,6 +27,6 @@ foo = do val <- dbl

27 \x => show val

28

29main : IO ()

30−main = do print dbl

30+main = do printLn dbl

31 putStrLn (foo 3)

32

test/reg029/reg029.idr+2−2

@@ -7,5 +7,5 @@ import System

7

8main : IO ()

9main = do

10− print !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

10+ printLn !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11− print !(getEnv "IDRIS_REG029_EXISTENT_VAR")

11+ printLn !(getEnv "IDRIS_REG029_EXISTENT_VAR")

test/reg031/reg031.idr+1−1

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

1module Main

2

3main : IO ()

4−main = print . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

4+main = printLn . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

5 where

6 -- make the values positive if the backend has signed chars

7 val : Char -> Int

test/reg040/reg040.idr+1−1

@@ -4,4 +4,4 @@ io : IO Int

4io = return 42

5

6main : IO ()

7−main = print $ unsafePerformIO io

7+main = printLn $ unsafePerformIO io

test/reg042/reg042.idr+1−1

@@ -21,4 +21,4 @@ g (C x y z) = x + y

21-- Here, we'd apply the not-a-function to the erased argument 4,

22-- which would make the program go wrong.

23main : IO ()

24−main = print $ g (proj 3 f 4)

24+main = printLn $ g (proj 3 f 4)

test/reg045/reg045.idr+1−1

@@ -15,5 +15,5 @@ foo : ListZ Nat

15foo = (1 :: 2 :: 3 :: Nil)

16

17main : IO ()

18−main = print foo

18+main = printLn foo

19

test/reg052/reg052.idr+1−1

@@ -5,4 +5,4 @@ impure_int : IO Int

5impure_int = return 41

6

7main : IO ()

8−main = impure_int >>= impure_op . prim__zextInt_B64 >>= print

8+main = impure_int >>= impure_op . prim__zextInt_B64 >>= printLn

test/sourceLocation001/SourceLoc.idr+4−4

@@ -36,7 +36,7 @@ using (ctxt : Vect n Ty)

36 Var : (i : Fin n) -> Tm ctxt (index i ctxt)

37 Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

38 App : Tm ctxt (Arr t t') -> Tm ctxt t -> Tm ctxt t'

39− ||| A term that makes the program halt and print where it halted

39+ ||| A term that makes the program halt and printLn where it halted

40 Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

41

42 data Env : Vect n Ty -> Type where

@@ -83,11 +83,11 @@ testTerm4 = App testTerm3 MkU

83namespace Main

84 main : IO ()

85 main = do putStrLn "Testing using definition"

86− print fromRHS

86+ printLn fromRHS

87 putStrLn "Testing using inline tactics"

88− print fromProofScript

88+ printLn fromProofScript

89 putStrLn "Testing using metavariable with later definition"

90− print fromMetavar

90+ printLn fromMetavar

91 putStrLn "-----------------------"

92 sequence_ $ with List [ exec testTerm1

93 , exec testTerm2

test/sugar001/test007.idr+4−4

@@ -35,7 +35,7 @@ runEval env e with (eval e) {

35}

36

37main : IO ()

38−main = do print [| (\x => x *2) (Just 4) |]

38+main = do printLn [| (\x => x *2) (Just 4) |]

39− print [| plus (Just 4) (Just 5) |]

39+ printLn [| plus (Just 4) (Just 5) |]

40− print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

40+ printLn (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41− print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41+ printLn (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

test/sugar004/sugar004.idr+1−1

@@ -9,7 +9,7 @@ foo x = let Just x' = x | Nothing => 100 in x'

9main : IO ()

10main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"

11 | (x :: y :: _) => putStrLn "Too many arguments!"

12− print (foo (Just (cast a)))

12+ printLn (foo (Just (cast a)))

13

14{-

15

test/sugar005/As.idr+9−9

@@ -24,13 +24,13 @@ same _ _ = Nothing

24

25namespace Main

26 main : IO ()

27− main = do print $ isS 0

27+ main = do printLn $ isS 0

28− print $ isS 1

28+ printLn $ isS 1

29− print $ hasS [0,0,0]

29+ printLn $ hasS [0,0,0]

30− print $ hasS [0,1,2]

30+ printLn $ hasS [0,1,2]

31− print $ isSS 5

31+ printLn $ isSS 5

32− print $ isSS 0

32+ printLn $ isSS 0

33− print $ same 1 1

33+ printLn $ same 1 1

34− print $ same 0 0

34+ printLn $ same 0 0

35− print $ same 1 0

35+ printLn $ same 1 0

36

test/totality004/totality004.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

21countStream x = x :: countStream (x + 1)

22

23main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

25

test/totality004/totality004a.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

21countStream x = x :: countStream (x + 1)

22

23main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

25

test/totality005/totality005.idr+1−1

@@ -7,4 +7,4 @@ fib : Stream Nat

7fib = 0 :: zipWithS (+) fib (1 :: fib)

8

9partial main : IO ()

10−main = print (take 15 fib)

10+main = printLn (take 15 fib)

test/tutorial002/tutorial002.idr+1−1

@@ -34,7 +34,7 @@ intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

34main : IO ()

35main = do putStr "Enter a number: "

36 x <- getLine

37− print (natToBin (fromInteger (cast x)))

37+ printLn (natToBin (fromInteger (cast x)))

38

39---------- Proofs ----------

40