use ProveArg

app/Commands/Dev/Anoma/Base.hs

@@ -3,6 +3,9 @@ module Commands.Dev.Anoma.Base where
 import Anoma.Effect (Anoma)
 import Anoma.Effect qualified as Anoma
 import Commands.Base hiding (Atom)
+import Commands.Dev.Anoma.Prove.Options.ProveArg
+import Data.ByteString.Base64 qualified as Base64
+import Juvix.Compiler.Nockma.Encoding.ByteString
 import Juvix.Compiler.Nockma.Pretty
 import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
 
@@ -26,28 +29,30 @@ data ParsedArgsMode
 runNock ::
   forall r.
   (Members '[Error SimpleError, Anoma] r, Members AppEffects r) =>
-  ParsedArgsMode ->
   AppPath File ->
-  Maybe (AppPath File) ->
+  [ProveArg] ->
   Sem r Anoma.RunNockmaResult
-runNock argsMode programFile margsFile = do
-  afile <- fromAppPathFile programFile
-  argsFile <- mapM fromAppPathFile margsFile
-  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))
+runNock programFile pargs = do
+  argsfile <- fromAppPathFile programFile
+  parsedTerm <- runAppError @JuvixError (Nockma.cueJammedFileOrPretty argsfile)
+  args <- mapM proveArgToTerm pargs
+  Anoma.runNockma
+    Anoma.RunNockmaInput
+      { _runNockmaProgram = parsedTerm,
+        _runNockmaArgs = args
+      }
+
+proveArgToTerm :: forall r. (Members '[Error SimpleError, Files, App] r) => ProveArg -> Sem r (Term Natural)
+proveArgToTerm = \case
+  ProveArgNat n -> return (toNock n)
+  ProveArgBytes n -> fromAppPathFile n >>= readFileBS' >>= fromBytes
+  ProveArgBase64 n -> do
+    res <- Base64.decode <$> (fromAppPathFile n >>= readFileBS')
+    bs <- asSimpleError (mkAnsiText @Text) (either (throw . pack) return res)
+    fromBytes bs
   where
-    go :: [Term Natural] -> Term Natural -> Sem r Anoma.RunNockmaResult
-    go args t =
-      Anoma.runNockma
-        Anoma.RunNockmaInput
-          { _runNockmaProgram = t,
-            _runNockmaArgs = args
-          }
+    fromBytes :: ByteString -> Sem r (Term Natural)
+    fromBytes b = TermAtom <$> asSimpleErrorShow @NockNaturalNaturalError (byteStringToAtom @Natural b)
 
 -- | Calls Anoma.Protobuf.Mempool.AddTransaction
 addTransaction ::

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 ParsedArgsModePretty (opts ^. proveFile) (opts ^. proveArgs)
+  res <- runNock (opts ^. proveFile) (opts ^. proveArgs)
   let traces = res ^. runNockmaTraces
   forM_ traces (renderStdOutLn . ppOutDefault)
   let provedCode = Encoding.jamToByteString (res ^. runNockmaResult)

app/Commands/Dev/Anoma/Prove/Options.hs

@@ -1,107 +1,24 @@
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE QuantifiedConstraints #-}
-
-module Commands.Dev.Anoma.Prove.Options where
+module Commands.Dev.Anoma.Prove.Options
+  ( module Commands.Dev.Anoma.Prove.Options,
+    module Commands.Dev.Anoma.Prove.Options.ProveArg,
+  )
+where
 
+import Commands.Dev.Anoma.Prove.Options.ProveArg
 import CommonOptions
-import Juvix.Data.IntegerWithBase
-import Juvix.Parser.Lexer
-import Juvix.Prelude.Parsing hiding (option, many)
-import Prelude qualified
-
-data ProveArgTag
-  = ProveArgNat
-  | ProveArgBase64
-  | ProveArgBytes
-  deriving stock (Eq, Bounded, Enum, Data)
-
-instance Show ProveArgTag where
-  show = \case
-    ProveArgNat -> "nat"
-    ProveArgBase64 -> "base64"
-    ProveArgBytes -> "bytes"
-
-type ProveArgType :: ProveArgTag -> GHCType
-type family ProveArgType s = res where
-  ProveArgType 'ProveArgNat = Natural
-  ProveArgType 'ProveArgBase64 = AppPath File
-  ProveArgType 'ProveArgBytes = AppPath File
-
-$(genDefunSymbols [''ProveArgType])
 
 data ProveOptions = ProveOptions
   { _proveFile :: AppPath File,
-    _proveArgs :: Maybe (AppPath File),
-    _proveArgs2 :: [ProveArg],
+    _proveArgs :: [ProveArg],
     _proveOutputFile :: Maybe (AppPath File)
   }
   deriving stock (Data)
 
-newtype ProveArg = ProveArg
-  { _proveArg :: Sigma ProveArgTag ProveArgTypeSym0
-  }
-
-$(genSingletons [''ProveArgTag])
-
 makeLenses ''ProveOptions
-makeLenses ''ProveArg
-
-type Parse = Parsec Void Text
-
-parseProveArg :: Parser ProveArg
-parseProveArg =
-  option
-    pp
-    ( long "arg"
-        <> completer (enumCompleter (Proxy @ProveArgTag))
-        <> metavar "ARG_TYPE:ARG"
-    )
-  where
-    pProveArgTag :: Parse ProveArgTag
-    pProveArgTag =
-      choice
-        [ chunk (show a) $> a
-          | a :: ProveArgTag <- allElements
-        ]
-
-    pAppPath :: Parse (AppPath File)
-    pAppPath = do
-      i <- mkPrepath . unpack <$> takeRest
-      return
-        AppPath
-          { _pathIsInput = True,
-            _pathPath = i
-          }
-
-    pProveArg :: Parse ProveArg
-    pProveArg = do
-      dty <- pProveArgTag
-      withSomeSing dty $ \ty -> do
-        chunk ":"
-        a <- pProveArgType ty
-        return (ProveArg (ty :&: a))
-
-    pProveArgType :: SProveArgTag t -> Parse (ProveArgType t)
-    pProveArgType p = do
-      ret <- case p of
-        SProveArgBytes -> pAppPath
-        SProveArgBase64 -> pAppPath
-        SProveArgNat -> do
-          off <- getOffset
-          i <- (^. withLocParam . integerWithBaseValue) <$> integerWithBase'
-          if
-              | i < 0 -> parseFailure off "Expected a non-negative integer"
-              | otherwise -> return (fromIntegral i)
-      eof
-      return ret
-
-    pp :: ReadM ProveArg
-    pp = eitherReader $ \strInput -> parseHelper pProveArg (pack strInput)
 
 parseProveOptions :: Parser ProveOptions
 parseProveOptions = do
   _proveFile <- parseInputFile FileExtNockma
-  _proveArgs <- optional anomaArgsOpt
-  _proveArgs2 <- many parseProveArg
+  _proveArgs <- many parseProveArg
   _proveOutputFile <- optional parseGenericOutputFile
   pure ProveOptions {..}

app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs

@@ -0,0 +1,82 @@
+module Commands.Dev.Anoma.Prove.Options.ProveArg
+  ( ProveArg (..),
+    parseProveArg,
+  )
+where
+
+import Commands.Dev.Anoma.Prove.Options.ProveArgTag
+import CommonOptions
+import Juvix.Data.IntegerWithBase
+import Juvix.Parser.Lexer
+import Juvix.Prelude.Parsing hiding (many, option)
+
+type Parse = Parsec Void Text
+
+newtype ProveArg' = ProveArg'
+  { _proveArg :: Sigma ProveArgTag ProveArgTypeSym0
+  }
+
+data ProveArg
+  = ProveArgNat Natural
+  | ProveArgBase64 (AppPath File)
+  | ProveArgBytes (AppPath File)
+  deriving stock (Data)
+
+parseProveArg :: Parser ProveArg
+parseProveArg = fromProveArg' <$> parseProveArg'
+  where
+    fromProveArg' :: ProveArg' -> ProveArg
+    fromProveArg' (ProveArg' (ty :&: a)) = case ty of
+      SProveArgTagNat -> ProveArgNat a
+      SProveArgTagBase64 -> ProveArgBase64 a
+      SProveArgTagBytes -> ProveArgBytes a
+
+parseProveArg' :: Parser ProveArg'
+parseProveArg' =
+  option
+    pp
+    ( long "arg"
+        <> completer (enumCompleter (Proxy @ProveArgTag))
+        <> metavar "ARG_TYPE:ARG"
+    )
+  where
+    pProveArgTag :: Parse ProveArgTag
+    pProveArgTag =
+      choice
+        [ chunk (show a) $> a
+          | a :: ProveArgTag <- allElements
+        ]
+
+    pAppPath :: Parse (AppPath File)
+    pAppPath = do
+      i <- mkPrepath . unpack <$> takeRest
+      return
+        AppPath
+          { _pathIsInput = True,
+            _pathPath = i
+          }
+
+    pProveArg' :: Parse ProveArg'
+    pProveArg' = do
+      dty <- pProveArgTag
+      withSomeSing dty $ \ty -> do
+        chunk ":"
+        a <- pProveArgType ty
+        return (ProveArg' (ty :&: a))
+
+    pProveArgType :: SProveArgTag t -> Parse (ProveArgType t)
+    pProveArgType p = do
+      ret <- case p of
+        SProveArgTagBytes -> pAppPath
+        SProveArgTagBase64 -> pAppPath
+        SProveArgTagNat -> do
+          off <- getOffset
+          i <- (^. withLocParam . integerWithBaseValue) <$> integerWithBase'
+          if
+              | i < 0 -> parseFailure off "Expected a non-negative integer"
+              | otherwise -> return (fromIntegral i)
+      eof
+      return ret
+
+    pp :: ReadM ProveArg'
+    pp = eitherReader $ \strInput -> parseHelper pProveArg' (pack strInput)

app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs

@@ -0,0 +1,27 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Commands.Dev.Anoma.Prove.Options.ProveArgTag where
+
+import CommonOptions
+import Prelude qualified
+
+data ProveArgTag
+  = ProveArgTagNat
+  | ProveArgTagBase64
+  | ProveArgTagBytes
+  deriving stock (Eq, Bounded, Enum, Data)
+
+instance Show ProveArgTag where
+  show = \case
+    ProveArgTagNat -> "nat"
+    ProveArgTagBase64 -> "base64"
+    ProveArgTagBytes -> "bytes"
+
+type ProveArgType :: ProveArgTag -> GHCType
+type family ProveArgType s = res where
+  ProveArgType 'ProveArgTagNat = Natural
+  ProveArgType 'ProveArgTagBase64 = AppPath File
+  ProveArgType 'ProveArgTagBytes = AppPath File
+
+$(genDefunSymbols [''ProveArgType])
+$(genSingletons [''ProveArgTag])

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

@@ -3,18 +3,19 @@ module Commands.Dev.Nockma.Run.Anoma where
 import Anoma.Effect
 import Commands.Base hiding (Atom)
 import Commands.Dev.Anoma.Base
+import Commands.Dev.Anoma.Prove.Options.ProveArg
 import Juvix.Compiler.Nockma.Pretty
 
 data RunCommandArgs = RunCommandArgs
-  { _runCommandArgsFile :: Maybe (AppPath File),
+  { _runCommandArgs :: [ProveArg],
     _runCommandProgramFile :: AppPath File
   }
 
 makeLenses ''RunCommandArgs
 
 runInAnoma :: forall r. (Members '[Error SimpleError, Anoma] r, Members AppEffects r) => RunCommandArgs -> Sem r ()
 runInAnoma runArgs = do
-  res <- runNock ParsedArgsModeJammedOrPretty (runArgs ^. runCommandProgramFile) (runArgs ^. runCommandArgsFile)
+  res <- runNock (runArgs ^. runCommandProgramFile) (runArgs ^. runCommandArgs)
   let traces = res ^. runNockmaTraces
   renderStdOutLn (annotate AnnImportant $ "Traces (" <> show (length traces) <> "):")
   forM_ traces $ \tr ->

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

@@ -15,5 +15,5 @@ runCommand opts = do
     runArgs =
       RunCommandArgs
         { _runCommandProgramFile = opts ^. nockmaRunEphemeralFile,
-          _runCommandArgsFile = opts ^. nockmaRunEphemeralArgs
+          _runCommandArgs = opts ^. nockmaRunEphemeralArgs
         }

app/Commands/Dev/Nockma/Run/EphemeralClient/Options.hs

@@ -1,11 +1,12 @@
 module Commands.Dev.Nockma.Run.EphemeralClient.Options where
 
+import Commands.Dev.Anoma.Prove.Options.ProveArg
 import CommonOptions
 
 data NockmaRunEphemeralClientOptions = NockmaRunEphemeralClientOptions
   { _nockmaRunEphemeralFile :: AppPath File,
     _nockmaRunEphemeralAnomaDir :: AppPath Dir,
-    _nockmaRunEphemeralArgs :: Maybe (AppPath File)
+    _nockmaRunEphemeralArgs :: [ProveArg]
   }
   deriving stock (Data)
 
@@ -14,6 +15,6 @@ makeLenses ''NockmaRunEphemeralClientOptions
 parseNockmaRunEphemeralClientOptions :: Parser NockmaRunEphemeralClientOptions
 parseNockmaRunEphemeralClientOptions = do
   _nockmaRunEphemeralFile <- parseInputFile FileExtNockma
-  _nockmaRunEphemeralArgs <- optional anomaArgsOpt
+  _nockmaRunEphemeralArgs <- many parseProveArg
   _nockmaRunEphemeralAnomaDir <- anomaDirOpt
   pure NockmaRunEphemeralClientOptions {..}

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

@@ -20,5 +20,5 @@ runCommand opts =
     runArgs =
       RunCommandArgs
         { _runCommandProgramFile = opts ^. nockmaRunWithClientFile,
-          _runCommandArgsFile = opts ^. nockmaRunWithClientArgs
+          _runCommandArgs = opts ^. nockmaRunWithClientArgs
         }

app/Commands/Dev/Nockma/Run/WithClient/Options.hs

@@ -1,13 +1,14 @@
 module Commands.Dev.Nockma.Run.WithClient.Options where
 
+import Commands.Dev.Anoma.Prove.Options.ProveArg
 import CommonOptions
 
 data NockmaRunWithClientOptions = NockmaRunWithClientOptions
   { _nockmaRunWithClientFile :: AppPath File,
     _nockmaRunWithClientGrpcPort :: Int,
     _nockmaRunWithClientNodeId :: Text,
     _nockmaRunWithClientUrl :: String,
-    _nockmaRunWithClientArgs :: Maybe (AppPath File)
+    _nockmaRunWithClientArgs :: [ProveArg]
   }
   deriving stock (Data)
 
@@ -16,7 +17,7 @@ makeLenses ''NockmaRunWithClientOptions
 parseNockmaRunWithClientOptions :: Parser NockmaRunWithClientOptions
 parseNockmaRunWithClientOptions = do
   _nockmaRunWithClientFile <- parseInputFile FileExtNockma
-  _nockmaRunWithClientArgs <- optional anomaArgsOpt
+  _nockmaRunWithClientArgs <- many parseProveArg
   _nockmaRunWithClientGrpcPort <-
     option
       (fromIntegral <$> naturalNumberOpt)

src/Juvix/Compiler/Nockma/Encoding/ByteString.hs

@@ -23,7 +23,7 @@ atomToByteStringLen len = fmap (padByteString len) . atomToByteString
 sha256Atom :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r ByteString
 sha256Atom = fmap sha256Natural . nockNatural
 
-byteStringToAtom :: (NockNatural a, Member (Error (ErrNockNatural a)) r) => ByteString -> Sem r (Atom a)
+byteStringToAtom :: forall a r. (NockNatural a, Member (Error (ErrNockNatural a)) r) => ByteString -> Sem r (Atom a)
 byteStringToAtom = fmap mkEmptyAtom . fromNatural . byteStringToNatural
 
 byteStringToNatural :: ByteString -> Natural