c74acae · Idris-dev · git.iko.soy

CHANGELOG+5

compare with master

unifiedsplit

@@ -1,6 +1,8 @@

1New in 0.9.18:

2--------------

3* Strings are now UTF8 encoded in the default back end

4+* Idris source files are now assumed to be in UTF8, regardless of locale

5+ settings.

4* Some reorganisation of primitives:

6* Some reorganisation of primitives:

5 + Buffer and BitVector primitives have been removed (they were not

7 + Buffer and BitVector primitives have been removed (they were not

6 tested sufficiently, and lack a maintainer)

8 tested sufficiently, and lack a maintainer)

@@ -21,6 +23,9 @@ New in 0.9.18:

21 requiring a separate lemma.

23 requiring a separate lemma.

22* Case alternatives are allowed to be impossible:

24* Case alternatives are allowed to be impossible:

23 case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }

25 case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }

26+* The default Semigroup and Monoid instances for Maybe are now prioritised

27+ choice, keeping the first success as Alternative does. The version that

28+ collects successes is now a named instance.

24

29

25New in 0.9.17:

30New in 0.9.17:

26--------------

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

libs/prelude/Prelude/Maybe.idr+18−10

@@ -78,17 +78,25 @@ instance (Eq a) => Eq (Maybe a) where

78 (Just _) == Nothing = False

79 (Just a) == (Just b) = a == b

80

81−-- Lift a semigroup into 'Maybe' forming a 'Monoid' according to

81+||| Prioritised choice. Just like the `Alternative` instance, the

82−-- <http://en.wikipedia.org/wiki/Monoid>: "Any semigroup S may be

82+||| `Semigroup` for `Maybe a` keeps the first succeeding computation.

83−-- turned into a monoid simply by adjoining an element i not in S

83+|||

84−-- and defining i+i = i and i+s = s = s+i for all s in S."

84+||| **NB**: This is a different choice than in the Haskell libraries.

85−

85+||| Use `collectJust` to get the Haskell behaviour.

86+instance Semigroup (Maybe a) where

87+ Nothing <+> m = m

88+ (Just x) <+> _ = Just x

89+

90+||| Transform any semigroup into a monoid by using `Nothing` as the

91+||| designated neutral element and collecting the contents of the

92+||| `Just` constructors using a semigroup structure on `a`. This is

93+||| the behaviour in the Haskell libraries.

86−instance (Semigroup a) => Semigroup (Maybe a) where

94+instance [collectJust] Semigroup a => Semigroup (Maybe a) where

87− Nothing <+> m = m

95+ Nothing <+> m = m

88− m <+> Nothing = m

96+ m <+> Nothing = m

89 (Just m1) <+> (Just m2) = Just (m1 <+> m2)

97 (Just m1) <+> (Just m2) = Just (m1 <+> m2)

90

98

91−instance (Semigroup a) => Monoid (Maybe a) where

99+instance Monoid (Maybe a) where

92 neutral = Nothing

100 neutral = Nothing

93

101

94instance (Monoid a, Eq a) => Cast a (Maybe a) where

102instance (Monoid a, Eq a) => Cast a (Maybe a) where

@@ -98,5 +106,5 @@ instance (Monoid a) => Cast (Maybe a) a where

98 cast = lowerMaybe

106 cast = lowerMaybe

99

107

100instance Foldable Maybe where

108instance Foldable Maybe where

101− foldr _ z Nothing = z

109+ foldr _ z Nothing = z

102 foldr f z (Just x) = f x z

110 foldr f z (Just x) = f x z

src/Idris/AbsSyntax.hs+3−1

@@ -816,7 +816,9 @@ targetCPU = do i <- getIState

816

817verbose :: Idris Bool

818verbose = do i <- getIState

819+ -- Quietness overrides verbosity

820+ return (not (opt_quiet (idris_options i)) &&

819− return (opt_verbose (idris_options i))

821+ opt_verbose (idris_options i))

820

822

821setVerbose :: Bool -> Idris ()

823setVerbose :: Bool -> Idris ()

822setVerbose t = do i <- getIState

824setVerbose t = do i <- getIState

src/Idris/Chaser.hs+2−1

@@ -15,6 +15,7 @@ import Control.Monad.State

15import Data.List

16

17import Debug.Trace

18+import Util.System (readSource, writeSource)

18

19

19data ModuleTree = MTree { mod_path :: IFileType,

20data ModuleTree = MTree { mod_path :: IFileType,

20 mod_needsRecheck :: Bool,

21 mod_needsRecheck :: Bool,

@@ -133,7 +134,7 @@ buildTree built fp = btree [] fp

133 children lit f done = -- idrisCatch

134 children lit f done = -- idrisCatch

134 do exist <- runIO $ doesFileExist f

135 do exist <- runIO $ doesFileExist f

135 if exist then do

136 if exist then do

136− file_in <- runIO $ readFile f

137+ file_in <- runIO $ readSource f

137 file <- if lit then tclift $ unlit f file_in else return file_in

138 file <- if lit then tclift $ unlit f file_in else return file_in

138 (_, _, modules, _) <- parseImports f file

139 (_, _, modules, _) <- parseImports f file

139 -- The chaser should never report warnings from sub-modules

140 -- The chaser should never report warnings from sub-modules

src/Idris/IdrisDoc.hs+7−2

@@ -1,5 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2{-# LANGUAGE OverloadedStrings #-}

3+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3

4

4-- | Generation of HTML documentation for Idris code

5-- | Generation of HTML documentation for Idris code

5module Idris.IdrisDoc (generateDocs) where

6module Idris.IdrisDoc (generateDocs) where

@@ -217,9 +218,11 @@ referredNss (n, Just d, _) =

217 names = concatMap (extractPTermNames) ts

218 names = concatMap (extractPTermNames) ts

218 in S.map getNs $ S.fromList names

219 in S.map getNs $ S.fromList names

219

220

220− where getFunDocs (FunDoc f) = [f]

221+ where getFunDocs (FunDoc f) = [f]

221− getFunDocs (DataDoc f fs) = f:fs

222+ getFunDocs (DataDoc f fs) = f:fs

222 getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

223 getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

224+ getFunDocs (NamedInstanceDoc _ fd) = [fd]

225+ getFunDocs (ModDoc _ _) = []

223 types (FD _ _ args t _) = t:(map second args)

226 types (FD _ _ args t _) = t:(map second args)

224 second (_, x, _, _) = x

227 second (_, x, _, _) = x

225

228

@@ -609,6 +612,8 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do

609 H.dt $ toHtml $ show name

612 H.dt $ toHtml $ show name

610 H.dd $ Docstrings.renderHtml docstring

613 H.dd $ Docstrings.renderHtml docstring

611

614

615+createOtherDoc ist (NamedInstanceDoc _ fd) = createFunDoc ist fd

616+

612createOtherDoc ist (ModDoc _ docstring) = do

617createOtherDoc ist (ModDoc _ docstring) = do

613 Docstrings.renderHtml docstring

618 Docstrings.renderHtml docstring

614

619

src/Idris/Interactive.hs+15−16

@@ -17,7 +17,6 @@ import Idris.Error

17import Idris.Delaborate

18import Idris.Output

19import Idris.IdeMode hiding (IdeModeCommand(..))

20−

21import Idris.Elab.Value

20import Idris.Elab.Value

22

21

23import Util.Pretty

22import Util.Pretty

@@ -34,7 +33,7 @@ import Debug.Trace

34

33

35caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

34caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

36caseSplitAt fn updatefile l n

35caseSplitAt fn updatefile l n

37− = do src <- runIO $ readFile fn

36+ = do src <- runIO $ readSource fn

38 res <- splitOnLine l n fn

37 res <- splitOnLine l n fn

39 iLOG (showSep "\n" (map show res))

38 iLOG (showSep "\n" (map show res))

40 let (before, (ap : later)) = splitAt (l-1) (lines src)

39 let (before, (ap : later)) = splitAt (l-1) (lines src)

@@ -42,14 +41,14 @@ caseSplitAt fn updatefile l n

42 let new = concat res'

41 let new = concat res'

43 if updatefile

42 if updatefile

44 then do let fb = fn ++ "~" -- make a backup!

43 then do let fb = fn ++ "~" -- make a backup!

45− runIO $ writeFile fb (unlines before ++ new ++ unlines later)

44+ runIO $ writeSource fb (unlines before ++ new ++ unlines later)

46 runIO $ copyFile fb fn

45 runIO $ copyFile fb fn

47 else -- do iputStrLn (show res)

46 else -- do iputStrLn (show res)

48 iPrintResult new

47 iPrintResult new

49

48

50addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

49addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

51addClauseFrom fn updatefile l n

50addClauseFrom fn updatefile l n

52− = do src <- runIO $ readFile fn

51+ = do src <- runIO $ readSource fn

53 let (before, tyline : later) = splitAt (l-1) (lines src)

52 let (before, tyline : later) = splitAt (l-1) (lines src)

54 let indent = getIndent 0 (show n) tyline

53 let indent = getIndent 0 (show n) tyline

55 cl <- getClause l n fn

54 cl <- getClause l n fn

@@ -57,7 +56,7 @@ addClauseFrom fn updatefile l n

57 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

56 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

58 if updatefile

57 if updatefile

59 then do let fb = fn ++ "~"

58 then do let fb = fn ++ "~"

60− runIO $ writeFile fb (unlines (before ++ nonblank) ++

59+ runIO $ writeSource fb (unlines (before ++ nonblank) ++

61 replicate indent ' ' ++

60 replicate indent ' ' ++

62 cl ++ "\n" ++

61 cl ++ "\n" ++

63 unlines rest)

62 unlines rest)

@@ -71,7 +70,7 @@ addClauseFrom fn updatefile l n

71

70

72addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

71addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

73addProofClauseFrom fn updatefile l n

72addProofClauseFrom fn updatefile l n

74− = do src <- runIO $ readFile fn

73+ = do src <- runIO $ readSource fn

75 let (before, tyline : later) = splitAt (l-1) (lines src)

74 let (before, tyline : later) = splitAt (l-1) (lines src)

76 let indent = getIndent 0 (show n) tyline

75 let indent = getIndent 0 (show n) tyline

77 cl <- getProofClause l n fn

76 cl <- getProofClause l n fn

@@ -79,7 +78,7 @@ addProofClauseFrom fn updatefile l n

79 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

78 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

80 if updatefile

79 if updatefile

81 then do let fb = fn ++ "~"

80 then do let fb = fn ++ "~"

82− runIO $ writeFile fb (unlines (before ++ nonblank) ++

81+ runIO $ writeSource fb (unlines (before ++ nonblank) ++

83 replicate indent ' ' ++

82 replicate indent ' ' ++

84 cl ++ "\n" ++

83 cl ++ "\n" ++

85 unlines rest)

84 unlines rest)

@@ -92,7 +91,7 @@ addProofClauseFrom fn updatefile l n

92

91

93addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()

92addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()

94addMissing fn updatefile l n

93addMissing fn updatefile l n

95− = do src <- runIO $ readFile fn

94+ = do src <- runIO $ readSource fn

96 let (before, tyline : later) = splitAt (l-1) (lines src)

95 let (before, tyline : later) = splitAt (l-1) (lines src)

97 let indent = getIndent 0 (show n) tyline

96 let indent = getIndent 0 (show n) tyline

98 i <- getIState

97 i <- getIState

@@ -106,7 +105,7 @@ addMissing fn updatefile l n

106 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

105 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

107 if updatefile

106 if updatefile

108 then do let fb = fn ++ "~"

107 then do let fb = fn ++ "~"

109− runIO $ writeFile fb (unlines (before ++ nonblank)

108+ runIO $ writeSource fb (unlines (before ++ nonblank)

110 ++ extras ++ unlines rest)

109 ++ extras ++ unlines rest)

111 runIO $ copyFile fb fn

110 runIO $ copyFile fb fn

112 else iPrintResult extras

111 else iPrintResult extras

@@ -141,7 +140,7 @@ addMissing fn updatefile l n

141

140

142makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

141makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

143makeWith fn updatefile l n

142makeWith fn updatefile l n

144− = do src <- runIO $ readFile fn

143+ = do src <- runIO $ readSource fn

145 let (before, tyline : later) = splitAt (l-1) (lines src)

144 let (before, tyline : later) = splitAt (l-1) (lines src)

146 let ind = getIndent tyline

145 let ind = getIndent tyline

147 let with = mkWith tyline n

146 let with = mkWith tyline n

@@ -151,7 +150,7 @@ makeWith fn updatefile l n

151 not (ind == getIndent x)) later

150 not (ind == getIndent x)) later

152 if updatefile then

151 if updatefile then

153 do let fb = fn ++ "~"

152 do let fb = fn ++ "~"

154− runIO $ writeFile fb (unlines (before ++ nonblank)

153+ runIO $ writeSource fb (unlines (before ++ nonblank)

155 ++ with ++ "\n" ++

154 ++ with ++ "\n" ++

156 unlines rest)

155 unlines rest)

157 runIO $ copyFile fb fn

156 runIO $ copyFile fb fn

@@ -164,7 +163,7 @@ doProofSearch :: FilePath -> Bool -> Bool ->

164doProofSearch fn updatefile rec l n hints Nothing

163doProofSearch fn updatefile rec l n hints Nothing

165 = doProofSearch fn updatefile rec l n hints (Just 10)

164 = doProofSearch fn updatefile rec l n hints (Just 10)

166doProofSearch fn updatefile rec l n hints (Just depth)

165doProofSearch fn updatefile rec l n hints (Just depth)

167− = do src <- runIO $ readFile fn

166+ = do src <- runIO $ readSource fn

168 let (before, tyline : later) = splitAt (l-1) (lines src)

167 let (before, tyline : later) = splitAt (l-1) (lines src)

169 ctxt <- getContext

168 ctxt <- getContext

170 mn <- case lookupNames n ctxt of

169 mn <- case lookupNames n ctxt of

@@ -192,7 +191,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

192 (\e -> return ("?" ++ show n))

191 (\e -> return ("?" ++ show n))

193 if updatefile then

192 if updatefile then

194 do let fb = fn ++ "~"

193 do let fb = fn ++ "~"

195− runIO $ writeFile fb (unlines before ++

194+ runIO $ writeSource fb (unlines before ++

196 updateMeta False tyline (show n) newmv ++ "\n"

195 updateMeta False tyline (show n) newmv ++ "\n"

197 ++ unlines later)

196 ++ unlines later)

198 runIO $ copyFile fb fn

197 runIO $ copyFile fb fn

@@ -241,7 +240,7 @@ addBracket True new | any isSpace new = '(' : new ++ ")"

241

240

242makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()

241makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()

243makeLemma fn updatefile l n

242makeLemma fn updatefile l n

244− = do src <- runIO $ readFile fn

243+ = do src <- runIO $ readSource fn

245 let (before, tyline : later) = splitAt (l-1) (lines src)

244 let (before, tyline : later) = splitAt (l-1) (lines src)

246

245

247 -- if the name is in braces, rather than preceded by a ?, treat it

246 -- if the name is in braces, rather than preceded by a ?, treat it

@@ -267,7 +266,7 @@ makeLemma fn updatefile l n

267

266

268 if updatefile then

267 if updatefile then

269 do let fb = fn ++ "~"

268 do let fb = fn ++ "~"

270− runIO $ writeFile fb (addLem before tyline lem lem_app later)

269+ runIO $ writeSource fb (addLem before tyline lem lem_app later)

271 runIO $ copyFile fb fn

270 runIO $ copyFile fb fn

272 else case idris_outputmode i of

271 else case idris_outputmode i of

273 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app

272 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app

@@ -285,7 +284,7 @@ makeLemma fn updatefile l n

285 " = ?" ++ show n ++ "_rhs"

284 " = ?" ++ show n ++ "_rhs"

286 if updatefile then

285 if updatefile then

287 do let fb = fn ++ "~"

286 do let fb = fn ++ "~"

288− runIO $ writeFile fb (addProv before tyline lem_app later)

287+ runIO $ writeSource fb (addProv before tyline lem_app later)

289 runIO $ copyFile fb fn

288 runIO $ copyFile fb fn

290 else case idris_outputmode i of

289 else case idris_outputmode i of

291 RawOutput _ -> iPrintResult $ lem_app

290 RawOutput _ -> iPrintResult $ lem_app

src/Idris/Parser.hs+2−1

@@ -43,6 +43,7 @@ import Idris.Docstrings hiding (Unchecked)

43import Paths_idris

44

45import Util.DynamicLinker

46+import Util.System (readSource, writeSource)

46import qualified Util.Pretty as P

47import qualified Util.Pretty as P

47

48

48import Idris.Core.TT

49import Idris.Core.TT

@@ -1345,7 +1346,7 @@ loadSource lidr f toline

1345 = do iLOG ("Reading " ++ f)

1346 = do iLOG ("Reading " ++ f)

1346 i <- getIState

1347 i <- getIState

1347 let def_total = default_total i

1348 let def_total = default_total i

1348− file_in <- runIO $ readFile f

1349+ file_in <- runIO $ readSource f

1349 file <- if lidr then tclift $ unlit f file_in else return file_in

1350 file <- if lidr then tclift $ unlit f file_in else return file_in

1350 (mdocs, mname, imports_in, pos) <- parseImports f file

1351 (mdocs, mname, imports_in, pos) <- parseImports f file

1351 ai <- getAutoImports

1352 ai <- getAutoImports

src/Idris/REPL.hs+2−2

@@ -1059,7 +1059,7 @@ process fn' (AddProof prf)

1059 else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"

1060 let fb = fn ++ "~"

1061 runIO $ copyFile fn fb -- make a backup in case something goes wrong!

1062− prog <- runIO $ readFile fb

1062+ prog <- runIO $ readSource fb

1063 i <- getIState

1064 let proofs = proof_list i

1065 n' <- case prf of

@@ -1071,7 +1071,7 @@ process fn' (AddProof prf)

1071 case lookup n proofs of

1072 Nothing -> iputStrLn "No proof to add"

1073 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls

1074− runIO $ writeFile fn (unlines prog')

1074+ runIO $ writeSource fn (unlines prog')

1075 removeProof n

1076 iputStrLn $ "Added proof " ++ show n

1077 where ls = (lines prog)

src/Util/System.hs+12−1

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

1−module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows) where

1+module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows,

2+ readSource, writeSource) where

2

3

3-- System helper functions.

4-- System helper functions.

4import Control.Monad (when)

5import Control.Monad (when)

@@ -26,6 +27,16 @@ tempfile :: IO (FilePath, Handle)

26tempfile = do dir <- getTemporaryDirectory

27tempfile = do dir <- getTemporaryDirectory

27 openTempFile (normalise dir) "idris"

28 openTempFile (normalise dir) "idris"

28

29

30+-- | Read a source file, same as readFile but make sure the encoding is utf-8.

31+readSource :: FilePath -> IO String

32+readSource f = do h <- openFile f ReadMode

33+ hSetEncoding h utf8

34+ hGetContents h

35+

36+-- | Write a source file, same as writeFile except the encoding is set to utf-8

37+writeSource :: FilePath -> String -> IO ()

38+writeSource f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> hPutStr h s)

39+

29withTempdir :: String -> (FilePath -> IO a) -> IO a

40withTempdir :: String -> (FilePath -> IO a) -> IO a

30withTempdir subdir callback

41withTempdir subdir callback

31 = do dir <- getTemporaryDirectory

42 = do dir <- getTemporaryDirectory

test/delab001/expected−1

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

1−Type checking ./delab001.idr

2foo : Nat -> String

1foo : Nat -> String

3foo n = case n of

2foo n = case n of

4 0 => "z"

3 0 => "z"

test/docs001/expected−1

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

1−Type checking ./docs001.idr

2Type class C

1Type class C

3 class

2 class

4

3

test/docs002/expected+3−5

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

1−Type checking ./docs002.idr

2−*docs002> T1 : Type

1+T1 : Type

3 Some documentation

2 Some documentation

4

3

5−*docs002> T2 : Type

4+T2 : Type

6 Some other documentation

5 Some other documentation

7

6

8−*docs002> T3 : Int

7+T3 : Int

9 Some provided postulate

8 Some provided postulate

10

9

11−*docs002> Bye bye

test/docs002/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 --nobanner --nocolor docs002.idr < input

2+idris --consolewidth 80 --nobanner --nocolor --quiet docs002.idr < input

3rm *.ibc

test/docs003/expected−1

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

1−Type checking ./docs003.idr

2Type class Functor

1Type class Functor

3 Functors

2 Functors

4

3

test/ffi001/expected−1

@@ -1,2 +1 @@

1−Type checking ./test022.idr

20.9995736030415051

10.9995736030415051

test/ffi003/expected−1

@@ -1,2 +1 @@

1−Type checking ./test024.idr

2testtest

1testtest

test/idrisdoc001/expected−2

@@ -1,5 +1,3 @@

1−Type checking ./TestEmpty.idr

2−Type checking ./TestPrivate.idr

3Warning: Ignoring empty or non-existing namespace 'TestEmpty'

1Warning: Ignoring empty or non-existing namespace 'TestEmpty'

4Warning: Ignoring empty or non-existing namespace 'TestPrivate'

2Warning: Ignoring empty or non-existing namespace 'TestPrivate'

5No namespaces to generate documentation for

3No namespaces to generate documentation for

test/idrisdoc001/run+1−1

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

1#!/usr/bin/env bash

2# Tests that no documentation is built for empty and/or private-only namespaces

3idris --mkdoc test_empty.ipkg

4−rm -rf *.ibc *_doc

4+rm -rf *.ibc *_doc

test/idrisdoc001/test_empty.ipkg+2

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

1package test_empty

2

3+opts = "--quiet"

4+

3modules = TestEmpty, TestPrivate

5modules = TestEmpty, TestPrivate

4

6

test/idrisdoc002/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestFunctions.idr

2Functions are documented

1Functions are documented

test/idrisdoc002/test_functions.ipkg+2

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

1package test_functions

2

3+opts = "--quiet"

4+

3modules = TestFunctions

5modules = TestFunctions

4

6

test/idrisdoc003/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestDatatypes.idr

2Data types are documented

1Data types are documented

test/idrisdoc003/test_datatypes.ipkg+2

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

1package test_datatypes

2

3+opts = "--quiet"

4+

3modules = TestDatatypes

5modules = TestDatatypes

4

6

test/idrisdoc004/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestTypeclasses.idr

2Typeclasses are documented

1Typeclasses are documented

test/idrisdoc004/test_typeclasses.ipkg+2

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

1package test_typeclasses

2

3+opts = "--quiet"

4+

3modules = TestTypeclasses

5modules = TestTypeclasses

4

6

test/idrisdoc005/expected−1

@@ -1,3 +1,2 @@

1−Type checking ./TestTracing.idr

2TestTracing: Check

1TestTracing: Check

3Prelude.Bool: Check

2Prelude.Bool: Check

test/idrisdoc005/test_tracing.ipkg+2

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

1package test_tracing

2

3+opts = "--quiet"

4+

3modules = TestTracing

5modules = TestTracing

4

6

test/idrisdoc006/expected−2

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

1−Type checking ./A/fully/Qualified/NAME.idr

2IdrisDoc file written

1IdrisDoc file written

3−Type checking ./B.idr

4A.fully.Qualified.NAME.html

2A.fully.Qualified.NAME.html

5B.html

3B.html

6A.fully.Qualified.NAME is in the index

4A.fully.Qualified.NAME is in the index

test/idrisdoc006/package_a.ipkg+2

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

1package test_merge

2

3+opts = "--quiet"

4+

3modules = A.fully.Qualified.NAME

5modules = A.fully.Qualified.NAME

4

6

test/idrisdoc006/package_b.ipkg+2

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

1package test_merge

2

3+opts = "--quiet"

4+

3modules = B

5modules = B

4

6

test/idrisdoc007/package.ipkg+2

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

1package do_not_delete

2

3+opts = "--quiet"

4+

3modules = A

5modules = A

4

6

test/idrisdoc008/expected−2

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

1−Type checking ./Abstract.idr

2−Type checking ./Visible.idr

3Abstract members are documented

1Abstract members are documented

4Public members are documented

2Public members are documented

test/idrisdoc008/visibility.ipkg+2

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

1package visibility

2

3+opts = "--quiet"

4+

3modules = Abstract, Visible

5modules = Abstract, Visible

4

6

test/idrisdoc009/expected−1

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

1−Type checking ./Test.idr

2Data type Test : Type

1Data type Test : Type

3 Docs for datatype Test.

2 Docs for datatype Test.

4

3

test/interactive001/expected−1

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

1−Type checking ./test032.idr

2isElem x [] = ?isElem_rhs_1

1isElem x [] = ?isElem_rhs_1

3isElem x (y :: xs) = ?isElem_rhs_3

2isElem x (y :: xs) = ?isElem_rhs_3

4

3

test/interactive002/expected−1

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

1−Type checking ./interactive002.idr

2Nat

1Nat

3Nat

2Nat

4Nat

3Nat

test/interactive003/expected−1

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

1−Type checking ./interactive003.idr

2ys

1ys

3x :: app xs ys

2x :: app xs ys

4[]

3[]

test/interactive004/expected−1

@@ -1,3 +1,2 @@

1−Type checking ./interactive004.idr

2plus ?foo_rhs2 ?foo_rhs3

1plus ?foo_rhs2 ?foo_rhs3

3append k m ?append_rhs2 ?append_rhs3

2append k m ?append_rhs2 ?append_rhs3

test/interactive005/expected−1

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

1−Type checking ./interactive005.idr

23 : Nat

13 : Nat

3Hello, World

2Hello, World

4main : IO ()

3main : IO ()

test/interactive006/expected−1

@@ -1,2 +1 @@

1−Type checking ./interactive006.idr

2plus ?foo_rhs2 ?foo_rhs3

1plus ?foo_rhs2 ?foo_rhs3

test/proof007/expected+1−1

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

1DefaultArgUnknownName.idr:9:6:

2When elaborating right hand side of test:

3−When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

3+When elaborating argument arg to function DefaultArgUnknownName.funWithBadDefArg:

4 No such variable sadgjhsag

test/proof007/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 --check $@ DefaultArgUnknownName.idr

2+idris --nocolour --consolewidth 80 --check $@ DefaultArgUnknownName.idr

3rm -f *.ibc

test/proof009/expected−1

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

1−Type checking ./proof009.idr

2

1

3

2

4---------- Goal: ----------

3---------- Goal: ----------

test/reg023/expected+2−2

@@ -1,5 +1,5 @@

1reg023.idr:7:5:When elaborating right hand side of bad:

2Can't unify

3− [94mNat[0m (Type of [91m0[0m)

3+ Nat (Type of 0)

4with

5− [92mf[0m [94mNat[0m (Expected type)

5+ f Nat (Expected type)

test/reg023/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg023.idr --check

2+idris --nocolour --consolewidth 80 $@ reg023.idr --check

3rm -f *.ibc

test/reg029/reg029.idr+1−1

@@ -3,7 +3,7 @@ module Main

3import System

4

5-- necessary to find the getenv symbol

6−%dynamic "libm"

6+%dynamic "libm","msvcrt"

7

8main : IO ()

9main = do

test/reg034/expected+2−2

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

1reg034.idr:6:5:When elaborating left hand side of bar:

2−Can't match on bar xs xs [91mRefl[0m

2+Can't match on bar xs xs Refl

3reg034.idr:9:5:When elaborating left hand side of foo:

4−Can't match on foo f x x [91mRefl[0m

4+Can't match on foo f x x Refl

test/reg034/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 --check reg034.idr

2+idris --nocolour --consolewidth 80 --check reg034.idr

3rm -f reg034 *.ibc

test/reg035/expected+2−2

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

1reg035b.idr:8:6:Can't convert

2− [94mAdditive[0m -> [94mNat[0m

2+ Additive -> Nat

3with

4− [94mFin[0m [91m0[0m

4+ Fin 0

test/reg035/run+3−3

@@ -1,5 +1,5 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 --check reg035.idr

2+idris --nocolour --consolewidth 80 --check reg035.idr

3−idris --consolewidth 80 --check reg035a.lidr

3+idris --nocolour --consolewidth 80 --check reg035a.lidr

4−idris --consolewidth 80 --check reg035b.idr

4+idris --nocolour --consolewidth 80 --check reg035b.idr

5rm -f *.ibc

test/reg039/expected−1

@@ -1,2 +1 @@

1−Type checking ./reg039.idr

2[3, 2, 1]

1[3, 2, 1]

test/reg041/expected−1

@@ -1,3 +1,2 @@

1−Type checking ./ott.idr

2?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)

1?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)

3Z

2Z

test/reg044/expected+4−4

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

1reg044.idr:4:4:When elaborating right hand side of Main.pf:

2Can't unify

3− [95mb[0m [94m=[0m [95mb[0m (Type of [91mRefl[0m)

3+ b = b (Type of Refl)

4with

5− [95ma[0m [94m=[0m [95mb[0m (Expected type)

5+ a = b (Expected type)

6

7Specifically:

8 Can't unify

9− [95mb[0m

9+ b

10 with

11− [95ma[0m

11+ a

test/reg044/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 reg044.idr --check

2+idris --nocolour --consolewidth 80 reg044.idr --check

3rm -f *.ibc

test/reg054/expected+4−4

@@ -1,10 +1,10 @@

1reg054.idr:18:5:When elaborating left hand side of inf:

2−When elaborating an application of constructor [91mMain.MkInfer[0m:

2+When elaborating an application of constructor Main.MkInfer:

3 Attempting concrete match on polymorphic argument: 0

4reg054.idr:34:7:When elaborating left hand side of weird:

5−When elaborating argument [95mx[0m to Main.weird:

5+When elaborating argument x to Main.weird:

6 No explicit types on left hand side: Char

7reg054.idr:37:9:Can't convert

8− [94mMaybe[0m a1

8+ Maybe a1

9with

10− [95ma[0m

10+ a

test/reg054/run+1−1

@@ -1,2 +1,2 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg054.idr --check

2+idris --nocolour --consolewidth 80 $@ reg054.idr --check

test/reg055/expected+3−3

@@ -1,9 +1,9 @@

1reg055.idr:5:3:When elaborating left hand side of g:

2−Can't match on g ([92mf[0m [91m0[0m)

2+Can't match on g (f 0)

3reg055.idr:8:3:When elaborating left hand side of h:

4Can't match on h x x

5reg055a.idr:8:5:When elaborating left hand side of foo:

6−When elaborating an application of constructor [91mFoo.CAny[0m:

6+When elaborating an application of constructor Foo.CAny:

7 Attempting concrete match on polymorphic argument: Nothing

8reg055a.idr:13:7:When elaborating left hand side of Foo.apply:

9−Can't match on apply (\[95mx[0m => \[95my[0m => [95mx[0m) a

9+Can't match on apply (\x => \y => x) a

test/reg055/run+2−2

@@ -1,5 +1,5 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg055.idr --check

2+idris --nocolour --consolewidth 80 $@ reg055.idr --check

3−idris --consolewidth 80 $@ reg055a.idr --check

3+idris --nocolour --consolewidth 80 $@ reg055a.idr --check

4rm -f *.ibc

5

test/runtest.pl+1−1

@@ -13,7 +13,7 @@ sub sandbox_path {

13 my $sandbox = abs_path("$test_dir/../../.cabal-sandbox/bin");

14

15 if ( -d $sandbox ) {

16− return "PATH=$sandbox:$PATH";

16+ return "PATH=\"$sandbox:$PATH\"";

17 } else {

18 return "";

19 }

test/totality007/expected−1

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

1−Type checking ./Totality.idr

2Totality.idr:4:1:

1Totality.idr:4:1:

3Totality.foo is not total as there are missing cases

2Totality.foo is not total as there are missing cases

4Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases

3Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases

test/totality007/totality.ipkg+1−1

@@ -2,6 +2,6 @@ package totality

2

3-- totality007

4-- Test that the package builder doesn't allow totality errors in a build

5−opts = "--consolewidth 80"

5+opts = "--quiet --consolewidth 80"

6sourcedir = src

7modules = Totality

test/tutorial006/expected+9−9

@@ -1,24 +1,24 @@

1tutorial006a.idr:5:23:When elaborating right hand side of vapp:

2−When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

2+When elaborating argument xs to constructor Data.VectType.Vect.:::

3 Can't unify

4− [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp [95mxs[0m [95mxs[0m)

4+ Vect (n + n) a (Type of vapp xs xs)

5 with

6− [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m (Expected type)

6+ Vect (plus n m) a (Expected type)

7

8 Specifically:

9 Can't unify

10− [92mplus[0m [95mn[0m [95mn[0m

10+ plus n n

11 with

12− [92mplus[0m [95mn[0m [95mm[0m

12+ plus n m

13tutorial006b.idr:10:10:

14When elaborating right hand side of with block in Main.parity:

15Can't unify

16− [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)

16+ Parity (plus (S j) (S j)) (Type of even)

17with

18− [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))) (Expected type)

18+ Parity (S (S (plus j j))) (Expected type)

19

20Specifically:

21 Can't unify

22− [92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)

22+ plus (S j) (S j)

23 with

24− [91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))

24+ S (S (plus j j))

test/tutorial006/run+2−2

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

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ tutorial006a.idr --check

2+idris --nocolour --consolewidth 80 $@ tutorial006a.idr --check

3−idris --consolewidth 80 $@ tutorial006b.idr --check

3+idris --nocolour --consolewidth 80 $@ tutorial006b.idr --check

4rm -f *.ibc

test/unique001/expected+6−6

@@ -3,17 +3,17 @@

338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

5unique001a.idr:33:11:Can't convert

6− [94mInt[0m -> [94mString[0m

6+ Int -> String

7with

8− UniqueType ([94mInt[0m -> [94mString[0m)

8+ UniqueType (Int -> String)

9unique001a.idr:44:12:Can't convert

10− [94mInt[0m -> [94mString[0m

10+ Int -> String

11with

12− UniqueType ([94mInt[0m -> [94mString[0m)

12+ UniqueType (Int -> String)

13unique001a.idr:55:12:Can't convert

14− UniqueType ([94mInt[0m -> [94mString[0m)

14+ UniqueType (Int -> String)

15with

16− [94mInt[0m -> [94mString[0m

16+ Int -> String

17unique001b.idr:16:7:Borrowed name xs must not be used on RHS

18unique001c.idr:46:6:Unique name f is used more than once

19unique001d.idr:3:7:Borrowed name x must not be used on RHS

test/unique001/run+6−6

@@ -1,9 +1,9 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique001.idr -o unique001

2+idris --nocolour --consolewidth 80 $@ unique001.idr -o unique001

3./unique001

4−idris --consolewidth 80 $@ unique001a.idr --check

4+idris --nocolour --consolewidth 80 $@ unique001a.idr --check

5−idris --consolewidth 80 $@ unique001b.idr --check

5+idris --nocolour --consolewidth 80 $@ unique001b.idr --check

6−idris --consolewidth 80 $@ unique001c.idr --check

6+idris --nocolour --consolewidth 80 $@ unique001c.idr --check

7−idris --consolewidth 80 $@ unique001d.idr --check

7+idris --nocolour --consolewidth 80 $@ unique001d.idr --check

8−idris --consolewidth 80 $@ unique001e.idr --check

8+idris --nocolour --consolewidth 80 $@ unique001e.idr --check

9rm -f unique001 *.ibc

test/unique002/expected+2−2

@@ -1,5 +1,5 @@

1unique002.idr:15:5:Unique name xs is used more than once

2unique002a.idr:15:5:Can't convert

3− [94mInt[0m -> [94mString[0m

3+ Int -> String

4with

5− UniqueType ([94mInt[0m -> [94mString[0m)

5+ UniqueType (Int -> String)

test/unique002/run+2−2

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

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique002.idr --check

2+idris --nocolour --consolewidth 80 $@ unique002.idr --check

3−idris --consolewidth 80 $@ unique002a.idr --check

3+idris --nocolour --consolewidth 80 $@ unique002a.idr --check

4rm -f *.ibc

test/unique003/expected+2−2

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

1unique003.idr:18:5:Can't convert

2− [94mInt[0m -> [94mString[0m

2+ Int -> String

3with

4− UniqueType ([94mInt[0m -> [94mString[0m)

4+ UniqueType (Int -> String)

test/unique003/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique003.idr --check

2+idris --nocolour --consolewidth 80 $@ unique003.idr --check

3rm -f *.ibc