From a4faa3118fa0e236d7586892265939fbaff6317c Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 24 Dec 2024 14:21:55 +0100 Subject: [PATCH] Modify how the arguments are passed to the anoma node (#3258) ![image](https://github.com/user-attachments/assets/bd683eed-bdb5-4370-a05e-1c3bc4aea650) --- app/Commands/Dev/Anoma/Base.hs | 42 +++++----- app/Commands/Dev/Anoma/Prove.hs | 2 +- app/Commands/Dev/Anoma/Prove/Options.hs | 11 ++- .../Dev/Anoma/Prove/Options/ProveArg.hs | 83 +++++++++++++++++++ .../Dev/Anoma/Prove/Options/ProveArgTag.hs | 42 ++++++++++ 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 +- app/CommonOptions.hs | 6 +- src/Juvix/Compiler/Concrete/Data.hs | 2 + src/Juvix/Compiler/Concrete/Data/Literal.hs | 61 ++------------ src/Juvix/Compiler/Concrete/Data/Stage.hs | 2 +- .../Compiler/Nockma/Encoding/ByteString.hs | 2 +- src/Juvix/Data/Error/GenericError.hs | 15 ++++ src/Juvix/Data/IntegerWithBase.hs | 59 +++++++++++++ src/Juvix/Parser/Lexer.hs | 8 +- src/Juvix/Prelude/Base/Foundation.hs | 2 +- 19 files changed, 259 insertions(+), 97 deletions(-) create mode 100644 app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs create mode 100644 app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs create mode 100644 src/Juvix/Data/IntegerWithBase.hs diff --git a/app/Commands/Dev/Anoma/Base.hs b/app/Commands/Dev/Anoma/Base.hs index c5d5396c7e..295136eb76 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,29 @@ 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 + bs <- Base64.decodeLenient <$> (fromAppPathFile n >>= readFileBS') + 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 3faf72d333..f40ce51826 100644 --- a/app/Commands/Dev/Anoma/Prove/Options.hs +++ b/app/Commands/Dev/Anoma/Prove/Options.hs @@ -1,10 +1,15 @@ -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 data ProveOptions = ProveOptions { _proveFile :: AppPath File, - _proveArgs :: Maybe (AppPath File), + _proveArgs :: [ProveArg], _proveOutputFile :: Maybe (AppPath File) } deriving stock (Data) @@ -14,6 +19,6 @@ makeLenses ''ProveOptions parseProveOptions :: Parser ProveOptions parseProveOptions = do _proveFile <- parseInputFile FileExtNockma - _proveArgs <- optional anomaArgsOpt + _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..e2273396e7 --- /dev/null +++ b/app/Commands/Dev/Anoma/Prove/Options/ProveArg.hs @@ -0,0 +1,83 @@ +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 (listCompleter [show a <> ":" | a <- allElements @ProveArgTag]) + <> metavar "ARG_TYPE:ARG" + <> helpDoc ("An argument to the program:" <> line <> proveArgTagHelp) + ) + 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..87cb171f82 --- /dev/null +++ b/app/Commands/Dev/Anoma/Prove/Options/ProveArgTag.hs @@ -0,0 +1,42 @@ +{-# 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]) + +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/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/app/CommonOptions.hs b/app/CommonOptions.hs index f1105d8c1d..3df1922c62 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 @@ -236,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 -> 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/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 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