From 5dcf62499df5cb861d153372ef3b4386dba25c98 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Mon, 19 Jun 2023 18:34:19 +0300 Subject: [PATCH] [ elab ] Make elab scripts be able to record warnings (#2999) --- CHANGELOG.md | 1 + libs/base/Language/Reflection.idr | 11 +++++++++++ src/TTImp/Elab/RunElab.idr | 14 ++++++++++---- tests/Main.idr | 2 +- .../reflection019/ElabScriptWarning.idr | 19 +++++++++++++++++++ tests/idris2/reflection019/expected | 14 ++++++++++++++ tests/idris2/reflection019/input | 3 +++ tests/idris2/reflection019/run | 3 +++ tests/idris2/reflection019/test.ipkg | 1 + 9 files changed, 63 insertions(+), 5 deletions(-) create mode 100644 tests/idris2/reflection019/ElabScriptWarning.idr create mode 100644 tests/idris2/reflection019/expected create mode 100644 tests/idris2/reflection019/input create mode 100755 tests/idris2/reflection019/run create mode 100644 tests/idris2/reflection019/test.ipkg diff --git a/CHANGELOG.md b/CHANGELOG.md index 68c16dcb72..68a40bb4d8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,7 @@ size-change termination by Lee, Jones and Ben-Amram. * New function option `%unsafe` to mark definitions that are escape hatches similar to the builtins `believe_me`, `assert_total`, etc. +* Elaborator scripts were made be able to record warnings. * Rudimentary support for defining lazy functions (addressing issue [#1066](https://github.com/idris-lang/idris2/issues/1066)). * `%hide` directives can now hide conflicting fixities from other modules. diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr index de51fd9751..512c576053 100644 --- a/libs/base/Language/Reflection.idr +++ b/libs/base/Language/Reflection.idr @@ -19,6 +19,7 @@ data Elab : Type -> Type where Pure : a -> Elab a Bind : Elab a -> (a -> Elab b) -> Elab b Fail : FC -> String -> Elab a + Warn : FC -> String -> Elab () Try : Elab a -> Elab a -> Elab a @@ -100,6 +101,9 @@ interface Monad m => Elaboration m where ||| Report an error in elaboration at some location failAt : FC -> String -> m a + ||| Report a warning in elaboration at some location + warnAt : FC -> String -> m () + ||| Try the first elaborator. If it fails, reset the elaborator state and ||| run the second try : Elab a -> Elab a -> m a @@ -161,6 +165,11 @@ export %inline fail : Elaboration m => String -> m a fail = failAt EmptyFC +export %inline +||| Report an error in elaboration +warn : Elaboration m => String -> m () +warn = warnAt EmptyFC + ||| Log the current goal type, if the log level is >= the given level export %inline logGoal : Elaboration m => String -> Nat -> String -> m () @@ -169,6 +178,7 @@ logGoal str n msg = whenJust !goal $ logTerm str n msg export Elaboration Elab where failAt = Fail + warnAt = Warn try = Try logMsg = LogMsg logTerm = LogTerm @@ -189,6 +199,7 @@ Elaboration Elab where public export Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where failAt = lift .: failAt + warnAt = lift .: warnAt try = lift .: try logMsg s = lift .: logMsg s logTerm s n = lift .: logTerm s n diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index 7fe18dd6a7..f3edfbd4fd 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -80,6 +80,11 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp = do defs <- get Ctxt nfOpts withAll defs env !(reflect fc defs False env tm) + reifyFC : Defs -> Closure vars -> Core FC + reifyFC defs mbfc = pure $ case !(evalClosure defs mbfc >>= reify defs) of + EmptyFC => fc + x => x + elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars) elabCon defs "Pure" [_,val] = do empty <- clearDefs defs @@ -99,10 +104,11 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp elabScript rig fc nest env r exp elabCon defs "Fail" [_, mbfc, msg] = do msg' <- evalClosure defs msg - let customFC = case !(evalClosure defs mbfc >>= reify defs) of - EmptyFC => fc - x => x - throw $ RunElabFail $ GenericMsg customFC !(reify defs msg') + throw $ RunElabFail $ GenericMsg !(reifyFC defs mbfc) !(reify defs msg') + elabCon defs "Warn" [mbfc, msg] + = do msg' <- evalClosure defs msg + recordWarning $ GenericWarn !(reifyFC defs mbfc) !(reify defs msg') + scriptRet () elabCon defs "Try" [_, elab1, elab2] = tryUnify (do constart <- getNextEntry res <- elabScript rig fc nest env !(evalClosure defs elab1) exp diff --git a/tests/Main.idr b/tests/Main.idr index bdffc4755a..a95634ac62 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -250,7 +250,7 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing "reflection005", "reflection006", "reflection007", "reflection008", "reflection009", "reflection010", "reflection011", "reflection012", "reflection013", "reflection014", "reflection015", "reflection016", - "reflection017", "reflection018"] + "reflection017", "reflection018", "reflection019"] idrisTestsWith : TestPool idrisTestsWith = MkTestPool "With abstraction" [] Nothing diff --git a/tests/idris2/reflection019/ElabScriptWarning.idr b/tests/idris2/reflection019/ElabScriptWarning.idr new file mode 100644 index 0000000000..bc12ee1c75 --- /dev/null +++ b/tests/idris2/reflection019/ElabScriptWarning.idr @@ -0,0 +1,19 @@ +module ElabScriptWarning + +import Language.Reflection + +%language ElabReflection + +showsWarning : a -> b -> Elab c +showsWarning x y = do + x' <- quote x + warnAt (getFC x') "The first argument worth a warning" + check =<< quote y + + + + + + +x : Nat +x = %runElab showsWarning "Suspicious" 15 diff --git a/tests/idris2/reflection019/expected b/tests/idris2/reflection019/expected new file mode 100644 index 0000000000..f151fb4962 --- /dev/null +++ b/tests/idris2/reflection019/expected @@ -0,0 +1,14 @@ +1/1: Building ElabScriptWarning (ElabScriptWarning.idr) +Warning: The first argument worth a warning + +ElabScriptWarning:19:27--19:39 + 15 | + 16 | + 17 | + 18 | x : Nat + 19 | x = %runElab showsWarning "Suspicious" 15 + ^^^^^^^^^^^^ + +ElabScriptWarning> ElabScriptWarning.x : Nat +ElabScriptWarning> 15 +ElabScriptWarning> Bye for now! diff --git a/tests/idris2/reflection019/input b/tests/idris2/reflection019/input new file mode 100644 index 0000000000..4fc6e1dbfd --- /dev/null +++ b/tests/idris2/reflection019/input @@ -0,0 +1,3 @@ +:t x +x +:q diff --git a/tests/idris2/reflection019/run b/tests/idris2/reflection019/run new file mode 100755 index 0000000000..a1e4637cd8 --- /dev/null +++ b/tests/idris2/reflection019/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner ElabScriptWarning.idr < input diff --git a/tests/idris2/reflection019/test.ipkg b/tests/idris2/reflection019/test.ipkg new file mode 100644 index 0000000000..2c5b5ab52d --- /dev/null +++ b/tests/idris2/reflection019/test.ipkg @@ -0,0 +1 @@ +package a-test