idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity

More improvements

Browse Source 
- More migrations from String to Doc
- File context in parser errors
This commit is contained in:
Giuseppe Lomurno 2020-08-12 00:27:52 +02:00 committed by G. Allais
parent 607352a191
commit f658ce357f
33 changed files with 195 additions and 68 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Core.idr
View File

@ -133,7 +133,7 @@ data Error : Type where
GenericMsg : FC -> String -> Error
TTCError : TTCErrorMsg -> Error
FileErr : String -> FileError -> Error
ParseFail : Show token =>
ParseFail : (Show token, Pretty token) =>
FC -> ParseError token -> Error
ModuleNotFound : FC -> List String -> Error
CyclicImports : List (List String) -> Error

6
src/Core/TT.idr
View File

@ -611,11 +611,11 @@ export
Show PartialReason where
show NotStrictlyPositive = "not strictly positive"
show (BadCall [n])
= "possibly not terminating due to call to " ++ show n
= "possibly not terminating due to call to " ++ show n
show (BadCall ns)
= "possibly not terminating due to calls to " ++ showSep ", " (map show ns)
= "possibly not terminating due to calls to " ++ showSep ", " (map show ns)
show (RecPath ns)
= "possibly not terminating due to recursive path " ++ showSep " -> " (map show ns)
= "possibly not terminating due to recursive path " ++ showSep " -> " (map show ns)
export
Pretty PartialReason where

107
src/Idris/Error.idr
View File

@ -15,6 +15,7 @@ import Idris.Pretty
import Parser.Source
import Data.List
import Data.List1
import Data.List.Extra
import Data.Maybe
import Data.Stream
@ -23,9 +24,13 @@ import Data.String.Extra
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Util
import System.File
import Utils.String
%default covering
joinNs : List String -> Doc (IdrisAnn)
joinNs ns = concatWith (surround dot) (pretty <$> reverse ns)
pshow : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -48,21 +53,83 @@ ploc : {auto o : Ref ROpts REPLOpts} ->
FC -> Core (Doc IdrisAnn)
ploc EmptyFC = pure emptyDoc
ploc fc@(MkFC fn s e) = do
let sr = fromInteger $ cast $ fst s
let sc = fromInteger $ cast $ snd s
let er = fromInteger $ cast $ fst e
let ec = fromInteger $ cast $ snd e
let (sr, sc) = bimap (fromInteger . cast) s
let (er, ec) = bimap (fromInteger . cast) e
let nsize = length $ show (er + 1)
let head = annotate FileCtxt (pretty fc)
let firstRow = annotate FileCtxt (spaces (cast $ nsize + 2) <+> pipe)
source <- lines <$> getCurrentElabSource
if sr == er
then do
let firstRow = annotate FileCtxt (spaces (cast $ nsize + 2) <+> pipe)
let line = (annotate FileCtxt pipe) <++> maybe emptyDoc pretty (elemAt source sr)
let emph = (annotate FileCtxt pipe) <++> spaces (cast sc) <+> annotate Error (pretty (Extra.replicate (ec `minus` sc) '^'))
pure $ vsep [emptyDoc, head, firstRow, annotate FileCtxt (space <+> pretty (sr + 1)) <++> align (vsep [line, emph]), emptyDoc]
else pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr (pretty <$> extractRange sr (Prelude.min er (sr + 5)) source)) <+> line
where
bimap : (a -> b) -> (a, a) -> (b, b)
bimap f (x, y) = (f x, f y)
extractRange : Nat -> Nat -> List String -> List String
extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
pad : Nat -> String -> String
pad size s = replicate (size `minus` length s) '0' ++ s
addLineNumbers : Nat -> Nat -> List (Doc IdrisAnn) -> List (Doc IdrisAnn)
addLineNumbers size st xs =
snd $ foldl (\(i, s), l => (S i, snoc s (space <+> annotate FileCtxt (pretty (pad size $ show $ i + 1) <++> pipe) <++> l))) (st, []) xs
-- Assumes the two FCs are sorted
ploc2 : {auto o : Ref ROpts REPLOpts} ->
FC -> FC -> Core (Doc IdrisAnn)
ploc2 fc EmptyFC = ploc fc
ploc2 EmptyFC fc = ploc fc
ploc2 (MkFC fn1 s1 e1) (MkFC fn2 s2 e2) =
do let (sr1, sc1) = bimap (fromInteger . cast) s1
let (sr2, sc2) = bimap (fromInteger . cast) s2
let (er1, ec1) = bimap (fromInteger . cast) e1
let (er2, ec2) = bimap (fromInteger . cast) e2
if (er2 > er1 + 5)
then pure $ !(ploc (MkFC fn1 s1 e1)) <+> line <+> !(ploc (MkFC fn2 s2 e2))
else do let nsize = length $ show (er2 + 1)
let head = annotate FileCtxt (pretty $ MkFC fn1 s1 e2)
let firstRow = annotate FileCtxt (spaces (cast $ nsize + 2) <+> pipe)
source <- lines <$> getCurrentElabSource
case (sr1 == er1, sr2 == er2, sr1 == sr2) of
(True, True, True) => do
let line = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty (Extra.replicate (ec1 `minus` sc1) '^'))
<+> spaces (cast $ sc2 `minus` ec1) <+> error (pretty (Extra.replicate (ec2 `minus` sc2) '^'))
pure $ vsep [emptyDoc, head, firstRow, fileCtxt (space <+> pretty (sr1 + 1)) <++> align (vsep [line, emph]), emptyDoc]
(True, True, False) => do
let line1 = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
let emph1 = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty (Extra.replicate (ec1 `minus` sc1) '^'))
let line2 = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr2)
let emph2 = fileCtxt pipe <++> spaces (cast sc2) <+> error (pretty (Extra.replicate (ec2 `minus` sc2) '^'))
let numbered = if (sr2 `minus` er1) == 1
then []
else addLineNumbers nsize (sr1 + 1) (pretty <$> extractRange (sr1 + 1) er1 source)
pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> pretty (sr1 + 1)) <++> align (vsep [line1, emph1])]
++ numbered
++ [fileCtxt (space <+> pretty (sr2 + 1)) <++> align (vsep [line2, emph2]), emptyDoc]
(True, False, _) => do
let line = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty (Extra.replicate (ec1 `minus` sc1) '^'))
pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> pretty (sr1 + 1)) <++> align (vsep [line, emph])]
++ addLineNumbers nsize (sr1 + 1) (pretty <$> extractRange (sr1 + 1) (Prelude.max er1 er2) source)
++ [emptyDoc]
(False, True, True) => do
let line = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty (Extra.replicate (ec1 `minus` sc1) '^'))
pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> pretty (sr1 + 1)) <++> align (vsep [line, emph])]
++ addLineNumbers nsize (sr1 + 1) (pretty <$> extractRange (sr1 + 1) (Prelude.max er1 er2) source)
++ [emptyDoc]
(False, True, False) => do
let top = addLineNumbers nsize (sr1 + 1) (pretty <$> extractRange (sr1 + 1) er1 source)
let line = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
let emph = fileCtxt pipe <++> spaces (cast sc2) <+> error (pretty (Extra.replicate (ec2 `minus` sc2) '^'))
pure $ vsep $ [emptyDoc, head, firstRow] ++ top ++ [fileCtxt (space <+> pretty (sr2 + 1)) <++> align (vsep [line, emph]), emptyDoc]
(_, _, _) => pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr1 (pretty <$> extractRange sr1 er2 source)) <+> line
where
bimap : (a -> b) -> (a, a) -> (b, b)
bimap f (x, y) = (f x, f y)
extractRange : Nat -> Nat -> List String -> List String
extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
pad : Nat -> String -> String
@ -90,15 +157,22 @@ perror (CantSolveEq fc env l r)
, code !(pshow env r) <+> dot
]) <+> line <+> !(ploc fc)
perror (PatternVariableUnifies fc env n tm)
= pure $ errorDesc (hsep [ reflow "Pattern variable"
= do let (min, max) = order fc (getLoc tm)
pure $ errorDesc (hsep [ reflow "Pattern variable"
, code (prettyVar n)
, reflow "unifies with" <+> colon
, code !(pshow env tm) <+> dot
]) <+> line <+> !(ploc fc)
]) <+> line <+> !(ploc2 min max) <+> line
<+> reflow "Suggestion: Use the same name for both pattern variables, since they unify."
where
prettyVar : Name -> Doc IdrisAnn
prettyVar (PV n _) = prettyVar n
prettyVar n = pretty n
order : FC -> FC -> (FC, FC)
order EmptyFC fc2 = (EmptyFC, fc2)
order fc1 EmptyFC = (fc1, EmptyFC)
order fc1@(MkFC _ sr1 sc1) fc2@(MkFC _ sr2 sc2) =
if sr1 < sr2 then (fc1, fc2) else if sr1 == sr2 && sc1 < sc2 then (fc1, fc2) else (fc2, fc1)
perror (CyclicMeta fc env n tm)
= pure $ errorDesc (reflow "Cycle detected in solution of metavariable" <++> meta (pretty !(prettyName n)) <++> equals
<++> code !(pshow env tm)) <+> line <+> !(ploc fc)
@ -114,7 +188,7 @@ perror (UndefinedName fc x)
= pure $ errorDesc (reflow "Undefined name" <++> code (pretty x) <+> dot) <++> line <+> !(ploc fc)
perror (InvisibleName fc n (Just ns))
= pure $ errorDesc ("Name" <++> code (pretty n) <++> reflow "is inaccessible since"
<++> code (concatWith (surround dot) (pretty <$> reverse ns)) <++> reflow "is not explicitly imported.")
<++> code (joinNs ns) <++> reflow "is not explicitly imported.")
<+> line <+> !(ploc fc)
<+> line <+> reflow "Suggestion: add an explicit" <++> keyword "export" <++> "or" <++> keyword ("public" <++> "export")
<++> reflow "modifier. By default, all names are" <++> keyword "private" <++> reflow "in namespace blocks."
@ -134,7 +208,7 @@ perror (NotCovering fc n (MissingCases cs))
= pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not covering.")
<+> line <+> !(ploc fc) <+> line
<+> reflow "Missing cases" <+> colon <+> line
<+> indent 4 (vsep !(traverse (pshow []) cs))
<+> indent 4 (vsep !(traverse (pshow []) cs)) <+> line
perror (NotCovering fc n (NonCoveringCall ns))
= pure $ errorDesc (pretty !(prettyName n) <++> reflow "is not covering.")
<+> line <+> !(ploc fc) <+> line
@ -244,7 +318,7 @@ perror (TryWithImplicits fc env imps)
tshow env (n, ty) = pure $ pretty n <++> colon <++> code !(pshow env ty)
perror (BadUnboundImplicit fc env n ty)
= pure $ errorDesc (reflow "Can't bind name" <++> code (pretty (nameRoot n)) <++> reflow "with type" <++> code !(pshow env ty)
<+> colon) <+> line <+> !(ploc fc) <+> line <+> reflow "Suggestion: try binding explicitly."
<+> colon) <+> line <+> !(ploc fc) <+> line <+> reflow "Suggestion: try an explicit bind."
perror (CantSolveGoal fc env g)
= let (_ ** (env', g')) = dropEnv env g in
pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env' g')
@ -264,7 +338,7 @@ perror (DeterminingArg fc n i env g)
<+> reflow "since I can't infer a value for argument" <++> code (pretty n) <+> dot)
<+> line <+> !(ploc fc)
perror (UnsolvedHoles hs)
= pure $ errorDesc (reflow "unsolved holes" <+> colon) <+> line <+> !(prettyHoles hs)
= pure $ errorDesc (reflow "Unsolved holes" <+> colon) <+> line <+> !(prettyHoles hs)
where
prettyHoles : List (FC, Name) -> Core (Doc IdrisAnn)
prettyHoles [] = pure emptyDoc
@ -332,14 +406,11 @@ perror (TTCError msg)
perror (FileErr fname err)
= pure $ errorDesc (reflow "File error in" <++> pretty fname <++> colon) <++> pretty (show err)
perror (ParseFail _ err)
= pure $ pretty (show err)
perror (ModuleNotFound _ ns)
= pure $ errorDesc (concatWith (surround dot) (pretty <$> reverse ns) <++> reflow "not found")
= pure $ pretty err
perror (ModuleNotFound fc ns)
= pure $ errorDesc ("Module" <++> annotate FileCtxt (joinNs ns) <++> reflow "not found") <+> line <+> !(ploc fc)
perror (CyclicImports ns)
= pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround (pretty " -> ")) (prettyMod <$> ns)
where
prettyMod : List String -> Doc IdrisAnn
prettyMod ns = concatWith (surround dot) (pretty <$> reverse ns)
= pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround (pretty " -> ")) (joinNs <$> ns)
perror ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness")
perror (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty str
perror (UserError str) = pure $ errorDesc (pretty "Error" <+> colon) <++> pretty str

2
src/Idris/IDEMode/REPL.idr
View File

@ -327,7 +327,7 @@ displayIDEResult outf i (REPL $ ProofFound x)
displayIDEResult outf i (REPL $ Missed cases)
= printIDEResult outf i
$ StringAtom $ showSep "\n"
$ map handleMissing cases
$ map handleMissing' cases
displayIDEResult outf i (REPL $ CheckedTotal xs)
= printIDEResult outf i
$ StringAtom $ showSep "\n"

1
src/Idris/Package.idr
View File

@ -24,6 +24,7 @@ import System.Directory
import System.File
import Text.Parser
import Text.PrettyPrint.Prettyprinter
import Utils.Binary
import Utils.String
import Utils.Path

8
src/Idris/Pretty.idr
View File

@ -32,10 +32,18 @@ colorAnn Keyword = color Red
colorAnn Pragma = color BrightMagenta
colorAnn Meta = color Green
export
error : Doc IdrisAnn -> Doc IdrisAnn
error = annotate Error
export
errorDesc : Doc IdrisAnn -> Doc IdrisAnn
errorDesc = annotate ErrorDesc
export
fileCtxt : Doc IdrisAnn -> Doc IdrisAnn
fileCtxt = annotate FileCtxt
export
keyword : Doc IdrisAnn -> Doc IdrisAnn
keyword = annotate Keyword

20
src/Idris/REPL.idr
View File

@ -913,13 +913,23 @@ mutual
prompt Execute = "[exec] "
export
handleMissing : MissedResult -> String
handleMissing (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs
handleMissing (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function"
handleMissing' : MissedResult -> String
handleMissing' (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs
handleMissing' (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function"
++ (case ns of
[f] => " " ++ show f
_ => "s: " ++ showSep ", " (map show ns)))
handleMissing (AllCasesCovered fn) = show fn ++ ": All cases covered"
handleMissing' (AllCasesCovered fn) = show fn ++ ": All cases covered"
export
handleMissing : MissedResult -> Doc IdrisAnn
handleMissing (CasesMissing x xs) = pretty x <+> colon <++> vsep (code . pretty <$> xs)
handleMissing (CallsNonCovering fn ns) =
pretty fn <+> colon <++> reflow "Calls non covering"
<++> (case ns of
[f] => "function" <++> code (pretty f)
_ => "functions:" <++> concatWith (surround (comma <+> space)) (code . pretty <$> ns))
handleMissing (AllCasesCovered fn) = pretty fn <+> colon <++> reflow "All cases covered"
export
handleResult : {auto c : Ref Ctxt Defs} ->
@ -951,7 +961,7 @@ mutual
displayResult CompilationFailed = printError (reflow "Compilation failed")
displayResult (Compiled f) = printResult (pretty "File" <++> pretty f <++> pretty "written")
displayResult (ProofFound x) = printResult (prettyTerm x)
displayResult (Missed cases) = printResult $ pretty $ showSep "\n" $ map handleMissing cases -- FIXME
displayResult (Missed cases) = printResult $ vsep (handleMissing <$> cases)
displayResult (CheckedTotal xs) = printResult (vsep (map (\(fn, tot) => pretty fn <++> pretty "is" <++> pretty tot) xs))
displayResult (FoundHoles []) = printResult (reflow "No holes")
displayResult (FoundHoles [x]) = printResult (reflow "1 hole" <+> colon <++> pretty x.name)

11
src/Parser/Lexer/Package.idr
View File

@ -4,6 +4,7 @@ import public Parser.Lexer.Common
import public Text.Lexer
import public Text.Parser
import public Text.Bounded
import Text.PrettyPrint.Prettyprinter
import Data.List
import Data.List1
@ -33,6 +34,16 @@ Show Token where
show Space = "Space"
show (StringLit s) = "StringLit: " ++ s
public export
Pretty Token where
pretty (Comment str) = "Comment:" <++> pretty str
pretty EndOfInput = "EndOfInput"
pretty Equals = "Equals"
pretty (DotSepIdent dsid) = "DotSepIdentifier:" <++> concatWith (surround dot) (pretty <$> List1.toList dsid)
pretty Separator = "Separator"
pretty Space = "Space"
pretty (StringLit s) = "StringLit:" <++> pretty s
equals : Lexer
equals = is '='

8
src/Parser/Support.idr
View File

@ -8,6 +8,7 @@ import Text.PrettyPrint.Prettyprinter.Util
import Core.TT
import Data.List
import Data.List.Views
import Data.Strings
import Parser.Unlit
import System.File
@ -35,7 +36,12 @@ Show tok => Show (ParseError tok) where
export
Pretty tok => Pretty (ParseError tok) where
pretty (ParseFail err loc toks)
= reflow "Parse error:" <++> pretty err <++> parens (reflow "next tokens:" <++> pretty (take 10 toks))
= reflow "Parse error" <+> prettyLine loc <+> ":" <+> line <+> pretty err <++> parens (reflow "next tokens:"
<++> brackets (align $ concatWith (surround (comma <+> space)) (pretty <$> take 10 toks)))
where
prettyLine : Maybe (Int, Int) -> Doc ann
prettyLine Nothing = emptyDoc
prettyLine (Just (r, c)) = space <+> "at" <++> "line" <++> pretty (r + 1) <+> ":" <+> pretty (c + 1)
pretty (LexFail (c, l, str))
= reflow "Lex error at" <++> pretty (c, l) <++> pretty "input:" <++> pretty str
pretty (FileFail err)

3
tests/chez/chez006/expected
View File

@ -11,8 +11,7 @@
42
1/1: Building TypeCase (TypeCase.idr)
Main> Main> Main.strangeId is total
Main> Main.strangeId':
strangeId' _
Main> Main.strangeId': strangeId' _
Main> Bye for now!
1/1: Building TypeCase2 (TypeCase2.idr)
Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument).

2
tests/idris2/basic005/expected
View File

@ -1,5 +1,5 @@
1/1: Building NoInfer (NoInfer.idr)
Error: unsolved holes:
Error: Unsolved holes:
Main.{_:1} introduced at:
NoInfer.idr:1:7--1:8
|

5
tests/idris2/basic011/expected
View File

@ -10,8 +10,9 @@ Dots2.idr:2:7--2:8
1/1: Building Dots3 (Dots3.idr)
Error: While processing left hand side of addBaz. Pattern variable z unifies with: ?y [no locals in scope].
Dots3.idr:5:29--5:30
Dots3.idr:5:13--5:30
|
5 | addBaz (x + y) (AddThings x z) = x + y
| ^
| ^ ^
Suggestion: Use the same name for both pattern variables, since they unify.

6
tests/idris2/basic025/expected
View File

@ -6,6 +6,8 @@ Main> [1, 2, 3, 4]
Main> [4, 3, 2, 1]
Main> [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
Main> [100, 99, 98, 97, 96, 95, 94, 93, 92, 91]
Main> Parse error: Invalid list range syntax (next tokens: [end of input])
Main> Parse error: Invalid list range syntax (next tokens: [end of input])
Main> Parse error at line 1:12:
Invalid list range syntax (next tokens: [end of input])
Main> Parse error at line 1:7:
Invalid list range syntax (next tokens: [end of input])
Main> Bye for now!

3
tests/idris2/coverage001/expected
View File

@ -1,6 +1,5 @@
1/1: Building Vect (Vect.idr)
Main> Main.append:
append (_ :: _) _
Main> Main.append: append (_ :: _) _
Main> Main.lookup: All cases covered
Main> Main.zip: All cases covered
Main> Bye for now!

3
tests/idris2/coverage002/expected
View File

@ -1,7 +1,6 @@
1/1: Building Vect (Vect.idr)
Main> Main.append: All cases covered
Main> Main.funny: All cases covered
Main> Main.notFunny:
notFunny (False :: (False :: (True :: (True :: _))))
Main> Main.notFunny: notFunny (False :: (False :: (True :: (True :: _))))
notFunny (False :: (True :: (True :: (True :: _))))
Main> Bye for now!

6
tests/idris2/coverage003/expected
View File

@ -6,10 +6,8 @@ Cover.idr:16:1--16:7
16 | badBar Z = Z
| ^^^^^^
Main> Main.foo:
foo (0, S _)
Main> Main.foo: foo (0, S _)
foo (S _, _)
Main> Main.bar:
bar _
Main> Main.bar: bar _
Main> Main.cty: All cases covered
Main> Bye for now!

3
tests/idris2/coverage004/expected
View File

@ -6,7 +6,6 @@ Cover.idr:14:1--14:4
14 | bad (Just 0) _ = False
| ^^^
Main> Main.okay:
okay (S _) IsNat
Main> Main.okay: okay (S _) IsNat
okay False IsBool
Main> Bye for now!

8
tests/idris2/error009/expected
View File

@ -1,2 +1,8 @@
Error: DoesntExist not found
Error: Module DoesntExist not found
Exists.idr:1:1--1:19
|
1 | import DoesntExist
| ^^^^^^^^^^^^^^^^^^
Main> Bye for now!

3
tests/idris2/interpreter003/expected
View File

@ -10,5 +10,6 @@ Main> "test"
Main> Imported module Data.Strings
Main> "hello"
Main> True
Main> Error loading module DoesNotExists: DoesNotExists not found
Main> Error loading module DoesNotExists: Module DoesNotExists not found
Main> Bye for now!

4
tests/idris2/perror001/expected
View File

@ -1,2 +1,4 @@
1/1: Building PError (PError.idr)
Error: Parse error: Expected ')' (next tokens: [identifier bar, identifier x, symbol =, let, identifier y, symbol =, literal 42, in, identifier y, symbol +])
Error: Parse error at line 5:1:
Expected ')' (next
tokens: [identifier bar, identifier x, symbol =, let, identifier y, symbol =, literal 42, in, identifier y, symbol +])

5
tests/idris2/perror002/expected
View File

@ -1,2 +1,5 @@
1/1: Building PError (PError.idr)
Error: Parse error: Expected ')' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input])
Error: Parse error at line 7:1:
Expected ')' (next
tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end
of input])

4
tests/idris2/perror003/expected
View File

@ -1,2 +1,4 @@
1/1: Building PError (PError.idr)
Error: Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz, symbol :, identifier Int, symbol ->])
Error: Parse error at line 5:17:
Expected 'case', 'if', 'do', application or operator expression (next
tokens: [symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz, symbol :, identifier Int, symbol ->])

4
tests/idris2/perror004/expected
View File

@ -1,2 +1,4 @@
1/1: Building PError (PError.idr)
Error: Parse error: Wrong number of 'with' arguments (next tokens: [symbol =, identifier x, identifier foo, identifier x, identifier y, symbol |, identifier True, symbol |, identifier True, symbol =])
Error: Parse error at line 4:33:
Wrong number of 'with' arguments (next
tokens: [symbol =, identifier x, identifier foo, identifier x, identifier y, symbol |, identifier True, symbol |, identifier True, symbol =])

5
tests/idris2/perror005/expected
View File

@ -1,2 +1,5 @@
1/1: Building PError (PError.idr)
Error: Parse error: Expected 'in' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input])
Error: Parse error at line 7:1:
Expected 'in' (next
tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end
of input])

5
tests/idris2/perror006/expected
View File

@ -1,2 +1,5 @@
1/1: Building PError (PError.idr)
Error: Parse error: Expected 'else' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input])
Error: Parse error at line 7:1:
Expected 'else' (next
tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end
of input])

10
tests/idris2/reg034/expected
View File

@ -1,6 +1,8 @@
1/1: Building void (void.idr)
void.idr:18:19--18:20:While processing left hand side of Calc at void.idr:18:1--20:1:
Can't match on ?y [no locals in scope] (Non linear pattern variable) at
18 Calc {y} ((~~) {z=y} {y=y} der (MkDPair y Refl)) = Calc der
^
Error: While processing left hand side of Calc. Can't match on ?y [no locals in scope] (Non linear pattern variable).
void.idr:18:19--18:20
|
18 | Calc {y} ((~~) {z=y} {y=y} der (MkDPair y Refl)) = Calc der
| ^

2
tests/idris2/reg034/run
View File

@ -1,3 +1,3 @@
$1 --check void.idr
$1 --no-color --check void.idr
rm -rf build

3
tests/idris2/total001/expected
View File

@ -1,6 +1,5 @@
1/1: Building Total (Total.idr)
Main> Main.lookup: All cases covered
Main> Main.lookup':
lookup' FZ _
Main> Main.lookup': lookup' FZ _
Main> Main.lookup'': Calls non covering function Main.lookup'
Main> Bye for now!

6
tests/idris2/total003/expected
View File

@ -1,8 +1,6 @@
1/1: Building Total (Total.idr)
Main> Main.onlyOne:
onlyOne _
Main> Main.onlyOne: onlyOne _
Main> Main.covered: All cases covered
Main> Main.matchInt: All cases covered
Main> Main.matchInt':
matchInt' _ _ _
Main> Main.matchInt': matchInt' _ _ _
Main> Bye for now!

1
tests/idris2/total007/expected
View File

@ -8,6 +8,7 @@ partial.idr:5:1--7:4
Missing cases:
foo Nothing
Error: qsortBad is not total, possibly not terminating due to recursive
path Main.qsortBad -> Main.qsortBad -> Main.qsortBad

1
tests/idris2/total008/expected
View File

@ -7,3 +7,4 @@ partial.idr:11:1--13:1
Missing cases:
foo (Just _)

3
tests/idris2/with003/expected
View File

@ -71,5 +71,6 @@ Mismatch between: Vect 0 ?elem and List ?a.
| ^^^^^^^
Main> the (Maybe Int) (pure 4) : Maybe Int
Main> Parse error: Unrecognised command (next tokens: [identifier t, with, symbol [, symbol ], literal 4, end of input])
Main> Parse error at line 1:2:
Unrecognised command (next tokens: [identifier t, with, symbol [, symbol ], literal 4, end of input])
Main> Bye for now!

3
tests/node/node006/expected
View File

@ -11,8 +11,7 @@
42
1/1: Building TypeCase (TypeCase.idr)
Main> Main> Main.strangeId is total
Main> Main.strangeId':
strangeId' _
Main> Main.strangeId': strangeId' _
Main> Bye for now!
1/1: Building TypeCase2 (TypeCase2.idr)
Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument).