[ 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

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

CONTRIBUTORS

@@ -81,6 +81,7 @@ Timmy Jose
 Tim Süberkrüb
 Tom Harley
 troiganto
+Viktor Yudov
 Wen Kokke
 Wind Wong
 Zoe Stafford

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)

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])

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)

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)

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

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
+     ^^^^
+

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

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

tests/cli/exec002/expected

@@ -0,0 +1,3 @@
+Hello!
+1 + 2 = 3
+Bye!

tests/cli/exec002/run

@@ -0,0 +1,6 @@
+. ../../testutils.sh
+
+idris2 \
+  --exec 'putStrLn "Hello!"' \
+  --exec 'putStrLn "1 + 2 = \{show $ 1 + 2}"' \
+  --exec 'putStrLn "Bye!"'

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
+     ^^^^^^^^^
+

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!"'

tests/cli/exec004/expected

@@ -0,0 +1,9 @@
+3
+------
+Error: Expected end of input.
+
+(Interactive):2:1--2:2
+ 1 | printLn $ 1
+ 2 | + 2
+     ^
+

tests/cli/exec004/run

@@ -0,0 +1,9 @@
+. ../../testutils.sh
+
+idris2 --exec 'printLn $ 1
+  + 2'
+
+echo "------"
+
+idris2 --exec 'printLn $ 1
++ 2'