5ea6aa0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Address semantic differences in putting things to STDOUT.

The changes are as follows: + `print` is for putting showable things to STDOUT. + `printLn` is for putting showable things to STDOUT with a new line + `putCharLn` for putting a single character to STDOUT, with a new line. Effects has been updated accordingly.

commit5ea6aa0520ae9927d2467a4553e8c64a4a4ca17c authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateThu 5 Mar 2015, 20:08 (12 years ago) parentb56f5c1

48 files changed+144−135

compare with master

unifiedsplit

benchmarks/quasigroups/Main.idr+2−2 benchmarks/trivial/sortvec.idr+2−3 contribs/lib/SQLite3/testunit.idr+14−14 libs/base/Data/Heap.idr+3−3 libs/effects/Effect/Exception.idr+3−4 libs/effects/Effect/StdIO.idr+7−3 libs/oldeffects/Effect/Exception.idr+3−4 libs/prelude/Prelude.idr+15−5 samples/binary.idr+1−2 samples/interp-alt.idr+2−2 samples/interp.idr+1−2 samples/javaffi.idr+1−1 test/basic002/test006.idr+1−1 test/basic003/test027.idr+3−3 test/basic004/test016.idr+1−1 test/basic005/test019.lidr+1−1 test/basic006/test020.idr+2−2 test/basic006/test020a.idr+1−1 test/basic011/basic011.idr+10−10 test/basic012/basic012.idr+4−4 test/dsl001/test001.idr+2−2 test/effects002/test025.idr+1−1 test/io002/test008.idr+1−1 test/io003/test018a.idr+1−1 test/primitives001/test005.idr+6−6 test/proof003/test015.idr+3−3 test/records001/test011.idr+5−5 test/records003/records003.idr+6−6 test/reg002/reg012.idr+1−1 test/reg004/reg004.idr+1−1 test/reg013/reg013.idr+3−3 test/reg016/reg016.idr+6−6 test/reg017/reg017.idr+1−1 test/reg018/reg018d.idr+1−1 test/reg027/reg027.idr+1−1 test/reg029/reg029.idr+2−2 test/reg031/reg031.idr+1−1 test/reg040/reg040.idr+1−1 test/reg042/reg042.idr+1−1 test/reg045/reg045.idr+1−1 test/sourceLocation001/SourceLoc.idr+4−4 test/sugar001/test007.idr+4−4 test/sugar004/sugar004.idr+1−1 test/sugar005/As.idr+9−9 test/totality004/totality004.idr+1−1 test/totality004/totality004a.idr+1−1 test/totality005/totality005.idr+1−1 test/tutorial002/tutorial002.idr+1−1

benchmarks/quasigroups/Main.idr+2−2

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

1414 Left err => putStrLn err

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

1616 putStrLn "Got board:"

17− print board

17+ printLn board

1818 putStrLn "Solving..."

1919 case fillBoard board legal of

2020 Nothing => putStrLn "No solution found"

2121 Just (solved ** _) => do

2222 putStrLn "Solution found:"

23− print solved

23+ printLn solved

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

benchmarks/trivial/sortvec.idr+2−3

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

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

1414

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

16−mkSortVec Z = return []

16+mkSortVec Z = return []

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

1818

1919main : IO ()

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

2121-- let arg = "2000"

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

2323 putStrLn "Made vector"

24− print (vsort vec)

25−

24+ printLn (vsort vec)

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

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

77 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))))))

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

99 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

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

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

1313 exec_db_v2 stmt -- execute the prepared query

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

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

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

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

1717 close_db db -- close the datbase

1818 return ()

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

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

2323 let x = (fst sql)

2424 let list = (snd sql)

25− liftIO(print x)

25+ liftIO(printLn x)

2626 stmt <- (prepare_db db x)

2727 bindMulti stmt list

2828 exec_db_v2 stmt

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

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

3636 let x = (fst sql)

3737 let list = (snd sql)

38− liftIO(print x)

38+ liftIO(printLn x)

3939 stmt <- (prepare_db db x)

4040 bindMulti stmt list

4141 exec_db_v2 stmt

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

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

4949 let x = (fst sql)

5050 let list = (snd sql)

51− liftIO(print x)

51+ liftIO(printLn x)

5252 stmt <- (prepare_db db x)

5353 bindMulti stmt list

5454 exec_db_v2 stmt

5555 res <- toList_v1 db

56− liftIO(print res)

56+ liftIO(printLn res)

5757 finalize_db stmt

5858 close_db db

5959 return ()

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

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

6565 let x = (fst sql)

6666 let list = (snd sql)

67− liftIO(print x)

67+ liftIO(printLn x)

6868 stmt <- (prepare_db db x)

6969 bindMulti stmt list

7070 exec_db_v2 stmt

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

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

7979 let x = (fst sql)

8080 let list = (snd sql)

81− liftIO(print x)

81+ liftIO(printLn x)

8282 stmt <- (prepare_db db x)

8383 bindMulti stmt list

8484 exec_db_v2 stmt

8585 res <- toList_v1 db

86− liftIO(print res)

86+ liftIO(printLn res)

8787 finalize_db stmt

8888 close_db db

8989 return ()

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

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

9595 let x = (fst sql)

9696 let list = (snd sql)

97− liftIO(print x)

97+ liftIO(printLn x)

9898 stmt <- (prepare_db db x)

9999 bindMulti stmt list

100100 exec_db_v2 stmt

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

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

109109 let x = (fst sql)

110110 let list = (snd sql)

111− liftIO(print x)

111+ liftIO(printLn x)

112112 stmt <- (prepare_db db x)

113113 bindMulti stmt list

114114 exec_db_v2 stmt

115115 res <- toList_v1 db

116− liftIO(print res)

116+ liftIO(printLn res)

117117 finalize_db stmt

118118 close_db db

119119 return ()

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

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

124124 let x = (fst sql)

125125 let list = (snd sql)

126− liftIO(print x)

126+ liftIO(printLn x)

127127 stmt <- (prepare_db db x)

128128 bindMulti stmt list

129129 exec_db_v2 stmt

130130 res <- toList_v1 db

131− liftIO(print res)

131+ liftIO(printLn res)

132132 finalize_db stmt

133133 close_db db

134134 return ()

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

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

182182 does seem to work correctly!

183183main : IO ()

184184main = do

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

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

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

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

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

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

188188 return ()

189189-}

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

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

44import System

55import Control.IOExcept

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

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

1010instance Handler (Exception a) Maybe where

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

1414 handle _ (Raise e) k = []

1515

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

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

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

1818 believe_me (exit 1)

1919

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

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

2626EXCEPTION : Type -> EFFECT

2727EXCEPTION t = MkEff () (Exception t)

2828

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

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

3030raise err = call $ Raise err

3131

3232

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

3939

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

4141-- handler can be introduced mid interpretation?

42−

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

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

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

4343putStr s = call $ PutStr s

4444

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

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

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

48+

4549||| Write a character to standard output.

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

4751putChar c = call $ PutCh c

4852

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

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

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

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

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

55+putCharLn c = putStrLn (singleton c)

5256

5357||| Read a string from standard input.

5458getStr : { [STDIO] } Eff String

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

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

44import System

55import Control.IOExcept

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

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

1010instance Handler (Exception a) Maybe where

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

1414 handle _ (Raise e) k = []

1515

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

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

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

1818 believe_me (exit 1)

1919

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

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

2626EXCEPTION : Type -> EFFECT

2727EXCEPTION t = MkEff () (Exception t)

2828

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

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

3030raise err = call $ Raise err

3131

3232

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

3939

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

4141-- handler can be introduced mid interpretation?

42−

libs/prelude/Prelude.idr+15−5

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

442442putStrLn : String -> IO' ffi ()

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

444444

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

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

446446partial

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

448−print x = putStrLn (show x)

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 ()

453+printLn x = putStrLn (show x)

449454

450455||| Read one line of input from stdin

451456partial

452457getLine : IO' ffi String

453−getLine = prim_read

458+getLine = prim_read

454459

455460||| Write a single character to stdout

456461partial

457462putChar : 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)

459469

460470||| Read a single character from stdin

461471partial

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

484494do_fopen : String -> String -> IO Ptr

485495do_fopen f m

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

487−

497+

488498||| Open a file

489499||| @ f the filename

490500||| @ 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

4141main : IO ()

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

4343 let n2 = zero # b1 # b1 # b1 # b0

44− print (adc n1 n2 b0)

44+ printLn (adc n1 n2 b0)

4545

4646

4747

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

9292 rewrite sym (plusZeroRightNeutral c) ;

9393 trivial;

9494}

95−

samples/interp-alt.idr+2−2

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

7777testFac = interp [] eFac 4

7878

7979main : IO ()

80−main = do print test

81− print testFac

80+main = do printLn test

81+ printLn testFac

samples/interp.idr+1−2

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

8888testFac = interp [] eFac 4

8989

9090main : IO ()

91−main = print testFac

92−

91+main = printLn testFac

samples/javaffi.idr+1−1

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

99main : IO ()

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

1111 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)

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

1919

2020main : IO ()

21−main = do print (natToBin 42)

21+main = do printLn (natToBin 42)

2222

2323---------- Proofs ----------

2424

test/basic003/test027.idr+3−3

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

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

2020

2121main : IO ()

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

23− print $ msum [1..10]

24− print $ mprod [1..10]

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

23+ printLn $ msum [1..10]

24+ printLn $ mprod [1..10]

2525

test/basic004/test016.idr+1−1

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

1313take n [] = []

1414

1515main : IO ()

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

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

1717

test/basic005/test019.lidr+1−1

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

1414> | False = ifFalse x

1515

1616> main : IO ()

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

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

1818

test/basic006/test020.idr+2−2

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

2121test x = "Number " ++ x

2222

2323main : IO ()

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

25− print (test 42)

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

25+ printLn (test 42)

2626

2727

test/basic006/test020a.idr+1−1

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

1616foo xs = reverse xs

1717

1818main : IO ()

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

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

2020

test/basic011/basic011.idr+10−10

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

33import Data.Hash

55main : IO ()

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

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

8− print $ hash "hello world"

9− print $ hash 'a'

10− print $ hash (the Bits8 3)

11− print $ hash (the Bits16 3)

12− print $ hash (the Bits32 3)

13− print $ hash (the Bits64 3)

14− print $ hash (the Int 3)

15− print $ hash (the Integer 3)

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

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

8+ printLn $ hash "hello world"

9+ printLn $ hash 'a'

10+ printLn $ hash (the Bits8 3)

11+ printLn $ hash (the Bits16 3)

12+ printLn $ hash (the Bits32 3)

13+ printLn $ hash (the Bits64 3)

14+ printLn $ hash (the Int 3)

15+ printLn $ hash (the Integer 3)

1616

test/basic012/basic012.idr+4−4

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

11import Data.Vect

22import Control.Monad.State

33import Control.Monad.Identity

4−

55VThing : Type

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

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

3131AnyST : Type -> Type -> Type

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

3333

34−foost: AnyST Int ()

34+foost : AnyST Int ()

3535foost = do x <- get

3636 put x

3737

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

5252

5353AppendType : Type

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

55−

55+

5656append : AppendType

5757append [] ys = ys

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

5959

6060main : IO ()

6161main = 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]

9696testEnv x = [x,x]

9797

9898main : IO ()

99−main = do { print testFac

100− print test }

99+main = do { printLn testFac

100+ printLn test }

101101

102102

103103

test/effects002/test025.idr+1−1

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

3030

3131main : IO ()

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

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

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

3434

3535

test/io002/test008.idr+1−1

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

2222 let x = "bar"

2323 putStrLn (show (getVal x 7 testlist))

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

25− print z

25+ printLn z

2626 case lookup x testlist of

2727 Just v => putStrLn (show v)

2828 Nothing => putStrLn "Not there!"

test/io003/test018a.idr+1−1

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

2727

2828repeatIO : Int -> IO ()

2929repeatIO 0 = return ()

30−repeatIO n = do print n

30+repeatIO n = do printLn n

3131 run mainProc

3232 repeatIO (n - 1)

3333

test/primitives001/test005.idr+6−6

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

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

99main : IO ()

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

11− print (abs (S Z))

12− print (span isAlpha tstr)

13− print (break isDigit tstr)

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

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

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

11+ printLn (abs (S Z))

12+ printLn (span isAlpha tstr)

13+ printLn (break isDigit tstr)

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

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

test/proof003/test015.idr+3−3

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

7272

7373main : IO ()

7474main = do let Just bin1 = natToBin 8 42

75− print bin1

75+ printLn bin1

7676 let Just bin2 = natToBin 8 89

77− print bin2

78− print (adc bin1 bin2 b0)

77+ printLn bin2

78+ printLn (adc bin1 bin2 b0)

7979

8080

8181

test/records001/test011.idr+5−5

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

2020main : IO ()

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

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

23− print $ name x

24− print $ name person

25− print $ things x

26− print $ more_things x

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

23+ printLn $ name x

24+ printLn $ name person

25+ printLn $ things x

26+ printLn $ more_things x

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

2828

test/records003/records003.idr+6−6

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

3838test = next_year idm_gbg

3939

4040main : IO ()

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

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

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

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

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

46− print (record { year } idm_gbg)

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

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

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

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

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

46+ printLn (record { year } idm_gbg)

4747

test/reg002/reg012.idr+1−1

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

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

3131

3232main : 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

1313 r2 = r

1414

1515main : 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

33main : IO ()

44main = do

5− print $ prim_lenString "hallo"

6− print $ prim_lenString "1"

7− print $ prim_lenString ""

5+ printLn $ prim_lenString "hallo"

6+ printLn $ prim_lenString "1"

7+ printLn $ prim_lenString ""

test/reg016/reg016.idr+6−6

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

11module Main

33main : IO ()

4−main = do print $ the Integer 429496729500000000000000

5−-- print $ the Integer 4294967296

6−-- print $ the Integer 4294967297

7−-- print $ the Int 4294967295

8−-- print $ the Int 4294967296

9−-- print $ the Int 4294967297

4+main = do printLn $ the Integer 429496729500000000000000

5+-- printLn $ the Integer 4294967296

6+-- printLn $ the Integer 4294967297

7+-- printLn $ the Int 4294967295

8+-- printLn $ the Int 4294967296

9+-- printLn $ the Int 4294967297

1010

1111

test/reg017/reg017.idr+1−1

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

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

1111

1212main : 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) =

1212 (v, x::vs)

1313

1414main : 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

2727 \x => show val

2828

2929main : IO ()

30−main = do print dbl

30+main = do printLn dbl

3131 putStrLn (foo 3)

3232

test/reg029/reg029.idr+2−2

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

88main : IO ()

99main = do

10− print !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11− print !(getEnv "IDRIS_REG029_EXISTENT_VAR")

10+ printLn !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11+ printLn !(getEnv "IDRIS_REG029_EXISTENT_VAR")

test/reg031/reg031.idr+1−1

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

11module Main

33main : 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"

55 where

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

77 val : Char -> Int

test/reg040/reg040.idr+1−1

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

44io = return 42

66main : 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

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

2222-- which would make the program go wrong.

2323main : 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

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

1616

1717main : IO ()

18−main = print foo

18+main = printLn foo

1919

test/sourceLocation001/SourceLoc.idr+4−4

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

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

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

3838 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

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

4141

4242 data Env : Vect n Ty -> Type where

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

8383namespace Main

8484 main : IO ()

8585 main = do putStrLn "Testing using definition"

86− print fromRHS

86+ printLn fromRHS

8787 putStrLn "Testing using inline tactics"

88− print fromProofScript

88+ printLn fromProofScript

8989 putStrLn "Testing using metavariable with later definition"

90− print fromMetavar

90+ printLn fromMetavar

9191 putStrLn "-----------------------"

9292 sequence_ $ with List [ exec testTerm1

9393 , exec testTerm2

test/sugar001/test007.idr+4−4

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

3535}

3636

3737main : IO ()

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

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

40− print (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"))))

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

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

40+ printLn (runEval [("x",21), ("y", 20)] (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'

99main : IO ()

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

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

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

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

1313

1414{-

1515

test/sugar005/As.idr+9−9

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

2424

2525namespace Main

2626 main : IO ()

27− main = do print $ isS 0

28− print $ isS 1

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

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

31− print $ isSS 5

32− print $ isSS 0

33− print $ same 1 1

34− print $ same 0 0

35− print $ same 1 0

27+ main = do printLn $ isS 0

28+ printLn $ isS 1

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

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

31+ printLn $ isSS 5

32+ printLn $ isSS 0

33+ printLn $ same 1 1

34+ printLn $ same 0 0

35+ printLn $ same 1 0

3636

test/totality004/totality004.idr+1−1

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

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

2222

2323main : IO ()

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

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

2525

test/totality004/totality004a.idr+1−1

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

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

2222

2323main : IO ()

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

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

2525

test/totality005/totality005.idr+1−1

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

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

99partial 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

3434main : IO ()

3535main = do putStr "Enter a number: "

3636 x <- getLine

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

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

3838

3939---------- Proofs ----------

4040