b06f843 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

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

810 , vector-binary-instances < 0.3

811 , xml < 1.4

812 , zlib < 0.6

813+ , safe

813 Extensions: MultiParamTypeClasses

814 Extensions: MultiParamTypeClasses

814 , DeriveFoldable

815 , DeriveFoldable

815 , DeriveTraversable

816 , DeriveTraversable

src/Idris/AbsSyntax.hs−6

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

606setWidth w = do ist <- getIState

607 put ist { idris_consolewidth = w }

608

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

615

609

616

610

617

611

src/Idris/AbsSyntaxTree.hs+24−21

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

66eInfoNames :: ElabInfo -> [Name]

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

68

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

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

70− opt_typecase :: Bool,

70+ opt_typecase :: Bool,

71− opt_typeintype :: Bool,

71+ opt_typeintype :: Bool,

72− opt_coverage :: Bool,

72+ opt_coverage :: Bool,

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

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

74− opt_errContext :: Bool,

74+ opt_errContext :: Bool,

75− opt_repl :: Bool,

75+ opt_repl :: Bool,

76− opt_verbose :: Bool,

76+ opt_verbose :: Bool,

77− opt_nobanner :: Bool,

77+ opt_nobanner :: Bool,

78− opt_quiet :: Bool,

78+ opt_quiet :: Bool,

79− opt_codegen :: Codegen,

79+ opt_codegen :: Codegen,

80− opt_outputTy :: OutputType,

80+ opt_outputTy :: OutputType,

81− opt_ibcsubdir :: FilePath,

81+ opt_ibcsubdir :: FilePath,

82− opt_importdirs :: [FilePath],

82+ opt_importdirs :: [FilePath],

83− opt_triple :: String,

83+ opt_triple :: String,

84− opt_cpu :: String,

84+ opt_cpu :: String,

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

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

86− opt_origerr :: Bool,

86+ opt_origerr :: Bool,

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

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

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

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

89− opt_optimise :: [Optimisation]

89+ opt_optimise :: [Optimisation]

90 }

91 deriving (Show, Eq)

92

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

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

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

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

154+ deriving (Show, Eq)

155+

154

156

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

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

156data IState = IState {

158data IState = IState {

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

467 | ShowOrigErr

469 | ShowOrigErr

468 | AutoWidth -- ^ Automatically adjust terminal width

470 | AutoWidth -- ^ Automatically adjust terminal width

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

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

472+ | UseConsoleWidth ConsoleWidth

470 deriving (Show, Eq)

473 deriving (Show, Eq)

471

474

472-- Parsed declarations

475-- Parsed declarations

src/Idris/CmdOptions.hs+30

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

11import Data.Char

12import Data.Maybe

13

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

15+

16+import Safe (lastMay)

17+

18+

19+

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

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

15

21

16runArgParser :: IO [Opt]

22runArgParser :: IO [Opt]

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

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

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

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

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

69

75

76+

70parseFlags :: Parser [Opt]

77parseFlags :: Parser [Opt]

71parseFlags = many $

78parseFlags = many $

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

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

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

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

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

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

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

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

141 <|> 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+

135 where

146 where

136 getExt s = case maybeRead s of

147 getExt s = case maybeRead s of

137 Just ext -> ext

148 Just ext -> ext

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

151parseCodegen :: String -> Codegen

162parseCodegen :: String -> Codegen

152parseCodegen "bytecode" = Bytecode

163parseCodegen "bytecode" = Bytecode

153parseCodegen cg = Via (map toLower cg)

164parseCodegen 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

1518

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

1520idrisMain opts =

1521+ do mapM_ setWidth (opt getConsoleWidth opts)

1521− do let inputs = opt getFile opts

1522+ let inputs = opt getFile opts

1522 let quiet = Quiet `elem` opts

1523 let quiet = Quiet `elem` opts

1523 let nobanner = NoBanner `elem` opts

1524 let nobanner = NoBanner `elem` opts

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

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

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

1533 let optimise = case opt getOptLevel opts of

1534 let optimise = case opt getOptLevel opts of

1534 [] -> 2

1535 [] -> 2

1535 xs -> last xs

1536 xs -> last xs

1537+

1536 setOptLevel optimise

1538 setOptLevel optimise

1537 let outty = case opt getOutputTy opts of

1539 let outty = case opt getOutputTy opts of

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

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

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

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

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

1555 putIState (i { default_total = True })

1557 putIState (i { default_total = True })

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

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

1557− when (not runrepl) $ setWidth InfinitelyWide

1559+

1560+

1561+

1558 mapM_ addLangExt (opt getLanguageExt opts)

1562 mapM_ addLangExt (opt getLanguageExt opts)

1559 setREPL runrepl

1563 setREPL runrepl

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

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

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

1777getCodegen (UseCodegen x) = Just x

1781getCodegen (UseCodegen x) = Just x

1778getCodegen _ = Nothing

1782getCodegen _ = Nothing

1779

1783

1784+

1785+getConsoleWidth :: Opt -> Maybe ConsoleWidth

1786+getConsoleWidth (UseConsoleWidth x) = Just x

1787+getConsoleWidth _ = Nothing

1788+

1789+

1780getExecScript :: Opt -> Maybe String

1790getExecScript :: Opt -> Maybe String

1781getExecScript (InterpretScript expr) = Just expr

1791getExecScript (InterpretScript expr) = Just expr

1782getExecScript _ = Nothing

1792getExecScript _ = Nothing

test/basic006/run+3−2

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

1#!/usr/bin/env bash

2+

2−idris $@ test020.idr -o test020

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

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

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

4./test020

5./test020

5rm -f test020 *.ibc

6rm -f test020 *.ibc

test/basic009/run+6−3

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

1#!/usr/bin/env bash

2+

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

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

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

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

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

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

6+

7+

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

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

test/docs001/expected+1−2

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

1Type checking ./docs001.idr

2−*docs001> Type class C

2+Type class C

3 class

4

5Parameters:

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

15 C (D a b)

16 another instance of class

17 a -- parameter type

18−*docs001> Bye bye

test/docs001/run+1−1

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

1#!/usr/bin/env bash

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

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

3rm *.ibc

test/docs002/run+1−1

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

1#!/usr/bin/env bash

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

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

3rm *.ibc

test/error003/expected+2−1

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

1+ErrorReflection.idr:68:5:

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

2+When elaborating right hand side of bad:

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

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

test/error003/run+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/error004/expected+6−3

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

1+FunErrTest.idr:35:10:

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

2+When elaborating right hand side of badCadr1:

2When elaborating argument cons1 to function FunErrTest.cadr:

3When elaborating argument cons1 to function FunErrTest.cadr:

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

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

5+FunErrTest.idr:38:10:

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

6+When elaborating right hand side of badCadr2:

5When elaborating argument cons2 to function FunErrTest.cadr:

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/error005/expected+2−1

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

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

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

15 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

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

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

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

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

19 When using 5 as a literal for a Fin 4

20 When using 5 as a literal for a Fin 4

test/error005/run+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/ffi002/run+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f test023 *.ibc

test/literate001/run+2−2

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

1#!/usr/bin/env bash

2−idris $@ test003a.lidr --check

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

3−idris $@ test003.lidr -o test003

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

4./test003

5rm -f test003 test003.ibc Lit.ibc

test/proof002/expected+2−1

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

1+Reflect.idr:208:38:

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

2+When elaborating right hand side of testReflect1:

2When elaborating an application of function Reflect.getJust:

3When elaborating an application of function Reflect.getJust:

3 Can't unify

4 Can't unify

4 IsJust (Just x1) (Type of ItIsJust)

5 IsJust (Just x1) (Type of ItIsJust)

test/proof002/run+2−2

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

1#!/usr/bin/env bash

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

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

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

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

4rm -f *.ibc

test/proof007/expected+2−1

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

1+DefaultArgUnknownName.idr:9:6:

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

2+When elaborating right hand side of test:

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

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

3 No such variable sadgjhsag

4 No such variable sadgjhsag

test/proof007/run+1−1

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

1#!/usr/bin/env bash

2−idris --check $@ DefaultArgUnknownName.idr

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

3rm -f *.ibc

test/quasiquote003/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ --check NoInfer.idr

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

3rm -f *.ibc

test/quasiquote004/expected+2−1

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

1+Quasiquote004.idr:50:25:

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

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

2Not a Nat goal

3Not a Nat goal

test/quasiquote004/run+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/reg003/run+2−2

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

1#!/usr/bin/env bash

2−idris --check reg003.idr

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

3−idris --check reg003a.idr

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

4rm -f *.ibc

test/reg006/expected+2−1

@@ -1 +1,2 @@

1+reg006.idr:17:1:

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

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

test/reg006/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ reg006.idr --check

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

3rm -f *.ibc

test/reg007/run+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/reg010/expected+2−1

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

1+reg010.idr:5:15:

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

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

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

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

test/reg010/run+1−1

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

1#!/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:

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

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

3+reg018a.idr:21:1:

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

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

5+reg018b.idr:8:1:

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

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

7+reg018c.idr:21:1:

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

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

9+reg018d.idr:8:1:

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

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

test/reg018/run+4−4

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

1#!/usr/bin/env bash

2−idris $@ reg018a.idr --check

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

3−idris $@ reg018b.idr --check

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

4−idris $@ reg018c.idr --check

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

5−idris $@ reg018d.idr --check

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

6rm *.ibc

test/reg023/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ reg023.idr --check

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

3rm -f *.ibc

test/reg027/expected+2−1

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

1<<int fn>>

26

3+reg027a.idr:9:10:

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

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

test/reg027/run+2−2

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

1#!/usr/bin/env bash

2−idris $@ reg027.idr -o reg027

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

3./reg027

4−idris $@ reg027a.idr --check

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

5rm -f reg027 *.ibc

test/reg028/expected+4−2

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

1+reg028.idr:5:1:

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

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

3+reg028a.idr:11:1:

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

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

test/reg028/run+2−2

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

1#!/usr/bin/env bash

2−idris $@ reg028.idr --check

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

3−idris $@ reg028a.idr --check

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

4rm -f *.ibc

test/reg034/run+1−1

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

1#!/usr/bin/env bash

2−idris --check reg034.idr

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

3rm -f reg034 *.ibc

test/reg035/run+3−3

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

1#!/usr/bin/env bash

2−idris --check reg035.idr

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

3−idris --check reg035a.lidr

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

4−idris --check reg035b.idr

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

5rm -f *.ibc

test/reg044/run+1−1

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

1#!/usr/bin/env bash

2−idris reg044.idr --check

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

3rm -f *.ibc

test/reg049/run+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/reg054/run+1−1

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

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

1#!/usr/bin/env bash

2−idris $@ reg055.idr --check

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

3−idris $@ reg055a.idr --check

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

4rm -f *.ibc

5

test/reg056/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ reg056.idr -o reg056

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

3rm -f *.ibc

test/totality001/expected+6−3

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

1+test010.idr:15:1:

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

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

3+test010a.idr:9:1:

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

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

5+test010b.idr:9:1:

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

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

test/totality001/run+3−3

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

1#!/usr/bin/env bash

2−idris $@ --check test010.idr

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

3−idris $@ --check test010a.idr

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

4−idris $@ --check test010b.idr

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

5

6rm -f *.ibc

test/totality002/expected+4−2

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

1+test017a.idr:7:1:

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

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

3+test017b.idr:4:1:

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

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

test/totality002/run+3−3

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

1#!/usr/bin/env bash

2−idris $@ --check test017.idr

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

3−idris $@ --check test017a.idr

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

4−idris $@ --check test017b.idr

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

5rm -f *.ibc

test/totality003/expected+2−1

@@ -1 +1,2 @@

1+totality003a.idr:5:1:

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

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

1#!/usr/bin/env bash

2−idris $@ totality003.idr --check

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

3−idris $@ totality003a.idr --check

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

4rm -f *.ibc

test/totality004/expected+4−2

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

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

2+totality004a.idr:13:1:

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

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

4+totality004a.idr:24:1:

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

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

test/totality004/run+2−2

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

1#!/usr/bin/env bash

2−idris $@ totality004.idr -o totality004

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

3./totality004

4−idris $@ --check totality004a.idr

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

5rm -f totality004 *.ibc

test/totality006/expected+4−2

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

1+totality006.idr:8:1:

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

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

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

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

4+totality006b.idr:10:1:

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

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

test/totality006/run+3−3

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

1#!/usr/bin/env bash

2−idris $@ totality006.idr --check

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

3−idris $@ totality006a.idr --check

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

4−idris $@ totality006b.idr --check

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

5rm -f *.ibc

test/totality007/expected+2−1

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

1Type checking ./Totality.idr

2+Totality.idr:4:1:

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

3+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

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

5+opts = "--consolewidth 80"

6sourcedir = src

7modules = Totality

test/totality008/expected+2−1

@@ -1 +1,2 @@

1+totality008.idr:7:1:

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

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

test/totality008/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ totality008.idr --check

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

3rm -f *.ibc

test/tutorial006/expected+2−1

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

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

11 with

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

13+tutorial006b.idr:10:10:

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

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

14Can't unify

15Can't unify

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

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

16with

17with

test/tutorial006/run+2−2

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

1#!/usr/bin/env bash

2−idris $@ tutorial006a.idr --check

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

3−idris $@ tutorial006b.idr --check

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

4rm -f *.ibc

test/unique001/expected+2−1

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

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

20+unique001e.idr:3:10:

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

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

test/unique001/run+6−6

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

1#!/usr/bin/env bash

2−idris $@ unique001.idr -o unique001

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

3./unique001

4−idris $@ unique001a.idr --check

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

5−idris $@ unique001b.idr --check

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

6−idris $@ unique001c.idr --check

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

7−idris $@ unique001d.idr --check

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

8−idris $@ unique001e.idr --check

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

9rm -f unique001 *.ibc

test/unique002/run+2−2

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

1#!/usr/bin/env bash

2−idris $@ unique002.idr --check

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

3−idris $@ unique002a.idr --check

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

4rm -f *.ibc

test/unique003/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ unique003.idr --check

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

3rm -f *.ibc