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