Skip to content

Commit

Permalink
cue the input file in the nockma dev commands
Browse files Browse the repository at this point in the history
  • Loading branch information
paulcadman committed Oct 3, 2024
1 parent b456251 commit b13a839
Show file tree
Hide file tree
Showing 5 changed files with 62 additions and 9 deletions.
2 changes: 1 addition & 1 deletion app/Commands/Dev/Nockma/Run.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
37 changes: 36 additions & 1 deletion src/Juvix/Compiler/Nockma/Encoding/Cue.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -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.
Expand Down
7 changes: 0 additions & 7 deletions src/Juvix/Compiler/Nockma/Evaluator/Error.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 10 additions & 0 deletions src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
Expand Down
15 changes: 15 additions & 0 deletions src/Juvix/Compiler/Nockma/Translation/FromSource/Error.hs
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit b13a839

Please sign in to comment.