The args file to the prove CLI is always a textual nock term

anoma · Dec 19, 2024 · 1550c09 · 1550c09
1 parent 4dcbf79
commit 1550c09
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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