From b13a8395de3e3ed105aafb8c4c5920eb92a0249f Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 27 Sep 2024 14:05:23 +0100 Subject: [PATCH] cue the input file in the nockma dev commands --- app/Commands/Dev/Nockma/Run.hs | 2 +- src/Juvix/Compiler/Nockma/Encoding/Cue.hs | 37 ++++++++++++++++++- src/Juvix/Compiler/Nockma/Evaluator/Error.hs | 7 ---- .../Nockma/Translation/FromSource/Base.hs | 10 +++++ .../Nockma/Translation/FromSource/Error.hs | 15 ++++++++ 5 files changed, 62 insertions(+), 9 deletions(-) create mode 100644 src/Juvix/Compiler/Nockma/Translation/FromSource/Error.hs diff --git a/app/Commands/Dev/Nockma/Run.hs b/app/Commands/Dev/Nockma/Run.hs index de1797a526..e66aa7ba34 100644 --- a/app/Commands/Dev/Nockma/Run.hs +++ b/app/Commands/Dev/Nockma/Run.hs @@ -14,7 +14,7 @@ runCommand opts = do afile <- fromAppPathFile inputFile argsFile <- mapM fromAppPathFile (opts ^. nockmaRunArgs) parsedArgs <- mapM (Nockma.parseTermFile >=> checkParsed) argsFile - parsedTerm <- Nockma.parseTermFile afile >>= checkParsed + parsedTerm <- Nockma.parseJammedFile afile case parsedTerm of t@(TermCell {}) -> do let formula = anomaCallTuple parsedArgs diff --git a/src/Juvix/Compiler/Nockma/Encoding/Cue.hs b/src/Juvix/Compiler/Nockma/Encoding/Cue.hs index ee20276373..ff6fd60c9d 100644 --- a/src/Juvix/Compiler/Nockma/Encoding/Cue.hs +++ b/src/Juvix/Compiler/Nockma/Encoding/Cue.hs @@ -154,7 +154,7 @@ atomToBits a' = do n <- nockNatural' a' return (integerToVectorBits @Integer (fromIntegral n)) --- | Transfor a vector of bits to a decoded term +-- | Transform a vector of bits to a decoded term cueFromBits :: forall a r. ( NockNatural a, @@ -168,6 +168,19 @@ cueFromBits :: Sem r (Term a) cueFromBits v = evalBitReader v (evalState (initCueState @a) (runReader initCueEnv cueFromBitsSem)) +cueFromByteString' :: + forall a r. + ( NockNatural a, + Members + '[ Error DecodingError, + Error (ErrNockNatural' a) + ] + r + ) => + ByteString -> + Sem r (Term a) +cueFromByteString' = cueFromBits . cloneFromByteString + cueFromBitsSem :: forall a r. ( NockNatural a, @@ -275,6 +288,28 @@ cueEither = . runErrorNoCallStack @DecodingError . cue' +cueFromByteString :: + -- NB: The signature returns the DecodingError in an Either to avoid + -- overlapping instances with `ErrNockNatural a` when errors are handled. See + -- the comment above `ErrNockNatural' a` for more explanation. + forall a r. + ( NockNatural a, + Member (Error (ErrNockNatural a)) r + ) => + ByteString -> + Sem r (Either DecodingError (Term a)) +cueFromByteString = + runErrorNoCallStackWith @(ErrNockNatural' a) (\(ErrNockNatural' e) -> throw e) + . runErrorNoCallStack @DecodingError + . cueFromByteString' + +cueFromByteString'' :: + forall a. + (NockNatural a) => + ByteString -> + Either (ErrNockNatural a) (Either DecodingError (Term a)) +cueFromByteString'' = run . runErrorNoCallStack . cueFromByteString + {- `ErrNockNatural a` must be wrapped in a newtype to avoid overlapping instances with `DecodingError` when errors are handled before the type variable `a` is resolved. diff --git a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs index c35c1a15c9..1f76d64566 100644 --- a/src/Juvix/Compiler/Nockma/Evaluator/Error.hs +++ b/src/Juvix/Compiler/Nockma/Evaluator/Error.hs @@ -26,13 +26,6 @@ data NockEvalError a | ErrDecodingFailed (DecodingFailed a) | ErrVerificationFailed (VerificationFailed a) -newtype GenericNockEvalError = GenericNockEvalError - { _genericNockEvalErrorMessage :: AnsiText - } - -class ToGenericNockEvalError a where - toGenericNockEvalError :: a -> GenericNockEvalError - data ExpectedCell a = ExpectedCell { _expectedCellCtx :: EvalCtx, _expectedCellAtom :: Atom a diff --git a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs index 4789007866..dcf01da0e2 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs @@ -14,6 +14,8 @@ import Juvix.Prelude qualified as Prelude import Juvix.Prelude.Parsing hiding (runParser) import Text.Megaparsec qualified as P import Text.Megaparsec.Char.Lexer qualified as L +import Juvix.Compiler.Nockma.Encoding.Cue qualified as Cue +import Data.ByteString qualified as BS type Parser = Parsec Void Text @@ -23,6 +25,14 @@ parseText = runParser noFile parseReplText :: Text -> Either MegaparsecError (ReplTerm Natural) parseReplText = runParserFor replTerm noFile +parseJammedFile :: (MonadIO m) => Prelude.Path Abs File -> m (Term Natural) +parseJammedFile fp = do + bs <- liftIO (BS.readFile (toFilePath fp)) + case Cue.cueFromByteString'' @Natural bs of + Left _ -> error "nock natural error" + Right (Left _) -> error "cue decoding error" + Right (Right t) -> return t + parseTermFile :: (MonadIO m) => Prelude.Path Abs File -> m (Either MegaparsecError (Term Natural)) parseTermFile fp = do txt <- readFile fp diff --git a/src/Juvix/Compiler/Nockma/Translation/FromSource/Error.hs b/src/Juvix/Compiler/Nockma/Translation/FromSource/Error.hs new file mode 100644 index 0000000000..fa19a1e71f --- /dev/null +++ b/src/Juvix/Compiler/Nockma/Translation/FromSource/Error.hs @@ -0,0 +1,15 @@ +module Juvix.Compiler.Nockma.Translation.FromSource.Error where + +import Juvix.Prelude.Base +import Juvix.Compiler.Nockma.Encoding.Cue qualified as Cue +import Juvix.Compiler.Nockma.Language (NockNaturalNaturalError) +import Juvix.Prelude.Pretty + +data CueDecodingError + = ErrDecodingError Cue.DecodingError + | ErrNockNaturalError NockNaturalNaturalError + deriving stock (Show) + +instance Pretty CueDecodingError where + pretty = \case + ErrDecodingError e -> undefined