Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

JuvixCore #1421

Merged
merged 85 commits into from
Aug 30, 2022
Merged
Show file tree
Hide file tree
Changes from 79 commits
Commits
Show all changes
85 commits
Select commit Hold shift + click to select a range
740347a
JuvixCore started
lukaszcz Jul 22, 2022
eb9f8b8
new recursors
lukaszcz Jul 25, 2022
853ab2a
recursors
lukaszcz Jul 25, 2022
7d69674
BuiltinOp
lukaszcz Jul 25, 2022
7360910
context draft
lukaszcz Jul 25, 2022
21baec6
recursors & context
lukaszcz Jul 26, 2022
9460d21
evaluator draft
lukaszcz Jul 26, 2022
9054530
info draft
lukaszcz Jul 26, 2022
ee90563
info based on Dynamic and TypeRep
lukaszcz Jul 27, 2022
64a7366
recursors redone
lukaszcz Jul 28, 2022
7003544
info types
lukaszcz Jul 28, 2022
8762780
comments
lukaszcz Jul 28, 2022
06d7959
lazy if & default case branch
lukaszcz Jul 28, 2022
4ae7ef8
fix computeFreeVarsInfo & computeIdentInfo
lukaszcz Jul 29, 2022
24140d3
comments
lukaszcz Jul 29, 2022
9d824c2
comments
lukaszcz Jul 29, 2022
3297ee6
refactor
lukaszcz Jul 29, 2022
427b4a5
refactor
lukaszcz Jul 29, 2022
0667b0c
fix ormolu & build errors
lukaszcz Jul 29, 2022
c8ee435
refactor
lukaszcz Aug 1, 2022
d7221a4
evaluator
lukaszcz Aug 1, 2022
2297617
bang patterns
lukaszcz Aug 1, 2022
df78c57
make ormolu happy
lukaszcz Aug 1, 2022
130df4b
evaluator: more readable but slightly slower handling of application
lukaszcz Aug 2, 2022
e929bef
refactor
lukaszcz Aug 2, 2022
f701084
refactor
lukaszcz Aug 2, 2022
b644b21
refactor
lukaszcz Aug 2, 2022
17d794e
make ormolu happy
lukaszcz Aug 3, 2022
45ba1ce
refactor
lukaszcz Aug 3, 2022
ac16483
BinderList
lukaszcz Aug 3, 2022
54c3c01
ArgsNumInfo
lukaszcz Aug 3, 2022
0dfc858
refactor InfoTable
lukaszcz Aug 3, 2022
1326544
remove stupid comment
lukaszcz Aug 3, 2022
d0f3b39
refactor for PR #1420
lukaszcz Aug 3, 2022
f3e7345
remove builtin boolean operations (can be implemeted with 'if')
lukaszcz Aug 8, 2022
89d71cf
pretty printing
lukaszcz Aug 8, 2022
f4354ca
parser for Node
lukaszcz Aug 10, 2022
7c5fc67
minor changes
lukaszcz Aug 10, 2022
0163e1f
minor refactor
lukaszcz Aug 10, 2022
97f3be2
minor refactor
lukaszcz Aug 10, 2022
1ae9664
JuvixCore evaluator CLI
lukaszcz Aug 11, 2022
f5c1c2e
transformations
lukaszcz Aug 11, 2022
0afabbb
refactor for PR #1443
lukaszcz Aug 11, 2022
5098e6e
JuvixCore parsing bugfixes
lukaszcz Aug 11, 2022
0cb52d7
JuvixCore pretty printing minor changes
lukaszcz Aug 15, 2022
4d2603a
String constants
lukaszcz Aug 15, 2022
68133a5
builtin nil & cons
lukaszcz Aug 15, 2022
e7e63eb
JuvixCore parsing improvements
lukaszcz Aug 15, 2022
ee68874
IO monad builtins
lukaszcz Aug 15, 2022
4c23f2b
comment
lukaszcz Aug 15, 2022
e4839e4
small changes
lukaszcz Aug 15, 2022
b2404dd
IO sequence
lukaszcz Aug 15, 2022
383acfa
evalIO bugfix
lukaszcz Aug 15, 2022
e180a23
polymorphic type variables
lukaszcz Aug 16, 2022
95e9922
case bugfixes
lukaszcz Aug 16, 2022
0d8d091
some tests
lukaszcz Aug 16, 2022
493db70
several tests
lukaszcz Aug 16, 2022
c5f09da
modulo
lukaszcz Aug 16, 2022
84415b6
make bind left-associative
lukaszcz Aug 18, 2022
c15974a
more tests
lukaszcz Aug 18, 2022
a0099a4
pretty printing improvements
lukaszcz Aug 18, 2022
f912995
structural equality
lukaszcz Aug 18, 2022
7355e15
remove Axiom & Suspended (axioms can be represented by special data c…
lukaszcz Aug 18, 2022
e8e0926
:l and :r REPL commands
lukaszcz Aug 19, 2022
c06cfb3
:l bugfix
lukaszcz Aug 19, 2022
3411903
--show-de-bruijn option for REPL
lukaszcz Aug 19, 2022
ae09332
tests
lukaszcz Aug 19, 2022
26e453f
minor changes
lukaszcz Aug 21, 2022
b74eb6a
Closure printing bugfix
lukaszcz Aug 21, 2022
74a1c4f
remove Data
lukaszcz Aug 21, 2022
ef50470
Pi node
lukaszcz Aug 21, 2022
259815b
minor
lukaszcz Aug 21, 2022
3272d03
eta-expansion bugfix
lukaszcz Aug 22, 2022
b146d0e
Positive evaluator tests
lukaszcz Aug 22, 2022
be8884b
negative tests
lukaszcz Aug 22, 2022
9c60989
test036 reference
lukaszcz Aug 22, 2022
7e10c7c
debugging builtins
lukaszcz Aug 22, 2022
e78be96
make ormolu happy
lukaszcz Aug 22, 2022
25bc4ba
refactor Info
lukaszcz Aug 26, 2022
fa06665
Info.lookup'
lukaszcz Aug 29, 2022
2133c22
remove 'nil' and 'cons' builtin constructors
lukaszcz Aug 29, 2022
10ee3cf
remove if, use builtin constructors for true, false
lukaszcz Aug 29, 2022
f7e8d1f
refactor: use underscore in field names
lukaszcz Aug 29, 2022
0fd5d1f
remove stupid comment
lukaszcz Aug 29, 2022
d0a3c96
change foldl to foldl'
lukaszcz Aug 29, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion app/App.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ import System.Console.ANSI qualified as Ansi
data App m a where
ExitMsg :: ExitCode -> Text -> App m ()
ExitJuvixError :: JuvixError -> App m a
PrintJuvixError :: JuvixError -> App m ()
ReadGlobalOptions :: App m GlobalOptions
RenderStdOut :: (HasAnsiBackend a, HasTextBackend a) => a -> App m ()
RunPipelineEither :: Sem PipelineEff a -> App m (Either JuvixError a)
Expand All @@ -31,11 +32,16 @@ runAppIO g = interpret $ \case
Say t
| g ^. globalOnlyErrors -> return ()
| otherwise -> embed (putStrLn t)
PrintJuvixError e -> do
printErr e
ExitJuvixError e -> do
(embed . hPutStrLn stderr . Error.render (not (g ^. globalNoColors)) (g ^. globalOnlyErrors)) e
printErr e
embed exitFailure
ExitMsg exitCode t -> embed (putStrLn t >> exitWith exitCode)
Raw b -> embed (ByteString.putStr b)
where
printErr e =
(embed . hPutStrLn stderr . Error.render (not (g ^. globalNoColors)) (g ^. globalOnlyErrors)) e

runPipeline :: Member App r => Sem PipelineEff a -> Sem r a
runPipeline p = do
Expand Down
11 changes: 11 additions & 0 deletions app/Commands/Dev.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
module Commands.Dev
( module Commands.Dev,
module Commands.Dev.Core,
module Commands.Dev.Internal,
module Commands.Dev.Parse,
module Commands.Dev.Scope,
Expand All @@ -8,6 +9,7 @@ module Commands.Dev
)
where

import Commands.Dev.Core
import Commands.Dev.Doc
import Commands.Dev.Internal
import Commands.Dev.Parse
Expand All @@ -21,6 +23,7 @@ data InternalCommand
= DisplayRoot
| Highlight HighlightOptions
| Internal MicroCommand
| Core CoreCommand
| MiniC
| MiniHaskell
| MonoJuvix
Expand All @@ -39,6 +42,7 @@ parseInternalCommand =
( mconcat
[ commandHighlight,
commandInternal,
commandCore,
commandMiniC,
commandMiniHaskell,
commandMonoJuvix,
Expand Down Expand Up @@ -96,6 +100,13 @@ commandInternal =
(Internal <$> parseMicroCommand)
(progDesc "Subcommands related to Internal")

commandCore :: Mod CommandFields InternalCommand
commandCore =
command "core" $
info
(Core <$> parseCoreCommand)
(progDesc "Subcommands related to JuvixCore")

commandMiniHaskell :: Mod CommandFields InternalCommand
commandMiniHaskell =
command "minihaskell" $
Expand Down
69 changes: 69 additions & 0 deletions app/Commands/Dev/Core.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
module Commands.Dev.Core where

import Juvix.Prelude hiding (Doc)
import Options.Applicative

data CoreCommand
= Repl CoreReplOptions
| Eval CoreEvalOptions

newtype CoreReplOptions = CoreReplOptions
{ _coreReplShowDeBruijn :: Bool
}

newtype CoreEvalOptions = CoreEvalOptions
{ _coreEvalNoIO :: Bool
}

makeLenses ''CoreReplOptions
makeLenses ''CoreEvalOptions

defaultCoreEvalOptions :: CoreEvalOptions
defaultCoreEvalOptions =
CoreEvalOptions
{ _coreEvalNoIO = False
}

parseCoreCommand :: Parser CoreCommand
parseCoreCommand =
hsubparser $
mconcat
[ commandRepl,
commandEval
]
where
commandRepl :: Mod CommandFields CoreCommand
commandRepl = command "repl" replInfo

commandEval :: Mod CommandFields CoreCommand
commandEval = command "eval" evalInfo

replInfo :: ParserInfo CoreCommand
replInfo =
info
(Repl <$> parseCoreReplOptions)
(progDesc "Start an interactive session of the JuvixCore evaluator")

evalInfo :: ParserInfo CoreCommand
evalInfo =
info
(Eval <$> parseCoreEvalOptions)
(progDesc "Evaluate a JuvixCore file and pretty print the result")

parseCoreEvalOptions :: Parser CoreEvalOptions
parseCoreEvalOptions = do
_coreEvalNoIO <-
switch
( long "no-io"
<> help "Don't interpret the IO effects"
)
pure CoreEvalOptions {..}

parseCoreReplOptions :: Parser CoreReplOptions
parseCoreReplOptions = do
_coreReplShowDeBruijn <-
switch
( long "show-de-bruijn"
<> help "Show variable de Bruijn indices"
)
pure CoreReplOptions {..}
152 changes: 152 additions & 0 deletions app/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,15 @@ import Juvix.Compiler.Concrete.Data.InfoTable qualified as Scoper
import Juvix.Compiler.Concrete.Pretty qualified as Scoper
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
import Juvix.Compiler.Core.Data.InfoTable qualified as Core
import Juvix.Compiler.Core.Error qualified as Core
import Juvix.Compiler.Core.Evaluator qualified as Core
import Juvix.Compiler.Core.Extra.Base qualified as Core
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Info.NoDisplayInfo qualified as Info
import Juvix.Compiler.Core.Language qualified as Core
import Juvix.Compiler.Core.Pretty qualified as Core
import Juvix.Compiler.Core.Translation.FromSource qualified as Core
import Juvix.Compiler.Internal.Pretty qualified as Internal
import Juvix.Compiler.Internal.Translation.FromAbstract qualified as Internal
import Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination qualified as Termination
Expand All @@ -39,6 +48,7 @@ import Juvix.Prelude.Pretty hiding (Doc)
import Options.Applicative
import System.Environment (getProgName)
import System.Process qualified as Process
import Text.Megaparsec.Pos qualified as M
import Text.Show.Pretty hiding (Html)

findRoot :: CommandGlobalOptions -> IO (FilePath, Package)
Expand Down Expand Up @@ -103,6 +113,7 @@ runCommand cmdWithOpts = do
(root, pkg) <- embed (findRoot cmdWithOpts)
case cmd of
(Dev DisplayRoot) -> say (pack root)
(Dev (Core cmd')) -> runCoreCommand globalOpts cmd'
_ -> do
-- Other commands require an entry point:
case getEntryPoint root pkg globalOpts of
Expand Down Expand Up @@ -264,6 +275,147 @@ runCommand cmdWithOpts = do
printSuccessExit (n <> " Terminates with order " <> show (toList k))
_ -> impossible

runCoreCommand :: Members '[Embed IO, App] r => GlobalOptions -> CoreCommand -> Sem r ()
runCoreCommand globalOpts = \case
Repl opts -> do
embed showReplWelcome
runRepl opts Core.emptyInfoTable
Eval opts ->
case globalOpts ^. globalInputFiles of
[] -> printFailureExit "Provide a JuvixCore file to run this command\nUse --help to see all the options"
files -> mapM_ (evalFile opts) files
where
runRepl ::
forall r.
Members '[Embed IO, App] r =>
CoreReplOptions ->
Core.InfoTable ->
Sem r ()
runRepl opts tab = do
embed (putStr "> ")
embed (hFlush stdout)
done <- embed isEOF
unless done $ do
s <- embed getLine
case fromText (strip s) of
":q" -> return ()
":h" -> do
embed showReplHelp
runRepl opts tab
':' : 'p' : ' ' : s' ->
case Core.parseText tab (fromString s') of
Left err -> do
printJuvixError (JuvixError err)
runRepl opts tab
Right (tab', Just node) -> do
renderStdOut (Core.ppOutDefault node)
embed (putStrLn "")
runRepl opts tab'
Right (tab', Nothing) ->
runRepl opts tab'
':' : 'e' : ' ' : s' ->
case Core.parseText tab (fromString s') of
Left err -> do
printJuvixError (JuvixError err)
runRepl opts tab
Right (tab', Just node) ->
replEval True tab' node
Right (tab', Nothing) ->
runRepl opts tab'
':' : 'l' : ' ' : f -> do
s' <- embed (readFile f)
case Core.runParser "" f Core.emptyInfoTable s' of
Left err -> do
printJuvixError (JuvixError err)
runRepl opts tab
Right (tab', Just node) ->
replEval False tab' node
Right (tab', Nothing) ->
runRepl opts tab'
":r" ->
runRepl opts Core.emptyInfoTable
_ ->
case Core.parseText tab s of
Left err -> do
printJuvixError (JuvixError err)
runRepl opts tab
Right (tab', Just node) ->
replEval False tab' node
Right (tab', Nothing) ->
runRepl opts tab'
where
replEval :: Bool -> Core.InfoTable -> Core.Node -> Sem r ()
replEval noIO tab' node = do
r <- doEval noIO defaultLoc tab' node
case r of
Left err -> do
printJuvixError (JuvixError err)
runRepl opts tab'
Right node'
| Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
runRepl opts tab'
Right node' -> do
renderStdOut (Core.ppOut docOpts node')
embed (putStrLn "")
runRepl opts tab'
where
defaultLoc = singletonInterval (mkLoc "stdin" 0 (M.initialPos "stdin"))
docOpts = set Core.optShowDeBruijnIndices (opts ^. coreReplShowDeBruijn) Core.defaultOptions

showReplWelcome :: IO ()
showReplWelcome = do
putStrLn "JuvixCore REPL"
putStrLn ""
putStrLn "Type \":h\" for help."
putStrLn ""

showReplHelp :: IO ()
showReplHelp = do
putStrLn ""
putStrLn "JuvixCore REPL"
putStrLn ""
putStrLn "Type in a JuvixCore program to evaluate."
putStrLn ""
putStrLn "Available commands:"
putStrLn ":p expr Pretty print \"expr\"."
putStrLn ":e expr Evaluate \"expr\" without interpreting IO actions."
putStrLn ":l file Load and evaluate \"file\". Resets REPL state."
putStrLn ":r Reset REPL state."
putStrLn ":q Quit."
putStrLn ":h Display this help message."
putStrLn ""

evalFile :: Members '[Embed IO, App] r => CoreEvalOptions -> FilePath -> Sem r ()
evalFile opts f = do
s <- embed (readFile f)
case Core.runParser "" f Core.emptyInfoTable s of
Left err -> exitJuvixError (JuvixError err)
Right (tab, Just node) -> do
r <- doEval (opts ^. coreEvalNoIO) defaultLoc tab node
case r of
Left err -> exitJuvixError (JuvixError err)
Right node'
| Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
return ()
Right node' -> do
renderStdOut (Core.ppOutDefault node')
embed (putStrLn "")
Right (_, Nothing) -> return ()
where
defaultLoc = singletonInterval (mkLoc f 0 (M.initialPos f))

doEval ::
Members '[Embed IO, App] r =>
Bool ->
Interval ->
Core.InfoTable ->
Core.Node ->
Sem r (Either Core.CoreError Core.Node)
doEval noIO loc tab node =
if noIO
then embed $ Core.catchEvalError loc (Core.eval (tab ^. Core.identContext) [] node)
else embed $ Core.catchEvalErrorIO loc (Core.evalIO (tab ^. Core.identContext) [] node)

showHelpText :: ParserPrefs -> IO ()
showHelpText p = do
progn <- getProgName
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
import Juvix.Compiler.Concrete.Language
import Juvix.Compiler.Concrete.Language qualified as L
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty
import Juvix.Compiler.Concrete.Translation.FromSource.Error qualified as Parser
import Juvix.Data.CodeAnn
import Juvix.Parser.Error qualified as Parser
import Juvix.Prelude

data MultipleDeclarations = MultipleDeclarations
Expand Down
4 changes: 2 additions & 2 deletions src/Juvix/Compiler/Concrete/Translation/FromSource.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module Juvix.Compiler.Concrete.Translation.FromSource
( module Juvix.Compiler.Concrete.Translation.FromSource,
module Juvix.Compiler.Concrete.Translation.FromSource.Data.Context,
module Juvix.Compiler.Concrete.Data.ParsedInfoTable,
module Juvix.Compiler.Concrete.Translation.FromSource.Error,
module Juvix.Parser.Error,
)
where

Expand All @@ -14,9 +14,9 @@ import Juvix.Compiler.Concrete.Extra (MonadParsec (takeWhile1P))
import Juvix.Compiler.Concrete.Extra qualified as P
import Juvix.Compiler.Concrete.Language
import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context
import Juvix.Compiler.Concrete.Translation.FromSource.Error
import Juvix.Compiler.Concrete.Translation.FromSource.Lexer hiding (symbol)
import Juvix.Compiler.Pipeline.EntryPoint
import Juvix.Parser.Error
import Juvix.Prelude
import Juvix.Prelude.Pretty (Pretty, prettyText)

Expand Down
Loading