idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 18:51:40 +03:00
Code Issues Projects Releases Wiki Activity
f67b303cca
Idris2/tests/idris2/perf/perf005/expected

46 lines
1.2 KiB
Plaintext
Raw Normal View History

Fix DPair parsing
2020-09-05 12:03:35 +03:00
1/2: Building NoRegression (NoRegression.idr)
2/2: Building Lambda (Lambda.idr)
Made unifying error msg nicer. (#1922) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-09-15 13:57:50 +03:00
Error: While processing right hand side of term. When unifying:
Term ?g (TyFunc ?tyA (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat))))))))
and:
Term Empty (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat)))))))
Adds bounds to compiler parser - Added primitive to compiler parser for precise text boundaries - Reworked parser with the new primitive
2020-08-05 02:00:40 +03:00
Mismatch between: TyFunc TyNat TyNat and TyNat.
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
Lambda:62:3--88:9
Fix DPair parsing
2020-09-05 12:03:35 +03:00
62 | Func
63 | (Func
64 | (Func
65 | (Func
66 | (Func
67 | (Func
Refactor grammar for dependent pairs As it was, there was significant backtracking for big expressions, getting to the end, not finding a **, so having to try again for application expressions. Fixes #532
2020-08-07 18:30:25 +03:00
Fix another DPair parsing regression
2020-10-02 12:40:20 +03:00
1/1: Building Bad1 (Bad1.idr)
[ new ] semantic highlighting in REPL & holes (#1836)
2021-08-13 18:00:54 +03:00
Error: Couldn't parse any alternatives:
1: Not the end of a block entry.
Improve parse error report Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-11 16:51:41 +03:00
[ new ] semantic highlighting in REPL & holes (#1836)
2021-08-13 18:00:54 +03:00
Bad1:3:20--3:21
[ test ] fix test suite output
2021-02-15 12:56:48 +03:00
1 | module Bad1
2 |
Improve parse error report Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-11 16:51:41 +03:00
3 | data Bad = BadDCon (x : Nat)
[ new ] semantic highlighting in REPL & holes (#1836)
2021-08-13 18:00:54 +03:00
^
... (2 others)
Fix another DPair parsing regression
2020-10-02 12:40:20 +03:00
1/1: Building Bad2 (Bad2.idr)
[ breaking ] remove parsing of dangling binders (#1711) * [ breaking ] remove parsing of dangling binders It used to be the case that ``` ID : Type -> Type ID a = a test : ID (a : Type) -> a -> a test = \ a, x => x ``` and ``` head : List $ a -> Maybe a head [] = Nothing head (x :: _) = Just x ``` were accepted but these are now rejected because: * `ID (a : Type) -> a -> a` is parsed as `(ID (a : Type)) -> a -> a` * `List $ a -> Maybe a` is parsed as `List (a -> Maybe a)` Similarly if you want to use a lambda / rewrite / let expression as part of the last argument of an application, the use of `$` or parens is now mandatory. This should hopefully allow us to make progress on #1703
2021-08-10 21:24:32 +03:00
Error: Cannot return a named argument.
Improve parse error report Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-11 16:51:41 +03:00
[ breaking ] remove parsing of dangling binders (#1711) * [ breaking ] remove parsing of dangling binders It used to be the case that ``` ID : Type -> Type ID a = a test : ID (a : Type) -> a -> a test = \ a, x => x ``` and ``` head : List $ a -> Maybe a head [] = Nothing head (x :: _) = Just x ``` were accepted but these are now rejected because: * `ID (a : Type) -> a -> a` is parsed as `(ID (a : Type)) -> a -> a` * `List $ a -> Maybe a` is parsed as `List (a -> Maybe a)` Similarly if you want to use a lambda / rewrite / let expression as part of the last argument of an application, the use of `$` or parens is now mandatory. This should hopefully allow us to make progress on #1703
2021-08-10 21:24:32 +03:00
Bad2:3:13--3:29
[ test ] fix test suite output
2021-02-15 12:56:48 +03:00
1 | module Bad2
2 |
Improve parse error report Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-11 16:51:41 +03:00
3 | badReturn : (whatever : Int)
[ breaking ] remove parsing of dangling binders (#1711) * [ breaking ] remove parsing of dangling binders It used to be the case that ``` ID : Type -> Type ID a = a test : ID (a : Type) -> a -> a test = \ a, x => x ``` and ``` head : List $ a -> Maybe a head [] = Nothing head (x :: _) = Just x ``` were accepted but these are now rejected because: * `ID (a : Type) -> a -> a` is parsed as `(ID (a : Type)) -> a -> a` * `List $ a -> Maybe a` is parsed as `List (a -> Maybe a)` Similarly if you want to use a lambda / rewrite / let expression as part of the last argument of an application, the use of `$` or parens is now mandatory. This should hopefully allow us to make progress on #1703
2021-08-10 21:24:32 +03:00
^^^^^^^^^^^^^^^^
Fix another DPair parsing regression
2020-10-02 12:40:20 +03:00
1/1: Building Bad3 (Bad3.idr)
Small improve Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-12 09:01:12 +03:00
Error: Couldn't parse declaration.
Improve parse error report Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-11 16:51:41 +03:00
[ cosmetic ] use the whole range when underlining the problem
2021-07-15 00:49:57 +03:00
Bad3:4:1--4:8
[ test ] fix test suite output
2021-02-15 12:56:48 +03:00
1 | module Bad3
2 |
3 | badExpr : ()
Improve parse error report Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-11 16:51:41 +03:00
4 | badExpr (whatever : ())
[ cosmetic ] use the whole range when underlining the problem
2021-07-15 00:49:57 +03:00
^^^^^^^
Improve parse error report Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-11 16:51:41 +03:00
Reference in New Issue Copy Permalink