From f9d045efcbcac7f3f197297fc5d206016ed96a59 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 23 Dec 2024 13:14:55 +0100 Subject: [PATCH 1/6] the sigma dream failed --- app/Commands/Dev/Anoma/Prove/Options.hs | 88 +++++++++++++++++++++ src/Juvix/Compiler/Concrete/Data.hs | 2 + src/Juvix/Compiler/Concrete/Data/Literal.hs | 61 ++------------ src/Juvix/Compiler/Concrete/Data/Stage.hs | 2 +- src/Juvix/Data/IntegerWithBase.hs | 59 ++++++++++++++ src/Juvix/Parser/Lexer.hs | 8 +- src/Juvix/Prelude/Base/Foundation.hs | 2 +- 7 files changed, 161 insertions(+), 61 deletions(-) create mode 100644 src/Juvix/Data/IntegerWithBase.hs diff --git a/app/Commands/Dev/Anoma/Prove/Options.hs b/app/Commands/Dev/Anoma/Prove/Options.hs index 3faf72d333..01bdfd372f 100644 --- a/app/Commands/Dev/Anoma/Prove/Options.hs +++ b/app/Commands/Dev/Anoma/Prove/Options.hs @@ -1,19 +1,107 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE QuantifiedConstraints #-} + module Commands.Dev.Anoma.Prove.Options where 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], _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 _proveOutputFile <- optional parseGenericOutputFile pure ProveOptions {..} diff --git a/src/Juvix/Compiler/Concrete/Data.hs b/src/Juvix/Compiler/Concrete/Data.hs index af6ea9c3f4..538a81ae68 100644 --- a/src/Juvix/Compiler/Concrete/Data.hs +++ b/src/Juvix/Compiler/Concrete/Data.hs @@ -14,6 +14,7 @@ module Juvix.Compiler.Concrete.Data module Juvix.Compiler.Concrete.Data.IsOpenShort, module Juvix.Compiler.Concrete.Data.LocalModuleOrigin, module Juvix.Data.NameId, + module Juvix.Data.IntegerWithBase, ) where @@ -30,5 +31,6 @@ import Juvix.Compiler.Concrete.Data.PublicAnn import Juvix.Compiler.Concrete.Data.ScopedName qualified import Juvix.Compiler.Concrete.Data.VisibilityAnn import Juvix.Compiler.Store.Scoped.Data.InfoTable +import Juvix.Data.IntegerWithBase import Juvix.Data.NameId import Juvix.Data.NameKind diff --git a/src/Juvix/Compiler/Concrete/Data/Literal.hs b/src/Juvix/Compiler/Concrete/Data/Literal.hs index 6f41c0a10d..8d4ef7ae3b 100644 --- a/src/Juvix/Compiler/Concrete/Data/Literal.hs +++ b/src/Juvix/Compiler/Concrete/Data/Literal.hs @@ -1,26 +1,15 @@ -module Juvix.Compiler.Concrete.Data.Literal where +module Juvix.Compiler.Concrete.Data.Literal + ( module Juvix.Compiler.Concrete.Data.Literal, + module Juvix.Data.IntegerWithBase, + ) +where import Juvix.Data.Fixity +import Juvix.Data.IntegerWithBase import Juvix.Extra.Serialize -import Juvix.Extra.Strings qualified as Str import Juvix.Prelude import Prettyprinter -data IntegerWithBase = IntegerWithBase - { _integerWithBaseBase :: IntegerBase, - _integerWithBaseValue :: Integer - } - deriving stock (Show, Eq, Ord, Generic, Data) - -data IntegerBase - = IntegerBaseBinary - | IntegerBaseOctal - | IntegerBaseDecimal - | IntegerBaseHexadecimal - deriving stock (Bounded, Enum, Show, Eq, Ord, Generic, Data) - -makeLenses ''IntegerWithBase - data Literal = LitString Text | LitIntegerWithBase IntegerWithBase @@ -28,55 +17,17 @@ data Literal type LiteralLoc = WithLoc Literal -instance Hashable IntegerBase - -instance Serialize IntegerBase - -instance NFData IntegerBase - -instance Hashable IntegerWithBase - -instance Serialize IntegerWithBase - -instance NFData IntegerWithBase - instance Hashable Literal instance Serialize Literal instance NFData Literal -instance HasAtomicity IntegerWithBase where - atomicity = const Atom - instance HasAtomicity Literal where atomicity = \case LitString {} -> Atom LitIntegerWithBase h -> atomicity h -integerBasePrefix :: IntegerBase -> Text -integerBasePrefix = \case - IntegerBaseBinary -> Str.binaryPrefix - IntegerBaseOctal -> Str.octalPrefix - IntegerBaseDecimal -> "" - IntegerBaseHexadecimal -> Str.hexadecimalPrefix - -instance Pretty IntegerWithBase where - pretty IntegerWithBase {..} = - let sign - | _integerWithBaseValue < 0 = "-" - | otherwise = "" - in sign - <> pretty (integerBasePrefix _integerWithBaseBase) - <> pretty (showNum (fromIntegral (abs _integerWithBaseValue))) - where - showNum :: Natural -> String - showNum n = case _integerWithBaseBase of - IntegerBaseBinary -> showBin n "" - IntegerBaseOctal -> showOct n "" - IntegerBaseDecimal -> showInt n "" - IntegerBaseHexadecimal -> showHex n "" - instance Pretty Literal where pretty = \case LitIntegerWithBase n -> pretty n diff --git a/src/Juvix/Compiler/Concrete/Data/Stage.hs b/src/Juvix/Compiler/Concrete/Data/Stage.hs index a768a36bbc..bc934ed766 100644 --- a/src/Juvix/Compiler/Concrete/Data/Stage.hs +++ b/src/Juvix/Compiler/Concrete/Data/Stage.hs @@ -9,6 +9,6 @@ data Stage deriving stock (Eq, Show) type AnyStage (k :: Stage -> GHC.Type) = - Σ Stage (TyCon1 k) + Sigma Stage (TyCon1 k) $(genSingletons [''Stage]) diff --git a/src/Juvix/Data/IntegerWithBase.hs b/src/Juvix/Data/IntegerWithBase.hs new file mode 100644 index 0000000000..60149b91cf --- /dev/null +++ b/src/Juvix/Data/IntegerWithBase.hs @@ -0,0 +1,59 @@ +module Juvix.Data.IntegerWithBase where + +import Juvix.Data.Fixity +import Juvix.Extra.Strings qualified as Str +import Juvix.Prelude.Base +import Juvix.Prelude.Pretty + +data IntegerWithBase = IntegerWithBase + { _integerWithBaseBase :: IntegerBase, + _integerWithBaseValue :: Integer + } + deriving stock (Show, Eq, Ord, Generic, Data) + +data IntegerBase + = IntegerBaseBinary + | IntegerBaseOctal + | IntegerBaseDecimal + | IntegerBaseHexadecimal + deriving stock (Bounded, Enum, Show, Eq, Ord, Generic, Data) + +instance Hashable IntegerWithBase + +instance Serialize IntegerWithBase + +instance NFData IntegerWithBase + +instance Hashable IntegerBase + +instance Serialize IntegerBase + +instance NFData IntegerBase + +makeLenses ''IntegerWithBase + +integerBasePrefix :: IntegerBase -> Text +integerBasePrefix = \case + IntegerBaseBinary -> Str.binaryPrefix + IntegerBaseOctal -> Str.octalPrefix + IntegerBaseDecimal -> "" + IntegerBaseHexadecimal -> Str.hexadecimalPrefix + +instance Pretty IntegerWithBase where + pretty IntegerWithBase {..} = + let sign + | _integerWithBaseValue < 0 = "-" + | otherwise = "" + in sign + <> pretty (integerBasePrefix _integerWithBaseBase) + <> pretty (showNum (fromIntegral (abs _integerWithBaseValue))) + where + showNum :: Natural -> String + showNum n = case _integerWithBaseBase of + IntegerBaseBinary -> showBin n "" + IntegerBaseOctal -> showOct n "" + IntegerBaseDecimal -> showInt n "" + IntegerBaseHexadecimal -> showHex n "" + +instance HasAtomicity IntegerWithBase where + atomicity = const Atom diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs index 711ec89608..6d92ee4f66 100644 --- a/src/Juvix/Parser/Lexer.hs +++ b/src/Juvix/Parser/Lexer.hs @@ -17,7 +17,7 @@ import Juvix.Prelude import Juvix.Prelude.Parsing as P hiding (hspace, space, space1) import Text.Megaparsec.Char.Lexer qualified as L -parseFailure :: Int -> String -> ParsecS r a +parseFailure :: Int -> String -> ParsecT Void Text m a parseFailure off str = P.parseError $ P.FancyError off (Set.singleton (P.ErrorFail str)) whiteSpace1 :: (MonadParsec e s m, Token s ~ Char) => m () @@ -118,7 +118,7 @@ space' special = | n > 1 -> go (n - 1) (acc <> pack txt <> en) | otherwise -> return (acc <> pack txt) -integerWithBase' :: ParsecS r (WithLoc IntegerWithBase) +integerWithBase' :: ParsecT Void Text m (WithLoc IntegerWithBase) integerWithBase' = P.try $ withLoc $ do minus <- optional (char '-') b <- integerBase' @@ -139,14 +139,14 @@ integerWithBase' = P.try $ withLoc $ do integer' :: ParsecS r (WithLoc Integer) integer' = fmap (^. integerWithBaseValue) <$> integerWithBase' -integerBase' :: ParsecS r IntegerBase +integerBase' :: ParsecT Void Text m IntegerBase integerBase' = baseprefix IntegerBaseBinary <|> baseprefix IntegerBaseOctal <|> baseprefix IntegerBaseHexadecimal <|> return IntegerBaseDecimal where - baseprefix :: IntegerBase -> ParsecS r IntegerBase + baseprefix :: IntegerBase -> ParsecT Void Text m IntegerBase baseprefix x = P.chunk (integerBasePrefix x) $> x number' :: ParsecS r (WithLoc Integer) -> Int -> Int -> ParsecS r (WithLoc Int) diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs index 9a93688882..a010b36b00 100644 --- a/src/Juvix/Prelude/Base/Foundation.hs +++ b/src/Juvix/Prelude/Base/Foundation.hs @@ -183,7 +183,7 @@ import Data.Set (Set) import Data.Set qualified as Set import Data.Singletons hiding ((@@)) import Data.Singletons.Sigma -import Data.Singletons.TH (genSingletons, promoteOrdInstances, singOrdInstances) +import Data.Singletons.TH (genDefunSymbols, genSingletons, promoteOrdInstances, singOrdInstances) import Data.Stream (Stream) import Data.Stream qualified as Stream import Data.String From a92f9fb30ebd2c3573c6a5e323275707f3b14682 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 23 Dec 2024 16:39:20 +0100 Subject: [PATCH 2/6] use ProveArg --- app/Commands/Dev/Anoma/Base.hs | 43 ++++---- app/Commands/Dev/Anoma/Prove.hs | 2 +- app/Commands/Dev/Anoma/Prove/Options.hs | 99 ++----------------- .../Dev/Anoma/Prove/Options/ProveArg.hs | 82 +++++++++++++++ .../Dev/Anoma/Prove/Options/ProveArgTag.hs | 27 +++++ app/Commands/Dev/Nockma/Run/Anoma.hs | 5 +- .../Dev/Nockma/Run/EphemeralClient.hs | 2 +- .../Dev/Nockma/Run/EphemeralClient/Options.hs | 5 +- app/Commands/Dev/Nockma/Run/WithClient.hs | 2 +- .../Dev/Nockma/Run/WithClient/Options.hs | 5 +- .../Compiler/Nockma/Encoding/ByteString.hs | 2 +- src/Juvix/Data/Error/GenericError.hs | 15 +++ 12 files changed, 169 insertions(+), 120 deletions(-) create mode 100644 app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs create mode 100644 app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs diff --git a/app/Commands/Dev/Anoma/Base.hs b/app/Commands/Dev/Anoma/Base.hs index c5d5396c7e..e6ed4655f9 100644 --- a/app/Commands/Dev/Anoma/Base.hs +++ b/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 :: diff --git a/app/Commands/Dev/Anoma/Prove.hs b/app/Commands/Dev/Anoma/Prove.hs index 182f5d0355..825526681a 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 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) diff --git a/app/Commands/Dev/Anoma/Prove/Options.hs b/app/Commands/Dev/Anoma/Prove/Options.hs index 01bdfd372f..f40ce51826 100644 --- a/app/Commands/Dev/Anoma/Prove/Options.hs +++ b/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 {..} diff --git a/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs b/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs new file mode 100644 index 0000000000..4fb0acc10e --- /dev/null +++ b/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) diff --git a/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs b/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs new file mode 100644 index 0000000000..28b7e36cac --- /dev/null +++ b/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]) diff --git a/app/Commands/Dev/Nockma/Run/Anoma.hs b/app/Commands/Dev/Nockma/Run/Anoma.hs index ede35370d0..26686a3394 100644 --- a/app/Commands/Dev/Nockma/Run/Anoma.hs +++ b/app/Commands/Dev/Nockma/Run/Anoma.hs @@ -3,10 +3,11 @@ 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 } @@ -14,7 +15,7 @@ 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 -> diff --git a/app/Commands/Dev/Nockma/Run/EphemeralClient.hs b/app/Commands/Dev/Nockma/Run/EphemeralClient.hs index 92193d30f5..d4ad94cb5f 100644 --- a/app/Commands/Dev/Nockma/Run/EphemeralClient.hs +++ b/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 } diff --git a/app/Commands/Dev/Nockma/Run/EphemeralClient/Options.hs b/app/Commands/Dev/Nockma/Run/EphemeralClient/Options.hs index df255a1b00..cfd10639f1 100644 --- a/app/Commands/Dev/Nockma/Run/EphemeralClient/Options.hs +++ b/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 {..} diff --git a/app/Commands/Dev/Nockma/Run/WithClient.hs b/app/Commands/Dev/Nockma/Run/WithClient.hs index 09f46a9dbd..74261f5ea2 100644 --- a/app/Commands/Dev/Nockma/Run/WithClient.hs +++ b/app/Commands/Dev/Nockma/Run/WithClient.hs @@ -20,5 +20,5 @@ runCommand opts = runArgs = RunCommandArgs { _runCommandProgramFile = opts ^. nockmaRunWithClientFile, - _runCommandArgsFile = opts ^. nockmaRunWithClientArgs + _runCommandArgs = opts ^. nockmaRunWithClientArgs } diff --git a/app/Commands/Dev/Nockma/Run/WithClient/Options.hs b/app/Commands/Dev/Nockma/Run/WithClient/Options.hs index 4713147fbe..c4ceb193e3 100644 --- a/app/Commands/Dev/Nockma/Run/WithClient/Options.hs +++ b/app/Commands/Dev/Nockma/Run/WithClient/Options.hs @@ -1,5 +1,6 @@ module Commands.Dev.Nockma.Run.WithClient.Options where +import Commands.Dev.Anoma.Prove.Options.ProveArg import CommonOptions data NockmaRunWithClientOptions = NockmaRunWithClientOptions @@ -7,7 +8,7 @@ data NockmaRunWithClientOptions = NockmaRunWithClientOptions _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) diff --git a/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs b/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs index a506116f74..677136cf99 100644 --- a/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs +++ b/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 diff --git a/src/Juvix/Data/Error/GenericError.hs b/src/Juvix/Data/Error/GenericError.hs index e8e07b6c54..fff3822fcf 100644 --- a/src/Juvix/Data/Error/GenericError.hs +++ b/src/Juvix/Data/Error/GenericError.hs @@ -89,6 +89,21 @@ render renderType endChar err = do lastChar :: Doc a lastChar = maybe "" pretty endChar +asSimpleError :: + forall err r a. + (Members '[Error SimpleError] r) => + (err -> AnsiText) -> + Sem (Error err ': r) a -> + Sem r a +asSimpleError f = mapError (SimpleError . f) + +asSimpleErrorShow :: + forall err r a. + (Show err, Members '[Error SimpleError] r) => + Sem (Error err ': r) a -> + Sem r a +asSimpleErrorShow = asSimpleError (mkAnsiText @Text . show) + -- | Render the error to Text. renderText :: (ToGenericError e, Member (Reader GenericOptions) r) => e -> Sem r Text renderText = render RenderText Nothing From cad50575b21c1d77862bc209a309b7aa771a4cf5 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 23 Dec 2024 16:46:28 +0100 Subject: [PATCH 3/6] completer adds ':' --- app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs b/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs index 4fb0acc10e..6abd0aac0b 100644 --- a/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs +++ b/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs @@ -36,7 +36,7 @@ parseProveArg' = option pp ( long "arg" - <> completer (enumCompleter (Proxy @ProveArgTag)) + <> completer (listCompleter [show a <> ":" | a <- allElements @ProveArgTag]) <> metavar "ARG_TYPE:ARG" ) where From b07a36b9115a95aaa916607635e49308bc925d38 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 23 Dec 2024 17:24:54 +0100 Subject: [PATCH 4/6] use decodeLenient --- app/Commands/Dev/Anoma/Base.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/app/Commands/Dev/Anoma/Base.hs b/app/Commands/Dev/Anoma/Base.hs index e6ed4655f9..295136eb76 100644 --- a/app/Commands/Dev/Anoma/Base.hs +++ b/app/Commands/Dev/Anoma/Base.hs @@ -47,8 +47,7 @@ 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) + bs <- Base64.decodeLenient <$> (fromAppPathFile n >>= readFileBS') fromBytes bs where fromBytes :: ByteString -> Sem r (Term Natural) From 74c4761504f0bd53bf80241276a31857185d4331 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 24 Dec 2024 10:42:06 +0100 Subject: [PATCH 5/6] add help --- app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs | 1 + app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs | 6 ++++++ app/CommonOptions.hs | 4 +--- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs b/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs index 6abd0aac0b..dac53128c7 100644 --- a/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs +++ b/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs @@ -38,6 +38,7 @@ parseProveArg' = ( long "arg" <> completer (listCompleter [show a <> ":" | a <- allElements @ProveArgTag]) <> metavar "ARG_TYPE:ARG" + <> helpDoc ("An argument to the program." <> line <> enumHelp @ProveArgTag proveArgTagHelp) ) where pProveArgTag :: Parse ProveArgTag diff --git a/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs b/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs index 28b7e36cac..0ecd46bb4b 100644 --- a/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs +++ b/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs @@ -25,3 +25,9 @@ type family ProveArgType s = res where $(genDefunSymbols [''ProveArgType]) $(genSingletons [''ProveArgTag]) + +proveArgTagHelp :: ProveArgTag -> AnsiDoc +proveArgTagHelp = \case + ProveArgTagNat -> "A natural number that is passed verbatim as a nockma atom" + ProveArgTagBase64 -> "A path to a file with a base64 encoded nockma atom" + ProveArgTagBytes -> "A path to a file with a byte encoded nockma atom" diff --git a/app/CommonOptions.hs b/app/CommonOptions.hs index f1105d8c1d..c68feb1a1e 100644 --- a/app/CommonOptions.hs +++ b/app/CommonOptions.hs @@ -226,9 +226,7 @@ fieldSizeOpt = eitherReader aux "cairo" -> Right $ Just cairoFieldSize "small" -> Right $ Just smallFieldSize _ -> - mapRight Just - . either Left checkAllowed - $ maybe (Left $ s <> " is not a valid field size") Right (readMaybe s :: Maybe Natural) + mapRight Just (checkAllowed =<< maybe (Left $ s <> " is not a valid field size") Right (readMaybe s :: Maybe Natural)) checkAllowed :: Natural -> Either String Natural checkAllowed n From 79dc587eccb558fe6a45a2e4682d42a2d1b94627 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 24 Dec 2024 11:31:56 +0100 Subject: [PATCH 6/6] improve help message --- .../Dev/Anoma/Prove/Options/ProveArg.hs | 2 +- .../Dev/Anoma/Prove/Options/ProveArgTag.hs | 19 ++++++++++++++----- app/CommonOptions.hs | 2 +- 3 files changed, 16 insertions(+), 7 deletions(-) diff --git a/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs b/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs index dac53128c7..e2273396e7 100644 --- a/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs +++ b/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs @@ -38,7 +38,7 @@ parseProveArg' = ( long "arg" <> completer (listCompleter [show a <> ":" | a <- allElements @ProveArgTag]) <> metavar "ARG_TYPE:ARG" - <> helpDoc ("An argument to the program." <> line <> enumHelp @ProveArgTag proveArgTagHelp) + <> helpDoc ("An argument to the program:" <> line <> proveArgTagHelp) ) where pProveArgTag :: Parse ProveArgTag diff --git a/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs b/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs index 0ecd46bb4b..87cb171f82 100644 --- a/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs +++ b/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs @@ -26,8 +26,17 @@ type family ProveArgType s = res where $(genDefunSymbols [''ProveArgType]) $(genSingletons [''ProveArgTag]) -proveArgTagHelp :: ProveArgTag -> AnsiDoc -proveArgTagHelp = \case - ProveArgTagNat -> "A natural number that is passed verbatim as a nockma atom" - ProveArgTagBase64 -> "A path to a file with a base64 encoded nockma atom" - ProveArgTagBytes -> "A path to a file with a byte encoded nockma atom" +proveArgTagHelp :: AnsiDoc +proveArgTagHelp = itemize (tagHelp <$> allElements) + where + tagHelp :: ProveArgTag -> AnsiDoc + tagHelp t = + let mvar, explain :: AnsiDoc + (mvar, explain) = first sty $ case t of + ProveArgTagNat -> ("NATURAL", "is passed verbatim as a nockma atom") + ProveArgTagBase64 -> ("FILE", "is a file with a base64 encoded nockma atom") + ProveArgTagBytes -> ("FILE", "is a file with a byte encoded nockma atom") + sty = annotate (bold <> colorDull Blue) + tagvar :: AnsiDoc + tagvar = sty (show t <> ":" <> mvar) + in tagvar <+> "where" <+> mvar <+> explain diff --git a/app/CommonOptions.hs b/app/CommonOptions.hs index c68feb1a1e..3df1922c62 100644 --- a/app/CommonOptions.hs +++ b/app/CommonOptions.hs @@ -234,7 +234,7 @@ fieldSizeOpt = eitherReader aux | otherwise = Left $ Prelude.show n <> " is not a recognized field size" enumHelp :: forall a. (Bounded a, Enum a, Show a) => (a -> AnsiDoc) -> AnsiDoc -enumHelp showHelp = vsep ["• " <> annotate bold (show x) <> ": " <> showHelp x | x <- allElements] +enumHelp showHelp = itemize [annotate bold (show x) <> ": " <> showHelp x | x <- allElements] enumReader :: forall a. (Bounded a, Enum a, Show a) => Proxy a -> ReadM a enumReader _ = eitherReader $ \val ->