git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4246 from eraserhd/pretty-warnings
45a3f93Jason Felice
CHANGELOG.md+15−3
compare with master
unifiedsplit
@@ -83,9 +83,21 @@
83 as they were given in the source files.
83 as they were given in the source files.
84+ Backslash, braces and percent symbols are now correctly pretty printed
84+ Backslash, braces and percent symbols are now correctly pretty printed
85 in LaTeX.
85 in LaTeX.
86−+ Parse errors have a new format, similar to GHC 8.2's default, due to a
86++ Errors and warnings now consistently have the following format:
87+ ```idris
88+ reg068.idr:1:6-8:
89+ |
90+ 1 | data nat : Type where --error
91+ | ~~~
92+ Main.nat has a name which may be implicitly bound.
93+ This is likely to lead to problems!
94+ ```
95+ The code is highlighted when highlighting information is available. How
96+ much highlighting information is available depends on where the error
97+ occurred.
87− switch from Trifecta to Megaparsec for parsing. This could possibly cause
98++ The parser provider has been switched from Trifecta to Megaparsec. This
88− some subtle deviations in parsing from previous versions of Idris.
99+ could possibly cause some subtle deviations in parsing from previous
100+ versions of Idris.
89+ Many more errors now report beginning *and* ending position (which may be
101+ Many more errors now report beginning *and* ending position (which may be
90 on different lines), instead of just a single point. The format is
102 on different lines), instead of just a single point. The format is
91 `Foo.idr:9:7-15:` if ending column is on the same line or
103 `Foo.idr:9:7-15:` if ending column is on the same line or
src/Idris/Elab/Clause.hs+3−4
@@ -28,7 +28,7 @@ import Idris.Elab.Type
28import Idris.Elab.Utils
28import Idris.Elab.Utils
29import Idris.Error
29import Idris.Error
30import Idris.Options
30import Idris.Options
31−import Idris.Output (iputStrLn, pshow, sendHighlighting)
31+import Idris.Output (iWarn, pshow, sendHighlighting)
32import Idris.PartialEval
32import Idris.PartialEval
33import Idris.Termination
33import Idris.Termination
34import Idris.Transforms
34import Idris.Transforms
@@ -205,9 +205,8 @@ elabClauses info' fc opts n_in cs =
205 case tree of
205 case tree of
206 CaseDef _ _ [] -> return ()
206 CaseDef _ _ [] -> return ()
207 CaseDef _ _ xs -> mapM_ (\x ->
207 CaseDef _ _ xs -> mapM_ (\x ->
208− iputStrLn $ show fc ++
209− ":warning - Unreachable case: " ++
208+ iWarn fc $ text "Unreachable case:" </> text (show (delab ist x))
210− show (delab ist x)) xs
209+ ) xs
211 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
210 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
212 let defaultcase = if knowncovering
211 let defaultcase = if knowncovering
213 then STerm Erased
212 then STerm Erased
src/Idris/Main.hs+3−3
@@ -195,7 +195,7 @@ idrisMain opts =
195 mapM_ (\str -> do ist <- getIState
195 mapM_ (\str -> do ist <- getIState
196 c <- colourise
196 c <- colourise
197 case parseExpr ist str of
197 case parseExpr ist str of
198− Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err
198+ Left err -> do emitWarning err
199 runIO $ exitWith (ExitFailure 1)
199 runIO $ exitWith (ExitFailure 1)
200 Right e -> process "" (Eval e))
200 Right e -> process "" (Eval e))
201 exprs
201 exprs
@@ -272,7 +272,7 @@ execScript :: String -> Idris ()
272execScript expr = do i <- getIState
272execScript expr = do i <- getIState
273 c <- colourise
273 c <- colourise
274 case parseExpr i expr of
274 case parseExpr i expr of
275− Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err
275+ Left err -> do emitWarning err
276 runIO $ exitWith (ExitFailure 1)
276 runIO $ exitWith (ExitFailure 1)
277 Right term -> do ctxt <- getContext
277 Right term -> do ctxt <- getContext
278 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term
278 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term
@@ -299,7 +299,7 @@ initScript = do script <- runIO $ getIdrisInitScript
299 runInit h
299 runInit h
300 processLine i cmd input clr =
300 processLine i cmd input clr =
301 case parseCmd i input cmd of
301 case parseCmd i input cmd of
302− Left err -> runIO . print . fixColour clr . parseErrorDoc $ err
302+ Left err -> emitWarning err
303 Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"
303 Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"
304 Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
304 Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
305 Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
305 Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
src/Idris/Output.hs+140−14
@@ -9,12 +9,13 @@ Maintainer : The Idris Community.
9{-# LANGUAGE FlexibleInstances #-}
9{-# LANGUAGE FlexibleInstances #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11
11
12−module Idris.Output (clearHighlights, idemodePutSExp, iPrintError, iPrintFunTypes,
12+module Idris.Output (clearHighlights, emitWarning, formatMessage, idemodePutSExp,
13− iPrintResult, iPrintTermWithType, iputGoal, iputStr, iputStrLn,
13+ iPrintError, iPrintFunTypes, iPrintResult, iPrintTermWithType,
14+ iputGoal, iputStr, iputStrLn, iRender, iRenderError,
14− iRender, iRenderError, iRenderOutput, iRenderResult, iWarn,
15+ iRenderOutput, iRenderResult, iWarn, prettyDocumentedIst,
15− prettyDocumentedIst, printUndefinedNames, pshow, renderExternal,
16+ printUndefinedNames, pshow, renderExternal, sendHighlighting,
16− sendHighlighting, sendParserHighlighting, warnTotality,
17+ sendParserHighlighting, warnTotality, writeHighlights,
17− writeHighlights) where
18+ OutputDoc(..), Message(..)) where
18
19
19import Idris.AbsSyntax
20import Idris.AbsSyntax
20import Idris.Colours (hEndColourise, hStartColourise)
21import Idris.Colours (hEndColourise, hStartColourise)
@@ -31,13 +32,15 @@ import Util.System (isATTY)
31
32
32import Prelude hiding ((<$>))
33import Prelude hiding ((<$>))
33
34
35+import Control.Arrow (first)
34import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
36import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
35import Data.List (intersperse, nub)
37import Data.List (intersperse, nub)
36−import Data.Maybe (fromMaybe)
38+import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
37import System.Console.Haskeline.MonadException (MonadException(controlIO),
39import System.Console.Haskeline.MonadException (MonadException(controlIO),
38 RunIO(RunIO))
40 RunIO(RunIO))
39import System.FilePath (replaceExtension)
41import System.FilePath (replaceExtension)
40import System.IO (Handle, hPutStr, hPutStrLn)
42import System.IO (Handle, hPutStr, hPutStrLn)
43+import System.IO.Error (tryIOError)
41
44
42instance MonadException m => MonadException (ExceptT Err m) where
45instance MonadException m => MonadException (ExceptT Err m) where
43 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
46 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
@@ -49,18 +52,141 @@ pshow ist err = displayDecorated (consoleDecorate ist) .
49 renderPretty 1.0 80 .
52 renderPretty 1.0 80 .
50 fmap (fancifyAnnots ist True) $ pprintErr ist err
53 fmap (fancifyAnnots ist True) $ pprintErr ist err
51
54
52−iWarn :: FC -> Doc OutputAnnotation -> Idris ()
55+type OutputDoc = Doc OutputAnnotation
56+
57+class Message a where
58+ messageExtent :: a -> FC
59+ messageText :: a -> OutputDoc
60+ messageSource :: a -> Maybe String
61+
62+data Ann = AText String | ATagged OutputAnnotation Ann | ASplit Ann Ann
63+
64+data SimpleWarning = SimpleWarning FC OutputDoc
65+instance Message SimpleWarning where
66+ messageExtent (SimpleWarning extent _) = extent
67+ messageText (SimpleWarning _ msg) = msg
68+ messageSource _ = Nothing
69+
70+formatMessage :: Message w => w -> Idris OutputDoc
71+formatMessage w = do
72+ i <- getIState
73+ maybeSource <- case messageSource w of
74+ Just src -> pure (Just src)
75+ Nothing -> readSource fc
76+ let maybeFormattedSource = maybeSource >>= layoutSource fc (idris_highlightedRegions i)
77+ return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)
78+ where
79+ fc :: FC
80+ fc = messageExtent w
81+
82+ layoutFC :: FC -> OutputDoc
83+ layoutFC fc@(FC fn _ _) | fn /= "" = text (show $ fc) <> colon
84+ layoutFC _ = empty
85+
86+ readSource :: FC -> Idris (Maybe String)
87+ readSource (FC fn _ _) = do
88+ result <- runIO $ tryIOError (readFile fn)
89+ case result of
90+ Left _ -> pure Nothing
91+ Right v -> pure (Just v)
92+ readSource _ = pure Nothing
93+
94+ layoutSource :: FC -> [(FC, OutputAnnotation)] -> String -> Maybe OutputDoc
95+ layoutSource (FC fn (si, sj) (ei, ej)) highlights src =
96+ if haveSource
97+ then Just source
98+ else Nothing
99+ where
100+ sourceLine :: Maybe String
101+ sourceLine = listToMaybe . drop (si - 1) . (++ ["<end of file>"]) . lines $ src
102+
103+ haveSource :: Bool
104+ haveSource = isJust sourceLine
105+
106+ line1 :: OutputDoc
107+ line1 = text $ replicate (length (show si)) ' ' ++ " |"
108+
109+ lineFC :: FC
110+ lineFC = FC fn (si, 1) (si, length (fromJust sourceLine))
111+
112+ intersects :: FC -> FC -> Bool
113+ intersects (FC fn1 s1 e1) (FC fn2 s2 e2)
114+ | fn1 /= fn2 = False
115+ | e1 < s2 = False
116+ | e2 < s1 = False
117+ | otherwise = True
118+ intersects _ _ = False
119+
120+ intersection :: FC -> FC -> FC
121+ intersection fc1@(FC fn1 s1 e1) fc2@(FC _ s2 e2)
122+ | intersects fc1 fc2 = FC fn1 (max s1 s2) (min e1 e2)
123+ | otherwise = NoFC
124+ intersection _ _ = NoFC
125+
126+ width :: Ann -> Int
127+ width (AText s) = length s
128+ width (ATagged _ n) = width n
129+ width (ASplit l r) = width l + width r
130+
131+ sourceDoc :: Ann -> OutputDoc
132+ sourceDoc (AText s) = text s
133+ sourceDoc (ATagged a n) = annotate a (sourceDoc n)
134+ sourceDoc (ASplit l r) = sourceDoc l <> sourceDoc r
135+
136+ insertAnnotation :: ((Int, Int), OutputAnnotation) -> Ann -> Ann
137+ insertAnnotation ((sj, ej), oa) (ATagged tag n) = ATagged tag (insertAnnotation ((sj, ej), oa) n)
138+ insertAnnotation ((sj, ej), oa) (ASplit l r)
139+ | w <- width l = ASplit (insertAnnotation ((sj, ej), oa) l) (insertAnnotation ((sj - w, ej - w), oa) r)
140+ insertAnnotation ((sj, ej), oa) a@(AText t)
141+ | sj <= 1, ej >= width a = ATagged oa a
142+ | sj > 1, sj <= width a = ASplit (AText $ take (sj - 1) t) (insertAnnotation ((1, ej - sj + 1), oa) (AText $ drop (sj - 1) t))
143+ | sj == 1, ej >= 1, ej < width a = ASplit (insertAnnotation ((1, ej), oa) (AText $ take ej t)) (AText $ drop ej t)
144+ | otherwise = a
145+
146+ highlightedSource :: OutputDoc
147+ highlightedSource = sourceDoc .
148+ foldr insertAnnotation (AText $ fromJust sourceLine) .
149+ map (\(FC _ (_, sj) (_, ej), ann) -> ((sj, ej), ann)) .
150+ map (first (intersection lineFC)) .
151+ filter (intersects lineFC . fst) $
152+ highlights
153+
154+ line2 :: OutputDoc
155+ line2 = text (show si ++ " | ") <> highlightedSource
156+
157+ indicator :: OutputDoc
158+ indicator = text (replicate (end - sj + 1) ch) <> ellipsis
159+ where
160+ (end, ch, ellipsis) = case (si == ei, sj == ej) of
161+ (True , True ) -> (ej, '^', empty)
162+ (True , False) -> (ej, '~', empty)
163+ (False, _ ) -> (length (fromJust sourceLine), '~', text " ...")
164+
165+ line3 :: OutputDoc
166+ line3 = line1 <> text (replicate sj ' ') <> indicator
167+
168+ source :: OutputDoc
169+ source = line1 <$$> line2 <$$> line3
170+ layoutSource _ _ _ = Nothing
171+
172+ layoutMessage :: OutputDoc -> Maybe OutputDoc -> OutputDoc -> OutputDoc
173+ layoutMessage loc (Just src) err = loc <$$> src <$$> err <$$> empty
174+ layoutMessage loc Nothing err = loc </> err
175+
176+iWarn :: FC -> OutputDoc -> Idris ()
53−iWarn fc err =
177+iWarn fc err = emitWarning $ SimpleWarning fc err
178+
179+emitWarning :: Message w => w -> Idris ()
180+emitWarning w =
54 do i <- getIState
181 do i <- getIState
55 case idris_outputmode i of
182 case idris_outputmode i of
56 RawOutput h ->
183 RawOutput h ->
184+ do formattedErr <- formatMessage w
57− do err' <- iRender . fmap (fancifyAnnots i True) $
185+ err' <- iRender . fmap (fancifyAnnots i True) $ formattedErr
58− case fc of
59− FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err
60− _ -> err
61 hWriteDoc h i err'
186 hWriteDoc h i err'
62 IdeMode n h ->
187 IdeMode n h ->
63− do err' <- iRender . fmap (fancifyAnnots i True) $ err
188+ do err' <- iRender . fmap (fancifyAnnots i True) $ messageText w
189+ let fc = messageExtent w
64 let (str, spans) = displaySpans err'
190 let (str, spans) = displaySpans err'
65 runIO . hPutStrLn h $
191 runIO . hPutStrLn h $
66 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
192 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
src/Idris/Parser.hs+18−21
@@ -36,7 +36,6 @@ import Idris.Parser.Ops
36import Idris.Termination
36import Idris.Termination
37import Idris.Unlit
37import Idris.Unlit
38
38
39−import qualified Util.Pretty
40import Util.System (readSource)
39import Util.System (readSource)
41
40
42import Prelude hiding (pi)
41import Prelude hiding (pi)
@@ -1062,15 +1061,15 @@ RHS ::= '=' Expr
1062RHSName ::= '{' FnName '}';
1061RHSName ::= '{' FnName '}';
1063@
1062@
1064-}
1063-}
1065−rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1064+rhs :: SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
1066rhs syn n = do lchar '='
1065rhs syn n = do lchar '='
1067 indentGt
1066 indentGt
1068− expr syn
1067+ withExtent $ expr syn
1069 <|> do symbol "?=";
1068 <|> do symbol "?=";
1070 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")
1069 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")
1071 r <- expr syn
1070 r <- expr syn
1072− return (addLet fc name r)
1071+ return (addLet fc name r, fc)
1073− <|> impossible
1072+ <|> withExtent impossible
1074 <?> "function right hand side"
1073 <?> "function right hand side"
1075 where mkN :: Name -> Name
1074 where mkN :: Name -> Name
1076 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1075 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
@@ -1112,33 +1111,34 @@ WhereOrTerminator ::= WhereBlock | Terminator;
1112clause :: SyntaxInfo -> IdrisParser PClause
1111clause :: SyntaxInfo -> IdrisParser PClause
1113clause syn
1112clause syn
1114 -- unnamed with or function clause (inside a with)
1113 -- unnamed with or function clause (inside a with)
1115− = appExtent (do
1116− wargs <- P.try (do pushIndent; some (wExpr syn))
1114+ = do wargs <- P.try (do pushIndent; some (wExpr syn))
1117 ist <- get
1115 ist <- get
1118 n <- case lastParse ist of
1116 n <- case lastParse ist of
1119 Just t -> return t
1117 Just t -> return t
1120 Nothing -> fail "Invalid clause"
1118 Nothing -> fail "Invalid clause"
1121− (do r <- rhs syn n
1119+ (do (r, fc) <- rhs syn n
1122 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1120 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1123 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1121 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1124 <|> ([], []) <$ terminator
1122 <|> ([], []) <$ terminator
1125− return $ \fc -> PClauseR fc wargs r wheres) <|> (do
1123+ return $ PClauseR fc wargs r wheres) <|> (do
1126 popIndent
1124 popIndent
1125+ ((wval, pn), fc) <- withExtent $ do
1127− keyword "with"
1126+ keyword "with"
1128− wval <- simpleExpr syn
1127+ wval <- bracketed syn
1129− pn <- optProof
1128+ pn <- optProof
1129+ return (wval, pn)
1130 openBlock
1130 openBlock
1131 ds <- some $ fnDecl syn
1131 ds <- some $ fnDecl syn
1132 let withs = concat ds
1132 let withs = concat ds
1133 closeBlock
1133 closeBlock
1134− return $ \fc -> PWithR fc wargs wval pn withs))
1134+ return $ PWithR fc wargs wval pn withs)
1135 -- <==
1135 -- <==
1136 <|> do ty <- P.try (do pushIndent
1136 <|> do ty <- P.try (do pushIndent
1137 ty <- simpleExpr syn
1137 ty <- simpleExpr syn
1138 symbol "<=="
1138 symbol "<=="
1139 return ty)
1139 return ty)
1140 (n, fc) <- withExtent (expandNS syn <$> fnName)
1140 (n, fc) <- withExtent (expandNS syn <$> fnName)
1141− r <- rhs syn n
1141+ (r, _) <- rhs syn n
1142 let wsyn = syn { syn_namespace = [] }
1142 let wsyn = syn { syn_namespace = [] }
1143 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1143 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1144 <|> ([], []) <$ terminator
1144 <|> ([], []) <$ terminator
@@ -1153,7 +1153,7 @@ clause syn
1153 <|> do pushIndent
1153 <|> do pushIndent
1154 (n, nfc, capp, wargs) <- lhs
1154 (n, nfc, capp, wargs) <- lhs
1155 modify $ \ist -> ist { lastParse = Just n }
1155 modify $ \ist -> ist { lastParse = Just n }
1156− (do (rs, fc) <- withExtent (rhs syn n)
1156+ (do (rs, fc) <- rhs syn n
1157 let wsyn = syn { syn_namespace = [] }
1157 let wsyn = syn { syn_namespace = [] }
1158 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1158 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1159 <|> ([], []) <$ terminator
1159 <|> ([], []) <$ terminator
@@ -1480,7 +1480,7 @@ parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [Im
1480parseImports fname input
1480parseImports fname input
1481 = do i <- getIState
1481 = do i <- getIState
1482 case runparser imports i fname input of
1482 case runparser imports i fname input of
1483− Left err -> ifail . show . parseErrorDoc $ err
1483+ Left err -> formatMessage err >>= ifail . show
1484 Right (x, annots, i) ->
1484 Right (x, annots, i) ->
1485 do putIState i
1485 do putIState i
1486 fname' <- runIO $ Dir.makeAbsolute fname
1486 fname' <- runIO $ Dir.makeAbsolute fname
@@ -1525,12 +1525,9 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Mark -> Idris [PDecl]
1525parseProg syn fname input mrk
1525parseProg syn fname input mrk
1526 = do i <- getIState
1526 = do i <- getIState
1527 case runparser mainProg i fname input of
1527 case runparser mainProg i fname input of
1528− Left err -> do let fc = errorExtent err
1528+ Left err -> do emitWarning err
1529 i <- getIState
1529 i <- getIState
1530− case idris_outputmode i of
1531− RawOutput h -> iputStrLn (show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)
1532− IdeMode n h -> iWarn fc (Util.Pretty.text $ errorMessage err)
1533− putIState (i { errSpan = Just fc })
1530+ putIState (i { errSpan = Just (messageExtent err) })
1534 return []
1531 return []
1535 Right (x, i) -> do putIState i
1532 Right (x, i) -> do putIState i
1536 reportParserWarnings
1533 reportParserWarnings
src/Idris/Parser/Stack.hs+8−11
@@ -13,8 +13,6 @@ module Idris.Parser.Stack
13 , runparser
13 , runparser
14 -- * Parse errors
14 -- * Parse errors
15 , ParseError
15 , ParseError
16− , errorExtent
17− , errorMessage
18 , prettyError
16 , prettyError
19 -- * Mark and restore
17 -- * Mark and restore
20 , Mark
18 , Mark
@@ -35,6 +33,7 @@ module Idris.Parser.Stack
35where
33where
36
34
37import Idris.Core.TT (FC(..))
35import Idris.Core.TT (FC(..))
36+import Idris.Output (Message(..))
38
37
39import Control.Arrow (app)
38import Control.Arrow (app)
40import Control.Monad.State.Strict (StateT(..), evalStateT)
39import Control.Monad.State.Strict (StateT(..), evalStateT)
@@ -44,6 +43,7 @@ import qualified Data.List.NonEmpty as NonEmpty
44import Data.Void (Void(..))
43import Data.Void (Void(..))
45import System.FilePath (addTrailingPathSeparator, splitFileName)
44import System.FilePath (addTrailingPathSeparator, splitFileName)
46import qualified Text.Megaparsec as P
45import qualified Text.Megaparsec as P
46+import qualified Util.Pretty as PP
47
47
48{- * Parsing -}
48{- * Parsing -}
49
49
@@ -64,15 +64,12 @@ runparser p i inputname s =
64
64
65data ParseError = ParseError String (P.ParseError (P.Token String) Void)
65data ParseError = ParseError String (P.ParseError (P.Token String) Void)
66
66
67−-- | Retrieve a parse error's FC
67+instance Message ParseError where
68−errorExtent :: ParseError -> FC
69−errorExtent (ParseError _ err) = sourcePositionFC pos
68+ messageExtent (ParseError _ err) = sourcePositionFC pos
70− where
69+ where
71− (pos NonEmpty.:| _) = P.errorPos err
70+ (pos NonEmpty.:| _) = P.errorPos err
72−
73−-- | A single-line parse error message, including location.
74−errorMessage :: ParseError -> String
75−errorMessage (ParseError _ err) = P.parseErrorTextPretty err
71+ messageText (ParseError _ err) = PP.text . init . P.parseErrorTextPretty $ err
72+ messageSource (ParseError src _) = Just src
76
73
77-- | A fully formatted parse error, with caret and bar, etc.
74-- | A fully formatted parse error, with caret and bar, etc.
78prettyError :: ParseError -> String
75prettyError :: ParseError -> String
src/Idris/Prover.hs+6−3
@@ -317,8 +317,9 @@ elabloop info fn d prompt prf e prev h env
317 (d, prev', st, done, prf', env', res) <-
317 (d, prev', st, done, prf', env', res) <-
318 idrisCatch
318 idrisCatch
319 (case cmd of
319 (case cmd of
320− Left err ->
320+ Left err -> do
321+ msg <- fmap (Left . Msg . show) (formatMessage err)
321− return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) . parseErrorDoc $ err)
322+ return (False, prev, e, False, prf, env, msg)
322 Right (Left cmd') ->
323 Right (Left cmd') ->
323 case cmd' of
324 case cmd' of
324 EQED -> do hs <- lifte e get_holes
325 EQED -> do hs <- lifte e get_holes
@@ -433,7 +434,9 @@ ploop fn d prompt prf e h
433 _ -> return ()
434 _ -> return ()
434 (d, st, done, prf', res) <- idrisCatch
435 (d, st, done, prf', res) <- idrisCatch
435 (case cmd of
436 (case cmd of
436− Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)
437+ Left err -> do
438+ msg <- fmap (Left . Msg . show) (formatMessage err)
439+ return (False, e, False, prf, msg)
437 Right Undo -> do (_, st) <- elabStep e loadState
440 Right Undo -> do (_, st) <- elabStep e loadState
438 return (True, st, False, init prf, Right $ iPrintResult "")
441 return (True, st, False, init prf, Right $ iPrintResult "")
439 Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
442 Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
src/Idris/REPL.hs+1−2
@@ -725,9 +725,8 @@ processInput cmd orig inputs efile
725 let opts = idris_options i
725 let opts = idris_options i
726 let quiet = opt_quiet opts
726 let quiet = opt_quiet opts
727 let fn = fromMaybe "" (listToMaybe inputs)
727 let fn = fromMaybe "" (listToMaybe inputs)
728− c <- colourise
729 case parseCmd i "(input)" cmd of
728 case parseCmd i "(input)" cmd of
730− Left err -> Just inputs <$ iputStrLn (show . fixColour c . parseErrorDoc $ err)
729+ Left err -> Just inputs <$ emitWarning err
731 Right (Right Reload) ->
730 Right (Right Reload) ->
732 reload orig inputs
731 reload orig inputs
733 Right (Right Watch) ->
732 Right (Right Watch) ->
test/basic002/expected+8
@@ -1,5 +1,13 @@
1test006.idr:25:23-27:
1test006.idr:25:23-27:
2+ |
3+25 | Main.parity_lemma_2 = proof {
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3test006.idr:32:23-27:
7test006.idr:32:23-27:
8+ |
9+32 | Main.parity_lemma_1 = proof {
10+ | ~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
5[False, True, False, True, False, True]
13[False, True, False, True, False, True]
test/basic006/expected+6−1
@@ -1,4 +1,8 @@
1+test020a.idr:16:10-19:
2+ |
3+16 | foo xs = reverse xs
4+ | ~~~~~~~~~~
1−test020a.idr:16:10-19:When checking right hand side of foo with expected type
5+When checking right hand side of foo with expected type
2 List a
6 List a
3
7
4When checking an application of function Prelude.List.reverse:
8When checking an application of function Prelude.List.reverse:
@@ -6,5 +10,6 @@ When checking an application of function Prelude.List.reverse:
6 Vect n a (Type of xs)
10 Vect n a (Type of xs)
7 and
11 and
8 List a (Expected type)
12 List a (Expected type)
13+
9[3, 2, 1]
14[3, 2, 1]
10"Number 42"
15"Number 42"
test/basic009/expected+18−3
@@ -1,7 +1,16 @@
1MAIN-PASS
1MAIN-PASS
2+Faulty.idr:6:9-11:
3+ |
4+6 | fault : num = Z
5+ | ~~~
2−Faulty.idr:6:9-11:num is bound as an implicit
6+num is bound as an implicit
3 Did you mean to refer to A.num?
7 Did you mean to refer to A.num?
8+
9+Faulty.idr:7:9-12:
10+ |
11+7 | fault = Refl
12+ | ~~~~
4−Faulty.idr:7:7-12:When checking right hand side of fault with expected type
13+When checking right hand side of fault with expected type
5 num = 0
14 num = 0
6
15
7Type mismatch between
16Type mismatch between
@@ -14,4 +23,10 @@ Specifically:
14 0
23 0
15 and
24 and
16 num
25 num
26+
27+Multiple.idr:3:21:
28+ |
29+3 | import Data.Vect as X
30+ | ^
17−Multiple.idr:3:21:import alias not unique: "X"
31+import alias not unique: "X"
32+
test/basic016/expected+1−1
@@ -1 +1 @@
1−Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB
1+ Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB
test/basic017/expected+6−1
@@ -1,3 +1,8 @@
1+basic017a.idr:11:8:
2+ |
3+11 | append : Vect n a -> Vect m a -> Vect (n + m) a
4+ | ^
1−basic017a.idr:11:8:When checking type of Main.append:
5+When checking type of Main.append:
2When checking an application of Main.Vect:
6When checking an application of Main.Vect:
3 No such variable n
7 No such variable n
8+
test/basic018/expected+14−1
@@ -1,10 +1,22 @@
1basic018.idr:7:12-16:
1basic018.idr:7:12-16:
2+ |
3+7 | Vect thing elem
4+ | ~~~~~
2thing is bound as an implicit
5thing is bound as an implicit
3 Did you mean to refer to Main.thing?
6 Did you mean to refer to Main.thing?
7+
4basic018.idr:12:8-12:
8basic018.idr:12:8-12:
9+ |
10+12 | test : thing = S 41
11+ | ~~~~~
5thing is bound as an implicit
12thing is bound as an implicit
6 Did you mean to refer to Main.thing?
13 Did you mean to refer to Main.thing?
14+
15+basic018.idr:13:8-11:
16+ |
17+13 | test = Refl
18+ | ~~~~
7−basic018.idr:13:6-11:When checking right hand side of test with expected type
19+When checking right hand side of test with expected type
8 thing = S 41
20 thing = S 41
9
21
10Type mismatch between
22Type mismatch between
@@ -17,3 +29,4 @@ Specifically:
17 42
29 42
18 and
30 and
19 thing
31 thing
32+
test/directives001/expected+36−6
@@ -1,12 +1,42 @@
1+directives001.idr:14:7:
2+ |
3+14 | mkFoo : String -> Foo
4+ | ^
1−directives001.idr:14:7:Use of deprecated name directives001.Foo
5+Use of deprecated name directives001.Foo
2To be replaced with `Bar`.
6To be replaced with `Bar`.
7+
8+directives001.idr:14:7:
9+ |
10+14 | mkFoo : String -> Foo
11+ | ^
3−directives001.idr:14:7:Use of deprecated name directives001.Foo
12+Use of deprecated name directives001.Foo
4To be replaced with `Bar`.
13To be replaced with `Bar`.
14+
15+directives001.idr:15:9-13:
16+ |
17+15 | mkFoo = MkFoo
18+ | ~~~~~
5−directives001.idr:15:7-13:Use of deprecated name directives001.Foo
19+Use of deprecated name directives001.Foo
6To be replaced with `Bar`.
20To be replaced with `Bar`.
21+
22+directives001.idr:15:9-13:
23+ |
24+15 | mkFoo = MkFoo
25+ | ~~~~~
7−directives001.idr:15:7-13:Use of deprecated name directives001.Foo
26+Use of deprecated name directives001.Foo
8To be replaced with `Bar`.
27To be replaced with `Bar`.
28+
29+directives001.idr:26:10-28:28:
30+ |
31+26 | main = do
32+ | ~~ ...
9−directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar
33+Use of a fragile construct directives001.mkBar
10How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
34How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
35+
36+directives001.idr:26:10-28:28:
37+ |
38+26 | main = do
39+ | ~~ ...
11−directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar
40+Use of a fragile construct directives001.mkBar
12How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
41How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
42+
test/directives002/expected+4
@@ -1,2 +1,6 @@
1directives002.idr:12:3-14:28:
1directives002.idr:12:3-14:28:
2+ |
3+12 | main = do
4+ | ~~~~~~~~~ ...
2directives002.Main.main is possibly not total due to: directives002.loop
5directives002.Main.main is possibly not total due to: directives002.loop
6+
test/effects003/expected+4
@@ -1,5 +1,9 @@
1hangman.idr:204:8-12:
1hangman.idr:204:8-12:
2+ |
3+204 | wlen = proof search
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3------------
7------------
4
8
56 guesses left
96 guesses left
test/error001/expected+6−1
@@ -1,4 +1,8 @@
1+test002.idr:1:6:
2+ |
3+1 | myid : (a : Type) -> a -> a
4+ | ^
1−test002.idr:1:6:Universe inconsistency.
5+Universe inconsistency.
2 Working on: ./test002.idr.z
6 Working on: ./test002.idr.z
3 Old domain: (6,6)
7 Old domain: (6,6)
4 New domain: (6,5)
8 New domain: (6,5)
@@ -6,3 +10,4 @@ test002.idr:1:6:Universe inconsistency.
6 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
10 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
7 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}
11 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}
8 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
12 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
13+
test/error003/expected+5−1
@@ -1,5 +1,9 @@
1−ErrorReflection.idr:68:5-20:
1+ErrorReflection.idr:68:7-20:
2+ |
3+68 | bad = Lam (Var Here)
4+ | ~~~~~~~~~~~~~~
2When checking right hand side of bad with expected type
5When checking right hand side of bad with expected type
3 Tm [] TUnit
6 Tm [] TUnit
4
7
5DSL type error: (t(504) => t'(503)) doesn't match ()
8DSL type error: (t(504) => t'(503)) doesn't match ()
9+
test/error004/expected+8
@@ -1,12 +1,20 @@
1FunErrTest.idr:35:12-18:
1FunErrTest.idr:35:12-18:
2+ |
3+35 | badCadr1 = cadr []
4+ | ~~~~~~~
2When checking right hand side of badCadr1 with expected type
5When checking right hand side of badCadr1 with expected type
3 Int
6 Int
4
7
5When checking argument cons2 to function FunErrTest.cadr:
8When checking argument cons2 to function FunErrTest.cadr:
6 Could not prove that [] has at least two elements.
9 Could not prove that [] has at least two elements.
10+
7FunErrTest.idr:38:12-19:
11FunErrTest.idr:38:12-19:
12+ |
13+38 | badCadr2 = cadr [1]
14+ | ~~~~~~~~
8When checking right hand side of badCadr2 with expected type
15When checking right hand side of badCadr2 with expected type
9 Int
16 Int
10
17
11When checking argument cons2 to function FunErrTest.cadr:
18When checking argument cons2 to function FunErrTest.cadr:
12 Could not prove that [] has at least two elements.
19 Could not prove that [] has at least two elements.
20+
test/error005/expected+30−5
@@ -1,31 +1,56 @@
1+error005.idr:11:7:
2+ |
3+11 | two = 2
4+ | ^
1−error005.idr:11:7:When checking right hand side of two with expected type
5+When checking right hand side of two with expected type
2 Fin 2
6 Fin 2
3
7
4When checking argument prf to function Data.Fin.fromInteger:
8When checking argument prf to function Data.Fin.fromInteger:
5 When using 2 as a literal for a Fin 2
9 When using 2 as a literal for a Fin 2
6 2 is not strictly less than 2
10 2 is not strictly less than 2
11+
12+error005.idr:14:12:
13+ |
14+14 | hahaha n = 0
15+ | ^
7−error005.idr:14:12:When checking right hand side of hahaha with expected type
16+When checking right hand side of hahaha with expected type
8 Fin n
17 Fin n
9
18
10When checking argument prf to function Data.Fin.fromInteger:
19When checking argument prf to function Data.Fin.fromInteger:
11 When using 0 as a literal for a Fin n
20 When using 0 as a literal for a Fin n
12 0 is not strictly less than n
21 0 is not strictly less than n
22+
23+error005.idr:20:11:
24+ |
25+20 | notOk n = 2
26+ | ^
13−error005.idr:20:11:When checking right hand side of notOk with expected type
27+When checking right hand side of notOk with expected type
14 Fin (plus 2 n)
28 Fin (plus 2 n)
15
29
16When checking argument prf to function Data.Fin.fromInteger:
30When checking argument prf to function Data.Fin.fromInteger:
17 When using 2 as a literal for a Fin (S (S n))
31 When using 2 as a literal for a Fin (S (S n))
18 2 is not strictly less than S (S n)
32 2 is not strictly less than S (S n)
33+
34+error005.idr:23:12-24:
35+ |
36+23 | b0rken n = fromInteger n
37+ | ~~~~~~~~~~~~~
19−error005.idr:23:12-24:When checking right hand side of b0rken with expected type
38+When checking right hand side of b0rken with expected type
20 Fin 3
39 Fin 3
21
40
22When checking argument prf to function Data.Fin.fromInteger:
41When checking argument prf to function Data.Fin.fromInteger:
23 When using n as a literal for a Fin 3
42 When using n as a literal for a Fin 3
24 Could not show that n is less than 3 because n is a bound
43 Could not show that n is less than 3 because n is a bound
25 variable instead of a constant Integer
44 variable instead of a constant Integer
45+
46+error005.idr:26:17:
47+ |
48+26 | x = the (Fin 4) 5
49+ | ^
26−error005.idr:26:17:When checking right hand side of x with expected type
50+When checking right hand side of x with expected type
27 Fin 4
51 Fin 4
28
52
29When checking argument prf to function Data.Fin.fromInteger:
53When checking argument prf to function Data.Fin.fromInteger:
30 When using 5 as a literal for a Fin 4
54 When using 5 as a literal for a Fin 4
31 5 is not strictly less than 4
55 5 is not strictly less than 4
56+
test/error006/expected+6−1
@@ -1,2 +1,7 @@
1+WithPatsNoWith.idr:4:1-13:
2+ |
3+4 | foo 1 | 2 | 3 = True
4+ | ~~~~~~~~~~~~~
1−WithPatsNoWith.idr:4:1-13:When checking left hand side of foo:
5+When checking left hand side of foo:
2unexpected patterns outside of "with" block
6unexpected patterns outside of "with" block
7+
test/error007/expected+4
@@ -1,4 +1,7 @@
1error007.idr:26:7-29:
1error007.idr:26:7-29:
2+ |
3+26 | send_page conn str code -- (prim__zextB32_Int code)
4+ | ~~~~~~~~~~~~~~~~~~~~~~~
2When checking right hand side of answer_to_connection with expected type
5When checking right hand side of answer_to_connection with expected type
3 IO Int
6 IO Int
4
7
@@ -13,3 +16,4 @@ When checking argument code to function Main.send_page:
13 Bits32
16 Bits32
14 and
17 and
15 Int
18 Int
19+
test/error008/expected+12−2
@@ -1,4 +1,14 @@
1+error008.idr:3:4:
2+ |
3+3 | s2 : x + sum Nil = x * fromInteger 0
4+ | ^
1−error008.idr:3:4:When checking type of Main.s2:
5+When checking type of Main.s2:
2Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
6Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
7+
8+error008a.idr:3:4:
9+ |
10+3 | s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0
11+ | ^
3−error008a.idr:3:4:When checking type of Main.s1:
12+When checking type of Main.s1:
4Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
13Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
14+
test/ffi002/expected+6−1
@@ -1 +1,6 @@
1+test023.idr:20:26-36:
2+ |
3+20 | %provide (t : Type) with badProvider
4+ | ~~~~~~~~~~~
1−test023.idr:20:26-36:Type provider error: Always fails
5+Type provider error: Always fails
6+
test/interfaces008/expected+4
@@ -1,2 +1,6 @@
1interfaces008.idr:20:18-23:
1interfaces008.idr:20:18-23:
2+ |
3+20 | implementation Foo2 a where
4+ | ~~~~~~
2Default implementations must be for a super interface constraint on the containing interface.
5Default implementations must be for a super interface constraint on the containing interface.
6+
test/layout001/expected+23−13
@@ -1,72 +1,82 @@
1−./layout001a.idr:5:1:
1+layout001a.idr:5:1:
2 |
2 |
35 | y
35 | y
4 | ^
4 | ^
5Wrong indention: should be greater than context indentation
5Wrong indention: should be greater than context indentation
6
6
7−./layout001b.idr:5:3:
7+layout001b.idr:5:3:
8 |
8 |
95 | = y
95 | = y
10 | ^
10 | ^
11Wrong indention: should be greater than context indentation
11Wrong indention: should be greater than context indentation
12
12
13−./layout001c.idr:3:1:
13+layout001c.idr:3:1:
14 |
14 |
153 | 2
153 | 2
16 | ^
16 | ^
17Wrong indention: should be greater than context indentation
17Wrong indention: should be greater than context indentation
18
18
19−./layout001e.idr:6:1:
19+layout001e.idr:6:1:
20 |
20 |
216 | 3
216 | 3
22 | ^
22 | ^
23Wrong indention: should be greater than context indentation
23Wrong indention: should be greater than context indentation
24
24
25−./layout001f.idr:6:2:
25+layout001f.idr:6:2:
26 |
26 |
276 | 3
276 | 3
28 | ^
28 | ^
29Wrong indention: should be greater than context indentation
29Wrong indention: should be greater than context indentation
30
30
31−./layout001g.idr:6:3:
31+layout001g.idr:6:3:
32 |
32 |
336 | 3
336 | 3
34 | ^
34 | ^
35Wrong indention: should be greater than context indentation
35Wrong indention: should be greater than context indentation
36
36
37−./layout001h.idr:6:3:
37+layout001h.idr:6:3:
38 |
38 |
396 | 3
396 | 3
40 | ^
40 | ^
41Wrong indention: should be greater than context indentation
41Wrong indention: should be greater than context indentation
42
42
43−./layout001i.idr:6:4:
43+layout001i.idr:6:4:
44 |
44 |
456 | 3
456 | 3
46 | ^
46 | ^
47Wrong indention: should be greater than context indentation
47Wrong indention: should be greater than context indentation
48
48
49−./layout001j.idr:6:5:
49+layout001j.idr:6:5:
50 |
50 |
516 | 3
516 | 3
52 | ^
52 | ^
53Wrong indention: should be greater than context indentation
53Wrong indention: should be greater than context indentation
54
54
55−./layout001l.idr:6:1:
55+layout001l.idr:6:1:
56 |
56 |
576 | y
576 | y
58 | ^
58 | ^
59Wrong indention: should be greater than context indentation
59Wrong indention: should be greater than context indentation
60
60
61+mplus1.idr:13:34-17:49:
62+ |
63+13 | term = do f <- factor
64+ | ~~~~~~~~~~~~~~ ...
61−mplus1.idr:13:31-17:49:When checking right hand side of term with expected type
65+When checking right hand side of term with expected type
62 Maybe Int
66 Maybe Int
63
67
64When checking an application of function Prelude.Applicative.pure:
68When checking an application of function Prelude.Applicative.pure:
65 No such variable f
69 No such variable f
70+
66−./mplus2.idr:17:37:
71+mplus2.idr:17:37:
67 |
72 |
6817 | `mplus` pure f
7317 | `mplus` pure f
69 | ^
74 | ^
70not end of block
75not end of block
71
76
77+mplus3.idr:11:1-16:
78+ |
79+11 | term = ?term_rhs
80+ | ~~~~~~~~~~~~~~~~
72−mplus3.idr:11:1-16:warning - Unreachable case: term
81+Unreachable case: term
82+
test/literate001/expected+6−1
@@ -1,4 +1,9 @@
1+./test003a.lidr:1:0:
2+ |
3+1 | Broken
4+ |^
1−./test003a.lidr:1:0:Program line next to comment
5+Program line next to comment
6+
2'a'
7'a'
3'd'
8'd'
4zabcdefg
9zabcdefg
test/meta002/expected+14−2
@@ -1,13 +1,25 @@
1DataDef.idr:74:1-8:
1DataDef.idr:74:1-8:
2+ |
3+74 | %runElab nope
4+ | ~~~~~~~~
2While running an elaboration script, the following error occurred:
5While running an elaboration script, the following error occurred:
3Prelude.Either.Either is already defined as a datatype.
6Prelude.Either.Either is already defined as a datatype.
7+
4−Tacs.idr:299:15-300:78:
8+Tacs.idr:299:17-300:78:
9+ |
10+299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
11+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
5When checking right hand side of testElab3 with expected type
12When checking right hand side of testElab3 with expected type
6 DPair Ty (Tm [])
13 DPair Ty (Tm [])
7
14
8Unifying ty and ARR ty t would lead to infinite value
15Unifying ty and ARR ty t would lead to infinite value
16+
9−AgdaStyleReflection.idr:315:5-20:
17+AgdaStyleReflection.idr:315:7-20:
18+ |
19+315 | baz = tactic trivial
20+ | ~~~~~~~~~~~~~~
10When checking right hand side of baz with expected type
21When checking right hand side of baz with expected type
11 (Nat, Void)
22 (Nat, Void)
12
23
13PROOF SEARCH FAILURE is not defined.
24PROOF SEARCH FAILURE is not defined.
25+
test/meta003/expected+4
@@ -1,6 +1,10 @@
1BadDef.idr:14:1-8:
1BadDef.idr:14:1-8:
2+ |
3+14 | %runElab mkBadDef1
4+ | ~~~~~~~~
2While running an elaboration script, the following error occurred:
5While running an elaboration script, the following error occurred:
3Type mismatch between
6Type mismatch between
4 ()
7 ()
5and
8and
6 String
9 String
10+
test/meta004/expected+4
@@ -1,3 +1,7 @@
1meta004.idr:50:1-8:
1meta004.idr:50:1-8:
2+ |
3+50 | %runElab domore
4+ | ~~~~~~~~
2While running an elaboration script, the following error occurred:
5While running an elaboration script, the following error occurred:
3Not an impossible case
6Not an impossible case
7+
test/proof001/expected+8
@@ -1,4 +1,12 @@
1test029.idr:29:25-29:
1test029.idr:29:25-29:
2+ |
3+29 | simple.append_lemma_2 = proof {
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3test029.idr:36:25-29:
7test029.idr:36:25-29:
8+ |
9+36 | simple.append_lemma_1 = proof {
10+ | ~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
test/proof002/expected+16
@@ -1,10 +1,25 @@
1Reflect.idr:175:21-25:
1Reflect.idr:175:21-25:
2+ |
3+175 | Reflect.appRExpr1 = proof {
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3Reflect.idr:184:21-25:
7Reflect.idr:184:21-25:
8+ |
9+184 | Reflect.appRExpr2 = proof {
10+ | ~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
5Reflect.idr:192:15-19:
13Reflect.idr:192:15-19:
14+ |
15+192 | Reflect.bp1 = proof {
16+ | ~~~~~
6This style of tactic proof is deprecated. See %runElab for the replacement.
17This style of tactic proof is deprecated. See %runElab for the replacement.
18+
7test030a.idr:12:26-37:
19test030a.idr:12:26-37:
20+ |
21+12 | testReflect1 {a} xs ys = AssocProof a
22+ | ~~~~~~~~~~~~
8When checking right hand side of testReflect1 with expected type
23When checking right hand side of testReflect1 with expected type
9 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs
24 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs
10
25
@@ -19,3 +34,4 @@ When checking an application of function Reflect.getJust:
19 Just x
34 Just x
20 and
35 and
21 Nothing
36 Nothing
37+
test/proof003/expected+24
@@ -1,15 +1,39 @@
1Parity.idr:17:18-22:
1Parity.idr:17:18-22:
2+ |
3+17 | parity_lemma_2 = proof {
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3Parity.idr:24:18-22:
7Parity.idr:24:18-22:
8+ |
9+24 | parity_lemma_1 = proof {
10+ | ~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
5test015.idr:88:15-19:
13test015.idr:88:15-19:
14+ |
15+88 | Main.ntbOdd = proof {
16+ | ~~~~~
6This style of tactic proof is deprecated. See %runElab for the replacement.
17This style of tactic proof is deprecated. See %runElab for the replacement.
18+
7test015.idr:97:16-20:
19test015.idr:97:16-20:
20+ |
21+97 | Main.ntbEven = proof {
22+ | ~~~~~
8This style of tactic proof is deprecated. See %runElab for the replacement.
23This style of tactic proof is deprecated. See %runElab for the replacement.
24+
9test015.idr:107:20-24:
25test015.idr:107:20-24:
26+ |
27+107 | Main.adc_lemma_2 = proof {
28+ | ~~~~~
10This style of tactic proof is deprecated. See %runElab for the replacement.
29This style of tactic proof is deprecated. See %runElab for the replacement.
30+
11test015.idr:142:20-24:
31test015.idr:142:20-24:
32+ |
33+142 | Main.adc_lemma_1 = proof {
34+ | ~~~~~
12This style of tactic proof is deprecated. See %runElab for the replacement.
35This style of tactic proof is deprecated. See %runElab for the replacement.
36+
1300101010
3700101010
1401011001
3801011001
15010000011
39010000011
test/proof007/expected+5−1
@@ -1,6 +1,10 @@
1−DefaultArgUnknownName.idr:9:6-23:
1+DefaultArgUnknownName.idr:9:8-23:
2+ |
3+9 | test = funWithBadDefArg
4+ | ~~~~~~~~~~~~~~~~
2When checking right hand side of test with expected type
5When checking right hand side of test with expected type
3 ()
6 ()
4
7
5When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:
8When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:
6 No such variable sadgjhsag
9 No such variable sadgjhsag
10+
test/proof008/expected+4
@@ -1,2 +1,6 @@
1ClaimAndUnfocus.idr:8:27-31:
1ClaimAndUnfocus.idr:8:27-31:
2+ |
3+8 | ClaimAndUnfocus.foo_rhs = proof
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
test/proof011/expected+10−2
@@ -1,4 +1,7 @@
1−proof011.idr:20:5-21:18:
1+proof011.idr:20:7-21:18:
2+ |
3+20 | = rewrite vassoc xs ys xs using vreplace in
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
2When checking right hand side of vassoc' with expected type
5When checking right hand side of vassoc' with expected type
3 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
6 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
4
7
@@ -8,7 +11,11 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
8 x ::
11 x ::
9 (xs ++ ys) ++
12 (xs ++ ys) ++
10 zs
13 zs
14+
11−proof011a.idr:14:5-37:
15+proof011a.idr:14:7-37:
16+ |
17+14 | = rewrite vassoc xs ys xs in Refl
18+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
12When checking right hand side of vassoc' with expected type
19When checking right hand side of vassoc' with expected type
13 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
20 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
14
21
@@ -18,3 +25,4 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
18 x ::
25 x ::
19 (xs ++ ys) ++
26 (xs ++ ys) ++
20 zs
27 zs
28+
test/quasiquote003/expected+6−1
@@ -1,4 +1,9 @@
1+NoInfer.idr:11:7-11:
2+ |
3+11 | zzz = `(FZ)
4+ | ~~~~~
1−NoInfer.idr:11:5-11:When checking right hand side of zzz with expected type
5+When checking right hand side of zzz with expected type
2 TT
6 TT
3
7
4No such variable k
8No such variable k
9+
test/quasiquote004/expected+17−1
@@ -1,11 +1,27 @@
1Quasiquote004.idr:39:26-30:
1Quasiquote004.idr:39:26-30:
2+ |
3+39 | Quasiquote004.getMeNat = proof
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3Quasiquote004.idr:42:28-32:
7Quasiquote004.idr:42:28-32:
8+ |
9+42 | Quasiquote004.fizzyIsAOK = proof
10+ | ~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
5Quasiquote004.idr:50:27-31:
13Quasiquote004.idr:50:27-31:
14+ |
15+50 | Quasiquote004.getMeNat' = proof
16+ | ~~~~~
6This style of tactic proof is deprecated. See %runElab for the replacement.
17This style of tactic proof is deprecated. See %runElab for the replacement.
18+
7−Quasiquote004.idr:50:25-51:18:
19+Quasiquote004.idr:50:27-51:18:
20+ |
21+50 | Quasiquote004.getMeNat' = proof
22+ | ~~~~~ ...
8When checking right hand side of Quasiquote004.getMeNat' with expected type
23When checking right hand side of Quasiquote004.getMeNat' with expected type
9 String
24 String
10
25
11Not a Nat goal
26Not a Nat goal
27+
test/quasiquote006/expected+16−4
@@ -1,19 +1,31 @@
1−quasiquote006.idr:9:3-10:
1+quasiquote006.idr:9:5-10:
2+ |
3+9 | b = `{Nil}
4+ | ~~~~~~
2When checking right hand side of b with expected type
5When checking right hand side of b with expected type
3 TTName
6 TTName
4
7
5Can't disambiguate name: ForeignEnv.Nil,
8Can't disambiguate name: ForeignEnv.Nil,
6 Prelude.List.Nil
9 Prelude.List.Nil
10+
7−quasiquote006.idr:12:3-17:
11+quasiquote006.idr:12:5-17:
12+ |
13+12 | c = `{alsdkjflkj}
14+ | ~~~~~~~~~~~~~
8When checking right hand side of c with expected type
15When checking right hand side of c with expected type
9 TTName
16 TTName
10
17
11No such variable alsdkjflkj
18No such variable alsdkjflkj
19+
12−quasiquote006.idr:15:3-11:
20+quasiquote006.idr:15:5-11:
21+ |
22+15 | d = `{(::)}
23+ | ~~~~~~~
13When checking right hand side of d with expected type
24When checking right hand side of d with expected type
14 TTName
25 TTName
15
26
16Can't disambiguate name: ForeignEnv.::,
27Can't disambiguate name: ForeignEnv.::,
17 Prelude.List.::,
28 Prelude.List.::,
18 Prelude.Stream.::
29 Prelude.Stream.::
30+
19−quasiquote006.idr:17:3:Main.d already defined
31+ quasiquote006.idr:17:3:Main.d already defined
test/reg017/expected+8
@@ -1,5 +1,13 @@
1reg017.idr:5:17-23:
1reg017.idr:5:17-23:
2+ |
3+5 | { default tactics { refine Refl; solve; } prfA : a = a } ->
4+ | ~~~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3reg017.idr:8:17-23:
7reg017.idr:8:17-23:
8+ |
9+8 | { default tactics { refine Refl; solve; } prfBC : b = c } ->
10+ | ~~~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
54
134
test/reg027/expected+6−1
@@ -1,2 +1,7 @@
1<<int fn>>
1<<int fn>>
2+reg027a.idr:9:16-30:
3+ |
4+9 | implementation Show (Int -> b) where
5+ | ~~~~~~~~~~~~~~~
2−reg027a.idr:9:16-30:Overlapping implementation: Show (Int -> a) already defined
6+Overlapping implementation: Show (Int -> a) already defined
7+
test/regression002/expected+238−36
@@ -1,13 +1,41 @@
1+reg003a.idr:4:13-38:
2+ |
3+4 | ECons : Nat -> OddList -> EvenList
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~
1−reg003a.idr:4:13-38:When checking type of Main.ECons:
5+When checking type of Main.ECons:
2No such variable OddList
6No such variable OddList
7+
8+reg003a.idr:7:13-38:
9+ |
10+7 | OCons : Nat -> EvenList -> OddList
11+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~
3−reg003a.idr:7:13-38:When checking type of Main.OCons:
12+When checking type of Main.OCons:
4No such variable EvenList
13No such variable EvenList
14+
15+reg003a.idr:9:6:
16+ |
17+9 | test : EvenList
18+ | ^
5−reg003a.idr:9:6:When checking type of Main.test:
19+When checking type of Main.test:
6No such variable EvenList
20No such variable EvenList
21+
7reg006.idr:17:1-23:
22reg006.idr:17:1-23:
23+ |
24+17 | lookup k Leaf = Nothing
25+ | ~~~~~~~~~~~~~~~~~~~~~~~
8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
26RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
27+
28+reg007.lidr:8:3-13:
29+ |
30+8 | > A.n = Z -- This is where it's at!
31+ | ~~~~~~~~~~~
9−reg007.lidr:8:3-13:A.n is already defined
32+A.n is already defined
33+
34+reg007.lidr:12:13-18:
35+ |
36+12 | > hurrah = isSame
37+ | ~~~~~~
10−reg007.lidr:12:13-18:When checking right hand side of hurrah with expected type
38+When checking right hand side of hurrah with expected type
11 0 = 1
39 0 = 1
12
40
13Type mismatch between
41Type mismatch between
@@ -20,40 +48,111 @@ Specifically:
20 1
48 1
21 and
49 and
22 0
50 0
51+
23reg010.idr:5:3-26:
52reg010.idr:5:3-26:
53+ |
54+5 | unsafeSubst P x x px | _ = px
55+ | ~~~~~~~~~~~~~~~~~~~~~~~~
24When checking left hand side of with block in usubst.unsafeSubst:
56When checking left hand side of with block in usubst.unsafeSubst:
25Can't match on with block in usubst.unsafeSubst warg a P x x px
57Can't match on with block in usubst.unsafeSubst warg a P x x px
58+
26reg018a.idr:16:1-18:
59reg018a.idr:16:1-18:
60+ |
61+16 | minusCoNat Z n = Z
62+ | ~~~~~~~~~~~~~~~~~~
27conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
63conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
64+
28reg018a.idr:21:1-42:
65reg018a.idr:21:1-42:
66+ |
67+21 | loopForever = minusCoNat infinity infinity
68+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
29conat.loopForever is possibly not total due to: conat.minusCoNat
69conat.loopForever is possibly not total due to: conat.minusCoNat
70+
30reg018b.idr:8:1-28:
71reg018b.idr:8:1-28:
72+ |
73+8 | showB (I x) = "I" ++ showB x
74+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
31A.showB is possibly not total due to recursive path A.showB --> A.showB
75A.showB is possibly not total due to recursive path A.showB --> A.showB
76+
32reg018b.idr:11:1-6:
77reg018b.idr:11:1-6:
78+ |
79+11 | Show B where show = showB
80+ | ~~~~~~
33A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
81A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
82+
34reg018c.idr:21:1-22:21:
83reg018c.idr:21:1-22:21:
84+ |
85+21 | inf (x :: xs) with (hdtl xs)
86+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
35CodataTest.inf is possibly not total due to: with block in CodataTest.inf
87CodataTest.inf is possibly not total due to: with block in CodataTest.inf
88+
89+reg018d.idr:8:1-39:
90+ |
91+8 | pull {n=Z} _ (x :: xs) = (x, xs)
92+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
36−reg018d.idr:8:1-39:Main.pull is not total as there are missing cases
93+Main.pull is not total as there are missing cases
94+
95+reg023.idr:7:7:
96+ |
97+7 | bad = Z
98+ | ^
37−reg023.idr:7:5-7:When checking right hand side of bad with expected type
99+When checking right hand side of bad with expected type
38 f Nat
100 f Nat
39
101
40Type mismatch between
102Type mismatch between
41 Nat (Type of 0)
103 Nat (Type of 0)
42and
104and
43 f Nat (Expected type)
105 f Nat (Expected type)
106+
107+reg028.idr:5:1-9:
108+ |
109+5 | bad Z = Z
110+ | ~~~~~~~~~
44−reg028.idr:5:1-9:tbad.bad is possibly not total due to: with block in tbad.bad
111+tbad.bad is possibly not total due to: with block in tbad.bad
112+
45reg028a.idr:17:14-18:
113reg028a.idr:17:14-18:
114+ |
115+17 | qsortLemma = proof
116+ | ~~~~~
46This style of tactic proof is deprecated. See %runElab for the replacement.
117This style of tactic proof is deprecated. See %runElab for the replacement.
118+
47reg028a.idr:11:1-14:
119reg028a.idr:11:1-14:
120+ |
121+11 | qsort' [] = []
122+ | ~~~~~~~~~~~~~~
48tbad.qsort' is possibly not total due to: with block in tbad.qsort'
123tbad.qsort' is possibly not total due to: with block in tbad.qsort'
124+
125+reg034.idr:6:1-14:
126+ |
127+6 | bar xs xs Refl = Refl
128+ | ~~~~~~~~~~~~~~
49−reg034.idr:6:1-14:When checking left hand side of bar:
129+When checking left hand side of bar:
50Can't match on bar xs xs Refl
130Can't match on bar xs xs Refl
131+
132+reg034.idr:9:1-14:
133+ |
134+9 | foo f x x Refl = Refl
135+ | ~~~~~~~~~~~~~~
51−reg034.idr:9:1-14:When checking left hand side of foo:
136+When checking left hand side of foo:
52Can't match on foo f x x Refl
137Can't match on foo f x x Refl
138+
139+reg035b.idr:8:14-38:
140+ |
141+8 | fins Z = ([] ** (finZEmpty {a=_}))
142+ | ~~~~~~~~~~~~~~~~~~~~~~~~~
53−reg035b.idr:8:12-38:No such variable __pi_arg
143+No such variable __pi_arg
144+
54reg044.idr:4:6-10:
145reg044.idr:4:6-10:
146+ |
147+4 | pf = proof
148+ | ~~~~~
55This style of tactic proof is deprecated. See %runElab for the replacement.
149This style of tactic proof is deprecated. See %runElab for the replacement.
150+
151+reg044.idr:4:6-6:13:
152+ |
153+4 | pf = proof
154+ | ~~~~~ ...
56−reg044.idr:4:4-6:13:When checking right hand side of Main.pf with expected type
155+When checking right hand side of Main.pf with expected type
57 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
156 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
58
157
59Type mismatch between
158Type mismatch between
@@ -66,73 +165,165 @@ Specifically:
66 b
165 b
67 and
166 and
68 a
167 a
168+
169+reg049.idr:2:11-14:
170+ |
171+2 | Bogus : Void
172+ | ~~~~
69−reg049.idr:2:11-14:When checking constructor Main.Bogus:
173+When checking constructor Main.Bogus:
70Void is not Main.Foo
174Void is not Main.Foo
175+
176+reg049.idr:5:8-12:
177+ |
178+5 | uhOh = Bogus
179+ | ~~~~~
71−reg049.idr:5:6-12:When checking right hand side of uhOh with expected type
180+When checking right hand side of uhOh with expected type
72 Void
181 Void
73
182
74No such variable Bogus
183No such variable Bogus
184+
75−./badbangop.idr:7:1:
185+badbangop.idr:7:1:
76 |
186 |
777 | (!) : List a -> Nat -> Maybe a
1877 | (!) : List a -> Nat -> Maybe a
78 | ^
188 | ^
79! is not a valid operator
189! is not a valid operator
80
190
81−./baddoublebang.idr:6:28:
191+baddoublebang.idr:6:28:
82 |
192 |
836 | doubleBang mmn = do pure !!mmn
1936 | doubleBang mmn = do pure !!mmn
84 | ^
194 | ^
85unexpected Operator without known fixity: !!
195unexpected Operator without known fixity: !!
86
196
197+reg054.idr:18:1-17:
198+ |
199+18 | inf (MkInfer _ Z) = True
200+ | ~~~~~~~~~~~~~~~~~
87−reg054.idr:18:1-17:When checking left hand side of inf:
201+When checking left hand side of inf:
88When checking an application of constructor Main.MkInfer:
202When checking an application of constructor Main.MkInfer:
89 Attempting concrete match on polymorphic argument: 0
203 Attempting concrete match on polymorphic argument: 0
204+
205+reg054.idr:34:1-18:
206+ |
207+34 | weird {x = Char} y = '5'
208+ | ~~~~~~~~~~~~~~~~~~
90−reg054.idr:34:1-18:When checking left hand side of weird:
209+When checking left hand side of weird:
91No explicit types on left hand side: Char
210No explicit types on left hand side: Char
211+
212+reg054.idr:37:1-30:
213+ |
214+37 | weird' {x = Prelude.Nat.Nat} y = Z
215+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
92−reg054.idr:37:1-30:When checking left hand side of weird':
216+When checking left hand side of weird':
93No explicit types on left hand side: Nat
217No explicit types on left hand side: Nat
218+
219+reg054.idr:40:1-7:
220+ |
221+40 | tctrick (Just x) = x
222+ | ~~~~~~~
94−reg054.idr:40:1-7:When checking left hand side of tctrick:
223+When checking left hand side of tctrick:
95When checking an application of Main.tctrick:
224When checking an application of Main.tctrick:
96 Type mismatch between
225 Type mismatch between
97 Maybe a1 (Type of Just x)
226 Maybe a1 (Type of Just x)
98 and
227 and
99 a (Expected type)
228 a (Expected type)
229+
230+reg055.idr:5:1-7:
231+ |
232+5 | g (f Z) = 1
233+ | ~~~~~~~
100−reg055.idr:5:1-7:When checking left hand side of g:
234+When checking left hand side of g:
101Can't match on g (f 0)
235Can't match on g (f 0)
236+
237+reg055.idr:8:1-5:
238+ |
239+8 | h x x = x
240+ | ~~~~~
102−reg055.idr:8:1-5:When checking left hand side of h:
241+When checking left hand side of h:
103Can't match on h x x
242Can't match on h x x
243+
244+reg055a.idr:8:1-18:
245+ |
246+8 | foo (CAny Nothing) = 42
247+ | ~~~~~~~~~~~~~~~~~~
104−reg055a.idr:8:1-18:When checking left hand side of foo:
248+When checking left hand side of foo:
105When checking an application of constructor Foo.CAny:
249When checking an application of constructor Foo.CAny:
106 Attempting concrete match on polymorphic argument: Nothing
250 Attempting concrete match on polymorphic argument: Nothing
251+
252+reg055a.idr:13:1-23:
253+ |
254+13 | apply (\x => \y => x) a = a
255+ | ~~~~~~~~~~~~~~~~~~~~~~~
107−reg055a.idr:13:1-23:When checking left hand side of Foo.apply:
256+When checking left hand side of Foo.apply:
108Can't match on apply (\x, y => x) a
257Can't match on apply (\x, y => x) a
258+
259+reg056.idr:7:16-25:
260+ |
261+7 | dodgy n m Refl impossible
262+ | ~~~~~~~~~~
109−reg056.idr:7:16-25:dodgy n m Refl is a valid case
263+dodgy n m Refl is a valid case
264+
265+reg056.idr:10:11-20:
266+ |
267+10 | nonk Refl impossible
268+ | ~~~~~~~~~~
110−reg056.idr:10:11-20:nonk Refl is a valid case
269+nonk Refl is a valid case
270+
271+reg068.idr:1:6-8:
272+ |
273+1 | data nat : Type where --error
274+ | ~~~
111−reg068.idr:1:6-8:Main.nat has a name which may be implicitly bound.
275+Main.nat has a name which may be implicitly bound.
112This is likely to lead to problems!
276This is likely to lead to problems!
277+
278+reg068.idr:2:8-10:
279+ |
280+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
281+ | ~~~
113−reg068.idr:2:8-10:Main.ze has a name which may be implicitly bound.
282+Main.ze has a name which may be implicitly bound.
114This is likely to lead to problems!
283This is likely to lead to problems!
284+
115reg068.idr:2:8-10:
285reg068.idr:2:8-10:
286+ |
287+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
288+ | ~~~
116nat is bound as an implicit
289nat is bound as an implicit
117 Did you mean to refer to Main.nat?
290 Did you mean to refer to Main.nat?
291+
292+reg068.idr:2:8-10:
293+ |
294+2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
295+ | ~~~
118−reg068.idr:2:8-10:When checking constructor Main.ze:
296+When checking constructor Main.ze:
119Type level variable nat is not Main.nat
297Type level variable nat is not Main.nat
298+
299+Mod.idr:11:1-22:
300+ |
301+11 | natexp k = S (natfn k)
302+ | ~~~~~~~~~~~~~~~~~~~~~~
120−Mod.idr:11:1-22:public export Mod.natexp can't refer to export Mod.natfn
303+public export Mod.natexp can't refer to export Mod.natfn
304+
121reg070.idr:7:1-7:
305reg070.idr:7:1-7:
306+ |
307+7 | Show Te where
308+ | ~~~~~~~
122Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show
309Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show
310+
123−./reg076.idr:8:1:
311+reg076.idr:8:1:
124 |
312 |
125−8 | <empty line>
313+8 | <end of file>
126 | ^
314 | ^
127Missing fixity declaration for Main.:>
315Missing fixity declaration for Main.:>
128
316
129−./reg077.idr:3:1:
317+reg077.idr:3:1:
130 |
318 |
131−3 | <empty line>
319+3 | <end of file>
132 | ^
320 | ^
133Missing fixity declaration for Main.:>>
321Missing fixity declaration for Main.:>>
134
322
135DoubleEquality.idr:4:83-103:
323DoubleEquality.idr:4:83-103:
324+ |
325+4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
326+ | ~~~~~~~~~~~~~~~~~~~~~
136When checking right hand side of oops with expected type
327When checking right hand side of oops with expected type
137 Void
328 Void
138
329
@@ -147,5 +338,16 @@ When checking argument value to function Prelude.Basics.the:
147 -0.0
338 -0.0
148 and
339 and
149 0.0
340 0.0
341+
342+Canonicity.idr:9:1-9:
343+ |
344+9 | f Nil = 0
345+ | ~~~~~~~~~
150−Canonicity.idr:9:1-9:Canonicity.f is not total as there are missing cases
346+Canonicity.f is not total as there are missing cases
347+
348+Canonicity.idr:12:1-20:
349+ |
350+12 | NaN = f (Cons 0 Nil)
351+ | ~~~~~~~~~~~~~~~~~~~~
151−Canonicity.idr:12:1-20:Canonicity.NaN is possibly not total due to: Canonicity.f
352+Canonicity.NaN is possibly not total due to: Canonicity.f
353+
test/sourceLocation001/expected+18−2
@@ -1,17 +1,33 @@
1SourceLoc.idr:12:19-25:
1SourceLoc.idr:12:19-25:
2+ |
3+12 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation
4+ | ~~~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3SourceLoc.idr:21:19-23:
7SourceLoc.idr:21:19-23:
8+ |
9+21 | fromProofScript = proof sourceLocation
10+ | ~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
5SourceLoc.idr:41:20-26:
13SourceLoc.idr:41:20-26:
14+ |
15+41 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t
16+ | ~~~~~~~
6This style of tactic proof is deprecated. See %runElab for the replacement.
17This style of tactic proof is deprecated. See %runElab for the replacement.
18+
7SourceLoc.idr:99:18-22:
19SourceLoc.idr:99:18-22:
20+ |
21+99 | SourceLoc.meta = proof
22+ | ~~~~~
8This style of tactic proof is deprecated. See %runElab for the replacement.
23This style of tactic proof is deprecated. See %runElab for the replacement.
24+
9Testing using definition
25Testing using definition
10FileLoc "SourceLoc.idr" (17, 11) (17, 16)
26FileLoc "SourceLoc.idr" (17, 11) (17, 16)
11Testing using inline tactics
27Testing using inline tactics
12−FileLoc "SourceLoc.idr" (21, 17) (21, 38)
28+FileLoc "SourceLoc.idr" (21, 19) (21, 38)
13Testing using metavariable with later definition
29Testing using metavariable with later definition
14−FileLoc "SourceLoc.idr" (99, 16) (100, 16)
30+FileLoc "SourceLoc.idr" (99, 18) (100, 16)
15-----------------------
31-----------------------
16Success!
32Success!
17Error at FileLoc "SourceLoc.idr" (73, 23) (73, 25)
33Error at FileLoc "SourceLoc.idr" (73, 23) (73, 25)
test/syntax001/expected+12−2
@@ -1,4 +1,8 @@
1+Syntax.idr:6:7-18:
2+ |
3+6 | foo = fnord "argh"
4+ | ~~~~~~~~~~~~
1−Syntax.idr:6:7-18:When checking right hand side of foo with expected type
5+When checking right hand side of foo with expected type
2 Nat
6 Nat
3
7
4When checking an application of function Prelude.Interfaces.+:
8When checking an application of function Prelude.Interfaces.+:
@@ -6,7 +10,12 @@ When checking an application of function Prelude.Interfaces.+:
6 String (Type of "argh")
10 String (Type of "argh")
7 and
11 and
8 Nat (Expected type)
12 Nat (Expected type)
13+
14+SyntaxTest.idr:5:7-18:
15+ |
16+5 | foo = fnord "argh"
17+ | ~~~~~~~~~~~~
9−SyntaxTest.idr:5:7-18:When checking right hand side of foo with expected type
18+When checking right hand side of foo with expected type
10 Nat
19 Nat
11
20
12When checking an application of function Prelude.Interfaces.+:
21When checking an application of function Prelude.Interfaces.+:
@@ -14,3 +23,4 @@ When checking an application of function Prelude.Interfaces.+:
14 String (Type of "argh")
23 String (Type of "argh")
15 and
24 and
16 Nat (Expected type)
25 Nat (Expected type)
26+
test/totality001/expected+18−3
@@ -1,3 +1,18 @@
1+test010.idr:15:1-30:
2+ |
3+15 | foo (MkBad f i) = f (MkBad' i)
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1−test010.idr:15:1-30:Main.foo is possibly not total due to: Main.MkBad
5+Main.foo is possibly not total due to: Main.MkBad
6+
7+test010a.idr:9:1-23:
8+ |
9+9 | bar = MkBad (\x => 3) 3
10+ | ~~~~~~~~~~~~~~~~~~~~~~~
2−test010a.idr:9:1-23:main.bar is possibly not total due to: main.MkBad
11+main.bar is possibly not total due to: main.MkBad
12+
13+test010b.idr:9:1-23:
14+ |
15+9 | bar = MkBad (\x => 3) 3
16+ | ~~~~~~~~~~~~~~~~~~~~~~~
3−test010b.idr:9:1-23:main.bar is possibly not total due to: main.MkBad
17+main.bar is possibly not total due to: main.MkBad
18+
test/totality002/expected+14−1
@@ -1,5 +1,18 @@
1test017.idr:94:26-30:
1test017.idr:94:26-30:
2+ |
3+94 | maxCommutativeStepCase = proof {
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3test017a.idr:7:1-24:
7test017a.idr:7:1-24:
8+ |
9+7 | vtrans [] _ = []
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~
4scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
11scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
12+
13+test017b.idr:4:1-9:
14+ |
15+4 | foo = foo
16+ | ~~~~~~~~~
5−test017b.idr:4:1-9:foo.foo is possibly not total due to recursive path foo.foo
17+foo.foo is possibly not total due to recursive path foo.foo
18+
test/totality003/expected+4
@@ -1,2 +1,6 @@
1totality003a.idr:5:1-13:
1totality003a.idr:5:1-13:
2+ |
3+5 | qsort [] = []
4+ | ~~~~~~~~~~~~~
2smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort
5smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort
6+
test/totality004/expected+10−1
@@ -1,4 +1,13 @@
1[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
1[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
2totality004a.idr:13:1-44:
2totality004a.idr:13:1-44:
3+ |
4+13 | process (Get f) (x :: xs) = process (f x) xs
5+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process
6Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process
7+
8+totality004a.idr:24:1-60:
9+ |
10+24 | main = printLn (take 10 (process doubleInt (countStream 1)))
11+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4−totality004a.idr:24:1-60:Main.main is possibly not total due to: Main.process
12+Main.main is possibly not total due to: Main.process
13+
test/totality006/expected+16−2
@@ -1,4 +1,18 @@
1+totality006.idr:8:1-29:
2+ |
3+8 | prf Z Z Oh impossible
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1−totality006.idr:8:1-29:Main.prf is not total as there are missing cases
5+Main.prf is not total as there are missing cases
6+
2−totality006a.idr:11:21-30:prf' (S _) (S _) Oh is a valid case
7+totality006a.idr:11:21-30:
8+ |
9+11 | prf' (S _) (S _) Oh impossible
10+ | ~~~~~~~~~~
11+prf' (S _) (S _) Oh is a valid case
12+
3totality006b.idr:10:1-34:
13totality006b.idr:10:1-34:
14+ |
15+10 | blargh [] (y :: xs) so = absurd so
16+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4totality006b.blargh is not total as there are missing cases
17totality006b.blargh is not total as there are missing cases
18+
test/totality007/expected+4
@@ -1,5 +1,9 @@
1Entering directory `./src'
1Entering directory `./src'
2Totality.idr:4:1-9:
2Totality.idr:4:1-9:
3+ |
4+4 | foo Z = Z
5+ | ~~~~~~~~~
3Totality.foo is not total as there are missing cases
6Totality.foo is not total as there are missing cases
7+
4Totality.idr:4:1-9:Could not build: Totality.foo is not total as there are missing cases
8Totality.idr:4:1-9:Could not build: Totality.foo is not total as there are missing cases
5Leaving directory `./src'
9Leaving directory `./src'
test/totality008/expected+6−1
@@ -1 +1,6 @@
1+totality008.idr:7:1-14:
2+ |
3+7 | ElimT _ C1 = 3
4+ | ~~~~~~~~~~~~~~
1−totality008.idr:7:1-14:Main.ElimT is possibly not total due to: Main.C2
5+Main.ElimT is possibly not total due to: Main.C2
6+
test/totality009/expected+60−10
@@ -1,10 +1,60 @@
1+TestLambdaPossible.idr:9:25-34:
2+ |
3+9 | wrongPossible = (\Flase impossible)
4+ | ~~~~~~~~~~
1−TestLambdaPossible.idr:9:25-34:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
5+Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
6+
7+TestLambdaPossible.idr:9:1-35:
8+ |
9+9 | wrongPossible = (\Flase impossible)
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2−TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
11+Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
12+
13+TestLambdaPossible.idr:12:25:
14+ |
15+12 | wrongPossible' x = case x of
16+ | ^
3−TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
17+Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
18+
19+TestLambdaPossible.idr:12:1-13:40:
20+ |
21+12 | wrongPossible' x = case x of
22+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
4−TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
23+Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
24+
25+TestLambdaPossible.idr:9:17-35:
26+ |
27+9 | wrongPossible = (\Flase impossible)
28+ | ~~~~~~~~~~~~~~~~~~~
5−TestLambdaPossible.idr:9:15-35:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
29+Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
30+
31+TestLambdaPossible.idr:9:1-35:
32+ |
33+9 | wrongPossible = (\Flase impossible)
34+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6−TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
35+Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
36+
37+TestLambdaPossible.idr:12:20-13:40:
38+ |
39+12 | wrongPossible' x = case x of
40+ | ~~~~~~~~~ ...
7−TestLambdaPossible.idr:12:18-13:40:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
41+Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
42+
43+TestLambdaPossible.idr:12:1-13:40:
44+ |
45+12 | wrongPossible' x = case x of
46+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
8−TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
47+Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
48+
49+TestLambdaPossible2.idr:10:1-35:
50+ |
51+10 | wrongPossible = (\Flase impossible)
52+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
9−TestLambdaPossible2.idr:10:1-35:TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34
53+TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34
54+
55+TestLambdaPossible2.idr:14:1-15:40:
56+ |
57+14 | wrongPossible' x = case x of
58+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
10−TestLambdaPossible2.idr:14:1-15:40:TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25
59+TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25
60+
test/totality010/expected+12−2
@@ -1,2 +1,12 @@
1+totality010.idr:27:1-35:
2+ |
3+27 | evenNotS MkEven ZeroEven impossible
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1−totality010.idr:27:1-35:Main.evenNotS is not total as there are missing cases
5+Main.evenNotS is not total as there are missing cases
6+
7+totality010.idr:30:1-40:
8+ |
9+30 | bad = evenNotS ZeroEven $ MkBad ZeroEven
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2−totality010.idr:30:1-40:Main.bad is possibly not total due to: Main.evenNotS
11+Main.bad is possibly not total due to: Main.evenNotS
12+
test/totality011/expected+4
@@ -1,2 +1,6 @@
1totality011.lidr:22:3-57:
1totality011.lidr:22:3-57:
2+ |
3+22 | > weCanOnlyGetOlder {t'' = Z} {t = Z} _ _ _ = LTEZero
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2Main.weCanOnlyGetOlder is not total as there are missing cases
5Main.weCanOnlyGetOlder is not total as there are missing cases
6+
test/totality012/expected+8
@@ -1,4 +1,12 @@
1totality012a.idr:9:1-10:27:
1totality012a.idr:9:1-10:27:
2+ |
3+9 | echo2 x = if (x == "quit") then PutStr "Bye!\n"
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
2Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2
5Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2
6+
3totality012b.idr:11:1-17:33:
7totality012b.idr:11:1-17:33:
8+ |
9+11 | echo = do PutStr "$ "
10+ | ~~~~~~~~~~~~~~~~~~~~~ ...
4Main.echo is possibly not total due to recursive path Main.echo
11Main.echo is possibly not total due to recursive path Main.echo
12+
test/totality013/expected+10−1
@@ -1,3 +1,12 @@
1totality013a.idr:5:3-49:
1totality013a.idr:5:3-49:
2+ |
3+5 | foo order x xs y ys _ = mtot order (x :: xs) ys
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot
5Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot
6+
7+totality013a.idr:9:3-36:
8+ |
9+9 | mtot order [] right = right
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3−totality013a.idr:9:3-36:Main.mtot is possibly not total due to: Main.foo
11+Main.mtot is possibly not total due to: Main.foo
12+
test/totality014/expected+7−2
@@ -1,8 +1,13 @@
1+totality014.idr:1:6-9:
2+ |
3+1 | data Con2 : Type where
4+ | ~~~~
1−totality014.idr:1:6-9:Universe inconsistency.
5+Universe inconsistency.
2 Working on: ./totality014.idr.w
6 Working on: ./totality014.idr.w
3 Old domain: (5,5)
7 Old domain: (5,5)
4 New domain: (5,4)
8 New domain: (5,4)
5 Involved constraints:
9 Involved constraints:
6 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
10 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
7 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
11 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
8− ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:27-29}
12+ ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:29}
13+
test/totality015/expected+16−2
@@ -1,4 +1,18 @@
1totality015a.idr:52:3-53:
1totality015a.idr:52:3-53:
2+ |
3+52 | quiz (num1 :: num2 :: nums) score = quiz nums score
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz
5Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz
6+
7+totality015a.idr:42:3-44:36:
8+ |
9+42 | correct nums score
10+ | ~~~~~~~~~~~~~~~~~~ ...
3−totality015a.idr:42:3-44:36:Main.correct is possibly not total due to: Main.quiz
11+Main.correct is possibly not total due to: Main.quiz
12+
13+totality015a.idr:47:3-49:28:
14+ |
15+47 | wrong nums ans score
16+ | ~~~~~~~~~~~~~~~~~~~~ ...
4−totality015a.idr:47:3-49:28:Main.wrong is possibly not total due to: Main.quiz
17+Main.wrong is possibly not total due to: Main.quiz
18+
test/totality016/expected+54−9
@@ -1,9 +1,54 @@
1+totality016.idr:15:1-21:
2+ |
3+15 | f1 (MkTP T1 x) = True
4+ | ~~~~~~~~~~~~~~~~~~~~~
1−totality016.idr:15:1-21:Main.f1 is not total as there are missing cases
5+Main.f1 is not total as there are missing cases
6+
7+totality016.idr:19:1-24:
8+ |
9+19 | f2 (MkTP T1 x, _) = True
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~
2−totality016.idr:19:1-24:Main.f2 is not total as there are missing cases
11+Main.f2 is not total as there are missing cases
12+
13+totality016.idr:23:1-29:
14+ |
15+23 | f3 ((MkTP T1 x, _), _) = True
16+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3−totality016.idr:23:1-29:Main.f3 is not total as there are missing cases
17+Main.f3 is not total as there are missing cases
18+
19+totality016.idr:27:1-14:
20+ |
21+27 | g1 T1 x = True
22+ | ~~~~~~~~~~~~~~
4−totality016.idr:27:1-14:Main.g1 is not total as there are missing cases
23+Main.g1 is not total as there are missing cases
24+
25+totality016.idr:31:1-17:
26+ |
27+31 | g2 (T1, x) = True
28+ | ~~~~~~~~~~~~~~~~~
5−totality016.idr:31:1-17:Main.g2 is not total as there are missing cases
29+Main.g2 is not total as there are missing cases
30+
31+totality016.idr:35:1-16:
32+ |
33+35 | h1 True x = True
34+ | ~~~~~~~~~~~~~~~~
6−totality016.idr:35:1-16:Main.h1 is not total as there are missing cases
35+Main.h1 is not total as there are missing cases
36+
37+totality016.idr:39:1-19:
38+ |
39+39 | h2 (True, x) = True
40+ | ~~~~~~~~~~~~~~~~~~~
7−totality016.idr:39:1-19:Main.h2 is not total as there are missing cases
41+Main.h2 is not total as there are missing cases
42+
43+totality016.idr:43:1-25:
44+ |
45+43 | h3 (MkTP2 (T1, x)) = True
46+ | ~~~~~~~~~~~~~~~~~~~~~~~~~
8−totality016.idr:43:1-25:Main.h3 is not total as there are missing cases
47+Main.h3 is not total as there are missing cases
48+
49+totality016.idr:47:1-30:
50+ |
51+47 | h4 (MkTP2 (T1, x), _) _ = True
52+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
9−totality016.idr:47:1-30:Main.h4 is not total as there are missing cases
53+Main.h4 is not total as there are missing cases
54+
test/totality017/expected+36−6
@@ -1,6 +1,36 @@
1+totality017.idr:19:1-15:
2+ |
3+19 | g1 T1 T1 = True
4+ | ~~~~~~~~~~~~~~~
1−totality017.idr:19:1-15:Main.g1 is not total as there are missing cases
5+Main.g1 is not total as there are missing cases
6+
7+totality017.idr:25:1-17:
8+ |
9+25 | g2 T1' T1' = True
10+ | ~~~~~~~~~~~~~~~~~
2−totality017.idr:25:1-17:Main.g2 is not total as there are missing cases
11+Main.g2 is not total as there are missing cases
12+
13+totality017.idr:31:1-13:
14+ |
15+31 | g3 T1' = True
16+ | ~~~~~~~~~~~~~
3−totality017.idr:31:1-13:Main.g3 is not total as there are missing cases
17+Main.g3 is not total as there are missing cases
18+
19+totality017.idr:37:1-36:
20+ |
21+37 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True
22+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4−totality017.idr:37:1-36:Main.g4 is not total as there are missing cases
23+Main.g4 is not total as there are missing cases
24+
25+totality017.idr:42:1-11:
26+ |
27+42 | f' 0 = True
28+ | ~~~~~~~~~~~
5−totality017.idr:42:1-11:Main.f' is not total as there are missing cases
29+Main.f' is not total as there are missing cases
30+
31+totality017.idr:47:1-17:
32+ |
33+47 | f (MkPP 0) = True
34+ | ~~~~~~~~~~~~~~~~~
6−totality017.idr:47:1-17:Main.f is not total as there are missing cases
35+Main.f is not total as there are missing cases
36+
test/totality018/expected+6−1
@@ -1 +1,6 @@
1+totality018.idr:12:1-10:
2+ |
3+12 | bar FZ = 0
4+ | ~~~~~~~~~~
1−totality018.idr:12:1-10:Main.bar is not total as there are missing cases
5+Main.bar is not total as there are missing cases
6+
test/totality019/expected+12−2
@@ -1,2 +1,12 @@
1+totality019.idr:8:1-36:
2+ |
3+8 | testCov False False = ?testCov_rhs_3
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1−totality019.idr:8:1-36:Main.testCov is not total as there are missing cases
5+Main.testCov is not total as there are missing cases
6+
7+totality019.idr:12:1-42:
8+ |
9+12 | testCov' (False ** False) = ?testCov_rhs_3
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2−totality019.idr:12:1-42:Main.testCov' is not total as there are missing cases
11+Main.testCov' is not total as there are missing cases
12+
test/totality020/expected+12−2
@@ -1,2 +1,12 @@
1+totality020.idr:4:14-23:
2+ |
3+4 | bug _ _ Refl impossible
4+ | ~~~~~~~~~~
1−totality020.idr:4:14-23:bug _ _ Refl is a valid case
5+bug _ _ Refl is a valid case
6+
7+totality020.idr:7:14-23:
8+ |
9+7 | foo a b Refl impossible
10+ | ~~~~~~~~~~
2−totality020.idr:7:14-23:foo a b Refl is a valid case
11+foo a b Refl is a valid case
12+
test/totality021/expected+20
@@ -1,10 +1,30 @@
1totality021.idr:8:1-67:
1totality021.idr:8:1-67:
2+ |
3+8 | sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'
5Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'
6+
3totality021.idr:12:1-66:
7totality021.idr:12:1-66:
8+ |
9+12 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'
11Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'
12+
5totality021.idr:18:1-26:
13totality021.idr:18:1-26:
14+ |
15+18 | v = sLevelNotSLevel l Refl
16+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~
6Main.v is possibly not total due to: Main.sLevelNotSLevel
17Main.v is possibly not total due to: Main.sLevelNotSLevel
18+
7totality021a.idr:9:1-37:
19totality021a.idr:9:1-37:
20+ |
21+9 | noNonEmptyPointInt {n} Nil impossible
22+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8Main.noNonEmptyPointInt is not total as there are missing cases
23Main.noNonEmptyPointInt is not total as there are missing cases
24+
9totality021a.idr:12:1-31:
25totality021a.idr:12:1-31:
26+ |
27+12 | myVoid = noNonEmptyPointInt [2]
28+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
10Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt
29Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt
30+
test/totality022/expected+6−1
@@ -1 +1,6 @@
1+totality022.idr:7:20-29:
2+ |
3+7 | f _ [] (RSnoc _ _) impossible -- = ?wat
4+ | ~~~~~~~~~~
1−totality022.idr:7:20-29:f _ [] (RSnoc _ _) is a valid case
5+f _ [] (RSnoc _ _) is a valid case
6+
test/totality023/expected+4
@@ -1,2 +1,6 @@
1totality023.idr:9:1-10:27:
1totality023.idr:9:1-10:27:
2+ |
3+9 | run (Do x f) = do r <- x
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~ ...
2Main.run is possibly not total due to recursive path Main.run --> Main.run
5Main.run is possibly not total due to recursive path Main.run --> Main.run
6+
test/tutorial002/expected+12
@@ -1,6 +1,18 @@
1tutorial002.idr:41:25-29:
1tutorial002.idr:41:25-29:
2+ |
3+41 | Main.natToBin_lemma_1 = proof
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3tutorial002.idr:48:18-22:
7tutorial002.idr:48:18-22:
8+ |
9+48 | parity_lemma_1 = proof
10+ | ~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
5tutorial002.idr:54:18-22:
13tutorial002.idr:54:18-22:
14+ |
15+54 | parity_lemma_2 = proof {
16+ | ~~~~~
6This style of tactic proof is deprecated. See %runElab for the replacement.
17This style of tactic proof is deprecated. See %runElab for the replacement.
18+
test/tutorial004/expected+8
@@ -1,4 +1,12 @@
1tutorial004.idr:46:14-18:
1tutorial004.idr:46:14-18:
2+ |
3+46 | plusredZ_S = proof {
4+ | ~~~~~
2This style of tactic proof is deprecated. See %runElab for the replacement.
5This style of tactic proof is deprecated. See %runElab for the replacement.
6+
3tutorial004.idr:53:14-18:
7tutorial004.idr:53:14-18:
8+ |
9+53 | plusredZ_Z = proof {
10+ | ~~~~~
4This style of tactic proof is deprecated. See %runElab for the replacement.
11This style of tactic proof is deprecated. See %runElab for the replacement.
12+
test/tutorial006/expected+9−1
@@ -1,4 +1,7 @@
1tutorial006a.idr:5:23-24:
1tutorial006a.idr:5:23-24:
2+ |
3+5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN
4+ | ~~
2When checking right hand side of vapp with expected type
5When checking right hand side of vapp with expected type
3 Vect (S len + m) a
6 Vect (S len + m) a
4
7
@@ -13,7 +16,11 @@ When checking argument xs to constructor Data.Vect.:::
13 plus len len
16 plus len len
14 and
17 and
15 plus len m
18 plus len m
19+
16−tutorial006b.idr:10:37-50:
20+tutorial006b.idr:10:39-50:
21+ |
22+10 | parity (S (S (j + j))) | Even = Even {n=S j}
23+ | ~~~~~~~~~~~~
17When checking right hand side of with block in Main.parity with expected type
24When checking right hand side of with block in Main.parity with expected type
18 Parity (S (S (j + j)))
25 Parity (S (S (j + j)))
19
26
@@ -27,3 +34,4 @@ Specifically:
27 plus (S j) (S j)
34 plus (S j) (S j)
28 and
35 and
29 S (S (plus j j))
36 S (S (plus j j))
37+
test/unique004/expected+58−9
@@ -1,26 +1,75 @@
1+unique001a.idr:35:16-43:50:
2+ |
3+35 | showStuff xs = do
4+ | ~~ ...
1−unique001a.idr:35:14-43:50:Type mismatch between
5+Type mismatch between
2 Int -> String
6 Int -> String
3and
7and
4 UniqueType (Int -> String)
8 UniqueType (Int -> String)
9+
10+unique001a.idr:46:17-54:28:
11+ |
12+46 | showStuff' xs = do
13+ | ~~ ...
5−unique001a.idr:46:15-54:28:Type mismatch between
14+Type mismatch between
6 Int -> String
15 Int -> String
7and
16and
8 UniqueType (Int -> String)
17 UniqueType (Int -> String)
18+
19+unique001a.idr:57:17-62:33:
20+ |
21+57 | showThings xs = do
22+ | ~~ ...
9−unique001a.idr:57:15-62:33:Type mismatch between
23+Type mismatch between
10 UniqueType (Int -> String)
24 UniqueType (Int -> String)
11and
25and
12 Int -> String
26 Int -> String
27+
28+unique001b.idr:18:19-42:
29+ |
30+18 | showU (x :: xs) = show x ++ "," ++ free xs
31+ | ~~~~~~~~~~~~~~~~~~~~~~~~
13−unique001b.idr:18:17-42:Borrowed name xs must not be used on RHS
32+Borrowed name xs must not be used on RHS
33+
34+unique001c.idr:47:14-62:
35+ |
36+47 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)
37+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
14−unique001c.idr:47:12-62:Unique name f is used more than once
38+Unique name f is used more than once
39+
40+unique001d.idr:4:18:
41+ |
42+4 | steal (Read x) = x
43+ | ^
15−unique001d.idr:4:16-18:Borrowed name x must not be used on RHS
44+Borrowed name x must not be used on RHS
45+
16unique001e.idr:4:12-40:
46unique001e.idr:4:12-40:
47+ |
48+4 | Nil : {a : UniqueType} -> BadList a
49+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
17Constructor Main.Nil has a UniqueType, but the data type does not
50Constructor Main.Nil has a UniqueType, but the data type does not
51+
52+unique002.idr:17:10-20:19:
53+ |
54+17 | foo xs = do -- let f = \x : Int => showU xs
55+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
18−unique002.idr:17:8-20:19:Unique name xs is used more than once
56+Unique name xs is used more than once
57+
58+unique002a.idr:17:10-20:19:
59+ |
60+17 | foo xs = do let f = \x : Int => showU xs
61+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
19−unique002a.idr:17:8-20:19:Type mismatch between
62+Type mismatch between
20 Int -> String
63 Int -> String
21and
64and
22 UniqueType (Int -> String)
65 UniqueType (Int -> String)
66+
67+unique003.idr:20:10-24:19:
68+ |
69+20 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context
70+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
23−unique003.idr:20:8-24:19:Type mismatch between
71+Type mismatch between
24 Int -> String
72 Int -> String
25and
73and
26 UniqueType (Int -> String)
74 UniqueType (Int -> String)
75+
test/universes001/expected+8−3
@@ -1,9 +1,14 @@
1+universes001.idr:7:7-21:
2+ |
3+7 | foo = Const (Const 0)
4+ | ~~~~~~~~~~~~~~~
1−universes001.idr:7:5-21:Universe inconsistency.
5+Universe inconsistency.
2 Working on: ./universes001.idr.x
6 Working on: ./universes001.idr.x
3 Old domain: (5,5)
7 Old domain: (5,5)
4 New domain: (5,4)
8 New domain: (5,4)
5 Involved constraints:
9 Involved constraints:
6− ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}
10+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:7-21}
7 ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}
11 ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}
8 ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}
12 ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}
9− ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}
13+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:7-21}
14+
test/universes002/expected+8−3
@@ -1,9 +1,14 @@
1+universes002.idr:45:11-48:
2+ |
3+45 | russell = lemma (MkMPair (MkMPair R lemma) REFL)
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1−universes002.idr:45:9-48:Universe inconsistency.
5+Universe inconsistency.
2 Working on: ./universes002.idr.b1
6 Working on: ./universes002.idr.b1
3 Old domain: (5,5)
7 Old domain: (5,5)
4 New domain: (5,4)
8 New domain: (5,4)
5 Involved constraints:
9 Involved constraints:
6− ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}
10+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:11-48}
7 ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}
11 ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}
8− ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}
12+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:11-48}
9 ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}
13 ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}
14+