b06f843 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2017 from reuleaux/issue2004

Issue2004

commitb06f8432af23147e91ea4a8815925a706016fc6b authorDavid Christiansen <david@davidchristiansen.dk> dateFri 20 Mar 2015, 06:45 (12 years ago) parent6ba74da 5b5da7a

65 files changed+204−131

compare with master

unifiedsplit

idris.cabal+1

@@ -810,6 +810,7 @@ Library

810810 , vector-binary-instances < 0.3

811811 , xml < 1.4

812812 , zlib < 0.6

813+ , safe

813814 Extensions: MultiParamTypeClasses

814815 , DeriveFoldable

815816 , DeriveTraversable

src/Idris/AbsSyntax.hs−6

@@ -606,12 +606,6 @@ setWidth :: ConsoleWidth -> Idris ()

606606setWidth w = do ist <- getIState

607607 put ist { idris_consolewidth = w }

608608

609−renderWidth :: Idris Int

610−renderWidth = do iw <- getWidth

611− case iw of

612− InfinitelyWide -> return 100000000

613− ColsWide n -> return (max n 1)

614− AutomaticWidth -> runIO getScreenWidth

615609

616610

617611

src/Idris/AbsSyntaxTree.hs+24−21

@@ -66,27 +66,27 @@ toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not impleme

6666eInfoNames :: ElabInfo -> [Name]

6767eInfoNames info = map fst (params info) ++ M.keys (inblock info)

6868

69−data IOption = IOption { opt_logLevel :: Int,

70− opt_typecase :: Bool,

71− opt_typeintype :: Bool,

72− opt_coverage :: Bool,

73− opt_showimp :: Bool, -- ^^ show implicits

74− opt_errContext :: Bool,

75− opt_repl :: Bool,

76− opt_verbose :: Bool,

77− opt_nobanner :: Bool,

78− opt_quiet :: Bool,

79− opt_codegen :: Codegen,

80− opt_outputTy :: OutputType,

81− opt_ibcsubdir :: FilePath,

82− opt_importdirs :: [FilePath],

83− opt_triple :: String,

84− opt_cpu :: String,

85− opt_cmdline :: [Opt], -- remember whole command line

86− opt_origerr :: Bool,

87− opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

88− opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

89− opt_optimise :: [Optimisation]

69+data IOption = IOption { opt_logLevel :: Int,

70+ opt_typecase :: Bool,

71+ opt_typeintype :: Bool,

72+ opt_coverage :: Bool,

73+ opt_showimp :: Bool, -- ^^ show implicits

74+ opt_errContext :: Bool,

75+ opt_repl :: Bool,

76+ opt_verbose :: Bool,

77+ opt_nobanner :: Bool,

78+ opt_quiet :: Bool,

79+ opt_codegen :: Codegen,

80+ opt_outputTy :: OutputType,

81+ opt_ibcsubdir :: FilePath,

82+ opt_importdirs :: [FilePath],

83+ opt_triple :: String,

84+ opt_cpu :: String,

85+ opt_cmdline :: [Opt], -- remember whole command line

86+ opt_origerr :: Bool,

87+ opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

88+ opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

89+ opt_optimise :: [Optimisation]

9090 }

9191 deriving (Show, Eq)

9292

@@ -151,6 +151,8 @@ data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

151151data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

152152 | ColsWide Int -- ^ Manually specified - must be positive

153153 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

154+ deriving (Show, Eq)

155+

154156

155157-- | The global state used in the Idris monad

156158data IState = IState {

@@ -467,6 +469,7 @@ data Opt = Filename String

467469 | ShowOrigErr

468470 | AutoWidth -- ^ Automatically adjust terminal width

469471 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

472+ | UseConsoleWidth ConsoleWidth

470473 deriving (Show, Eq)

471474

472475-- Parsed declarations

src/Idris/CmdOptions.hs+30

@@ -11,6 +11,12 @@ import Options.Applicative.Arrows

1111import Data.Char

1212import Data.Maybe

1313

14+import Text.ParserCombinators.ReadP hiding (many, option)

15+

16+import Safe (lastMay)

17+

18+

19+

1420import qualified Text.PrettyPrint.ANSI.Leijen as PP

1521

1622runArgParser :: IO [Opt]

@@ -67,6 +73,7 @@ parser = runA $ proc () -> do

6773 files <- asA (many $ argument (fmap Filename str) (metavar "FILES")) -< ()

6874 A parseVersion >>> A helper -< (flags ++ files)

6975

76+

7077parseFlags :: Parser [Opt]

7178parseFlags = many $

7279 flag' NoBanner (long "nobanner" <> help "Suppress the banner")

@@ -132,6 +139,10 @@ parseFlags = many $

132139 <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

133140 <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

134141 <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")

142+

143+ <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

144+

145+

135146 where

136147 getExt s = case maybeRead s of

137148 Just ext -> ext

@@ -151,3 +162,22 @@ preProcOpts (x:xs) ys = preProcOpts xs (x:ys)

151162parseCodegen :: String -> Codegen

152163parseCodegen "bytecode" = Bytecode

153164parseCodegen cg = Via (map toLower cg)

165+

166+

167+

168+

169+parseConsoleWidth :: Monad m => String -> m ConsoleWidth

170+parseConsoleWidth "auto" = return AutomaticWidth

171+parseConsoleWidth "infinite" = return InfinitelyWide

172+parseConsoleWidth s =

173+ case lastMay (readP_to_S (integerReader) s) of

174+ Just (r, _) -> return $ ColsWide r

175+ _ -> fail $ "Cannot parse: " ++ s

176+

177+

178+

179+integerReader :: ReadP Int

180+integerReader = do

181+ digits <- many1 $ satisfy isDigit

182+ return $ read digits

183+

src/Idris/REPL.hs+12−2

@@ -1518,7 +1518,8 @@ loadInputs inputs toline -- furthest line to read in input source files

15181518

15191519idrisMain :: [Opt] -> Idris ()

15201520idrisMain opts =

1521− do let inputs = opt getFile opts

1521+ do mapM_ setWidth (opt getConsoleWidth opts)

1522+ let inputs = opt getFile opts

15221523 let quiet = Quiet `elem` opts

15231524 let nobanner = NoBanner `elem` opts

15241525 let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts

@@ -1533,6 +1534,7 @@ idrisMain opts =

15331534 let optimise = case opt getOptLevel opts of

15341535 [] -> 2

15351536 xs -> last xs

1537+

15361538 setOptLevel optimise

15371539 let outty = case opt getOutputTy opts of

15381540 [] -> if Interface `elem` opts then

@@ -1554,7 +1556,9 @@ idrisMain opts =

15541556 when (DefaultTotal `elem` opts) $ do i <- getIState

15551557 putIState (i { default_total = True })

15561558 setColourise $ not quiet && last (True : opt getColour opts)

1557− when (not runrepl) $ setWidth InfinitelyWide

1559+

1560+

1561+

15581562 mapM_ addLangExt (opt getLanguageExt opts)

15591563 setREPL runrepl

15601564 setQuiet (quiet || isJust script || not (null immediate))

@@ -1777,6 +1781,12 @@ getCodegen :: Opt -> Maybe Codegen

17771781getCodegen (UseCodegen x) = Just x

17781782getCodegen _ = Nothing

17791783

1784+

1785+getConsoleWidth :: Opt -> Maybe ConsoleWidth

1786+getConsoleWidth (UseConsoleWidth x) = Just x

1787+getConsoleWidth _ = Nothing

1788+

1789+

17801790getExecScript :: Opt -> Maybe String

17811791getExecScript (InterpretScript expr) = Just expr

17821792getExecScript _ = Nothing

test/basic006/run+3−2

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

11#!/usr/bin/env bash

2−idris $@ test020.idr -o test020

3−idris $@ test020a.idr --check --nocolor

3+idris --consolewidth 80 $@ test020.idr -o test020

4+idris --consolewidth 80 $@ test020a.idr --check --nocolor

45./test020

56rm -f test020 *.ibc

test/basic009/run+6−3

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

11#!/usr/bin/env bash

2−idris $@ Main.idr --nocolour --check && echo MAIN-PASS

3−idris $@ Faulty.idr --nocolour --check && echo FAULTY-PASS

4−idris $@ Multiple.idr --nocolour --check && echo MULTIPLE-PASS

3+idris --consolewidth 80 $@ Main.idr --nocolour --check && echo MAIN-PASS

4+idris --consolewidth 80 $@ Faulty.idr --nocolour --check && echo FAULTY-PASS

5+idris --consolewidth 80 $@ Multiple.idr --nocolour --check && echo MULTIPLE-PASS

58rm -f *.ibc B/*.ibc

test/docs001/expected+1−2

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

11Type checking ./docs001.idr

2−*docs001> Type class C

2+Type class C

33 class

55Parameters:

@@ -15,4 +15,3 @@ Instances:

1515 C (D a b)

1616 another instance of class

1717 a -- parameter type

18−*docs001> Bye bye

test/docs001/run+1−1

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

11#!/usr/bin/env bash

2−idris --nobanner --nocolor docs001.idr < input

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

33rm *.ibc

test/docs002/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm *.ibc

test/error003/expected+2−1

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

1−ErrorReflection.idr:68:5:When elaborating right hand side of bad:

1+ErrorReflection.idr:68:5:

2+When elaborating right hand side of bad:

23DSL type error: (t(503) => t'(504)) doesn't match ()

test/error003/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ ErrorReflection.idr --nocolour --check

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

33rm -f *.ibc

test/error004/expected+6−3

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

1−FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:

1+FunErrTest.idr:35:10:

2+When elaborating right hand side of badCadr1:

23When elaborating argument cons1 to function FunErrTest.cadr:

34 Could not prove that [] has at least two elements.

4−FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

5+FunErrTest.idr:38:10:

6+When elaborating right hand side of badCadr2:

57When elaborating argument cons2 to function FunErrTest.cadr:

6− Could not prove that tail [(fromInteger 1)] has at least two elements.

8+ Could not prove that tail [(fromInteger 1)] has at least two

9+ elements.

test/error004/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ FunErrTest.idr --nocolour --check

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

33rm -f *.ibc

test/error005/expected+2−1

@@ -13,7 +13,8 @@ When elaborating argument prf to function Data.Fin.fromInteger:

1313error005.idr:23:24:When elaborating right hand side of b0rken:

1414When elaborating argument prf to function Data.Fin.fromInteger:

1515 When using n as a literal for a Fin 3

16− Could not show that n is less than 3 because n is a bound variable instead of a constant Integer

16+ Could not show that n is less than 3 because n is a bound

17+ variable instead of a constant Integer

1718error005.idr:28:1:When elaborating right hand side of x:

1819When elaborating argument prf to function Data.Fin.fromInteger:

1920 When using 5 as a literal for a Fin 4

test/error005/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ --check --nocolour error005.idr

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

33rm -f *.ibc

test/ffi002/run+1−1

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

11#!/usr/bin/env bash

2−idris --quiet test023.idr -o test023

2+idris --consolewidth 80 --quiet test023.idr -o test023

33rm -f test023 *.ibc

test/literate001/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ test003a.lidr --check

3−idris $@ test003.lidr -o test003

2+idris --consolewidth 80 $@ test003a.lidr --check

3+idris --consolewidth 80 $@ test003.lidr -o test003

44./test003

55rm -f test003 test003.ibc Lit.ibc

test/proof002/expected+2−1

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

1−Reflect.idr:208:38:When elaborating right hand side of testReflect1:

1+Reflect.idr:208:38:

2+When elaborating right hand side of testReflect1:

23When elaborating an application of function Reflect.getJust:

34 Can't unify

45 IsJust (Just x1) (Type of ItIsJust)

test/proof002/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ test030.idr --check --nocolour

3−idris $@ test030a.idr --check --nocolour

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

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

44rm -f *.ibc

test/proof007/expected+2−1

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

1−DefaultArgUnknownName.idr:9:6:When elaborating right hand side of test:

1+DefaultArgUnknownName.idr:9:6:

2+When elaborating right hand side of test:

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

34 No such variable sadgjhsag

test/proof007/run+1−1

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

11#!/usr/bin/env bash

2−idris --check $@ DefaultArgUnknownName.idr

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

33rm -f *.ibc

test/quasiquote003/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ --check NoInfer.idr

2+idris --consolewidth 80 $@ --check NoInfer.idr

33rm -f *.ibc

test/quasiquote004/expected+2−1

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

1−Quasiquote004.idr:50:25:When elaborating right hand side of Quasiquote004.getMeNat':

1+Quasiquote004.idr:50:25:

2+When elaborating right hand side of Quasiquote004.getMeNat':

23Not a Nat goal

test/quasiquote004/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ --check --nocolour Quasiquote004.idr

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

33rm -f *.ibc

test/reg003/run+2−2

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

11#!/usr/bin/env bash

2−idris --check reg003.idr

3−idris --check reg003a.idr

2+idris --consolewidth 80 --check reg003.idr

3+idris --consolewidth 80 --check reg003a.idr

44rm -f *.ibc

test/reg006/expected+2−1

@@ -1 +1,2 @@

1−reg006.idr:17:1:RBTree.lookup is possibly not total due to: RBTree.case block in lookup

1+reg006.idr:17:1:

2+RBTree.lookup is possibly not total due to: RBTree.case block in lookup

test/reg006/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ reg006.idr --check

2+idris --consolewidth 80 $@ reg006.idr --check

33rm -f *.ibc

test/reg007/run+1−1

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

11#!/usr/bin/env bash

2−idris --nocolour --check $@ reg007.lidr

2+idris --consolewidth 80 --nocolour --check $@ reg007.lidr

33rm -f *.ibc

test/reg010/expected+2−1

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

1−reg010.idr:5:15:When elaborating left hand side of with block in usubst.unsafeSubst:

1+reg010.idr:5:15:

2+When elaborating left hand side of with block in usubst.unsafeSubst:

23Can't match on with block in usubst.unsafeSubst warg a P x x px

test/reg010/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ reg010.idr --check --nocolour

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

test/reg018/expected+10−5

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

1−reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

2−reg018a.idr:21:1:conat.loopForever is possibly not total due to: conat.minusCoNat

3−reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

4−reg018c.idr:21:1:CodataTest.inf is possibly not total due to: with block in CodataTest.inf

5−reg018d.idr:8:1:Main.pull is not total as there are missing cases

1+reg018a.idr:16:1:

2+conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

3+reg018a.idr:21:1:

4+conat.loopForever is possibly not total due to: conat.minusCoNat

5+reg018b.idr:8:1:

6+A.showB is possibly not total due to recursive path A.showB

7+reg018c.idr:21:1:

8+CodataTest.inf is possibly not total due to: with block in CodataTest.inf

9+reg018d.idr:8:1:

10+Main.pull is not total as there are missing cases

test/reg018/run+4−4

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

11#!/usr/bin/env bash

2−idris $@ reg018a.idr --check

3−idris $@ reg018b.idr --check

4−idris $@ reg018c.idr --check

5−idris $@ reg018d.idr --check

2+idris --consolewidth 80 $@ reg018a.idr --check

3+idris --consolewidth 80 $@ reg018b.idr --check

4+idris --consolewidth 80 $@ reg018c.idr --check

5+idris --consolewidth 80 $@ reg018d.idr --check

66rm *.ibc

test/reg023/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ reg023.idr --check

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

33rm -f *.ibc

test/reg027/expected+2−1

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

11<<int fn>>

226

3−reg027a.idr:9:10:Overlapping instance: Show (Int -> a) already defined

3+reg027a.idr:9:10:

4+Overlapping instance: Show (Int -> a) already defined

test/reg027/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ reg027.idr -o reg027

2+idris --consolewidth 80 $@ reg027.idr -o reg027

33./reg027

4−idris $@ reg027a.idr --check

4+idris --consolewidth 80 $@ reg027a.idr --check

55rm -f reg027 *.ibc

test/reg028/expected+4−2

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

1−reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad

2−reg028a.idr:11:1:tbad.qsort' is possibly not total due to: with block in tbad.qsort'

1+reg028.idr:5:1:

2+tbad.bad is possibly not total due to: with block in tbad.bad

3+reg028a.idr:11:1:

4+tbad.qsort' is possibly not total due to: with block in tbad.qsort'

test/reg028/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ reg028.idr --check

3−idris $@ reg028a.idr --check

2+idris --consolewidth 80 $@ reg028.idr --check

3+idris --consolewidth 80 $@ reg028a.idr --check

44rm -f *.ibc

test/reg034/run+1−1

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

11#!/usr/bin/env bash

2−idris --check reg034.idr

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

33rm -f reg034 *.ibc

test/reg035/run+3−3

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

11#!/usr/bin/env bash

2−idris --check reg035.idr

3−idris --check reg035a.lidr

4−idris --check reg035b.idr

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

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

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

55rm -f *.ibc

test/reg044/run+1−1

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

11#!/usr/bin/env bash

2−idris reg044.idr --check

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

33rm -f *.ibc

test/reg049/run+1−1

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

11#!/usr/bin/env bash

2−idris --nocolour --check $@ reg049.idr

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

33rm -f *.ibc

test/reg054/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ reg054.idr --check

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

test/reg055/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ reg055.idr --check

3−idris $@ reg055a.idr --check

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

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

44rm -f *.ibc

test/reg056/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ reg056.idr -o reg056

2+idris --consolewidth 80 $@ reg056.idr -o reg056

33rm -f *.ibc

test/totality001/expected+6−3

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

1−test010.idr:15:1:Main.foo is possibly not total due to: Main.MkBad

2−test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad

3−test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad

1+test010.idr:15:1:

2+Main.foo is possibly not total due to: Main.MkBad

3+test010a.idr:9:1:

4+main.bar is possibly not total due to: main.MkBad

5+test010b.idr:9:1:

6+main.bar is possibly not total due to: main.MkBad

test/totality001/run+3−3

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

11#!/usr/bin/env bash

2−idris $@ --check test010.idr

3−idris $@ --check test010a.idr

4−idris $@ --check test010b.idr

2+idris --consolewidth 80 $@ --check test010.idr

3+idris --consolewidth 80 $@ --check test010a.idr

4+idris --consolewidth 80 $@ --check test010b.idr

66rm -f *.ibc

test/totality002/expected+4−2

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

1−test017a.idr:7:1:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

2−test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo

1+test017a.idr:7:1:

2+scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

3+test017b.idr:4:1:

4+foo.foo is possibly not total due to recursive path foo.foo

test/totality002/run+3−3

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

11#!/usr/bin/env bash

2−idris $@ --check test017.idr

3−idris $@ --check test017a.idr

4−idris $@ --check test017b.idr

2+idris --consolewidth 80 $@ --check test017.idr

3+idris --consolewidth 80 $@ --check test017a.idr

4+idris --consolewidth 80 $@ --check test017b.idr

55rm -f *.ibc

test/totality003/expected+2−1

@@ -1 +1,2 @@

1−totality003a.idr:5:1:smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort

1+totality003a.idr:5:1:

2+smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort

test/totality003/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ totality003.idr --check

3−idris $@ totality003a.idr --check

2+idris --consolewidth 80 $@ totality003.idr --check

3+idris --consolewidth 80 $@ totality003a.idr --check

44rm -f *.ibc

test/totality004/expected+4−2

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

11[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

2−totality004a.idr:13:1:Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

3−totality004a.idr:24:1:Main.main is possibly not total due to: Main.process

2+totality004a.idr:13:1:

3+Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

4+totality004a.idr:24:1:

5+Main.main is possibly not total due to: Main.process

test/totality004/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ totality004.idr -o totality004

2+idris --consolewidth 80 $@ totality004.idr -o totality004

33./totality004

4−idris $@ --check totality004a.idr

4+idris --consolewidth 80 $@ --check totality004a.idr

55rm -f totality004 *.ibc

test/totality006/expected+4−2

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

1−totality006.idr:8:1:Main.prf is not total as there are missing cases

1+totality006.idr:8:1:

2+Main.prf is not total as there are missing cases

23totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case

3−totality006b.idr:10:1:totality006b.blargh is not total as there are missing cases

4+totality006b.idr:10:1:

5+totality006b.blargh is not total as there are missing cases

test/totality006/run+3−3

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

11#!/usr/bin/env bash

2−idris $@ totality006.idr --check

3−idris $@ totality006a.idr --check

4−idris $@ totality006b.idr --check

2+idris --consolewidth 80 $@ totality006.idr --check

3+idris --consolewidth 80 $@ totality006a.idr --check

4+idris --consolewidth 80 $@ totality006b.idr --check

55rm -f *.ibc

test/totality007/expected+2−1

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

11Type checking ./Totality.idr

2−Totality.idr:4:1:Totality.foo is not total as there are missing cases

2+Totality.idr:4:1:

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

34Totality.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 = ""

5+opts = "--consolewidth 80"

66sourcedir = src

77modules = Totality

test/totality008/expected+2−1

@@ -1 +1,2 @@

1−totality008.idr:7:1:Main.ElimT is possibly not total due to: Main.c2

1+totality008.idr:7:1:

2+Main.ElimT is possibly not total due to: Main.c2

test/totality008/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ totality008.idr --check

2+idris --consolewidth 80 $@ totality008.idr --check

33rm -f *.ibc

test/tutorial006/expected+2−1

@@ -10,7 +10,8 @@ When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::

1010 [92mplus[0m [95mn[0m [95mn[0m

1111 with

1212 [92mplus[0m [95mn[0m [95mm[0m

13−tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

13+tutorial006b.idr:10:10:

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

1415Can't unify

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

1617with

test/tutorial006/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ tutorial006a.idr --check

3−idris $@ tutorial006b.idr --check

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

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

44rm -f *.ibc

test/unique001/expected+2−1

@@ -17,4 +17,5 @@ with

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

20−unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not

20+unique001e.idr:3:10:

21+Constructor Main.Nil has a UniqueType, but the data type does not

test/unique001/run+6−6

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

11#!/usr/bin/env bash

2−idris $@ unique001.idr -o unique001

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

33./unique001

4−idris $@ unique001a.idr --check

5−idris $@ unique001b.idr --check

6−idris $@ unique001c.idr --check

7−idris $@ unique001d.idr --check

8−idris $@ unique001e.idr --check

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

99rm -f unique001 *.ibc

test/unique002/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ unique002.idr --check

3−idris $@ unique002a.idr --check

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

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

44rm -f *.ibc

test/unique003/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ unique003.idr --check

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

33rm -f *.ibc