c74acae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical

commitc74acae90398bf7465cd4d4bed4c0c8c95270ff1 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 2 Apr 2015, 15:33 (12 years ago) parent5804426 4359edd

69 files changed+150−128

compare with master

unifiedsplit

CHANGELOG+5

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

11New in 0.9.18:

22--------------

33* 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.

46* Some reorganisation of primitives:

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

68 tested sufficiently, and lack a maintainer)

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

2123 requiring a separate lemma.

2224* Case alternatives are allowed to be impossible:

2325 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.

2429

2530New in 0.9.17:

2631--------------

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

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

7878 (Just _) == Nothing = False

7979 (Just a) == (Just b) = a == b

8080

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

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

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

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

85−

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

87− Nothing <+> m = m

88− m <+> Nothing = m

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

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

83+|||

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

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.

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

95+ Nothing <+> m = m

96+ m <+> Nothing = m

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

9098

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

99+instance Monoid (Maybe a) where

92100 neutral = Nothing

93101

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

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

98106 cast = lowerMaybe

99107

100108instance Foldable Maybe where

101− foldr _ z Nothing = z

109+ foldr _ z Nothing = z

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

src/Idris/AbsSyntax.hs+3−1

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

816816

817817verbose :: Idris Bool

818818verbose = do i <- getIState

819− return (opt_verbose (idris_options i))

819+ -- Quietness overrides verbosity

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

821+ opt_verbose (idris_options i))

820822

821823setVerbose :: Bool -> Idris ()

822824setVerbose t = do i <- getIState

src/Idris/Chaser.hs+2−1

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

1515import Data.List

1616

1717import Debug.Trace

18+import Util.System (readSource, writeSource)

1819

1920data ModuleTree = MTree { mod_path :: IFileType,

2021 mod_needsRecheck :: Bool,

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

133134 children lit f done = -- idrisCatch

134135 do exist <- runIO $ doesFileExist f

135136 if exist then do

136− file_in <- runIO $ readFile f

137+ file_in <- runIO $ readSource f

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

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

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

src/Idris/IdrisDoc.hs+7−2

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

11{-# LANGUAGE PatternGuards #-}

22{-# LANGUAGE OverloadedStrings #-}

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

45-- | Generation of HTML documentation for Idris code

56module Idris.IdrisDoc (generateDocs) where

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

217218 names = concatMap (extractPTermNames) ts

218219 in S.map getNs $ S.fromList names

219220

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

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

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

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

222223 getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

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

225+ getFunDocs (ModDoc _ _) = []

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

224227 second (_, x, _, _) = x

225228

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

609612 H.dt $ toHtml $ show name

610613 H.dd $ Docstrings.renderHtml docstring

611614

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

616+

612617createOtherDoc ist (ModDoc _ docstring) = do

613618 Docstrings.renderHtml docstring

614619

src/Idris/Interactive.hs+15−16

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

1717import Idris.Delaborate

1818import Idris.Output

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

20−

2120import Idris.Elab.Value

2221

2322import Util.Pretty

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

3433

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

3635caseSplitAt fn updatefile l n

37− = do src <- runIO $ readFile fn

36+ = do src <- runIO $ readSource fn

3837 res <- splitOnLine l n fn

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

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

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

4241 let new = concat res'

4342 if updatefile

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

4645 runIO $ copyFile fb fn

4746 else -- do iputStrLn (show res)

4847 iPrintResult new

4948

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

5150addClauseFrom fn updatefile l n

52− = do src <- runIO $ readFile fn

51+ = do src <- runIO $ readSource fn

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

5453 let indent = getIndent 0 (show n) tyline

5554 cl <- getClause l n fn

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

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

5857 if updatefile

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

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

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

6160 replicate indent ' ' ++

6261 cl ++ "\n" ++

6362 unlines rest)

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

7170

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

7372addProofClauseFrom fn updatefile l n

74− = do src <- runIO $ readFile fn

73+ = do src <- runIO $ readSource fn

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

7675 let indent = getIndent 0 (show n) tyline

7776 cl <- getProofClause l n fn

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

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

8079 if updatefile

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

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

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

8382 replicate indent ' ' ++

8483 cl ++ "\n" ++

8584 unlines rest)

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

9291

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

9493addMissing fn updatefile l n

95− = do src <- runIO $ readFile fn

94+ = do src <- runIO $ readSource fn

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

9796 let indent = getIndent 0 (show n) tyline

9897 i <- getIState

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

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

107106 if updatefile

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

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

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

110109 ++ extras ++ unlines rest)

111110 runIO $ copyFile fb fn

112111 else iPrintResult extras

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

141140

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

143142makeWith fn updatefile l n

144− = do src <- runIO $ readFile fn

143+ = do src <- runIO $ readSource fn

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

146145 let ind = getIndent tyline

147146 let with = mkWith tyline n

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

151150 not (ind == getIndent x)) later

152151 if updatefile then

153152 do let fb = fn ++ "~"

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

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

155154 ++ with ++ "\n" ++

156155 unlines rest)

157156 runIO $ copyFile fb fn

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

164163doProofSearch fn updatefile rec l n hints Nothing

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

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

167− = do src <- runIO $ readFile fn

166+ = do src <- runIO $ readSource fn

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

169168 ctxt <- getContext

170169 mn <- case lookupNames n ctxt of

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

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

193192 if updatefile then

194193 do let fb = fn ++ "~"

195− runIO $ writeFile fb (unlines before ++

194+ runIO $ writeSource fb (unlines before ++

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

197196 ++ unlines later)

198197 runIO $ copyFile fb fn

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

241240

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

243242makeLemma fn updatefile l n

244− = do src <- runIO $ readFile fn

243+ = do src <- runIO $ readSource fn

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

246245

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

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

267266

268267 if updatefile then

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

271270 runIO $ copyFile fb fn

272271 else case idris_outputmode i of

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

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

285284 " = ?" ++ show n ++ "_rhs"

286285 if updatefile then

287286 do let fb = fn ++ "~"

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

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

289288 runIO $ copyFile fb fn

290289 else case idris_outputmode i of

291290 RawOutput _ -> iPrintResult $ lem_app

src/Idris/Parser.hs+2−1

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

4343import Paths_idris

4444

4545import Util.DynamicLinker

46+import Util.System (readSource, writeSource)

4647import qualified Util.Pretty as P

4748

4849import Idris.Core.TT

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

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

13461347 i <- getIState

13471348 let def_total = default_total i

1348− file_in <- runIO $ readFile f

1349+ file_in <- runIO $ readSource f

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

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

13511352 ai <- getAutoImports

src/Idris/REPL.hs+2−2

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

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

10601060 let fb = fn ++ "~"

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

1062− prog <- runIO $ readFile fb

1062+ prog <- runIO $ readSource fb

10631063 i <- getIState

10641064 let proofs = proof_list i

10651065 n' <- case prf of

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

10711071 case lookup n proofs of

10721072 Nothing -> iputStrLn "No proof to add"

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

1074− runIO $ writeFile fn (unlines prog')

1074+ runIO $ writeSource fn (unlines prog')

10751075 removeProof n

10761076 iputStrLn $ "Added proof " ++ show n

10771077 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

34-- System helper functions.

45import Control.Monad (when)

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

2627tempfile = do dir <- getTemporaryDirectory

2728 openTempFile (normalise dir) "idris"

2829

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+

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

3041withTempdir subdir callback

3142 = do dir <- getTemporaryDirectory

test/delab001/expected−1

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

1−Type checking ./delab001.idr

21foo : Nat -> String

32foo n = case n of

43 0 => "z"

test/docs001/expected−1

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

1−Type checking ./docs001.idr

21Type class C

32 class

test/docs002/expected+3−5

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

1−Type checking ./docs002.idr

2−*docs002> T1 : Type

1+T1 : Type

32 Some documentation

5−*docs002> T2 : Type

4+T2 : Type

65 Some other documentation

8−*docs002> T3 : Int

7+T3 : Int

98 Some provided postulate

109

11−*docs002> Bye bye

test/docs002/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm *.ibc

test/docs003/expected−1

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

1−Type checking ./docs003.idr

21Type class Functor

32 Functors

test/ffi001/expected−1

@@ -1,2 +1 @@

1−Type checking ./test022.idr

210.9995736030415051

test/ffi003/expected−1

@@ -1,2 +1 @@

1−Type checking ./test024.idr

21testtest

test/idrisdoc001/expected−2

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

1−Type checking ./TestEmpty.idr

2−Type checking ./TestPrivate.idr

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

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

53No namespaces to generate documentation for

test/idrisdoc001/run+1−1

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

11#!/usr/bin/env bash

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

33idris --mkdoc test_empty.ipkg

4−rm -rf *.ibc *_doc

4+rm -rf *.ibc *_doc

test/idrisdoc001/test_empty.ipkg+2

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

11package test_empty

3+opts = "--quiet"

35modules = TestEmpty, TestPrivate

test/idrisdoc002/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestFunctions.idr

21Functions are documented

test/idrisdoc002/test_functions.ipkg+2

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

11package test_functions

3+opts = "--quiet"

35modules = TestFunctions

test/idrisdoc003/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestDatatypes.idr

21Data types are documented

test/idrisdoc003/test_datatypes.ipkg+2

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

11package test_datatypes

3+opts = "--quiet"

35modules = TestDatatypes

test/idrisdoc004/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestTypeclasses.idr

21Typeclasses are documented

test/idrisdoc004/test_typeclasses.ipkg+2

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

11package test_typeclasses

3+opts = "--quiet"

35modules = TestTypeclasses

test/idrisdoc005/expected−1

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

1−Type checking ./TestTracing.idr

21TestTracing: Check

32Prelude.Bool: Check

test/idrisdoc005/test_tracing.ipkg+2

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

11package test_tracing

3+opts = "--quiet"

35modules = TestTracing

test/idrisdoc006/expected−2

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

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

21IdrisDoc file written

3−Type checking ./B.idr

42A.fully.Qualified.NAME.html

53B.html

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

test/idrisdoc006/package_a.ipkg+2

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

11package test_merge

3+opts = "--quiet"

35modules = A.fully.Qualified.NAME

test/idrisdoc006/package_b.ipkg+2

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

11package test_merge

3+opts = "--quiet"

35modules = B

test/idrisdoc007/package.ipkg+2

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

11package do_not_delete

3+opts = "--quiet"

35modules = A

test/idrisdoc008/expected−2

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

1−Type checking ./Abstract.idr

2−Type checking ./Visible.idr

31Abstract members are documented

42Public members are documented

test/idrisdoc008/visibility.ipkg+2

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

11package visibility

3+opts = "--quiet"

35modules = Abstract, Visible

test/idrisdoc009/expected−1

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

1−Type checking ./Test.idr

21Data type Test : Type

32 Docs for datatype Test.

test/interactive001/expected−1

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

1−Type checking ./test032.idr

21isElem x [] = ?isElem_rhs_1

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

test/interactive002/expected−1

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

1−Type checking ./interactive002.idr

21Nat

32Nat

43Nat

test/interactive003/expected−1

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

1−Type checking ./interactive003.idr

21ys

32x :: app xs ys

43[]

test/interactive004/expected−1

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

1−Type checking ./interactive004.idr

21plus ?foo_rhs2 ?foo_rhs3

32append k m ?append_rhs2 ?append_rhs3

test/interactive005/expected−1

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

1−Type checking ./interactive005.idr

213 : Nat

32Hello, World

43main : IO ()

test/interactive006/expected−1

@@ -1,2 +1 @@

1−Type checking ./interactive006.idr

21plus ?foo_rhs2 ?foo_rhs3

test/proof007/expected+1−1

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

11DefaultArgUnknownName.idr:9:6:

22When 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:

44 No such variable sadgjhsag

test/proof007/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm -f *.ibc

test/proof009/expected−1

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

1−Type checking ./proof009.idr

43---------- Goal: ----------

test/reg023/expected+2−2

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

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

22Can't unify

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

3+ Nat (Type of 0)

44with

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

5+ f Nat (Expected type)

test/reg023/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm -f *.ibc

test/reg029/reg029.idr+1−1

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

33import System

55-- necessary to find the getenv symbol

6−%dynamic "libm"

6+%dynamic "libm","msvcrt"

88main : IO ()

99main = do

test/reg034/expected+2−2

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

11reg034.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

33reg034.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 @@

11#!/usr/bin/env bash

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

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

33rm -f reg034 *.ibc

test/reg035/expected+2−2

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

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

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

2+ Additive -> Nat

33with

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

4+ Fin 0

test/reg035/run+3−3

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

11#!/usr/bin/env bash

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

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

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

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

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

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

55rm -f *.ibc

test/reg039/expected−1

@@ -1,2 +1 @@

1−Type checking ./reg039.idr

21[3, 2, 1]

test/reg041/expected−1

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

1−Type checking ./ott.idr

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

32Z

test/reg044/expected+4−4

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

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

22Can't unify

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

3+ b = b (Type of Refl)

44with

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

5+ a = b (Expected type)

77Specifically:

88 Can't unify

9− [95mb[0m

9+ b

1010 with

11− [95ma[0m

11+ a

test/reg044/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm -f *.ibc

test/reg054/expected+4−4

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

11reg054.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:

33 Attempting concrete match on polymorphic argument: 0

44reg054.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:

66 No explicit types on left hand side: Char

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

8− [94mMaybe[0m a1

8+ Maybe a1

99with

10− [95ma[0m

10+ a

test/reg054/run+1−1

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

11#!/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 @@

11reg055.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)

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

44Can't match on h x x

55reg055a.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:

77 Attempting concrete match on polymorphic argument: Nothing

88reg055a.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 @@

11#!/usr/bin/env bash

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

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

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

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

44rm -f *.ibc

test/runtest.pl+1−1

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

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

1414

1515 if ( -d $sandbox ) {

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

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

1717 } else {

1818 return "";

1919 }

test/totality007/expected−1

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

1−Type checking ./Totality.idr

21Totality.idr:4:1:

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

43Totality.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

33-- totality007

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

5−opts = "--consolewidth 80"

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

66sourcedir = src

77modules = Totality

test/tutorial006/expected+9−9

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

11tutorial006a.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.:::

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

55 with

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

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

88 Specifically:

99 Can't unify

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

10+ plus n n

1111 with

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

12+ plus n m

1313tutorial006b.idr:10:10:

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

1515Can'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)

1717with

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

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

1919

2020Specifically:

2121 Can't unify

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

22+ plus (S j) (S j)

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

11#!/usr/bin/env bash

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

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

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

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

44rm -f *.ibc

test/unique001/expected+6−6

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

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

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

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

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

6+ Int -> String

77with

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

8+ UniqueType (Int -> String)

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

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

10+ Int -> String

1111with

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

12+ UniqueType (Int -> String)

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

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

14+ UniqueType (Int -> String)

1515with

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

16+ Int -> String

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

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

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

test/unique001/run+6−6

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

11#!/usr/bin/env bash

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

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

33./unique001

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

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

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

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

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

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

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

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

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

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

99rm -f unique001 *.ibc

test/unique002/expected+2−2

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

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

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

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

3+ Int -> String

44with

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

5+ UniqueType (Int -> String)

test/unique002/run+2−2

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

11#!/usr/bin/env bash

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

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

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

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

44rm -f *.ibc

test/unique003/expected+2−2

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

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

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

2+ Int -> String

33with

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

4+ UniqueType (Int -> String)

test/unique003/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm -f *.ibc