From 0961d874d3e39aec0e42612200284d9dcc66d326 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 5 Nov 2024 17:11:24 +0100 Subject: [PATCH] `juvix dev nockma run --anoma-dir ./anoma --args` are given as a nockma list (#3142) When we run nockma code in the anoma node, the arguments should be given as a nockma list. I.e. a nil terminated tuple. --- app/Commands/Dev/Nockma/Run.hs | 2 +- app/Commands/Dev/Nockma/Run/Options.hs | 2 +- src/Juvix/Compiler/Nockma/Language.hs | 18 ++++++++++++++++-- 3 files changed, 18 insertions(+), 4 deletions(-) diff --git a/app/Commands/Dev/Nockma/Run.hs b/app/Commands/Dev/Nockma/Run.hs index 50f90c369b..0c5c884291 100644 --- a/app/Commands/Dev/Nockma/Run.hs +++ b/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) <- diff --git a/app/Commands/Dev/Nockma/Run/Options.hs b/app/Commands/Dev/Nockma/Run/Options.hs index f3236e11e8..3ee5813608 100644 --- a/app/Commands/Dev/Nockma/Run/Options.hs +++ b/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, ..} diff --git a/src/Juvix/Compiler/Nockma/Language.hs b/src/Juvix/Compiler/Nockma/Language.hs index 024e35efc2..a51d115c11 100644 --- a/src/Juvix/Compiler/Nockma/Language.hs +++ b/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