From 8f1f2760a8100e7b9e3c9a2e30b63b652c7e40ff Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 10 Dec 2024 09:09:08 +0300 Subject: [PATCH] [ new ] `--exec` takes arbitrary expression (#3438) * [ cleanup ] Remove redudant `assert_total`s in `Text.Parser.Core` * [ new ] `--exec` takes arbitrary expression * [ fix ] Update `expected` in test `chez/chez031` * [ doc ] Update `CHANGELOG_NEXT.md` --- CHANGELOG_NEXT.md | 3 +++ CONTRIBUTORS | 1 + libs/contrib/Text/Parser/Core.idr | 22 ++++++++++---------- src/Idris/CommandLine.idr | 2 +- src/Idris/SetOptions.idr | 8 ++++++-- src/Libraries/Text/Parser/Core.idr | 22 ++++++++++---------- tests/chez/chez031/expected | 2 -- tests/cli/exec001/expected | 13 ++++++++++++ tests/cli/exec001/issue3398.idr | 11 ++++++++++ tests/cli/exec001/run | 8 ++++++++ tests/cli/exec002/expected | 3 +++ tests/cli/exec002/run | 6 ++++++ tests/cli/exec003/expected | 32 ++++++++++++++++++++++++++++++ tests/cli/exec003/run | 9 +++++++++ tests/cli/exec004/expected | 9 +++++++++ tests/cli/exec004/run | 9 +++++++++ 16 files changed, 133 insertions(+), 27 deletions(-) create mode 100644 tests/cli/exec001/expected create mode 100644 tests/cli/exec001/issue3398.idr create mode 100755 tests/cli/exec001/run create mode 100644 tests/cli/exec002/expected create mode 100755 tests/cli/exec002/run create mode 100644 tests/cli/exec003/expected create mode 100755 tests/cli/exec003/run create mode 100644 tests/cli/exec004/expected create mode 100755 tests/cli/exec004/run diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 7bb8f7cec7..281711609d 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -29,6 +29,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * CLI errors will now be printed to `stderr` instead of `stdout`. +* The `idris2 --exec` command now takes an arbitrary expression, not just the + function name. + ### Building/Packaging changes * The Nix flake's `buildIdris` function now returns a set with `executable` and diff --git a/CONTRIBUTORS b/CONTRIBUTORS index d0b2f997d7..e5e12b037a 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -81,6 +81,7 @@ Timmy Jose Tim Süberkrüb Tom Harley troiganto +Viktor Yudov Wen Kokke Wind Wong Zoe Stafford diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr index 2dc7c9812f..d5d4601000 100644 --- a/libs/contrib/Text/Parser/Core.idr +++ b/libs/contrib/Text/Parser/Core.idr @@ -302,7 +302,7 @@ doParse s com (Try g) xs = case doParse s com g xs of res => res doParse s com Commit xs = Res s True (irrelevantBounds ()) xs doParse s com (MustWork g) xs = - case assert_total (doParse s com g xs) of + case doParse s com g xs of Failure com' _ errs => Failure com' True errs res => res doParse s com (Terminal err f) [] = Failure com False (Error "End of input" Nothing ::: Nil) @@ -324,7 +324,7 @@ doParse s com (Alt {c1} {c2} x y) xs -- If the alternative had committed, don't try the -- other branch (and reset commit flag) then Failure com fatal errs - else case (assert_total doParse s False y xs) of + else case doParse s False y xs of (Failure com'' fatal' errs') => if com'' || fatal' -- Only add the errors together if the second branch -- is also non-committed and non-fatal. @@ -334,27 +334,27 @@ doParse s com (Alt {c1} {c2} x y) xs -- Successfully parsed the first option, so use the outer commit flag Res s _ val xs => Res s com val xs doParse s com (SeqEmpty act next) xs - = case assert_total (doParse s com act xs) of + = case doParse s com act xs of Failure com fatal errs => Failure com fatal errs Res s com v xs => - mergeWith v (assert_total $ doParse s com (next v.val) xs) + mergeWith v $ doParse s com (next v.val) xs doParse s com (SeqEat act next) xs - = case assert_total (doParse s com act xs) of + = case doParse s com act xs of Failure com fatal errs => Failure com fatal errs Res s com v xs => - mergeWith v (assert_total $ doParse s com (next v.val) xs) + mergeWith v $ assert_total doParse s com (next v.val) xs doParse s com (ThenEmpty act next) xs - = case assert_total (doParse s com act xs) of + = case doParse s com act xs of Failure com fatal errs => Failure com fatal errs Res s com v xs => - mergeWith v (assert_total $ doParse s com next xs) + mergeWith v $ doParse s com next xs doParse s com (ThenEat act next) xs - = case assert_total (doParse s com act xs) of + = case doParse s com act xs of Failure com fatal errs => Failure com fatal errs Res s com v xs => - mergeWith v (assert_total $ doParse s com next xs) + mergeWith v $ assert_total doParse s com next xs doParse s com (Bounds act) xs - = case assert_total (doParse s com act xs) of + = case doParse s com act xs of Failure com fatal errs => Failure com fatal errs Res s com v xs => Res s com (const v <$> v) xs doParse s com Position [] = Failure com False (Error "End of input" Nothing ::: Nil) diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index c0835f53e5..85f5f8493b 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -234,7 +234,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--output", "-o"] [Required "file"] (\f => [OutputFile f, Quiet]) (Just "Specify output file"), MkOpt ["--exec", "-x"] [Required "name"] (\f => [ExecFn f, Quiet]) - (Just "Execute function after checking source file"), + (Just "Execute expression"), MkOpt ["--no-prelude"] [] [NoPrelude] (Just "Don't implicitly import Prelude"), MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f]) diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 62b9e2fe50..679cdd88f5 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -13,6 +13,7 @@ import Libraries.Data.List.Extra import Idris.CommandLine import Idris.Package.Types +import Idris.Parser import Idris.Pretty import Idris.ProcessIdr import Idris.REPL @@ -514,8 +515,11 @@ postOptions res (OutputFile outfile :: rest) = do ignore $ compileExp (PRef EmptyFC (UN $ Basic "main")) outfile ignore $ postOptions res rest pure False -postOptions res (ExecFn str :: rest) - = do ignore $ execExp (PRef EmptyFC (UN $ Basic str)) +postOptions res (ExecFn expr :: rest) + = do setCurrentElabSource expr + let Right (_, _, e) = runParser (Virtual Interactive) Nothing expr $ aPTerm <* eoi + | Left err => throw err + ignore $ execExp e ignore $ postOptions res rest pure False postOptions res (CheckOnly :: rest) diff --git a/src/Libraries/Text/Parser/Core.idr b/src/Libraries/Text/Parser/Core.idr index adb8080248..b9f1e0e496 100644 --- a/src/Libraries/Text/Parser/Core.idr +++ b/src/Libraries/Text/Parser/Core.idr @@ -335,7 +335,7 @@ doParse s ws com (Try g) xs = case doParse s ws com g xs of res => res doParse s ws com Commit xs = Res s ws True (irrelevantBounds ()) xs doParse s ws com (MustWork g) xs = - case assert_total (doParse s ws com g xs) of + case doParse s ws com g xs of Failure com' _ errs => Failure com' True errs res => res doParse s ws com (Terminal err f) [] = Failure com False (Error "End of input" Nothing ::: Nil) @@ -357,7 +357,7 @@ doParse s ws com (Alt {c1} {c2} x y) xs -- If the alternative had committed, don't try the -- other branch (and reset commit flag) then Failure com fatal errs - else case (assert_total doParse s ws False y xs) of + else case doParse s ws False y xs of (Failure com'' fatal' errs') => if com'' || fatal' -- Only add the errors together if the second branch -- is also non-committed and non-fatal. @@ -367,27 +367,27 @@ doParse s ws com (Alt {c1} {c2} x y) xs -- Successfully parsed the first option, so use the outer commit flag Res s ws _ val xs => Res s ws com val xs doParse s ws com (SeqEmpty act next) xs - = case assert_total (doParse s ws com act xs) of + = case doParse s ws com act xs of Failure com fatal errs => Failure com fatal errs Res s ws com v xs => - mergeWith v (assert_total $ doParse s ws com (next v.val) xs) + mergeWith v $ doParse s ws com (next v.val) xs doParse s ws com (SeqEat act next) xs - = case assert_total (doParse s ws com act xs) of + = case doParse s ws com act xs of Failure com fatal errs => Failure com fatal errs Res s ws com v xs => - mergeWith v (assert_total $ doParse s ws com (next v.val) xs) + mergeWith v $ assert_total doParse s ws com (next v.val) xs doParse s ws com (ThenEmpty act next) xs - = case assert_total (doParse s ws com act xs) of + = case doParse s ws com act xs of Failure com fatal errs => Failure com fatal errs Res s ws com v xs => - mergeWith v (assert_total $ doParse s ws com next xs) + mergeWith v $ doParse s ws com next xs doParse s ws com (ThenEat act next) xs - = case assert_total (doParse s ws com act xs) of + = case doParse s ws com act xs of Failure com fatal errs => Failure com fatal errs Res s ws com v xs => - mergeWith v (assert_total $ doParse s ws com next xs) + mergeWith v $ assert_total doParse s ws com next xs doParse s ws com (Bounds act) xs - = case assert_total (doParse s ws com act xs) of + = case doParse s ws com act xs of Failure com fatal errs => Failure com fatal errs Res s ws com v xs => Res s ws com (const v <$> v) xs doParse s ws com Position [] = Failure com False (Error "End of input" Nothing ::: Nil) diff --git a/tests/chez/chez031/expected b/tests/chez/chez031/expected index f858a296c8..6fd3c35f74 100644 --- a/tests/chez/chez031/expected +++ b/tests/chez/chez031/expected @@ -3,8 +3,6 @@ Error: The given specifier '["scheme,racket:+"]' was not accepted by any backend Some backends have additional specifier rules, refer to their documentation. Specifiers:29:1--30:35 - 29 | %foreign "scheme,racket:+" - 30 | plusRacketFail : Int -> Int -> Int Error: The given specifier '["scheme,racket:+"]' was not accepted by any backend. Available backends: chez, chez-sep, racket, node, javascript, refc, gambit, vmcode-interp diff --git a/tests/cli/exec001/expected b/tests/cli/exec001/expected new file mode 100644 index 0000000000..dfe33b5142 --- /dev/null +++ b/tests/cli/exec001/expected @@ -0,0 +1,13 @@ +Hi, XX! +Hi, YY! +Hi, XX! +Hi, YY! +------ +Error: Ambiguous elaboration. Possible results: + Main.XX.main + Main.YY.main + +(Interactive):1:1--1:5 + 1 | main + ^^^^ + diff --git a/tests/cli/exec001/issue3398.idr b/tests/cli/exec001/issue3398.idr new file mode 100644 index 0000000000..109d424a54 --- /dev/null +++ b/tests/cli/exec001/issue3398.idr @@ -0,0 +1,11 @@ +namespace XX + + export + main : IO () + main = putStrLn "Hi, XX!" + +namespace YY + + export + main : IO () + main = putStrLn "Hi, YY!" diff --git a/tests/cli/exec001/run b/tests/cli/exec001/run new file mode 100755 index 0000000000..d31c7f519f --- /dev/null +++ b/tests/cli/exec001/run @@ -0,0 +1,8 @@ +. ../../testutils.sh + +idris2 --exec XX.main issue3398.idr +idris2 --exec YY.main issue3398.idr +idris2 --exec Main.XX.main issue3398.idr +idris2 --exec Main.YY.main issue3398.idr +echo "------" +idris2 --exec main issue3398.idr diff --git a/tests/cli/exec002/expected b/tests/cli/exec002/expected new file mode 100644 index 0000000000..fce434d226 --- /dev/null +++ b/tests/cli/exec002/expected @@ -0,0 +1,3 @@ +Hello! +1 + 2 = 3 +Bye! diff --git a/tests/cli/exec002/run b/tests/cli/exec002/run new file mode 100755 index 0000000000..5ab7d8afbc --- /dev/null +++ b/tests/cli/exec002/run @@ -0,0 +1,6 @@ +. ../../testutils.sh + +idris2 \ + --exec 'putStrLn "Hello!"' \ + --exec 'putStrLn "1 + 2 = \{show $ 1 + 2}"' \ + --exec 'putStrLn "Bye!"' diff --git a/tests/cli/exec003/expected b/tests/cli/exec003/expected new file mode 100644 index 0000000000..be8013ddfd --- /dev/null +++ b/tests/cli/exec003/expected @@ -0,0 +1,32 @@ +Hello! +Error: Can't find an implementation for Num (IO ?a). + +(Interactive):1:1--1:6 + 1 | 1 + 2 + ^^^^^ + +------ +Hello! +Error: Do block cannot be empty + +(Interactive):1:1--1:3 + 1 | do + ^^ + +------ +Hello! +Error: Couldn't parse any alternatives: +1: Expected 'case', 'if', 'do', application or operator expression. + +(Interactive):1:1--1:3 + 1 | !! + ^^ +... (84 others) +------ +Hello! +Error: Undefined name undefined. + +(Interactive):1:1--1:10 + 1 | undefined + ^^^^^^^^^ + diff --git a/tests/cli/exec003/run b/tests/cli/exec003/run new file mode 100755 index 0000000000..388dc1e7ab --- /dev/null +++ b/tests/cli/exec003/run @@ -0,0 +1,9 @@ +. ../../testutils.sh + +idris2 --exec 'putStrLn "Hello!"' --exec "1 + 2" --exec 'putStrLn "Bye!"' +echo "------" +idris2 --exec 'putStrLn "Hello!"' --exec "do" --exec 'putStrLn "Bye!"' +echo "------" +idris2 --exec 'putStrLn "Hello!"' --exec "!!" --exec 'putStrLn "Bye!"' +echo "------" +idris2 --exec 'putStrLn "Hello!"' --exec "undefined" --exec 'putStrLn "Bye!"' diff --git a/tests/cli/exec004/expected b/tests/cli/exec004/expected new file mode 100644 index 0000000000..3167c2a135 --- /dev/null +++ b/tests/cli/exec004/expected @@ -0,0 +1,9 @@ +3 +------ +Error: Expected end of input. + +(Interactive):2:1--2:2 + 1 | printLn $ 1 + 2 | + 2 + ^ + diff --git a/tests/cli/exec004/run b/tests/cli/exec004/run new file mode 100755 index 0000000000..e98c25b1d1 --- /dev/null +++ b/tests/cli/exec004/run @@ -0,0 +1,9 @@ +. ../../testutils.sh + +idris2 --exec 'printLn $ 1 + + 2' + +echo "------" + +idris2 --exec 'printLn $ 1 ++ 2'