idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

[ fix ] codegen issue when using partial case statements in prelude. (#2952)

Browse Source
This commit is contained in:
Steve Dunham 2023-04-23 03:07:04 -07:00 committed by GitHub
parent a423715da1
commit 3ad391d597
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 8 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/TTImp/ProcessDef.idr
View File

@ -844,7 +844,7 @@ mkRunTime fc n
mkCrash : {vars : _} -> String -> Term vars
mkCrash msg
= apply fc (Ref fc Func (NS builtinNS (UN $ Basic "idris_crash")))
= apply fc (Ref fc Func (UN $ Basic "prim__crash"))
[Erased fc Placeholder, PrimVal fc (Str msg)]
matchAny : Term vars -> Term vars

2
tests/Main.idr
View File

@ -89,7 +89,7 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
"error011", "error012", "error013", "error014", "error015",
"error016", "error017", "error018", "error019", "error020",
"error021", "error022", "error023", "error024", "error025",
"error026",
"error026", "error027",
-- Parse errors
"perror001", "perror002", "perror003", "perror004", "perror005",
"perror006", "perror007", "perror008", "perror009", "perror010",

2
tests/idris2/error027/Issue2950.idr Normal file
View File

@ -0,0 +1,2 @@
main : IO ()
main = printLn $ mod 10 0

1
tests/idris2/error027/expected Normal file
View File

@ -0,0 +1 @@
ERROR: Unhandled input for Prelude.Num.case block in mod at Prelude.Num:94:3--96:44

3
tests/idris2/error027/run Executable file
View File

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 --exec main Issue2950.idr