The args file to the prove CLI must now be textual nock term (#3253)

This PR makes the behaviour of the anoma prove CLI arguments match the
documented behaviour.

Previously the arguments file was expected to be jammed bytes unless it
had the extension `.debug.nockma`. Now the arguments file **must** be a
textual nock term of the form `[arg1 arg2 ... argn 0]` i.e a Nock list
of arguments and the file can have any name.

For example:

Test.juvix
```
module Test;

import Stdlib.Prelude open;

main : List Nat -> List Nat
  | xs := map \{ x := x * 2 } xs;
```

If you want to pass the list`[1;2;3]` as the argument you create a file:

Test.args
```
[[1 2 3 0] 0]
```

And run:

```
$ juvix compile anoma Test.juvix
$ juvix dev anoma prove Test.nockma --args Test.args
$ juvix dev nockma encode --from bytes --to text < Test.proved.nockma
[2 4 6 0]
```

* Fixes #3248

app/Commands/Dev/Anoma/Base.hs

@@ -16,17 +16,28 @@ cellOrFail term f = case term of
   TermAtom {} -> exitFailMsg "Expected nockma input to be a cell"
   t@(TermCell {}) -> inject (f t)
 
+data ParsedArgsMode
+  = -- | The args file is a pretty nockma term
+    ParsedArgsModePretty
+  | -- | The args file is either a pretty nockma term or a jammed nockma term
+    ParsedArgsModeJammedOrPretty
+
 -- | Calls Anoma.Protobuf.NockService.Prove
 runNock ::
   forall r.
   (Members '[Error SimpleError, Anoma] r, Members AppEffects r) =>
+  ParsedArgsMode ->
   AppPath File ->
   Maybe (AppPath File) ->
   Sem r Anoma.RunNockmaResult
-runNock programFile margsFile = do
+runNock argsMode programFile margsFile = do
   afile <- fromAppPathFile programFile
   argsFile <- mapM fromAppPathFile margsFile
-  parsedArgs <- runAppError @JuvixError (mapM Nockma.cueJammedFileOrPretty argsFile)
+  parsedArgs <- runAppError @JuvixError $ do
+    let argsParser = case argsMode of
+          ParsedArgsModeJammedOrPretty -> Nockma.cueJammedFileOrPretty
+          ParsedArgsModePretty -> Nockma.parsePrettyTerm
+    mapM argsParser argsFile
   parsedTerm <- runAppError @JuvixError (Nockma.cueJammedFileOrPretty afile)
   cellOrFail parsedTerm (go (maybe [] unfoldList parsedArgs))
   where

app/Commands/Dev/Anoma/Prove.hs

@@ -10,7 +10,7 @@ import Juvix.Compiler.Nockma.Pretty hiding (Path)
 
 runCommand :: forall r. (Members (Anoma ': Error SimpleError ': AppEffects) r) => ProveOptions -> Sem r ()
 runCommand opts = do
-  res <- runNock (opts ^. proveFile) (opts ^. proveArgs)
+  res <- runNock ParsedArgsModePretty (opts ^. proveFile) (opts ^. proveArgs)
   let traces = res ^. runNockmaTraces
   forM_ traces (renderStdOutLn . ppOutDefault)
   let provedCode = Encoding.jamToByteString (res ^. runNockmaResult)

app/Commands/Dev/Nockma/Run/Anoma.hs

@@ -14,7 +14,7 @@ makeLenses ''RunCommandArgs
 
 runInAnoma :: forall r. (Members '[Error SimpleError, Anoma] r, Members AppEffects r) => RunCommandArgs -> Sem r ()
 runInAnoma runArgs = do
-  res <- runNock (runArgs ^. runCommandProgramFile) (runArgs ^. runCommandArgsFile)
+  res <- runNock ParsedArgsModeJammedOrPretty (runArgs ^. runCommandProgramFile) (runArgs ^. runCommandArgsFile)
   let traces = res ^. runNockmaTraces
   renderStdOutLn (annotate AnnImportant $ "Traces (" <> show (length traces) <> "):")
   forM_ traces $ \tr ->

src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs

@@ -32,6 +32,14 @@ parseText = runParser noFile
 parseReplText :: Text -> Either MegaparsecError (ReplTerm Natural)
 parseReplText = runParserFor replTerm noFile
 
+-- | Parse the file as an annotated unjammed term.
+parsePrettyTerm ::
+  forall r.
+  (Members '[Files, Error JuvixError] r) =>
+  Prelude.Path Abs File ->
+  Sem r (Term Natural)
+parsePrettyTerm f = evalHighlightBuilder (parseTermFile f)
+
 -- | If the file ends in .debug.nockma it parses an annotated unjammed term. Otherwise
 -- it is equivalent to cueJammedFile
 cueJammedFileOrPretty ::
@@ -40,7 +48,7 @@ cueJammedFileOrPretty ::
   Prelude.Path Abs File ->
   Sem r (Term Natural)
 cueJammedFileOrPretty f
-  | f `hasExtensions` nockmaDebugFileExts = evalHighlightBuilder (parseTermFile f)
+  | f `hasExtensions` nockmaDebugFileExts = parsePrettyTerm f
   | otherwise = cueJammedFile f
 
 -- | If the file ends in .debug.nockma it parses an annotated unjammed program. Otherwise