[ elab ] Make elab scripts be able to record warnings (#2999)

This commit is contained in:
Denis Buzdalov 2023-06-19 18:34:19 +03:00 committed by GitHub
parent 9f20ba2609
commit 5dcf62499d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 63 additions and 5 deletions

View File

@ -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.

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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!

View File

@ -0,0 +1,3 @@
:t x
x
:q

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

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner ElabScriptWarning.idr < input

View File

@ -0,0 +1 @@
package a-test