1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-03 09:41:10 +03:00

Add dev core from-concrete command (#1833)

This commit is contained in:
janmasrovira 2023-02-10 12:37:28 +01:00 committed by GitHub
parent 1876883445
commit 207b1594f8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 199 additions and 141 deletions

View File

@ -4,6 +4,7 @@ import Commands.Base
import Commands.Dev.Core.Asm as Asm
import Commands.Dev.Core.Compile as Compile
import Commands.Dev.Core.Eval as Eval
import Commands.Dev.Core.FromConcrete as FromConcrete
import Commands.Dev.Core.Options
import Commands.Dev.Core.Read as Read
import Commands.Dev.Core.Repl as Repl
@ -14,6 +15,7 @@ runCommand = \case
Repl opts -> Repl.runCommand opts
Eval opts -> Eval.runCommand opts
Read opts -> Read.runCommand opts
FromConcrete opts -> FromConcrete.runCommand opts
Strip opts -> Strip.runCommand opts
CoreAsm opts -> Asm.runCommand opts
CoreCompile opts -> Compile.runCommand opts

View File

@ -0,0 +1,72 @@
module Commands.Dev.Core.FromConcrete where
import Commands.Base
import Commands.Dev.Core.FromConcrete.Options
import Evaluator
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Pretty qualified as Core
import Juvix.Compiler.Core.Transformation qualified as Core
import Juvix.Compiler.Core.Translation
runCommand :: forall r. Members '[Embed IO, App] r => CoreFromConcreteOptions -> Sem r ()
runCommand localOpts = do
tab <- (^. coreResultTable) <$> runPipeline (localOpts ^. coreFromConcreteInputFile) upToCore
path :: Path Abs File <- someBaseToAbs' (localOpts ^. coreFromConcreteInputFile . pathPath)
let tab' :: InfoTable = Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
inInputModule :: IdentifierInfo -> Bool
inInputModule = (== Just path) . (^? identifierLocation . _Just . intervalFile)
mainIdens :: [IdentifierInfo] =
sortOn
(^. identifierLocation)
(filter inInputModule (toList (tab' ^. infoIdentifiers)))
mainInfo :: Maybe IdentifierInfo
mainInfo = do
s <- tab' ^. infoMain
tab' ^. infoIdentifiers . at s
selInfo :: Maybe IdentifierInfo
selInfo = do
s <- localOpts ^. coreFromConcreteSymbolName
find (^. identifierName . to (== s)) mainIdens
goPrint :: Sem r ()
goPrint = forM_ nodes printNode
where
printNode :: (Text, Core.Node) -> Sem r ()
printNode (name, node) = do
renderStdOut (name <> " = ")
renderStdOut (Core.ppOut localOpts node)
newline
newline
nodes :: [(Text, Core.Node)]
| isJust (localOpts ^. coreFromConcreteSymbolName) = [fromMaybe err (getDef selInfo)]
| otherwise = mapMaybe (getDef . Just) mainIdens
goEval :: Sem r ()
goEval = evalAndPrint localOpts tab' evalNode
where
evalNode :: Core.Node
| isJust (localOpts ^. coreFromConcreteSymbolName) = getNode' selInfo
| otherwise = getNode' mainInfo
getDef :: Maybe IdentifierInfo -> Maybe (Text, Core.Node)
getDef i = (getName' i,) <$> getNode i
getName' :: Maybe IdentifierInfo -> Text
getName' m = fromMaybe err m ^. identifierName
getNode' :: Maybe IdentifierInfo -> Core.Node
getNode' m = fromMaybe err (getNode m)
getNode :: Maybe IdentifierInfo -> Maybe Core.Node
getNode m = m >>= \i -> tab' ^. identContext . at (i ^. identifierSymbol)
err :: a
err = error "function not found"
if
| localOpts ^. coreFromConcreteEval -> goEval
| otherwise -> goPrint

View File

@ -0,0 +1,60 @@
module Commands.Dev.Core.FromConcrete.Options where
import CommonOptions
import Evaluator qualified as Eval
import Juvix.Compiler.Core.Data.TransformationId
import Juvix.Compiler.Core.Pretty.Options qualified as Core
data CoreFromConcreteOptions = CoreFromConcreteOptions
{ _coreFromConcreteTransformations :: [TransformationId],
_coreFromConcreteShowDeBruijn :: Bool,
_coreFromConcreteNoIO :: Bool,
_coreFromConcreteEval :: Bool,
_coreFromConcreteInputFile :: AppPath File,
_coreFromConcreteSymbolName :: Maybe Text
}
deriving stock (Data)
makeLenses ''CoreFromConcreteOptions
instance CanonicalProjection CoreFromConcreteOptions Core.Options where
project c =
Core.defaultOptions
{ Core._optShowDeBruijnIndices = c ^. coreFromConcreteShowDeBruijn
}
instance CanonicalProjection CoreFromConcreteOptions Eval.EvalOptions where
project c =
Eval.EvalOptions
{ _evalInputFile = c ^. coreFromConcreteInputFile,
_evalNoIO = c ^. coreFromConcreteNoIO
}
parseCoreFromConcreteOptions :: Parser CoreFromConcreteOptions
parseCoreFromConcreteOptions = do
_coreFromConcreteTransformations <- optTransformationIds
_coreFromConcreteShowDeBruijn <-
switch
( long "show-de-bruijn"
<> help "Show variable de Bruijn indices"
)
_coreFromConcreteEval <-
switch
( long "eval"
<> help "Evaluate the main function"
)
_coreFromConcreteNoIO <-
switch
( long "no-io"
<> help "Don't interpret the IO effects"
)
_coreFromConcreteInputFile <- parseInputJuvixFile
_coreFromConcreteSymbolName <-
optional $
strOption
( long "symbol-name"
<> short 's'
<> help "Print/eval a specific function identifier (default for eval: main)"
<> metavar "NAME"
)
pure CoreFromConcreteOptions {..}

View File

@ -3,6 +3,7 @@ module Commands.Dev.Core.Options where
import Commands.Dev.Core.Asm.Options
import Commands.Dev.Core.Compile.Options
import Commands.Dev.Core.Eval.Options
import Commands.Dev.Core.FromConcrete.Options
import Commands.Dev.Core.Read.Options
import Commands.Dev.Core.Repl.Options
import Commands.Dev.Core.Strip.Options
@ -12,6 +13,7 @@ data CoreCommand
= Repl CoreReplOptions
| Eval CoreEvalOptions
| Read CoreReadOptions
| FromConcrete CoreFromConcreteOptions
| Strip CoreStripOptions
| CoreAsm CoreAsmOptions
| CoreCompile CoreCompileOptions
@ -25,6 +27,7 @@ parseCoreCommand =
commandEval,
commandRead,
commandStrip,
commandFromConcrete,
commandAsm,
commandCompile
]
@ -44,6 +47,9 @@ parseCoreCommand =
commandAsm :: Mod CommandFields CoreCommand
commandAsm = command "asm" asmInfo
commandFromConcrete :: Mod CommandFields CoreCommand
commandFromConcrete = command "from-concrete" fromSourceInfo
commandCompile :: Mod CommandFields CoreCommand
commandCompile = command "compile" compileInfo
@ -53,6 +59,12 @@ parseCoreCommand =
(Repl <$> parseCoreReplOptions)
(progDesc "Start an interactive session of the JuvixCore evaluator")
fromSourceInfo :: ParserInfo CoreCommand
fromSourceInfo =
info
(FromConcrete <$> parseCoreFromConcreteOptions)
(progDesc "Read a Juvix file and compile it to core")
evalInfo :: ParserInfo CoreCommand
evalInfo =
info

View File

@ -2,7 +2,6 @@ module Commands.Dev.Internal where
import Commands.Base
import Commands.Dev.Internal.Arity qualified as Arity
import Commands.Dev.Internal.CoreEval qualified as InternalCoreEval
import Commands.Dev.Internal.Options
import Commands.Dev.Internal.Pretty qualified as InternalPretty
import Commands.Dev.Internal.Typecheck qualified as InternalTypecheck
@ -12,4 +11,3 @@ runCommand = \case
Pretty opts -> InternalPretty.runCommand opts
Arity opts -> Arity.runCommand opts
TypeCheck opts -> InternalTypecheck.runCommand opts
CoreEval opts -> InternalCoreEval.runCommand opts

View File

@ -1,32 +0,0 @@
module Commands.Dev.Internal.CoreEval where
import Commands.Base
import Commands.Dev.Internal.CoreEval.Options
import Data.HashMap.Internal.Strict (elems)
import Data.HashMap.Strict qualified as HashMap
import Evaluator
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Language.Base
import Juvix.Compiler.Core.Transformation qualified as Core
import Juvix.Compiler.Core.Translation
import Safe (headMay)
getSymbol :: forall r. Member App r => InfoTable -> Text -> Sem r Symbol
getSymbol tab name = maybe failAction (return . (^. identifierSymbol)) mIdent
where
identifiers :: [IdentifierInfo]
identifiers = elems (tab ^. infoIdentifiers)
mIdent :: Maybe IdentifierInfo
mIdent = headMay (filter ((== name) . (^. identifierName)) identifiers)
failAction :: Sem r a
failAction = exitMsg (ExitFailure 1) (name <> " is not a function identifier")
runCommand :: (Members '[Embed IO, App] r) => InternalCoreEvalOptions -> Sem r ()
runCommand localOpts = do
tab <- (^. coreResultTable) <$> runPipeline (localOpts ^. internalCoreEvalInputFile) upToCore
let tab' = Core.applyTransformations (project localOpts ^. internalCoreEvalTransformations) tab
ms <- mapM (getSymbol tab') (localOpts ^. internalCoreEvalSymbolName)
let symbol = ms <|> (tab' ^. infoMain)
forM_ (symbol >>= ((tab' ^. identContext) HashMap.!?)) (evalAndPrint localOpts tab')

View File

@ -1,54 +0,0 @@
module Commands.Dev.Internal.CoreEval.Options where
import CommonOptions
import Evaluator qualified as Eval
import Juvix.Compiler.Core.Data.TransformationId
import Juvix.Compiler.Core.Pretty.Options qualified as Core
data InternalCoreEvalOptions = InternalCoreEvalOptions
{ _internalCoreEvalTransformations :: [TransformationId],
_internalCoreEvalShowDeBruijn :: Bool,
_internalCoreEvalNoIO :: Bool,
_internalCoreEvalInputFile :: AppPath File,
_internalCoreEvalSymbolName :: Maybe Text
}
deriving stock (Data)
makeLenses ''InternalCoreEvalOptions
instance CanonicalProjection InternalCoreEvalOptions Core.Options where
project c =
Core.defaultOptions
{ Core._optShowDeBruijnIndices = c ^. internalCoreEvalShowDeBruijn
}
instance CanonicalProjection InternalCoreEvalOptions Eval.EvalOptions where
project c =
Eval.EvalOptions
{ _evalInputFile = c ^. internalCoreEvalInputFile,
_evalNoIO = c ^. internalCoreEvalNoIO
}
parseInternalCoreEval :: Parser InternalCoreEvalOptions
parseInternalCoreEval = do
_internalCoreEvalTransformations <- optTransformationIds
_internalCoreEvalShowDeBruijn <-
switch
( long "show-de-bruijn"
<> help "Show variable de Bruijn indices"
)
_internalCoreEvalNoIO <-
switch
( long "no-io"
<> help "Don't interpret the IO effects"
)
_internalCoreEvalInputFile <- parseInputJuvixFile
_internalCoreEvalSymbolName <-
optional $
strOption
( long "symbol-name"
<> short 's'
<> help "Evaluate a function identifier (default: main)"
<> metavar "NAME"
)
pure InternalCoreEvalOptions {..}

View File

@ -1,7 +1,6 @@
module Commands.Dev.Internal.Options where
import Commands.Dev.Internal.Arity.Options
import Commands.Dev.Internal.CoreEval.Options
import Commands.Dev.Internal.Pretty.Options
import Commands.Dev.Internal.Typecheck.Options
import CommonOptions
@ -10,7 +9,6 @@ data InternalCommand
= Pretty InternalPrettyOptions
| TypeCheck InternalTypeOptions
| Arity InternalArityOptions
| CoreEval InternalCoreEvalOptions
deriving stock (Data)
parseInternalCommand :: Parser InternalCommand
@ -19,8 +17,7 @@ parseInternalCommand =
mconcat
[ commandPretty,
commandArity,
commandTypeCheck,
commandCoreEval
commandTypeCheck
]
where
commandArity :: Mod CommandFields InternalCommand
@ -32,9 +29,6 @@ parseInternalCommand =
commandTypeCheck :: Mod CommandFields InternalCommand
commandTypeCheck = command "typecheck" typeCheckInfo
commandCoreEval :: Mod CommandFields InternalCommand
commandCoreEval = command "core-eval" coreEvalInfo
arityInfo :: ParserInfo InternalCommand
arityInfo =
info
@ -52,9 +46,3 @@ parseInternalCommand =
info
(TypeCheck <$> parseInternalType)
(progDesc "Translate a Juvix file to Internal and typecheck the result")
coreEvalInfo :: ParserInfo InternalCommand
coreEvalInfo =
info
(CoreEval <$> parseInternalCoreEval)
(progDesc "Translate a Juvix file to Core and evaluate the result")

View File

@ -39,6 +39,13 @@ data AnsiText = forall t.
{ _ansiText :: t
}
instance HasTextBackend Text where
toTextStream = toTextStream . pretty
toTextDoc = toTextDoc . pretty
instance HasAnsiBackend Text where
toAnsiDoc = pretty
instance HasTextBackend AnsiText where
toTextStream (AnsiText t) = toTextStream t
toTextDoc (AnsiText t) = toTextDoc t

View File

@ -0,0 +1,45 @@
working-directory: ./../../../../tests
tests:
- name: core-from-concrete-eval
command:
- juvix
- dev
- core
- from-concrete
- --eval
args:
- positive/Internal/LiteralInt.juvix
stdout: |
suc (suc zero)
exit-status: 0
- name: core-from-concrete-eval
command:
- juvix
- dev
- core
- from-concrete
- --eval
- --transforms
- nat-to-int
args:
- positive/Internal/LiteralInt.juvix
stdout: |
2
exit-status: 0
- name: core-from-concrete-eval-s
command:
- juvix
- dev
- core
- from-concrete
- --eval
- --symbol-name
- f
args:
- positive/Internal/LiteralInt.juvix
stdout: |
suc zero
exit-status: 0

View File

@ -50,43 +50,3 @@ tests:
matches: |-
(.+)\/([^\/]+)\.juvix\:[0-9]*\:[0-9]*\-[0-9]*\: error
exit-status: 1
- name: internal-core-eval
command:
- juvix
- dev
- internal
- core-eval
args:
- positive/Internal/LiteralInt.juvix
stdout: |
suc (suc zero)
exit-status: 0
- name: internal-core-eval-transform
command:
- juvix
- dev
- internal
- core-eval
- --transforms
- nat-to-int
args:
- positive/Internal/LiteralInt.juvix
stdout: |
2
exit-status: 0
- name: internal-core-eval-symbol-name
command:
- juvix
- dev
- internal
- core-eval
- --symbol-name
- f
args:
- positive/Internal/LiteralInt.juvix
stdout: |
suc zero
exit-status: 0