From b99dd052244ce2cd2daaa28854ec4490c5204955 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 27 Apr 2024 10:08:09 -0700 Subject: [PATCH] [ parser ] Add support for impossible lambdas --- CHANGELOG_NEXT.md | 3 +++ src/Idris/Parser.idr | 13 ++++++++++++- tests/idris2/error/perror032/LambdaImpossible.idr | 2 ++ tests/idris2/error/perror032/expected | 1 + tests/idris2/error/perror032/run | 3 +++ 5 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 tests/idris2/error/perror032/LambdaImpossible.idr create mode 100644 tests/idris2/error/perror032/expected create mode 100644 tests/idris2/error/perror032/run diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index dd7503d02b..f6c3865cc9 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -46,6 +46,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO environment variable adds to the "Package Search Paths." Functionally this is not a breaking change. +* The compiler now supports `impossible` in a non-case lambda. You can now + write `\ Refl impossible`. + ### Backend changes #### RefC Backend diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 0be4fc5262..f566523c49 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -782,10 +782,21 @@ mutual commit switch <- optional (bounds $ decoratedKeyword fname "case") case switch of - Nothing => continueLam + Nothing => continueLamImpossible <|> continueLam Just r => continueLamCase r where + continueLamImpossible : Rule PTerm + continueLamImpossible = do + lhs <- bounds (opExpr plhs fname indents) + end <- bounds (decoratedKeyword fname "impossible") + pure ( + let fc = boundToFC fname (mergeBounds lhs end) + alt = (MkImpossible fc lhs.val) + fcCase = boundToFC fname lhs + n = MN "lcase" 0 in + (PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $ + PCase (virtualiseFC fc) [] (PRef fcCase n) [alt])) bindAll : List (RigCount, WithBounds PTerm, PTerm) -> PTerm -> PTerm bindAll [] scope = scope diff --git a/tests/idris2/error/perror032/LambdaImpossible.idr b/tests/idris2/error/perror032/LambdaImpossible.idr new file mode 100644 index 0000000000..cb297aad13 --- /dev/null +++ b/tests/idris2/error/perror032/LambdaImpossible.idr @@ -0,0 +1,2 @@ +foo : 2 = 3 -> Void +foo = (\Refl impossible) diff --git a/tests/idris2/error/perror032/expected b/tests/idris2/error/perror032/expected new file mode 100644 index 0000000000..cf05142e32 --- /dev/null +++ b/tests/idris2/error/perror032/expected @@ -0,0 +1 @@ +1/1: Building LambdaImpossible (LambdaImpossible.idr) diff --git a/tests/idris2/error/perror032/run b/tests/idris2/error/perror032/run new file mode 100644 index 0000000000..73f5a2aecc --- /dev/null +++ b/tests/idris2/error/perror032/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check LambdaImpossible.idr