parse nockma arguments as a list

app/Commands/Dev/Nockma/Run.hs

@@ -20,7 +20,7 @@ runCommand opts = do
     t@(TermCell {}) -> case opts ^. nockmaRunAnomaDir of
       Just path -> do
         anomaDir <- AnomaPath <$> fromAppPathDir path
-        runInAnoma anomaDir t (unfoldTuple parsedArgs)
+        runInAnoma anomaDir t (fromMaybe [] (unfoldList <$> parsedArgs))
       Nothing -> do
         let formula = anomaCallTuple parsedArgs
         (counts, res) <-

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

@@ -21,7 +21,7 @@ parseNockmaRunOptions = do
         somePreFileOpt
         ( long "args"
             <> metavar "ARGS_FILE"
-            <> help "Path to file containing args"
+            <> help "Path to file containing args. When run on anoma, the args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0])."
             <> action "file"
         )
     pure AppPath {_pathIsInput = True, ..}

src/Juvix/Compiler/Nockma/Language.hs

@@ -561,8 +561,22 @@ instance (NockmaEq a) => NockmaEq (Term a) where
 instance (NockmaEq a) => NockmaEq (Cell a) where
   nockmaEq (Cell l r) (Cell l' r') = nockmaEq l l' && nockmaEq r r'
 
-unfoldTuple :: Maybe (Term Natural) -> [Term Natural]
-unfoldTuple = maybe [] (toList . unfoldTuple1)
+unfoldList :: Term Natural -> [Term Natural]
+unfoldList = ensureNockmList . nonEmpty . unfoldTuple
+  where
+    ensureNockmList :: Maybe (NonEmpty (Term Natural)) -> [Term Natural]
+    ensureNockmList = \case
+      Nothing -> err
+      Just l -> case l ^. _unsnoc1 of
+        (ini, lst)
+          | lst == nockNilTagged "unfoldList" -> ini
+          | otherwise -> err
+      where
+        err :: x
+        err = error "Nockma lists must have the form [x1 .. xn 0]"
+
+unfoldTuple :: Term Natural -> [Term Natural]
+unfoldTuple = toList . unfoldTuple1
 
 unfoldTuple1 :: Term Natural -> NonEmpty (Term Natural)
 unfoldTuple1 = nonEmpty' . run . execOutputList . go