Support prove argument list of base64 jammed nouns

app/Commands/Dev/Anoma/Base.hs

@@ -6,9 +6,11 @@ import Commands.Base hiding (Atom)
 import Commands.Dev.Anoma.Prove.Options.ProveArg
 import Data.ByteString qualified as BS
 import Data.ByteString.Base64 qualified as Base64
+import Data.ByteString.Char8 qualified as BC
 import Juvix.Compiler.Nockma.Encoding.ByteString
 import Juvix.Compiler.Nockma.Pretty
 import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
+import Juvix.Compiler.Nockma.Translation.FromTree (foldTermsOrNil)
 
 cellOrFail ::
   forall x r a.
@@ -46,6 +48,11 @@ runNock programAppPath pargs = do
 prepareArg :: forall r. (Members '[Error SimpleError, Files, App] r) => ProveArg -> Sem r Anoma.RunNockmaArg
 prepareArg = \case
   ProveArgNat n -> return (Anoma.RunNockmaArgTerm (toNock n))
+  ProveArgList f -> do
+    bs <- readAppFile f
+    let bss = map Base64.decodeLenient (BC.split '\n' bs)
+    atoms <- map TermAtom <$> mapM decodeAtom bss
+    return (Anoma.RunNockmaArgTerm (foldTermsOrNil atoms))
   ProveArgFile ArgFileSpec {..} -> do
     bs <- asBytes <$> readAppFile _argFileSpecFile
     toArg bs
@@ -59,18 +66,18 @@ prepareArg = \case
           let cell :: Nockma.Term Natural = (fromIntegral @_ @Natural (BS.length bs)) # payload
           return (Anoma.RunNockmaArgTerm cell)
 
-      decodeAtom :: ByteString -> Sem r (Nockma.Atom Natural)
-      decodeAtom =
-        asSimpleErrorShow @NockNaturalNaturalError
-          . byteStringToAtom @Natural
-
       asBytes :: ByteString -> ByteString
       asBytes = case _argFileSpecEncoding of
         EncodingBytes -> id
         EncodingBase64 -> Base64.decodeLenient
+  where
+    readAppFile :: AppPath File -> Sem r ByteString
+    readAppFile f = fromAppPathFile f >>= readFileBS'
 
-      readAppFile :: AppPath File -> Sem r ByteString
-      readAppFile f = fromAppPathFile f >>= readFileBS'
+    decodeAtom :: ByteString -> Sem r (Nockma.Atom Natural)
+    decodeAtom =
+      asSimpleErrorShow @NockNaturalNaturalError
+        . byteStringToAtom @Natural
 
 -- | Calls Anoma.Protobuf.Mempool.AddTransaction
 addTransaction ::

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

@@ -42,6 +42,7 @@ data ArgFileSpec = ArgFileSpec
 
 data ProveArg
   = ProveArgNat Natural
+  | ProveArgList (AppPath File)
   | ProveArgFile ArgFileSpec
   deriving stock (Data)
 
@@ -51,6 +52,7 @@ parseProveArg = fromProveArg' <$> parseProveArg'
     fromProveArg' :: ProveArg' -> ProveArg
     fromProveArg' (ProveArg' (ty :&: a)) = case ty of
       SProveArgTagNat -> ProveArgNat a
+      SProveArgTagList -> ProveArgList a
       SProveArgTagByteArray -> fileHelper a EncodingBytes DecodingByteArray
       SProveArgTagBase64 -> fileHelper a EncodingBase64 DecodingJammed
       SProveArgTagBytes -> fileHelper a EncodingBytes DecodingJammed
@@ -105,6 +107,7 @@ parseProveArg' =
       ret <- case p of
         SProveArgTagByteArray -> pAppPath
         SProveArgTagBytes -> pAppPath
+        SProveArgTagList -> pAppPath
         SProveArgTagBase64 -> pAppPath
         SProveArgTagBase64UnJammed -> pAppPath
         SProveArgTagBytesUnJammed -> pAppPath

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

@@ -9,6 +9,7 @@ import Prelude qualified
 data ProveArgTag
   = ProveArgTagNat
   | ProveArgTagByteArray
+  | ProveArgTagList
   | ProveArgTagBytesUnJammed
   | ProveArgTagBase64UnJammed
   | ProveArgTagBase64
@@ -19,6 +20,7 @@ instance Show ProveArgTag where
   show = \case
     ProveArgTagNat -> "nat"
     ProveArgTagByteArray -> "bytearray"
+    ProveArgTagList -> "list"
     ProveArgTagBase64 -> "base64"
     ProveArgTagBytes -> "bytes"
     ProveArgTagBytesUnJammed -> "bytes-unjammed"
@@ -28,6 +30,7 @@ type ProveArgType :: ProveArgTag -> GHCType
 type family ProveArgType s = res where
   ProveArgType 'ProveArgTagNat = Natural
   ProveArgType 'ProveArgTagByteArray = AppPath File
+  ProveArgType 'ProveArgTagList = AppPath File
   ProveArgType 'ProveArgTagBase64 = AppPath File
   ProveArgType 'ProveArgTagBytes = AppPath File
   ProveArgType 'ProveArgTagBytesUnJammed = AppPath File
@@ -47,6 +50,7 @@ proveArgTagHelp = itemize (tagHelp <$> allElements)
           (mvar, explain) = first sty $ case t of
             ProveArgTagNat -> ("NATURAL", "is passed verbatim as a nockma atom")
             ProveArgTagByteArray -> ("FILE", "is a file containing bytes that respresent a ByteArray")
+            ProveArgTagList -> ("FILE", "is a file containing a newline delimited list of byte64 bytes that respresents a list of jammed nouns")
             ProveArgTagBase64 -> ("FILE", "is a file containing a base64 encoded nockma atom that represents a" <+> jammedNoun)
             ProveArgTagBytes -> ("FILE", "is a file containing bytes of a nockma atom that represents a" <+> jammedNoun)
             ProveArgTagBase64UnJammed -> ("FILE", "is a file containing a base64 encoded nockma atom that represents an" <+> unjammedAtom)

src/Juvix/Compiler/Nockma/Translation/FromTree.hs

@@ -11,6 +11,7 @@ module Juvix.Compiler.Nockma.Translation.FromTree
     FunctionCtx (..),
     FunctionId (..),
     closurePath,
+    foldTermsOrNil,
     foldTermsOrQuotedNil,
     sub,
     nockNatLiteral,