From 1550c09c7be84c77cc2ce005ebb4f6b2c58528de Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 19 Dec 2024 13:57:59 +0000
Subject: [PATCH] The args file to the prove CLI is always a textual nock term

---
 app/Commands/Dev/Anoma/Base.hs                    | 15 +++++++++++++--
 app/Commands/Dev/Anoma/Prove.hs                   |  2 +-
 app/Commands/Dev/Nockma/Run/Anoma.hs              |  2 +-
 .../Nockma/Translation/FromSource/Base.hs         | 10 +++++++++-
 4 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/app/Commands/Dev/Anoma/Base.hs b/app/Commands/Dev/Anoma/Base.hs
index 6b70873771..c5d5396c7e 100644
--- a/app/Commands/Dev/Anoma/Base.hs
+++ b/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
diff --git a/app/Commands/Dev/Anoma/Prove.hs b/app/Commands/Dev/Anoma/Prove.hs
index 825526681a..182f5d0355 100644
--- a/app/Commands/Dev/Anoma/Prove.hs
+++ b/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)
diff --git a/app/Commands/Dev/Nockma/Run/Anoma.hs b/app/Commands/Dev/Nockma/Run/Anoma.hs
index c075918656..ede35370d0 100644
--- a/app/Commands/Dev/Nockma/Run/Anoma.hs
+++ b/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 ->
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
index ca715fc001..edde43c889 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
+++ b/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