anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-04 05:33:27 +03:00
Code Issues Projects Releases Wiki Activity

Add Geb Backend Evaluator with some extra subcommands (#1808)

Browse Source 
This PR introduces an evaluator for the Geb STLC interface/fragment and
other related commands, including a REPL to interact with his backend.

-
https://github.com/anoma/geb/blob/mariari/binaries/src/specs/lambda.lisp

We have included a REPL and support for commands such as read and eval
here. Check out:

```
juvix dev geb --help
```

- [x] Add Geb evaluator with the two basic eval strategies.
- [x] Add quasi quoter: return morphisms from typed geb values.
- [x] Add type/object inference for morphisms.
- [x] All combined: morphisms-eval-to-morphisms
- [x] Parse and pretty printer Geb values (without quoting them)
- [x] Parse files containing Geb terms:
- [x] Saved in a .lisp file according to anoma/geb example (typed
object).
  - [x] Store in a .geb file simple as simple lisp expression.
- [x] Add related commands to the CLI for `dev geb`:
  - [x] Subcommand: eval
  - [x] Subcommand: read
  - [x] Subcommand: infer
  - [x] Subcommand: repl
  - [x] Subcommand: check 
- [x] Minor changes `hom` by `!->` in the Geb prettyprinter
- [x] Add tests for:
   - [x] New subcommand (smoke tests)
   - [x] Eval

Issues to solve after merging this PR: 

- Add location to Geb ast for proper error location.
- Add tests for all related subcommands, e.g. check, and infer.
- Check compilation from Core to Geb: (run inferObject with the type
provided by the core node).
- [x] Update the vs code-plugin to load Geb repl and eval.
(31994c8684)
This commit is contained in:
Jonathan Cubides 2023-02-22 15:27:40 +01:00 committed by GitHub
parent f4591be3bd
commit 9a4da4cab8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
84 changed files with 3071 additions and 113 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Makefile
View File

@ -22,6 +22,9 @@ EXAMPLE_WEBAPP_OUTPUT=_docs/examples/webapp
WEBAPP_EXAMPLES=TicTacToe/Web/TicTacToe.juvix
DEMO_EXAMPLE=examples/demo/Demo.juvix
MAKEAUXFLAGS?=-s
MAKE=make ${MAKEAUXFLAGS}
ORGTOMDPRG ?=pandoc
ORGOPTS=--from org --to markdown_strict -s -o $@
@ -46,7 +49,7 @@ clean: clean-runtime
.PHONY: clean-runtime
clean-runtime: clean-juvix-build
@cd runtime && make clean
@cd runtime && ${MAKE} clean
.PHONY: clean-juvix-build
clean-juvix-build:
@ -130,9 +133,6 @@ haddock :
# -- Codebase Health
# ------------------------------------------------------------------------------
MAKEAUXFLAGS?=-s
MAKE=make ${MAKEAUXFLAGS}
ORMOLU?=stack exec -- ormolu
ORMOLUFILES = $(shell git ls-files '*.hs' '*.hs-boot' | grep -v '^contrib/')
ORMOLUFLAGS?=--no-cabal

2
app/Commands/Dev.hs
View File

@ -8,6 +8,7 @@ import Commands.Base
import Commands.Dev.Asm qualified as Asm
import Commands.Dev.Core qualified as Core
import Commands.Dev.DisplayRoot qualified as DisplayRoot
import Commands.Dev.Geb qualified as Geb
import Commands.Dev.Highlight qualified as Highlight
import Commands.Dev.Internal qualified as Internal
import Commands.Dev.MiniC qualified as MiniC
@ -26,6 +27,7 @@ runCommand = \case
MiniC opts -> MiniC.runCommand opts
Termination opts -> Termination.runCommand opts
Core opts -> Core.runCommand opts
Geb opts -> Geb.runCommand opts
Asm opts -> Asm.runCommand opts
Runtime opts -> Runtime.runCommand opts
DisplayRoot opts -> DisplayRoot.runCommand opts

10
app/Commands/Dev/Core/Read.hs
View File

@ -8,7 +8,15 @@ import Juvix.Compiler.Core.Scoper qualified as Scoper
import Juvix.Compiler.Core.Transformation qualified as Core
import Juvix.Compiler.Core.Translation.FromSource qualified as Core
runCommand :: forall r a. (Members '[Embed IO, App] r, CanonicalProjection a Eval.EvalOptions, CanonicalProjection a Core.Options, CanonicalProjection a CoreReadOptions) => a -> Sem r ()
runCommand ::
forall r a.
( Members '[Embed IO, App] r,
CanonicalProjection a Eval.EvalOptions,
CanonicalProjection a Core.Options,
CanonicalProjection a CoreReadOptions
) =>
a ->
Sem r ()
runCommand opts = do
inputFile :: Path Abs File <- someBaseToAbs' sinputFile
s' <- embed . readFile . toFilePath $ inputFile

21
app/Commands/Dev/Geb.hs Normal file
View File

@ -0,0 +1,21 @@
module Commands.Dev.Geb
( module Commands.Dev.Geb,
module Commands.Dev.Geb.Options,
)
where
import Commands.Base
import Commands.Dev.Geb.Eval as Eval
import Commands.Dev.Geb.Infer as Check
import Commands.Dev.Geb.Infer as Infer
import Commands.Dev.Geb.Options
import Commands.Dev.Geb.Read as Read
import Commands.Dev.Geb.Repl as Repl
runCommand :: forall r. (Members '[Embed IO, App] r) => GebCommand -> Sem r ()
runCommand = \case
GebCommandRepl opts -> Repl.runCommand opts
GebCommandEval opts -> Eval.runCommand opts
GebCommandRead opts -> Read.runCommand opts
GebCommandInfer opts -> Infer.runCommand opts
GebCommandCheck opts -> Check.runCommand opts

23
app/Commands/Dev/Geb/Check.hs Normal file
View File

@ -0,0 +1,23 @@
module Commands.Dev.Geb.Check where
import Commands.Base
import Commands.Dev.Geb.Infer.Options
import Juvix.Compiler.Backend.Geb qualified as Geb
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
runCommand ::
forall r.
(Member App r, Member (Embed IO) r) =>
GebInferOptions ->
Sem r ()
runCommand opts = do
let b :: SomeBase File
b = opts ^. gebInferOptionsInputFile . pathPath
f :: Path Abs File <- someBaseToAbs' b
content :: Text <- embed (readFile (toFilePath f))
case Geb.runParser' f content of
Right tyMorph@(Geb.TypedMorphism {}) -> do
case run . runError @CheckingError $ (Geb.check' tyMorph) of
Left err -> exitJuvixError (JuvixError err)
Right _ -> renderStdOut ("Well done! It typechecks" :: Text)
Left err -> exitJuvixError (JuvixError err)

54
app/Commands/Dev/Geb/Eval.hs Normal file
View File

@ -0,0 +1,54 @@
module Commands.Dev.Geb.Eval where
import Commands.Base
import Commands.Dev.Geb.Eval.Options
import Juvix.Compiler.Backend.Geb.Evaluator qualified as Geb
import Juvix.Compiler.Backend.Geb.Language qualified as Geb
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
import Juvix.Compiler.Backend.Geb.Translation.FromSource qualified as Geb
runCommand ::
forall r a.
( Members '[App, Embed IO] r,
CanonicalProjection a Geb.EvaluatorOptions,
CanonicalProjection a GebEvalOptions
) =>
a ->
Sem r ()
runCommand opts = do
let b :: SomeBase File
b = project opts ^. gebEvalOptionsInputFile . pathPath
f :: Path Abs File <- someBaseToAbs' b
content :: Text <- embed (readFile (toFilePath f))
case Geb.runParser f content of
Left err -> exitJuvixError (JuvixError err)
Right gebTerm -> do
evalAndPrint opts gebTerm
embed (putStrLn "")
evalAndPrint ::
forall r a.
( Members '[App, Embed IO] r,
CanonicalProjection a Geb.EvaluatorOptions
) =>
a ->
Geb.Expression ->
Sem r ()
evalAndPrint opts = \case
Geb.ExpressionMorphism morphism -> do
let opts' :: Geb.EvaluatorOptions = project opts
let env :: Geb.Env =
Geb.Env
{ _envEvaluatorOptions = opts',
_envContext = mempty
}
if
| opts' ^. Geb.evaluatorOptionsOutputMorphism ->
case Geb.evalAndOutputMorphism' env morphism of
Left err -> exitJuvixError err
Right m -> renderStdOut (Geb.ppOut opts' m)
| otherwise ->
case Geb.eval' env morphism of
Left err -> exitJuvixError err
Right m -> renderStdOut (Geb.ppOut opts' m)
Geb.ExpressionObject _ -> error Geb.objNoEvalMsg

37
app/Commands/Dev/Geb/Eval/Options.hs Normal file
View File

@ -0,0 +1,37 @@
module Commands.Dev.Geb.Eval.Options where
import CommonOptions
import Juvix.Compiler.Backend.Geb.Evaluator qualified as Geb
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
data GebEvalOptions = GebEvalOptions
{ _gebEvalOptionsInputFile :: AppPath File,
_gebEvalOptionsOutputMorphism :: Bool
}
deriving stock (Data)
makeLenses ''GebEvalOptions
instance CanonicalProjection GebEvalOptions Geb.EvaluatorOptions where
project x =
Geb.EvaluatorOptions
{ _evaluatorOptionsOutputMorphism = (x ^. gebEvalOptionsOutputMorphism)
}
instance CanonicalProjection GebEvalOptions Geb.Options where
project _ = Geb.defaultOptions
parseGebEvalOptions :: Parser GebEvalOptions
parseGebEvalOptions = do
_gebEvalOptionsInputFile <- parseInputJuvixGebFile
_gebEvalOptionsOutputMorphism <- optOutputMorphism
pure GebEvalOptions {..}
optOutputMorphism :: Parser Bool
optOutputMorphism =
switch
( long "output-morphism"
<> short 'm'
<> showDefault
<> help "Output a Geb morphism back from a Geb value"
)

24
app/Commands/Dev/Geb/Infer.hs Normal file
View File

@ -0,0 +1,24 @@
module Commands.Dev.Geb.Infer where
import Commands.Base
import Commands.Dev.Geb.Infer.Options
import Juvix.Compiler.Backend.Geb qualified as Geb
runCommand ::
forall r.
(Member App r, Member (Embed IO) r) =>
GebInferOptions ->
Sem r ()
runCommand opts = do
let b :: SomeBase File
b = opts ^. gebInferOptionsInputFile . pathPath
f :: Path Abs File <- someBaseToAbs' b
content :: Text <- embed (readFile (toFilePath f))
case Geb.runParser f content of
Right (Geb.ExpressionMorphism gebTerm) ->
case Geb.inferObject' gebTerm of
Left err -> exitJuvixError (JuvixError err)
Right obj -> renderStdOut (Geb.ppOut opts obj)
Right (Geb.ExpressionObject _) ->
exitJuvixError (error @JuvixError "No inference for objects")
Left err -> exitJuvixError (JuvixError err)

19
app/Commands/Dev/Geb/Infer/Options.hs Normal file
View File

@ -0,0 +1,19 @@
module Commands.Dev.Geb.Infer.Options where
import CommonOptions
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
newtype GebInferOptions = GebInferOptions
{ _gebInferOptionsInputFile :: AppPath File
}
deriving stock (Data)
makeLenses ''GebInferOptions
instance CanonicalProjection GebInferOptions Geb.Options where
project _ = Geb.defaultOptions
parseGebInferOptions :: Parser GebInferOptions
parseGebInferOptions = do
_gebInferOptionsInputFile <- parseInputJuvixGebFile
pure GebInferOptions {..}

76
app/Commands/Dev/Geb/Options.hs Normal file
View File

@ -0,0 +1,76 @@
module Commands.Dev.Geb.Options
( module Commands.Dev.Geb.Options,
module Commands.Dev.Geb.Eval.Options,
module Commands.Dev.Geb.Repl.Options,
)
where
import Commands.Dev.Geb.Eval.Options
import Commands.Dev.Geb.Infer.Options
import Commands.Dev.Geb.Read.Options
import Commands.Dev.Geb.Repl.Options
import CommonOptions
data GebCommand
= GebCommandRepl GebReplOptions
| GebCommandEval GebEvalOptions
| GebCommandRead GebReadOptions
| GebCommandInfer GebInferOptions
| GebCommandCheck GebInferOptions
deriving stock (Data)
parseGebCommand :: Parser GebCommand
parseGebCommand =
hsubparser $
mconcat
[ commandRepl,
commandEval,
commandRead,
commandInfer,
commandCheck
]
where
commandRepl :: Mod CommandFields GebCommand
commandRepl = command "repl" replInfo
commandEval :: Mod CommandFields GebCommand
commandEval = command "eval" evalInfo
commandRead :: Mod CommandFields GebCommand
commandRead = command "read" readInfo
commandInfer :: Mod CommandFields GebCommand
commandInfer = command "infer" inferInfo
commandCheck :: Mod CommandFields GebCommand
commandCheck = command "check" checkInfo
replInfo :: ParserInfo GebCommand
replInfo =
info
(GebCommandRepl <$> parseGebReplOptions)
(progDesc "Start an interactive session of the JuvixGeb evaluator")
evalInfo :: ParserInfo GebCommand
evalInfo =
info
(GebCommandEval <$> parseGebEvalOptions)
(progDesc "Evaluate a JuvixGeb file and pretty print the result")
readInfo :: ParserInfo GebCommand
readInfo =
info
(GebCommandRead <$> parseGebReadOptions)
(progDesc "Read a JuvixGeb file and pretty print it")
inferInfo :: ParserInfo GebCommand
inferInfo =
info
(GebCommandInfer <$> parseGebInferOptions)
(progDesc "Infer the Geb object for a Geb morphism found in the given file. ")
checkInfo :: ParserInfo GebCommand
checkInfo =
info
(GebCommandInfer <$> parseGebInferOptions)
(progDesc "Check the given Geb object matches the given Geb morphism")

22
app/Commands/Dev/Geb/Read.hs Normal file
View File

@ -0,0 +1,22 @@
module Commands.Dev.Geb.Read where
import Commands.Base
import Commands.Dev.Geb.Read.Options
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
import Juvix.Compiler.Backend.Geb.Translation.FromSource qualified as Geb
runCommand ::
forall r.
(Member App r, Member (Embed IO) r) =>
GebReadOptions ->
Sem r ()
runCommand opts = do
let b :: SomeBase File
b = opts ^. gebReadOptionsInputFile . pathPath
f :: Path Abs File <- someBaseToAbs' b
content :: Text <- embed (readFile (toFilePath f))
case Geb.runParser f content of
Left err -> exitJuvixError (JuvixError err)
Right gebTerm -> do
renderStdOut (Geb.ppOut opts gebTerm)
embed (putStrLn "")

19
app/Commands/Dev/Geb/Read/Options.hs Normal file
View File

@ -0,0 +1,19 @@
module Commands.Dev.Geb.Read.Options where
import CommonOptions
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
newtype GebReadOptions = GebReadOptions
{ _gebReadOptionsInputFile :: AppPath File
}
deriving stock (Data)
makeLenses ''GebReadOptions
instance CanonicalProjection GebReadOptions Geb.Options where
project _ = Geb.defaultOptions
parseGebReadOptions :: Parser GebReadOptions
parseGebReadOptions = do
_gebReadOptionsInputFile <- parseInputJuvixGebFile
pure GebReadOptions {..}

317
app/Commands/Dev/Geb/Repl.hs Normal file
View File

@ -0,0 +1,317 @@
{-# LANGUAGE QuasiQuotes #-}
module Commands.Dev.Geb.Repl where
import Commands.Base hiding (command)
import Commands.Dev.Geb.Repl.Format
import Commands.Dev.Geb.Repl.Options
import Control.Exception (throwIO)
import Control.Monad.State.Strict qualified as State
import Data.String.Interpolate (i, __i)
import Juvix.Compiler.Backend.Geb qualified as Geb
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
import Juvix.Data.Error.GenericError qualified as Error
import Juvix.Extra.Version
import Juvix.Prelude.Pretty qualified as P
import System.Console.ANSI qualified as Ansi
import System.Console.Haskeline
import System.Console.Repline qualified as Repline
type ReplS = State.StateT ReplState IO
type Repl a = Repline.HaskelineT ReplS a
data ReplState = ReplState
{ _replContextEntryPoint :: Maybe EntryPoint,
_replStateInvokeDir :: Path Abs Dir,
_replStateGlobalOptions :: GlobalOptions
}
makeLenses ''ReplState
replPath :: Path Abs File
replPath = $(mkAbsFile "/repl.geb")
runCommand :: (Members '[Embed IO, App] r) => GebReplOptions -> Sem r ()
runCommand replOpts = do
root <- askPkgDir
buildDir <- askBuildDir
package <- askPackage
invokeDir <- askInvokeDir
globalOptions <- askGlobalOptions
let getReplEntryPoint :: SomeBase File -> Repl EntryPoint
getReplEntryPoint inputFile = do
gopts <- State.gets (^. replStateGlobalOptions)
absInputFile :: Path Abs File <- replMakeAbsolute inputFile
return $
EntryPoint
{ _entryPointRoot = root,
_entryPointBuildDir = buildDir,
_entryPointResolverRoot = root,
_entryPointNoTermination = gopts ^. globalNoTermination,
_entryPointNoPositivity = gopts ^. globalNoPositivity,
_entryPointNoStdlib = gopts ^. globalNoStdlib,
_entryPointPackage = package,
_entryPointModulePaths = pure absInputFile,
_entryPointGenericOptions = project gopts,
_entryPointStdin = Nothing
}
embed
( State.evalStateT
(replAction replOpts getReplEntryPoint)
( ReplState
{ _replContextEntryPoint = Nothing,
_replStateGlobalOptions = globalOptions,
_replStateInvokeDir = invokeDir
}
)
)
loadEntryPoint :: EntryPoint -> Repl ()
loadEntryPoint ep = do
State.modify
( set
replContextEntryPoint
(Just ep)
)
let epPath :: Path Abs File = ep ^. entryPointModulePaths . _head1
liftIO (putStrLn . pack $ "OK loaded " <> toFilePath epPath)
content <- liftIO (readFile (toFilePath epPath))
let evalRes =
Geb.runEval $
Geb.RunEvalArgs
{ _runEvalArgsContent = content,
_runEvalArgsInputFile = epPath,
_runEvalArgsEvaluatorOptions = Geb.defaultEvaluatorOptions
}
printEvalResult evalRes
reloadFile :: String -> Repl ()
reloadFile _ = do
mentryPoint <- State.gets ((^. replContextEntryPoint))
maybe noFileLoadedMsg loadEntryPoint mentryPoint
pSomeFile :: String -> SomeBase File
pSomeFile = someFile . unpack . strip . pack
type ReplEntryPoint = SomeBase File -> Repl EntryPoint
loadFile :: ReplEntryPoint -> SomeBase File -> Repl ()
loadFile getReplEntryPoint f = do
entryPoint <- getReplEntryPoint f
loadEntryPoint entryPoint
inferObject :: String -> Repl ()
inferObject gebMorphism = Repline.dontCrash $ do
case Geb.runParser replPath (pack gebMorphism) of
Left err -> printError (JuvixError err)
Right (Geb.ExpressionMorphism morphism) -> do
case Geb.inferObject' morphism of
Right obj -> renderOut (Geb.ppOut Geb.defaultEvaluatorOptions obj)
Left err -> printError (JuvixError err)
Right _ -> printError (error "Inference only works on Geb morphisms.")
checkTypedMorphism :: String -> Repl ()
checkTypedMorphism gebMorphism = Repline.dontCrash $ do
case Geb.runParser' replPath (pack gebMorphism) of
Left err -> printError (JuvixError err)
Right tyMorphism@(Geb.TypedMorphism {}) -> do
case run . runError @CheckingError $ Geb.check' tyMorphism of
Right obj -> renderOut (Geb.ppOut Geb.defaultEvaluatorOptions obj)
Left err -> printError (JuvixError err)
runReplCommand :: String -> Repl ()
runReplCommand input =
Repline.dontCrash $
do
let evalRes =
Geb.runEval $
Geb.RunEvalArgs
{ _runEvalArgsContent = pack input,
_runEvalArgsInputFile = replPath,
_runEvalArgsEvaluatorOptions = Geb.defaultEvaluatorOptions
}
printEvalResult evalRes
evalAndOutputMorphism :: String -> Repl ()
evalAndOutputMorphism input =
Repline.dontCrash $ do
let evalRes =
Geb.runEval $
Geb.RunEvalArgs
{ _runEvalArgsContent = pack input,
_runEvalArgsInputFile = replPath,
_runEvalArgsEvaluatorOptions =
Geb.defaultEvaluatorOptions
{ Geb._evaluatorOptionsOutputMorphism = True
}
}
printEvalResult evalRes
options :: ReplEntryPoint -> [(String, String -> Repl ())]
options replEntryPoint =
[ ("help", Repline.dontCrash . helpText),
-- `multiline` is included here for auto-completion purposes only.
-- `repline`'s `multilineCommand` logic overrides this no-op.
(multilineCmd, Repline.dontCrash . \_ -> return ()),
("check", checkTypedMorphism),
("load", Repline.dontCrash . loadFile replEntryPoint . pSomeFile),
("morphism", evalAndOutputMorphism),
("quit", quit),
("reload", Repline.dontCrash . reloadFile),
("root", printRoot),
("type", inferObject),
("version", displayVersion)
]
optsCompleter :: ReplEntryPoint -> Repline.WordCompleter ReplS
optsCompleter replEntryPoint n = do
let names = (":" <>) . fst <$> options replEntryPoint
return (filter (isPrefixOf n) names)
prefix :: Maybe Char
prefix = Just ':'
multilineCommand :: Maybe String
multilineCommand = Just multilineCmd
tabComplete :: ReplEntryPoint -> Repline.CompleterStyle ReplS
tabComplete replEntryPoint =
Repline.Prefix
(Repline.wordCompleter (optsCompleter replEntryPoint))
defaultMatcher
replAction :: GebReplOptions -> ReplEntryPoint -> ReplS ()
replAction replOpts replEntryPoint =
Repline.evalReplOpts
Repline.ReplOpts
{ prefix,
multilineCommand,
initialiser = initSession replOpts,
finaliser = endSession,
command = runReplCommand,
options = options replEntryPoint,
tabComplete = tabComplete replEntryPoint,
banner
}
defaultMatcher :: [(String, CompletionFunc ReplS)]
defaultMatcher = [(":load", Repline.fileCompleter)]
banner :: Repline.MultiLine -> Repl String
banner = \case
Repline.MultiLine -> return "... "
Repline.SingleLine -> replPromptText
noFileLoadedMsg :: Repl ()
noFileLoadedMsg =
renderOut
. ReplMessageDoc
$ P.annotate
ReplError
"No file loaded. Load a file using the `:load FILE` command."
<> P.line
initSession :: GebReplOptions -> Repl ()
initSession replOpts
| replOpts ^. gebReplOptionsSilent = return ()
| otherwise = renderOut welcomeMsg
welcomeMsg :: ReplMessageDoc
welcomeMsg =
ReplMessageDoc $
P.annotate ReplIntro "Welcome to the Juvix Geb REPL!"
<> P.line
<> normal [i|Juvix v#{versionTag}: https://juvix.org.|]
<> P.line
<> normal "Type :help for help."
<> P.line
replPromptText :: Repl String
replPromptText = do
r <- replText . ReplMessageDoc $ P.annotate ReplPrompt "geb> "
return (unpack r)
helpText :: String -> Repl ()
helpText _ =
renderOutNormal
[__i|
EXPRESSION Evaluate a Geb morphism
:help Print this help
:load FILE Load a file into the REPL
:reload Reload the currently loaded file
:check EXPRESSION Check the type of a Geb morphism
:type EXPRESSION Infer the type of a Geb morphism
:morphism EXPRESSION Read back after evaluate a Geb morphism
:version Display the Juvix version
:multiline Enter multiline mode
:root Print the root directory of the REPL
:version Display the Juvix version
:quit Exit the REPL
|]
multilineCmd :: String
multilineCmd = "multiline"
quit :: String -> Repl ()
quit _ = liftIO (throwIO Interrupt)
endSession :: Repl Repline.ExitDecision
endSession = return Repline.Exit
printRoot :: String -> Repl ()
printRoot _ = do
r <- State.gets (^. replStateInvokeDir)
renderOutNormal $ pack (toFilePath r)
displayVersion :: String -> Repl ()
displayVersion _ = renderOutNormal versionTag
replMakeAbsolute :: SomeBase b -> Repl (Path Abs b)
replMakeAbsolute = \case
Abs p -> return p
Rel r -> do
invokeDir <- State.gets (^. replStateInvokeDir)
return (invokeDir <//> r)
replText :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl Text
replText t = do
opts <- State.gets (^. replStateGlobalOptions)
hasAnsi <- liftIO (Ansi.hSupportsANSIColor stdout)
return $ P.toAnsiText (not (opts ^. globalNoColors) && hasAnsi) t
render' :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl ()
render' t = do
opts <- State.gets (^. replStateGlobalOptions)
hasAnsi <- liftIO (Ansi.hSupportsANSIColor stdout)
liftIO (P.renderIO (not (opts ^. globalNoColors) && hasAnsi) t)
renderOut :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl ()
renderOut t = render' t >> liftIO (putStrLn "")
renderOutNormal :: Text -> Repl ()
renderOutNormal = renderOut . ReplMessageDoc . normal
printError :: JuvixError -> Repl ()
printError e = do
opts <- State.gets (^. replStateGlobalOptions)
hasAnsi <- liftIO (Ansi.hSupportsANSIColor stderr)
let useAnsi = (not (opts ^. globalNoColors) && hasAnsi)
errorText <-
replText . ReplMessageDoc
$ P.annotate
ReplError
$ pretty
( run
. runReader (project' @GenericOptions opts)
$ Error.render useAnsi False e
)
liftIO $ hPutStrLn stderr errorText
printEvalResult :: Either JuvixError Geb.RunEvalResult -> Repl ()
printEvalResult = \case
Left err -> printError err
Right (Geb.RunEvalResultGebValue v) ->
renderOut (Geb.ppOut Geb.defaultEvaluatorOptions v)
Right (Geb.RunEvalResultMorphism morphism) ->
renderOut (Geb.ppOut Geb.defaultEvaluatorOptions morphism)

40
app/Commands/Dev/Geb/Repl/Format.hs Normal file
View File

@ -0,0 +1,40 @@
module Commands.Dev.Geb.Repl.Format
( module Commands.Dev.Geb.Repl.Format,
pretty,
)
where
import Juvix.Prelude
import Juvix.Prelude.Pretty
import Prettyprinter.Render.Terminal
data ReplStyle
= ReplPrompt
| ReplName
| ReplError
| ReplIntro
| ReplNormal
newtype ReplMessageDoc = ReplMessageDoc (Doc ReplStyle)
instance HasAnsiBackend ReplMessageDoc where
toAnsiStream (ReplMessageDoc o) = reAnnotateS stylize (layoutPretty defaultLayoutOptions o)
toAnsiDoc (ReplMessageDoc o) = reAnnotate stylize o
instance HasTextBackend ReplMessageDoc where
toTextDoc (ReplMessageDoc o) = unAnnotate o
toTextStream (ReplMessageDoc o) = unAnnotateS (layoutPretty defaultLayoutOptions o)
stylize :: ReplStyle -> AnsiStyle
stylize = \case
ReplPrompt -> color Blue
ReplName -> color Green
ReplError -> color Red
ReplNormal -> color Blue
ReplIntro -> bold
normal :: Text -> Doc ReplStyle
normal = annotate ReplNormal . pretty
ppOutput :: Doc ReplStyle -> AnsiText
ppOutput = AnsiText . ReplMessageDoc

25
app/Commands/Dev/Geb/Repl/Options.hs Normal file
View File

@ -0,0 +1,25 @@
module Commands.Dev.Geb.Repl.Options where
import CommonOptions
newtype GebReplOptions = GebReplOptions
{ _gebReplOptionsSilent :: Bool
}
deriving stock (Data)
makeLenses ''GebReplOptions
defaultGebReplOptions :: GebReplOptions
defaultGebReplOptions =
GebReplOptions
{ _gebReplOptionsSilent = False
}
parseGebReplOptions :: Parser GebReplOptions
parseGebReplOptions = do
_gebReplOptionsSilent <-
switch
( long "--silent"
<> help "Don't show the Juvix information in the REPL"
)
pure GebReplOptions {..}

11
app/Commands/Dev/Options.hs
View File

@ -2,6 +2,7 @@ module Commands.Dev.Options
( module Commands.Dev.Options,
module Commands.Dev.Asm.Options,
module Commands.Dev.Core.Options,
module Commands.Dev.Geb.Options,
module Commands.Dev.Internal.Options,
module Commands.Dev.Parse.Options,
module Commands.Dev.Highlight.Options,
@ -14,6 +15,7 @@ where
import Commands.Dev.Asm.Options hiding (Compile)
import Commands.Dev.Core.Options
import Commands.Dev.DisplayRoot.Options
import Commands.Dev.Geb.Options
import Commands.Dev.Highlight.Options
import Commands.Dev.Internal.Options
import Commands.Dev.MiniC.Options
@ -28,6 +30,7 @@ data DevCommand
| Highlight HighlightOptions
| Internal InternalCommand
| Core CoreCommand
| Geb GebCommand
| Asm AsmCommand
| Runtime RuntimeCommand
| MiniC MiniCOptions
@ -43,6 +46,7 @@ parseDevCommand =
[ commandHighlight,
commandInternal,
commandCore,
commandGeb,
commandAsm,
commandRuntime,
commandMiniC,
@ -74,6 +78,13 @@ commandInternal =
(Internal <$> parseInternalCommand)
(progDesc "Subcommands related to Internal")
commandGeb :: Mod CommandFields DevCommand
commandGeb =
command "geb" $
info
(Geb <$> parseGebCommand)
(progDesc "Subcommands related to JuvixGeb")
commandCore :: Mod CommandFields DevCommand
commandCore =
command "core" $

2
app/Commands/Extra/Compile/Options.hs
View File

@ -57,7 +57,7 @@ parseCompileOptions = do
)
_compileTerm <-
switch
( short 'T'
( short 'G'
<> long "only-term"
<> help "Produce term output only (for targets: geb)"
)

18
app/CommonOptions.hs
View File

@ -47,6 +47,18 @@ parseInputJuvixCoreFile = do
)
pure AppPath {_pathIsInput = True, ..}
parseInputJuvixGebFile :: Parser (AppPath File)
parseInputJuvixGebFile = do
_pathPath <-
argument
someFileOpt
( metavar "JUVIX_GEB_FILE"
<> help "Path to a .geb or custom .lisp file"
<> completer juvixGebCompleter
<> completer juvixGebLispCompleter
)
pure AppPath {_pathIsInput = True, ..}
parseInputJuvixAsmFile :: Parser (AppPath File)
parseInputJuvixAsmFile = do
_pathPath <-
@ -130,6 +142,12 @@ juvixCompleter = extCompleter "juvix"
juvixCoreCompleter :: Completer
juvixCoreCompleter = extCompleter "jvc"
juvixGebLispCompleter :: Completer
juvixGebLispCompleter = extCompleter "lisp"
juvixGebCompleter :: Completer
juvixGebCompleter = extCompleter "geb"
juvixAsmCompleter :: Completer
juvixAsmCompleter = extCompleter "jva"

2
juvix-stdlib

@ -1 +1 @@
Subproject commit 6f77cb9251e5f2eeccf650e77e572c1261c28f00
Subproject commit 3a7d37febd078380032d409531123c9436256b86

12
src/Juvix/Compiler/Backend/Geb.hs
View File

@ -1,4 +1,14 @@
module Juvix.Compiler.Backend.Geb (module Juvix.Compiler.Backend.Geb.Language, module Juvix.Compiler.Backend.Geb.Translation) where
module Juvix.Compiler.Backend.Geb
( module Juvix.Compiler.Backend.Geb.Language,
module Juvix.Compiler.Backend.Geb.Translation,
module Juvix.Compiler.Backend.Geb.Evaluator,
module Juvix.Compiler.Backend.Geb.Pretty,
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking,
)
where
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking
import Juvix.Compiler.Backend.Geb.Evaluator
import Juvix.Compiler.Backend.Geb.Language
import Juvix.Compiler.Backend.Geb.Pretty hiding (group, list)
import Juvix.Compiler.Backend.Geb.Translation

295
src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking.hs Normal file
View File

@ -0,0 +1,295 @@
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking
( module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking,
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Data.Types,
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error,
)
where
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Data.Types
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
import Juvix.Compiler.Backend.Geb.Data.Context as Context
import Juvix.Compiler.Backend.Geb.Extra
import Juvix.Compiler.Backend.Geb.Language
check' :: Member (Error CheckingError) r => TypedMorphism -> Sem r TypedMorphism
check' tyMorph = do
runReader defaultInferenceEnv $ check (tyMorph ^. typedMorphism) (tyMorph ^. typedMorphismObject)
return tyMorph
check :: Members '[Reader InferenceEnv, Error CheckingError] r => Morphism -> Object -> Sem r ()
check morph obj' = do
obj <-
runReader
(defaultInferenceEnv {_inferenceEnvTypeInfo = Just obj'})
(inferObject morph)
unless
(obj == obj')
( throw $
CheckingErrorTypeMismatch
TypeMismatch
{ _typeMismatchMorphism = morph,
_typeMismatchExpected = obj,
_typeMismatchActual = obj
}
)
checkSameType :: InferEffects r => [Morphism] -> Sem r ()
checkSameType = \case
[] -> return ()
(x : xs) -> do
obj <- inferObject x
checkListSameType xs obj
checkListSameType :: InferEffects r => [Morphism] -> Object -> Sem r ()
checkListSameType morphs obj = mapM_ (`check` obj) morphs
inferObject' :: Morphism -> Either CheckingError Object
inferObject' = run . runError . runReader defaultInferenceEnv . inferObject
type InferEffects r = Members '[Reader InferenceEnv, Error CheckingError] r
inferObject ::
Members '[Reader InferenceEnv, Error CheckingError] r =>
Morphism ->
Sem r Object
inferObject = \case
MorphismUnit -> return ObjectTerminal
MorphismInteger {} -> return ObjectInteger
MorphismAbsurd x -> inferObjectAbsurd x
MorphismApplication app -> inferObjectApplication app
MorphismPair pair -> inferObjectPair pair
MorphismCase c -> inferObjectCase c
MorphismFirst p -> inferObjectFirst p
MorphismSecond p -> inferObjectSecond p
MorphismLambda l -> inferObjectLambda l
MorphismBinop op -> inferObjectBinop op
MorphismVar v -> inferObjectVar v
MorphismLeft a -> inferObjectLeft a
MorphismRight b -> inferObjectRight b
-- FIXME: Depends on fixing anoma/geb#53
inferObjectAbsurd :: InferEffects r => Morphism -> Sem r Object
inferObjectAbsurd x =
throw
( CheckingErrorLackOfInformation
LackOfInformation
{ _lackOfInformationMorphism = Just x,
_lacOfInformationHelperObject = Nothing,
_lackOfInformationMessage = "Absurd"
}
)
inferObjectApplication :: InferEffects r => Application -> Sem r Object
inferObjectApplication app = do
let lType = app ^. applicationDomainType
rType = app ^. applicationCodomainType
homTy =
ObjectHom $
Hom {_homDomain = lType, _homCodomain = rType}
check (app ^. applicationLeft) homTy
check (app ^. applicationRight) lType
return rType
inferObjectLambda :: InferEffects r => Lambda -> Sem r Object
inferObjectLambda l = do
let aType = l ^. lambdaVarType
bType = l ^. lambdaBodyType
ctx <- asks (^. inferenceEnvContext)
local
( const
( InferenceEnv
{ _inferenceEnvContext = Context.cons aType ctx,
_inferenceEnvTypeInfo = Just aType
}
)
)
(check (l ^. lambdaBody) bType)
return $
ObjectHom $
Hom
{ _homDomain = aType,
_homCodomain = bType
}
inferObjectPair :: InferEffects r => Pair -> Sem r Object
inferObjectPair pair = do
let lType = pair ^. pairLeftType
rType = pair ^. pairRightType
check (pair ^. pairLeft) lType
check (pair ^. pairRight) rType
return $
ObjectProduct
Product
{ _productLeft = lType,
_productRight = rType
}
inferObjectCase :: InferEffects r => Case -> Sem r Object
inferObjectCase c = do
let aType = c ^. caseLeftType
bType = c ^. caseRightType
vType =
ObjectCoproduct $
Coproduct
{ _coproductLeft = aType,
_coproductRight = bType
}
cType = c ^. caseCodomainType
leftType =
ObjectHom $
Hom
{ _homDomain = aType,
_homCodomain = cType
}
rightType =
ObjectHom $
Hom
{ _homDomain = bType,
_homCodomain = cType
}
check (c ^. caseOn) vType
check (c ^. caseLeft) leftType
check (c ^. caseRight) rightType
return cType
inferObjectFirst :: InferEffects r => First -> Sem r Object
inferObjectFirst p = do
let leftType = p ^. firstLeftType
rightType = p ^. firstRightType
pairType =
ObjectProduct $
Product
{ _productLeft = leftType,
_productRight = rightType
}
check (p ^. firstValue) pairType
return leftType
inferObjectSecond :: InferEffects r => Second -> Sem r Object
inferObjectSecond p = do
let leftType = p ^. secondLeftType
rightType = p ^. secondRightType
pairType =
ObjectProduct $
Product
{ _productLeft = leftType,
_productRight = rightType
}
check (p ^. secondValue) pairType
return rightType
inferObjectVar :: InferEffects r => Var -> Sem r Object
inferObjectVar v = do
ctx <- asks (^. inferenceEnvContext)
return $ Context.lookup (v ^. varIndex) ctx
inferObjectBinop :: InferEffects r => Binop -> Sem r Object
inferObjectBinop opApp = do
let outTy = objectBinop opApp
leftArg = opApp ^. binopLeft
rightArg = opApp ^. binopRight
args = [leftArg, rightArg]
case opApp ^. binopOpcode of
OpAdd -> do
checkListSameType args ObjectInteger
return outTy
OpSub -> do
checkListSameType args ObjectInteger
return outTy
OpMul -> do
checkListSameType args ObjectInteger
return outTy
OpDiv -> do
checkListSameType args ObjectInteger
return outTy
OpMod -> do
checkListSameType args ObjectInteger
return outTy
OpLt -> do
checkListSameType args ObjectInteger
return outTy
OpEq -> do
checkSameType args
return outTy
-- FIXME: Once https://github.com/anoma/geb/issues/53 is fixed,
-- Update: inferObjectLeft and inferObjectRight to use the same code
inferObjectLeft :: InferEffects r => Morphism -> Sem r Object
inferObjectLeft a =
do
tyInfo <- asks (^. inferenceEnvTypeInfo)
case tyInfo of
Just cTy@(ObjectCoproduct coprod) -> do
let leftTy = coprod ^. coproductLeft
aTy <-
local
(over inferenceEnvTypeInfo (const (Just leftTy)))
(inferObject a)
unless
(aTy == leftTy)
( throw $
CheckingErrorTypeMismatch
TypeMismatch
{ _typeMismatchExpected = aTy,
_typeMismatchActual = leftTy,
_typeMismatchMorphism = MorphismLeft a
}
)
return cTy
Just ty ->
throw $
CheckingErrorWrongObject
WrongObject
{ _wrongObjectExpected = Nothing,
_wrongObjectActual = Just ty,
_wrongObjectMorphism = MorphismLeft a,
_wrongObjectMessage = "Expected a coproduct object for a left morphism."
}
Nothing ->
throw $
CheckingErrorLackOfInformation
LackOfInformation
{ _lackOfInformationMorphism = Just (MorphismLeft a),
_lacOfInformationHelperObject = tyInfo,
_lackOfInformationMessage = "on a left morphism"
}
inferObjectRight :: InferEffects r => Morphism -> Sem r Object
inferObjectRight bMorph = do
tyInfo <- asks (^. inferenceEnvTypeInfo)
case tyInfo of
Just cTy@(ObjectCoproduct coprod) -> do
let rightTy = coprod ^. coproductRight
bTy <-
local
(over inferenceEnvTypeInfo (const (Just rightTy)))
(inferObject bMorph)
unless
(bTy == rightTy)
( throw $
CheckingErrorTypeMismatch
TypeMismatch
{ _typeMismatchExpected = bTy,
_typeMismatchActual = rightTy,
_typeMismatchMorphism = MorphismRight bMorph
}
)
return cTy
Just ty ->
throw $
CheckingErrorWrongObject
WrongObject
{ _wrongObjectExpected = Nothing,
_wrongObjectActual = Just ty,
_wrongObjectMorphism = MorphismRight bMorph,
_wrongObjectMessage = "Expected a coproduct object for a right morphism."
}
Nothing ->
throw $
CheckingErrorLackOfInformation
LackOfInformation
{ _lackOfInformationMorphism = Just (MorphismRight bMorph),
_lacOfInformationHelperObject = tyInfo,
_lackOfInformationMessage = "on a right morphism"
}

23
src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Data/Types.hs Normal file
View File

@ -0,0 +1,23 @@
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Data.Types where
import Juvix.Compiler.Backend.Geb.Data.Context as Context
import Juvix.Compiler.Backend.Geb.Language
data InferenceEnv = InferenceEnv
{ -- | The context of the term being inferred.
_inferenceEnvContext :: Context Object,
-- | A Geb object to help the inference process.
-- This is needed because some morphisms lack of type information.
-- For example, the case of the left injection of a coproduct.
_inferenceEnvTypeInfo :: Maybe Object
}
deriving stock (Show, Generic)
makeLenses ''InferenceEnv
defaultInferenceEnv :: InferenceEnv
defaultInferenceEnv =
InferenceEnv
{ _inferenceEnvContext = mempty,
_inferenceEnvTypeInfo = Nothing
}

141
src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Error.hs Normal file
View File

@ -0,0 +1,141 @@
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error where
import Juvix.Compiler.Backend.Geb.Language
import Juvix.Compiler.Backend.Geb.Pretty
-- | Errors that can occur during type checking / inference
data CheckingError
= CheckingErrorTypeMismatch TypeMismatch
| CheckingErrorLackOfInformation LackOfInformation
| CheckingErrorWrongObject WrongObject
deriving stock (Show, Eq)
data TypeMismatch = TypeMismatch
{ _typeMismatchExpected :: Object,
_typeMismatchActual :: Object,
_typeMismatchMorphism :: Morphism
}
deriving stock (Show, Eq)
data LackOfInformation = LackOfInformation
{ _lackOfInformationMorphism :: Maybe Morphism,
_lacOfInformationHelperObject :: Maybe Object,
_lackOfInformationMessage :: String
}
deriving stock (Show, Eq)
data WrongObject = WrongObject
{ _wrongObjectExpected :: Maybe Object,
_wrongObjectActual :: Maybe Object,
_wrongObjectMorphism :: Morphism,
_wrongObjectMessage :: String
}
deriving stock (Show, Eq)
makeLenses ''TypeMismatch
makeLenses ''LackOfInformation
makeLenses ''WrongObject
instance ToGenericError TypeMismatch where
genericError e = ask >>= generr
where
generr opts =
return
GenericError
{ _genericErrorLoc = defaultLoc,
_genericErrorMessage = ppOutput msg,
_genericErrorIntervals = [defaultLoc]
}
where
opts' = fromGenericOptions opts
morph = e ^. typeMismatchMorphism
expected = e ^. typeMismatchExpected
actual = e ^. typeMismatchActual
msg =
"The"
<+> ppCode' opts' morph
<+> "has object:"
<> line
<> indent' (ppCode' opts' actual)
<> line
<> "but is expected to have as object:"
<> line
<> indent' (ppCode' opts' expected)
instance ToGenericError LackOfInformation where
genericError e = ask >>= generr
where
generr opts =
return
GenericError
{ _genericErrorLoc = defaultLoc,
_genericErrorMessage = ppOutput msg,
_genericErrorIntervals = [defaultLoc]
}
where
opts' = fromGenericOptions opts
morph = e ^. lackOfInformationMorphism
obj = e ^. lacOfInformationHelperObject
msg =
"Lack of information:"
<> line
<> indent' (pretty (e ^. lackOfInformationMessage))
<> case morph of
Nothing -> mempty
Just m ->
line
<> "The morphism:"
<> line
<> indent' (ppCode' opts' m)
<> case obj of
Nothing -> mempty
Just o ->
line
<> "The object:"
<> line
<> indent' (ppCode' opts' o)
instance ToGenericError WrongObject where
genericError e = ask >>= generr
where
generr opts =
return
GenericError
{ _genericErrorLoc = defaultLoc,
_genericErrorMessage = ppOutput msg,
_genericErrorIntervals = [defaultLoc]
}
where
opts' = fromGenericOptions opts
msg =
pretty (e ^. wrongObjectMessage)
<> line
<> "The morphism:"
<> line
<> indent' (ppCode' opts' (e ^. wrongObjectMorphism))
<> case e ^. wrongObjectExpected of
Nothing -> mempty
Just o ->
line
<> "The expected object:"
<> line
<> indent' (ppCode' opts' o)
<> case e ^. wrongObjectActual of
Nothing -> mempty
Just o ->
line
<> "The actual object:"
<> line
<> indent' (ppCode' opts' o)
instance ToGenericError CheckingError where
genericError = \case
CheckingErrorTypeMismatch e -> genericError e
CheckingErrorLackOfInformation e -> genericError e
CheckingErrorWrongObject e -> genericError e
mockFile :: Path Abs File
mockFile = $(mkAbsFile "/geb-checking-error")
defaultLoc :: Interval
defaultLoc = singletonInterval (mkInitialLoc mockFile)

9
src/Juvix/Compiler/Backend/Geb/Data/Context.hs Normal file
View File

@ -0,0 +1,9 @@
module Juvix.Compiler.Backend.Geb.Data.Context
( module Juvix.Compiler.Backend.Geb.Data.Context,
module Juvix.Compiler.Core.Data.BinderList,
)
where
import Juvix.Compiler.Core.Data.BinderList
type Context a = BinderList a

335
src/Juvix/Compiler/Backend/Geb/Evaluator.hs Normal file
View File

@ -0,0 +1,335 @@
module Juvix.Compiler.Backend.Geb.Evaluator
( module Juvix.Compiler.Backend.Geb.Evaluator,
module Juvix.Compiler.Backend.Geb.Evaluator.Options,
module Juvix.Compiler.Backend.Geb.Evaluator.Data,
)
where
import Control.Exception qualified as Exception
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking as Geb
import Juvix.Compiler.Backend.Geb.Data.Context as Context
import Juvix.Compiler.Backend.Geb.Evaluator.Data
import Juvix.Compiler.Backend.Geb.Evaluator.Error
import Juvix.Compiler.Backend.Geb.Evaluator.Options
import Juvix.Compiler.Backend.Geb.Language
import Juvix.Compiler.Backend.Geb.Translation.FromSource as Geb
data RunEvalArgs = RunEvalArgs
{ _runEvalArgsInputFile :: Path Abs File,
_runEvalArgsContent :: Text,
_runEvalArgsEvaluatorOptions :: EvaluatorOptions
}
makeLenses ''RunEvalArgs
runEval :: RunEvalArgs -> Either JuvixError RunEvalResult
runEval RunEvalArgs {..} =
case Geb.runParser _runEvalArgsInputFile _runEvalArgsContent of
Right (ExpressionMorphism m) -> do
let env :: Env =
Env
{ _envEvaluatorOptions = _runEvalArgsEvaluatorOptions,
_envContext = mempty
}
if _runEvalArgsEvaluatorOptions ^. evaluatorOptionsOutputMorphism
then RunEvalResultMorphism <$> evalAndOutputMorphism' env m
else RunEvalResultGebValue <$> eval' env m
Right _ -> Left (error @JuvixError objNoEvalMsg)
Left err -> Left (JuvixError err)
objNoEvalMsg :: Text
objNoEvalMsg = "Geb objects cannot be evaluated, only morphisms."
eval' :: Env -> Morphism -> Either JuvixError GebValue
eval' env m =
run . runError $
mapError (JuvixError @EvalError) $
runReader env $
eval m
evalAndOutputMorphism' :: Env -> Morphism -> Either JuvixError Morphism
evalAndOutputMorphism' env m = run . runError $ runReader env (evalAndOutputMorphism m)
evalAndOutputMorphism ::
Members '[Reader Env, Error JuvixError] r =>
Morphism ->
Sem r Morphism
evalAndOutputMorphism m = do
val :: GebValue <- mapError (JuvixError @EvalError) $ eval m
obj :: Object <-
runReader defaultInferenceEnv $
mapError (JuvixError @CheckingError) (inferObject m)
if
| requiresObjectInfo val -> quote (Just obj) val
| otherwise -> quote Nothing val
type EvalEffects r = Members '[Reader Env, Error EvalError] r
eval :: EvalEffects r => Morphism -> Sem r GebValue
eval morph =
case morph of
MorphismAbsurd x -> evalAbsurd x
MorphismApplication app -> evalApp app
MorphismBinop op -> evalBinop op
MorphismCase c -> evalCase c
MorphismFirst f -> evalFirst f
MorphismInteger i -> return $ GebValueMorphismInteger i
MorphismLambda l -> evalLambda l
MorphismLeft m -> GebValueMorphismLeft <$> eval m
MorphismPair p -> evalPair p
MorphismRight m -> GebValueMorphismRight <$> eval m
MorphismSecond s -> evalSecond s
MorphismUnit -> return GebValueMorphismUnit
MorphismVar x -> evalVar x
evalVar :: EvalEffects r => Var -> Sem r GebValue
evalVar var = do
ctx <- asks (^. envContext)
let val = Context.lookup (var ^. varIndex) ctx
return val
evalAbsurd :: EvalEffects r => Morphism -> Sem r GebValue
evalAbsurd morph =
throw
EvalError
{ _evalErrorMsg = "Absurd can not be evaluated.",
_evalErrorGebValue = Nothing,
_evalErrorGebExpression = Just morph
}
evalPair :: EvalEffects r => Pair -> Sem r GebValue
evalPair pair = do
left <- eval $ pair ^. pairLeft
right <- eval $ pair ^. pairRight
return $
GebValueMorphismPair $
ValueMorphismPair
{ _valueMorphismPairLeft = left,
_valueMorphismPairRight = right
}
evalFirst :: EvalEffects r => First -> Sem r GebValue
evalFirst f = do
res <- eval $ f ^. firstValue
case res of
GebValueMorphismPair pair -> return $ pair ^. valueMorphismPairLeft
_ ->
throw
EvalError
{ _evalErrorMsg = "First can only be applied to pairs.",
_evalErrorGebValue = Nothing,
_evalErrorGebExpression = Just (MorphismFirst f)
}
evalSecond :: EvalEffects r => Second -> Sem r GebValue
evalSecond s = do
res <- eval $ s ^. secondValue
case res of
GebValueMorphismPair pair -> return $ pair ^. valueMorphismPairRight
_ ->
throw
EvalError
{ _evalErrorMsg = "Second can only be applied to pairs.",
_evalErrorGebValue = Just res,
_evalErrorGebExpression = Just (MorphismSecond s)
}
evalApp :: EvalEffects r => Application -> Sem r GebValue
evalApp app = do
arg <- eval (app ^. applicationRight)
apply (app ^. applicationLeft) arg
apply ::
EvalEffects r =>
Morphism ->
GebValue ->
Sem r GebValue
apply fun' arg = do
fun <- eval fun'
case fun of
GebValueClosure cls ->
do
let clsEnv = cls ^. valueClosureEnv
bodyEnv = Context.cons arg clsEnv
local (over envContext (const bodyEnv)) $
eval (cls ^. valueClosureLambdaBody)
_ ->
throw $
EvalError
{ _evalErrorMsg = "Can only apply functions.",
_evalErrorGebValue = (Just fun),
_evalErrorGebExpression = Nothing
}
evalLambda :: EvalEffects r => Lambda -> Sem r GebValue
evalLambda lambda = do
ctx <- asks (^. envContext)
return $
GebValueClosure $
ValueClosure
{ _valueClosureLambdaBody = lambda ^. lambdaBody,
_valueClosureEnv = ctx
}
evalCase :: EvalEffects r => Case -> Sem r GebValue
evalCase c = do
vCaseOn <- eval $ c ^. caseOn
case vCaseOn of
GebValueMorphismLeft leftArg -> apply (c ^. caseLeft) leftArg
GebValueMorphismRight rightArg -> apply (c ^. caseRight) rightArg
_ ->
throw
EvalError
{ _evalErrorMsg = "Case can only be applied to terms of the coproduct object.",
_evalErrorGebValue = Just vCaseOn,
_evalErrorGebExpression = Just (MorphismCase c)
}
evalBinop ::
Members '[Reader Env, Error EvalError] r =>
Binop ->
Sem r GebValue
evalBinop binop = do
left <- eval $ binop ^. binopLeft
right <- eval $ binop ^. binopRight
let lfPair m1 m2 =
( GebValueMorphismPair
( ValueMorphismPair
{ _valueMorphismPairLeft = m1,
_valueMorphismPairRight = m2
}
)
)
case (left, right) of
(GebValueMorphismInteger l, GebValueMorphismInteger r) ->
case binop ^. binopOpcode of
OpAdd -> return $ GebValueMorphismInteger $ l + r
OpSub -> return $ GebValueMorphismInteger $ l - r
OpMul -> return $ GebValueMorphismInteger $ l * r
OpDiv -> return $ GebValueMorphismInteger $ l `div` r
OpMod -> return $ GebValueMorphismInteger $ l `mod` r
OpLt ->
if
| l < r -> return valueTrue
| otherwise -> return valueFalse
OpEq ->
if
| l < r -> return valueTrue
| otherwise -> return valueFalse
(m1, m2) -> case binop ^. binopOpcode of
OpEq ->
if
| sameKind m1 m2 ->
if
| m1 == m2 -> return valueTrue
| otherwise -> return valueFalse
| otherwise ->
throw
EvalError
{ _evalErrorMsg = "Equality can only be applied to values of the same kind.",
_evalErrorGebValue = Just (lfPair m1 m2),
_evalErrorGebExpression = (Just (MorphismBinop binop))
}
_ ->
throw
EvalError
{ _evalErrorMsg = "Cannot apply operation",
_evalErrorGebValue = Just (lfPair m1 m2),
_evalErrorGebExpression = Just (MorphismBinop binop)
}
sameKind :: GebValue -> GebValue -> Bool
sameKind l r = case (l, r) of
(GebValueMorphismInteger _, GebValueMorphismInteger _) -> True
(GebValueMorphismUnit, GebValueMorphismUnit) -> True
(GebValueMorphismLeft _, GebValueMorphismLeft _) -> True
(GebValueMorphismRight _, GebValueMorphismRight _) -> True
(GebValueMorphismPair _, GebValueMorphismPair _) -> True
(GebValueClosure _, GebValueClosure _) -> True
_ -> False
valueTrue :: GebValue
valueTrue = GebValueMorphismLeft GebValueMorphismUnit
valueFalse :: GebValue
valueFalse = GebValueMorphismRight GebValueMorphismUnit
requiresObjectInfo :: GebValue -> Bool
requiresObjectInfo = \case
GebValueMorphismUnit -> False
GebValueMorphismInteger {} -> False
GebValueClosure {} -> True
GebValueMorphismLeft {} -> True
GebValueMorphismRight {} -> True
GebValueMorphismPair {} -> True
quote :: Maybe Object -> GebValue -> Sem r Morphism
quote ty = \case
GebValueClosure cls -> quoteClosure ty cls
GebValueMorphismInteger i -> return $ MorphismInteger i
GebValueMorphismLeft m -> quoteValueMorphismLeft ty m
GebValueMorphismPair m -> quoteValueMorphismPair ty m
GebValueMorphismRight m -> quoteMorphismRight ty m
GebValueMorphismUnit -> return MorphismUnit
quoteClosure :: Maybe Object -> ValueClosure -> Sem r Morphism
quoteClosure ty cls =
quoteError
"Not implemented yet"
(Just (GebValueClosure cls))
ty
quoteValueMorphismPair :: Maybe Object -> ValueMorphismPair -> Sem r Morphism
quoteValueMorphismPair ty vpair = do
case ty of
Just (ObjectProduct prod) -> do
let (a, b) = (prod ^. productLeft, prod ^. productRight)
pLeft <- quote (Just a) (vpair ^. valueMorphismPairLeft)
pRight <- quote (Just b) (vpair ^. valueMorphismPairRight)
return $
MorphismPair
Pair
{ _pairLeft = pLeft,
_pairRight = pRight,
_pairLeftType = a,
_pairRightType = b
}
Just _ ->
quoteError
"type mismatch (pair). Expected a product"
(Just (GebValueMorphismPair vpair))
ty
Nothing ->
quoteError
"need object info"
(Just (GebValueMorphismPair vpair))
ty
quoteValueMorphismLeft :: Maybe Object -> GebValue -> Sem r Morphism
quoteValueMorphismLeft ty m = case ty of
Just (ObjectCoproduct _) -> MorphismLeft <$> quote ty m
Just _ ->
quoteError
"type mismatch (left). Expected a coproduct"
(Just (GebValueMorphismLeft m))
ty
Nothing -> quoteError "need object info" (Just (GebValueMorphismLeft m)) ty
quoteMorphismRight :: Maybe Object -> GebValue -> Sem r Morphism
quoteMorphismRight ty r = case ty of
Just (ObjectCoproduct _) -> MorphismRight <$> quote ty r
Just _ ->
quoteError
"type mismatch (right). Expected a coproduct"
(Just (GebValueMorphismRight r))
ty
Nothing -> quoteError "need object info" (Just (GebValueMorphismRight r)) ty
quoteError :: Text -> Maybe GebValue -> Maybe Object -> a
quoteError msg val gebExpr =
Exception.throw
QuoteError
{ _quoteErrorMsg = msg,
_quoteErrorGebValue = val,
_quoteErrorGebExpression = gebExpr
}

10
src/Juvix/Compiler/Backend/Geb/Evaluator/Data.hs Normal file
View File

@ -0,0 +1,10 @@
module Juvix.Compiler.Backend.Geb.Evaluator.Data
( module Juvix.Compiler.Backend.Geb.Evaluator.Data.Env,
module Juvix.Compiler.Backend.Geb.Evaluator.Data.Values,
module Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult,
)
where
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Env
import Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values

20
src/Juvix/Compiler/Backend/Geb/Evaluator/Data/Env.hs Normal file
View File

@ -0,0 +1,20 @@
module Juvix.Compiler.Backend.Geb.Evaluator.Data.Env where
import Juvix.Compiler.Backend.Geb.Data.Context as Context
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
import Juvix.Compiler.Backend.Geb.Evaluator.Options
import Juvix.Compiler.Backend.Geb.Language
data Env = Env
{ _envEvaluatorOptions :: EvaluatorOptions,
_envContext :: Context GebValue
}
makeLenses ''Env
defaultEvalEnv :: Env
defaultEvalEnv =
Env
{ _envEvaluatorOptions = defaultEvaluatorOptions,
_envContext = mempty
}

13
src/Juvix/Compiler/Backend/Geb/Evaluator/Data/RunEvalResult.hs Normal file
View File

@ -0,0 +1,13 @@
module Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult (module Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult) where
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
import Juvix.Compiler.Backend.Geb.Language
data RunEvalResult
= RunEvalResultGebValue GebValue
| RunEvalResultMorphism Morphism
deriving stock (Show, Eq)
instance HasAtomicity RunEvalResult where
atomicity (RunEvalResultGebValue v) = atomicity v
atomicity (RunEvalResultMorphism m) = atomicity m

53
src/Juvix/Compiler/Backend/Geb/Evaluator/Data/Values.hs Normal file
View File

@ -0,0 +1,53 @@
module Juvix.Compiler.Backend.Geb.Evaluator.Data.Values where
import Juvix.Compiler.Backend.Geb.Data.Context as Context
import Juvix.Compiler.Backend.Geb.Language hiding (show)
data GebValue
= GebValueMorphismUnit
| GebValueMorphismInteger Integer
| GebValueMorphismLeft GebValue
| GebValueMorphismRight GebValue
| GebValueMorphismPair ValueMorphismPair
| GebValueClosure ValueClosure
deriving stock (Show, Eq, Generic)
data ValueMorphismPair = ValueMorphismPair
{ _valueMorphismPairLeft :: GebValue,
_valueMorphismPairRight :: GebValue
}
deriving stock (Show, Eq, Generic)
data ValueMorphismCase = ValueMorphismCase
{ _valueMorphismCaseOn :: GebValue,
_valueMorphismCaseLeft :: GebValue,
_valueMorphismCaseRight :: GebValue
}
deriving stock (Show, Eq, Generic)
data ValueMorphismBinop = ValueMorphismBinop
{ _valueMorphismBinopOpcode :: Opcode,
_valueMorphismBinopLeft :: GebValue,
_valueMorphismBinopRight :: GebValue
}
deriving stock (Show, Eq, Generic)
data ValueClosure = ValueClosure
{ _valueClosureEnv :: Context GebValue,
_valueClosureLambdaBody :: Morphism
}
deriving stock (Show, Eq, Generic)
instance HasAtomicity GebValue where
atomicity = \case
GebValueMorphismInteger {} -> Atom
GebValueMorphismLeft {} -> Aggregate appFixity
GebValueMorphismPair {} -> Aggregate appFixity
GebValueMorphismRight {} -> Aggregate appFixity
GebValueMorphismUnit -> Atom
GebValueClosure {} -> Aggregate appFixity
makeLenses ''ValueMorphismPair
makeLenses ''ValueMorphismCase
makeLenses ''ValueMorphismBinop
makeLenses ''ValueClosure

86
src/Juvix/Compiler/Backend/Geb/Evaluator/Error.hs Normal file
View File

@ -0,0 +1,86 @@
module Juvix.Compiler.Backend.Geb.Evaluator.Error where
import GHC.Exception qualified as Exception
import GHC.Show qualified as S
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
import Juvix.Compiler.Backend.Geb.Language
import Juvix.Compiler.Backend.Geb.Pretty
data EvalError = EvalError
{ _evalErrorMsg :: !Text,
_evalErrorGebValue :: !(Maybe GebValue),
_evalErrorGebExpression :: !(Maybe Morphism)
}
data QuoteError = QuoteError
{ _quoteErrorMsg :: Text,
_quoteErrorGebValue :: Maybe GebValue,
_quoteErrorGebExpression :: Maybe Object
}
makeLenses ''EvalError
makeLenses ''QuoteError
-- TODO: Make this a proper error with a location
instance ToGenericError EvalError where
genericError e =
return
GenericError
{ _genericErrorLoc = defaultLoc,
_genericErrorMessage = AnsiText (pack $ S.show e),
_genericErrorIntervals = []
}
mockFile :: Path Abs File
mockFile = $(mkAbsFile "/geb-eval-error")
defaultLoc :: Interval
defaultLoc = singletonInterval (mkInitialLoc mockFile)
instance Show EvalError where
show :: EvalError -> String
show (EvalError {..}) =
"evaluation error: "
<> fromText _evalErrorMsg
<> "\n"
<> case _evalErrorGebValue of
Nothing -> ""
Just val -> "Value:\n" <> fromText (ppTrace val)
<> "\n"
<> case _evalErrorGebExpression of
Nothing -> ""
Just expr ->
"Morphism:\n"
<> fromText (ppTrace expr)
<> "\n"
evalError ::
Member (Error JuvixError) r =>
Text ->
Maybe GebValue ->
Maybe Morphism ->
Sem r a
evalError msg val m =
throw . JuvixError $
( EvalError
{ _evalErrorMsg = msg,
_evalErrorGebValue = val,
_evalErrorGebExpression = m
}
)
instance Exception.Exception QuoteError
instance Show QuoteError where
show :: QuoteError -> String
show QuoteError {..} =
"Quote error: "
<> fromText _quoteErrorMsg
<> case _quoteErrorGebValue of
Nothing -> ""
Just val -> ": " <> fromText (ppTrace val)
<> case _quoteErrorGebExpression of
Nothing -> ""
Just expr ->
"GebObject associated:\n"
<> fromText (ppTrace expr)

19
src/Juvix/Compiler/Backend/Geb/Evaluator/Options.hs Normal file
View File

@ -0,0 +1,19 @@
module Juvix.Compiler.Backend.Geb.Evaluator.Options where
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
import Juvix.Prelude
newtype EvaluatorOptions = EvaluatorOptions
{ _evaluatorOptionsOutputMorphism :: Bool
}
makeLenses ''EvaluatorOptions
instance CanonicalProjection EvaluatorOptions Geb.Options where
project _ = Geb.defaultOptions
defaultEvaluatorOptions :: EvaluatorOptions
defaultEvaluatorOptions =
EvaluatorOptions
{ _evaluatorOptionsOutputMorphism = False
}

26
src/Juvix/Compiler/Backend/Geb/Extra.hs
View File

@ -41,3 +41,29 @@ mkOr arg1 arg2 =
_lambdaBody = arg2
}
}
objectLeftCase :: Case -> Object
objectLeftCase Case {..} =
ObjectHom
Hom
{ _homDomain = _caseLeftType,
_homCodomain = _caseCodomainType
}
objectRightCase :: Case -> Object
objectRightCase Case {..} =
ObjectHom
Hom
{ _homDomain = _caseRightType,
_homCodomain = _caseCodomainType
}
objectBinop :: Binop -> Object
objectBinop op = case op ^. binopOpcode of
OpAdd -> ObjectInteger
OpSub -> ObjectInteger
OpMul -> ObjectInteger
OpDiv -> ObjectInteger
OpMod -> ObjectInteger
OpEq -> objectBool
OpLt -> objectBool

117
src/Juvix/Compiler/Backend/Geb/Keywords.hs Normal file
View File

@ -0,0 +1,117 @@
module Juvix.Compiler.Backend.Geb.Keywords
( module Juvix.Compiler.Backend.Geb.Keywords,
module Juvix.Data.Keyword,
module Juvix.Data.Keyword.All,
)
where
import Juvix.Data.Keyword
import Juvix.Data.Keyword.All
import Juvix.Extra.Strings qualified as Str
import Juvix.Prelude
allKeywordStrings :: HashSet Text
allKeywordStrings = keywordsStrings allKeywords
allKeywords :: [Keyword]
allKeywords =
[ kwGebMorphismAbsurd,
kwGebMorphismUnit,
kwGebMorphismLeft,
kwGebMorphismRight,
kwGebMorphismCase,
kwGebMorphismPair,
kwGebMorphismFirst,
kwGebMorphismSecond,
kwGebMorphismLambda,
kwGebMorphismApplication,
kwGebObjectInteger,
kwGebBinopAdd,
kwGebBinopSub,
kwGebBinopMul,
kwGebBinopDiv,
kwGebBinopMod,
kwGebBinopEq,
kwGebBinopLt,
kwGebObjectInitial,
kwGebObjectTerminal,
kwGebObjectProduct,
kwGebObjectCoproduct,
kwGebObjectHom,
kwGebVar
]
kwGebMorphismAbsurd :: Keyword
kwGebMorphismAbsurd = asciiKw Str.gebAbsurd
kwGebMorphismUnit :: Keyword
kwGebMorphismUnit = asciiKw Str.gebUnit
kwGebMorphismLeft :: Keyword
kwGebMorphismLeft = asciiKw Str.gebLeft
kwGebMorphismRight :: Keyword
kwGebMorphismRight = asciiKw Str.gebRight
kwGebMorphismCase :: Keyword
kwGebMorphismCase = asciiKw Str.gebCase
kwGebMorphismPair :: Keyword
kwGebMorphismPair = asciiKw Str.gebPair
kwGebMorphismFirst :: Keyword
kwGebMorphismFirst = asciiKw Str.gebFst
kwGebMorphismSecond :: Keyword
kwGebMorphismSecond = asciiKw Str.gebSnd
kwGebMorphismLambda :: Keyword
kwGebMorphismLambda = asciiKw Str.gebLamb
kwGebMorphismApplication :: Keyword
kwGebMorphismApplication = asciiKw Str.gebApp
kwGebBinopAdd :: Keyword
kwGebBinopAdd = asciiKw Str.gebAdd
kwGebBinopSub :: Keyword
kwGebBinopSub = asciiKw Str.gebSub
kwGebBinopMul :: Keyword
kwGebBinopMul = asciiKw Str.gebMul
kwGebBinopDiv :: Keyword
kwGebBinopDiv = asciiKw Str.gebDiv
kwGebBinopMod :: Keyword
kwGebBinopMod = asciiKw Str.gebMod
kwGebBinopEq :: Keyword
kwGebBinopEq = asciiKw Str.gebEq
kwGebBinopLt :: Keyword
kwGebBinopLt = asciiKw Str.gebLt
kwGebObjectInteger :: Keyword
kwGebObjectInteger = asciiKw Str.gebInteger
kwGebVar :: Keyword
kwGebVar = asciiKw Str.gebVar
kwGebObjectInitial :: Keyword
kwGebObjectInitial = asciiKw Str.gebInitial
kwGebObjectTerminal :: Keyword
kwGebObjectTerminal = asciiKw Str.gebTerminal
kwGebObjectProduct :: Keyword
kwGebObjectProduct = asciiKw Str.gebProd
kwGebObjectCoproduct :: Keyword
kwGebObjectCoproduct = asciiKw Str.gebCoprod
kwGebObjectHom :: Keyword
kwGebObjectHom = asciiKw Str.gebHom
kwTyped :: Keyword
kwTyped = asciiKw Str.gebTyped

48
src/Juvix/Compiler/Backend/Geb/Language.hs
View File

@ -13,8 +13,9 @@ import Juvix.Prelude hiding (First, Product)
-}
-- | Represents GEB's `case-on`. `_caseOn` is the value matched on of type
-- `Dom`, `_caseLeft` has type `_caseLeftType -> _caseCodomainType` and
-- `_caseRight` has type `_caseRightType -> _caseCodomainType`.
-- `_caseLeftType + _caseRightType`, `_caseLeft` has type `_caseLeftType ->
-- _caseCodomainType` and `_caseRight` has type `_caseRightType ->
-- _caseCodomainType`.
data Case = Case
{ _caseLeftType :: Object,
_caseRightType :: Object,
@ -23,6 +24,7 @@ data Case = Case
_caseLeft :: Morphism,
_caseRight :: Morphism
}
deriving stock (Show, Eq, Generic)
data Pair = Pair
{ _pairLeftType :: Object,
@ -30,24 +32,28 @@ data Pair = Pair
_pairLeft :: Morphism,
_pairRight :: Morphism
}
deriving stock (Show, Eq, Generic)
data First = First
{ _firstLeftType :: Object,
_firstRightType :: Object,
_firstValue :: Morphism
}
deriving stock (Show, Eq, Generic)
data Second = Second
{ _secondLeftType :: Object,
_secondRightType :: Object,
_secondValue :: Morphism
}
deriving stock (Show, Eq, Generic)
data Lambda = Lambda
{ _lambdaVarType :: Object,
_lambdaBodyType :: Object,
_lambdaBody :: Morphism
}
deriving stock (Show, Eq, Generic)
data Application = Application
{ _applicationDomainType :: Object,
@ -55,8 +61,10 @@ data Application = Application
_applicationLeft :: Morphism,
_applicationRight :: Morphism
}
deriving stock (Show, Eq, Generic)
newtype Var = Var {_varIndex :: Int}
deriving stock (Show, Eq, Generic)
data Opcode
= OpAdd
@ -66,12 +74,14 @@ data Opcode
| OpMod
| OpEq
| OpLt
deriving stock (Show, Eq, Generic)
data Binop = Binop
{ _binopOpcode :: Opcode,
_binopLeft :: Morphism,
_binopRight :: Morphism
}
deriving stock (Show, Eq, Generic)
-- | Corresponds to the GEB type for terms (morphisms of the category): `stlc`
-- (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp).
@ -89,22 +99,26 @@ data Morphism
| MorphismVar Var
| MorphismInteger Integer
| MorphismBinop Binop
deriving stock (Show, Eq, Generic)
data Product = Product
{ _productLeft :: Object,
_productRight :: Object
}
deriving stock (Show, Eq, Generic)
data Coproduct = Coproduct
{ _coproductLeft :: Object,
_coproductRight :: Object
}
deriving stock (Show, Eq, Generic)
-- | Function type
data Hom = Hom
{ _homDomain :: Object,
_homCodomain :: Object
}
deriving stock (Show, Eq, Generic)
-- | Corresponds to the GEB type for types (objects of the category): `substobj`
-- (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp).
@ -118,6 +132,27 @@ data Object
| -- | function type
ObjectHom Hom
| ObjectInteger
deriving stock (Show, Eq, Generic)
data Expression
= ExpressionMorphism Morphism
| ExpressionObject Object
deriving stock (Show, Eq, Generic)
data TypedMorphism = TypedMorphism
{ _typedMorphism :: Morphism,
_typedMorphismObject :: Object
}
deriving stock (Show, Eq, Generic)
instance HasAtomicity Opcode where
atomicity OpAdd = Atom
atomicity OpSub = Atom
atomicity OpMul = Atom
atomicity OpDiv = Atom
atomicity OpMod = Atom
atomicity OpEq = Atom
atomicity OpLt = Atom
instance HasAtomicity Morphism where
atomicity = \case
@ -144,6 +179,14 @@ instance HasAtomicity Object where
ObjectHom {} -> Aggregate appFixity
ObjectInteger -> Atom
instance HasAtomicity Expression where
atomicity = \case
ExpressionMorphism m -> atomicity m
ExpressionObject o -> atomicity o
instance HasAtomicity TypedMorphism where
atomicity _ = Aggregate appFixity
makeLenses ''Case
makeLenses ''Pair
makeLenses ''First
@ -157,3 +200,4 @@ makeLenses ''Product
makeLenses ''Coproduct
makeLenses ''Hom
makeLenses ''Object
makeLenses ''TypedMorphism

184
src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs
View File

@ -5,10 +5,12 @@ module Juvix.Compiler.Backend.Geb.Pretty.Base
)
where
import Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
import Juvix.Compiler.Backend.Geb.Language
import Juvix.Compiler.Backend.Geb.Pretty.Keywords
import Juvix.Compiler.Backend.Geb.Pretty.Options
import Juvix.Data.CodeAnn
import Juvix.Extra.Strings qualified as Str
doc :: (HasAtomicity c, PrettyCode c) => Options -> c -> Doc Ann
doc opts x =
@ -39,12 +41,22 @@ docLisp opts packageName entryName morph obj =
( "defparameter"
<+> pretty entryName
<> line
<> indent' (parens ("typed" <+> doc opts morph <+> doc opts obj))
<> indent'
( parens
( "typed"
<> line
<> indent'
(vsep [doc opts morph, doc opts obj])
)
)
)
class PrettyCode c where
ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
ppCode' :: (PrettyCode c) => Options -> c -> Doc Ann
ppCode' opts = run . runReader opts . ppCode
instance PrettyCode Case where
ppCode Case {..} = do
lty <- ppArg _caseLeftType
@ -53,7 +65,8 @@ instance PrettyCode Case where
val <- ppArg _caseOn
left <- ppArg _caseLeft
right <- ppArg _caseRight
return $ kwCaseOn <+> lty <+> rty <+> cod <+> val <+> left <+> right
return $
kwCaseOn <> line <> indent 2 (vsep [lty, rty, cod, val, left, right])
instance PrettyCode Pair where
ppCode Pair {..} = do
@ -61,28 +74,28 @@ instance PrettyCode Pair where
rty <- ppArg _pairRightType
left <- ppArg _pairLeft
right <- ppArg _pairRight
return $ kwPair <+> lty <+> rty <+> left <+> right
return $ kwPair <> line <> indent' (vsep [lty, rty, left, right])
instance PrettyCode First where
ppCode First {..} = do
lty <- ppArg _firstLeftType
rty <- ppArg _firstRightType
val <- ppArg _firstValue
return $ kwFst <+> lty <+> rty <+> val
return $ kwFst <> line <> indent' (vsep [lty, rty, val])
instance PrettyCode Second where
ppCode Second {..} = do
lty <- ppArg _secondLeftType
rty <- ppArg _secondRightType
val <- ppArg _secondValue
return $ kwSnd <+> lty <+> rty <+> val
return $ kwSnd <> line <> indent' (vsep [lty, rty, val])
instance PrettyCode Lambda where
ppCode Lambda {..} = do
vty <- ppArg _lambdaVarType
bty <- ppArg _lambdaBodyType
body <- ppArg _lambdaBody
return $ kwLamb <+> vty <+> bty <+> body
return $ kwLamb <> line <> indent' (vsep [vty, bty, body])
instance PrettyCode Application where
ppCode Application {..} = do
@ -90,7 +103,7 @@ instance PrettyCode Application where
cod <- ppArg _applicationCodomainType
left <- ppArg _applicationLeft
right <- ppArg _applicationRight
return $ kwApp <+> dom <+> cod <+> left <+> right
return $ kwApp <> line <> indent' (vsep [dom, cod, left, right])
instance PrettyCode Var where
ppCode Var {..} = return $ annotate AnnLiteralInteger (pretty _varIndex)
@ -110,7 +123,7 @@ instance PrettyCode Binop where
op <- ppCode _binopOpcode
left <- ppArg _binopLeft
right <- ppArg _binopRight
return $ op <+> left <+> right
return $ op <> line <> indent' (vsep [left, right])
instance PrettyCode Morphism where
ppCode = \case
@ -121,10 +134,10 @@ instance PrettyCode Morphism where
return kwUnit
MorphismLeft val -> do
v <- ppArg val
return $ kwLeft <+> v
return $ kwLeft <> line <> indent' v
MorphismRight val -> do
v <- ppArg val
return $ kwRight <+> v
return $ kwRight <> line <> indent' v
MorphismCase x -> ppCode x
MorphismPair x -> ppCode x
MorphismFirst x -> ppCode x
@ -141,28 +154,86 @@ instance PrettyCode Product where
ppCode Product {..} = do
left <- ppArg _productLeft
right <- ppArg _productRight
return $ kwProd <+> left <+> right
return $ kwProd <> line <> indent' (vsep [left, right])
instance PrettyCode Coproduct where
ppCode Coproduct {..} = do
left <- ppArg _coproductLeft
right <- ppArg _coproductRight
return $ kwCoprod <+> left <+> right
return $ kwCoprod <> line <> indent' (vsep [left, right])
instance PrettyCode Hom where
ppCode Hom {..} = do
dom <- ppArg _homDomain
cod <- ppArg _homCodomain
return $ kwHom <+> dom <+> cod
return $ kwHom <> line <> indent' (vsep [dom, cod])
instance PrettyCode Object where
ppCode =
\case
ObjectInitial -> return kwInitial
ObjectTerminal -> return kwTerminal
ObjectProduct x -> ppCode x
ObjectCoproduct x -> ppCode x
ObjectHom x -> ppCode x
ObjectInteger -> return kwInteger
instance PrettyCode Expression where
ppCode = \case
ObjectInitial -> return kwInitial
ObjectTerminal -> return kwTerminal
ObjectProduct x -> ppCode x
ObjectCoproduct x -> ppCode x
ObjectHom x -> ppCode x
ObjectInteger -> return kwInteger
ExpressionMorphism x -> ppCode x
ExpressionObject x -> ppCode x
instance PrettyCode TypedMorphism where
ppCode TypedMorphism {..} = do
m <- ppArg _typedMorphism
o <- ppArg _typedMorphismObject
return $ kwTyped <> line <> indent' (vsep [m, o])
instance PrettyCode ValueClosure where
ppCode cls = do
lamb <- ppArg (cls ^. valueClosureLambdaBody)
env <- mapM ppArg (toList (cls ^. valueClosureEnv))
return $
kwClosure
<> line
<> indent'
( vsep
[ parens
( kwClosureEnv
<> line
<> indent'
( if null env
then kwNil
else (vsep env)
)
),
lamb
]
)
instance PrettyCode ValueMorphismPair where
ppCode ValueMorphismPair {..} = do
left <- ppArg _valueMorphismPairLeft
right <- ppArg _valueMorphismPairRight
return $ kwPair <> line <> indent' (vsep [left, right])
instance PrettyCode GebValue where
ppCode = \case
GebValueMorphismUnit -> return kwUnit
GebValueMorphismInteger n -> return $ annotate AnnLiteralInteger (pretty n)
GebValueMorphismLeft val -> do
v <- ppArg val
return $ kwLeft <> line <> indent' v
GebValueMorphismRight val -> do
v <- ppArg val
return $ kwRight <> line <> indent' v
GebValueMorphismPair x -> ppCode x
GebValueClosure x -> ppCode x
instance PrettyCode RunEvalResult where
ppCode = \case
RunEvalResultMorphism m -> ppCode m
RunEvalResultGebValue v -> ppCode v
--------------------------------------------------------------------------------
-- helper functions
@ -197,76 +268,3 @@ ppLRExpression ::
ppLRExpression associates fixlr e =
parensIf (atomParens associates (atomicity e) fixlr)
<$> ppCode e
--------------------------------------------------------------------------------
-- keywords
--------------------------------------------------------------------------------
kwAbsurd :: Doc Ann
kwAbsurd = keyword Str.gebAbsurd
kwUnit :: Doc Ann
kwUnit = keyword Str.gebUnit
kwLeft :: Doc Ann
kwLeft = keyword Str.gebLeft
kwRight :: Doc Ann
kwRight = keyword Str.gebRight
kwFst :: Doc Ann
kwFst = keyword Str.gebFst
kwSnd :: Doc Ann
kwSnd = keyword Str.gebSnd
kwPair :: Doc Ann
kwPair = keyword Str.gebPair
kwLamb :: Doc Ann
kwLamb = keyword Str.gebLamb
kwApp :: Doc Ann
kwApp = keyword Str.gebApp
kwVar :: Doc Ann
kwVar = keyword Str.gebVar
kwAdd :: Doc Ann
kwAdd = keyword Str.gebAdd
kwSub :: Doc Ann
kwSub = keyword Str.gebSub
kwMul :: Doc Ann
kwMul = keyword Str.gebMul
kwDiv :: Doc Ann
kwDiv = keyword Str.gebDiv
kwMod :: Doc Ann
kwMod = keyword Str.gebMod
kwEq :: Doc Ann
kwEq = keyword Str.gebEq
kwLt :: Doc Ann
kwLt = keyword Str.gebLt
kwInitial :: Doc Ann
kwInitial = keyword Str.gebInitial
kwTerminal :: Doc Ann
kwTerminal = keyword Str.gebTerminal
kwProd :: Doc Ann
kwProd = keyword Str.gebProd
kwCoprod :: Doc Ann
kwCoprod = keyword Str.gebCoprod
kwHom :: Doc Ann
kwHom = keyword Str.gebHom
kwInteger :: Doc Ann
kwInteger = keyword Str.gebInteger

113
src/Juvix/Compiler/Backend/Geb/Pretty/Keywords.hs Normal file
View File

@ -0,0 +1,113 @@
module Juvix.Compiler.Backend.Geb.Pretty.Keywords where
import Juvix.Compiler.Backend.Geb.Language
import Juvix.Data.CodeAnn
import Juvix.Extra.Strings qualified as Str
keywords :: [Doc Ann]
keywords =
[ kwInitial,
kwTerminal,
kwProd,
kwCoprod,
kwHom,
kwInteger,
kwEq,
kwLt,
kwAbsurd,
kwUnit,
kwLeft,
kwRight,
kwFst,
kwSnd,
kwPair,
kwLamb,
kwApp,
kwVar,
kwAdd,
kwSub,
kwMul,
kwDiv,
kwMod
]
kwAbsurd :: Doc Ann
kwAbsurd = keyword Str.gebAbsurd
kwUnit :: Doc Ann
kwUnit = keyword Str.gebUnit
kwLeft :: Doc Ann
kwLeft = keyword Str.gebLeft
kwRight :: Doc Ann
kwRight = keyword Str.gebRight
kwFst :: Doc Ann
kwFst = keyword Str.gebFst
kwSnd :: Doc Ann
kwSnd = keyword Str.gebSnd
kwPair :: Doc Ann
kwPair = keyword Str.gebPair
kwLamb :: Doc Ann
kwLamb = keyword Str.gebLamb
kwClosure :: Doc Ann
kwClosure = keyword Str.gebValueClosure
kwClosureEnv :: Doc Ann
kwClosureEnv = keyword Str.gebValueClosureEnv
kwNil :: Doc Ann
kwNil = keyword Str.lispNil
kwApp :: Doc Ann
kwApp = keyword Str.gebApp
kwVar :: Doc Ann
kwVar = keyword Str.gebVar
kwAdd :: Doc Ann
kwAdd = keyword Str.gebAdd
kwSub :: Doc Ann
kwSub = keyword Str.gebSub
kwMul :: Doc Ann
kwMul = keyword Str.gebMul
kwDiv :: Doc Ann
kwDiv = keyword Str.gebDiv
kwMod :: Doc Ann
kwMod = keyword Str.gebMod
kwEq :: Doc Ann
kwEq = keyword Str.gebEq
kwLt :: Doc Ann
kwLt = keyword Str.gebLt
kwInitial :: Doc Ann
kwInitial = keyword Str.gebInitial
kwTerminal :: Doc Ann
kwTerminal = keyword Str.gebTerminal
kwProd :: Doc Ann
kwProd = keyword Str.gebProd
kwCoprod :: Doc Ann
kwCoprod = keyword Str.gebCoprod
kwHom :: Doc Ann
kwHom = keyword Str.gebHom
kwInteger :: Doc Ann
kwInteger = keyword Str.gebInteger
kwTyped :: Doc Ann
kwTyped = keyword Str.gebTyped

2
src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs
View File

@ -12,7 +12,7 @@ defaultOptions :: Options
defaultOptions = Options
traceOptions :: Options
traceOptions = Options
traceOptions = defaultOptions
fromGenericOptions :: GenericOptions -> Options
fromGenericOptions _ = defaultOptions

4
src/Juvix/Compiler/Backend/Geb/Translation.hs
View File

@ -1,12 +1,14 @@
module Juvix.Compiler.Backend.Geb.Translation
( module Juvix.Compiler.Backend.Geb.Translation,
module Juvix.Compiler.Backend.Geb.Translation.FromCore,
module Juvix.Compiler.Backend.Geb.Translation.FromSource,
)
where
import Juvix.Compiler.Backend.Geb.Language
import Juvix.Compiler.Backend.Geb.Pretty
import Juvix.Compiler.Backend.Geb.Translation.FromCore
import Juvix.Compiler.Backend.Geb.Translation.FromCore hiding (Env)
import Juvix.Compiler.Backend.Geb.Translation.FromSource
newtype Result = Result
{ _resultCode :: Text

324
src/Juvix/Compiler/Backend/Geb/Translation/FromSource.hs Normal file
View File

@ -0,0 +1,324 @@
module Juvix.Compiler.Backend.Geb.Translation.FromSource
( module Juvix.Compiler.Backend.Geb.Translation.FromSource,
module Juvix.Parser.Error,
)
where
import Juvix.Compiler.Backend.Geb.Keywords
import Juvix.Compiler.Backend.Geb.Language (typedMorphism)
import Juvix.Compiler.Backend.Geb.Language qualified as Geb
import Juvix.Compiler.Backend.Geb.Translation.FromSource.Lexer
import Juvix.Parser.Error
import Juvix.Prelude
import Text.Megaparsec qualified as P
import Text.Megaparsec.Char.Lexer qualified as P
data LispDefParameter = LispDefParameter
{ _lispDefParameterName :: Text,
_lispDefParameterMorphism :: Geb.TypedMorphism
}
makeLenses ''LispDefParameter
fromSource ::
Member (Error JuvixError) r =>
Path Abs File ->
Text ->
Sem r Geb.Expression
fromSource fileName input =
case runParser fileName input of
Left err -> throw (JuvixError err)
Right gebTerm -> pure gebTerm
runParser ::
Path Abs File ->
Text ->
Either MegaparsecError Geb.Expression
runParser fileName input =
do
let parser :: ParsecS r Geb.Expression
parser
| isJuvixGebFile fileName = parseGeb
| isLispFile fileName = parseGebLisp
| otherwise = error "unknown file extension"
case run $
P.runParserT parser (fromAbsFile fileName) input of
Left err -> Left (MegaparsecError err)
Right gebTerm -> Right gebTerm
runParser' ::
Path Abs File ->
Text ->
Either MegaparsecError Geb.TypedMorphism
runParser' fileName input =
do
let parser :: ParsecS r Geb.TypedMorphism
parser
| isJuvixGebFile fileName = parseTypedMorphism
| isLispFile fileName = parseGebLisp'
| otherwise = error "unknown file extension"
case run $
P.runParserT parser (fromAbsFile fileName) input of
Left err -> Left (MegaparsecError err)
Right gebTerm -> Right gebTerm
parseLispSymbol :: ParsecS r Text
parseLispSymbol =
P.label "<lisp symbol>" $ do
lexeme $
P.takeWhile1P Nothing validChars
where
validChars :: Char -> Bool
validChars = (`notElem` ("() " :: String))
parseLispList :: ParsecS r ()
parseLispList =
P.label "<lisp list>" $
lexeme . parens $
P.skipSome parseLispExpr
parseLispExpr :: ParsecS r ()
parseLispExpr =
void parseLispSymbol
<|> parseLispList
parseTypedMorphism :: ParsecS r Geb.TypedMorphism
parseTypedMorphism =
parens $ do
symbol "typed"
m <- morphism
o <- object
return $
Geb.TypedMorphism
{ _typedMorphism = m,
_typedMorphismObject = o
}
parseDefParameter :: ParsecS r LispDefParameter
parseDefParameter =
P.label "<defparameter>" $ do
parens $ do
symbol "defparameter"
n <- parseLispSymbol
m <- parseTypedMorphism
return
LispDefParameter
{ _lispDefParameterName = n,
_lispDefParameterMorphism = m
}
parseGebLisp :: ParsecS r Geb.Expression
parseGebLisp = do
tyMorph <- parseGebLisp'
return $
Geb.ExpressionMorphism $
tyMorph
^. typedMorphism
parseGebLisp' :: ParsecS r Geb.TypedMorphism
parseGebLisp' = do
space
P.label "<defpackage>" parseLispExpr
P.label "<in-package>" parseLispExpr
entry <- parseDefParameter
P.eof
return $
entry
^. lispDefParameterMorphism
parseGebExpression :: ParsecS r Geb.Expression
parseGebExpression =
P.try (Geb.ExpressionObject <$> object)
<|> Geb.ExpressionMorphism <$> morphism
parseGeb :: ParsecS r Geb.Expression
parseGeb =
P.label "<geb program>" $
space *> parseGebExpression <* P.eof
morphism :: ParsecS r Geb.Morphism
morphism =
P.label "<geb morphism>" $ do
morphismUnit
<|> Geb.MorphismInteger <$> morphismInteger
<|> parens
( Geb.MorphismAbsurd <$> morphismAbsurd
<|> Geb.MorphismLeft <$> morphismLeft
<|> Geb.MorphismRight <$> morphismRight
<|> Geb.MorphismCase <$> morphismCase
<|> Geb.MorphismPair <$> morphismPair
<|> Geb.MorphismFirst <$> morphismFirst
<|> Geb.MorphismSecond <$> morphismSecond
<|> Geb.MorphismLambda <$> morphismLambda
<|> Geb.MorphismApplication <$> morphismApplication
<|> Geb.MorphismVar <$> morphismVar
<|> Geb.MorphismBinop <$> morphismBinop
)
parseNatural :: ParsecS r Integer
parseNatural = lexeme P.decimal
morphismInteger :: ParsecS r Integer
morphismInteger = parseNatural
opcode :: ParsecS r Geb.Opcode
opcode =
P.label "<geb Opcode>" $
Geb.OpAdd <$ kw kwGebBinopAdd
<|> Geb.OpSub <$ kw kwGebBinopSub
<|> Geb.OpMul <$ kw kwGebBinopMul
<|> Geb.OpDiv <$ kw kwGebBinopDiv
<|> Geb.OpMod <$ kw kwGebBinopMod
<|> Geb.OpEq <$ kw kwGebBinopEq
<|> Geb.OpLt <$ kw kwGebBinopLt
morphismBinop :: ParsecS r Geb.Binop
morphismBinop = do
P.label "<geb MorphismBinop>" $ do
op <- opcode
m1 <- morphism
m2 <- morphism
return
Geb.Binop
{ _binopOpcode = op,
_binopLeft = m1,
_binopRight = m2
}
object :: ParsecS r Geb.Object
object =
P.label "<geb Object>" $ do
objectInitial
<|> objectTerminal
<|> Geb.ObjectInteger <$ (kw kwGebObjectInteger)
<|> parens
( Geb.ObjectProduct <$> objectProduct
<|> Geb.ObjectCoproduct <$> objectCoproduct
<|> Geb.ObjectHom <$> objectHom
)
morphismUnit :: ParsecS r Geb.Morphism
morphismUnit = do
P.label "<geb MorphismUnit>" $ do
kw kwGebMorphismUnit
return Geb.MorphismUnit
morphismAbsurd :: ParsecS r Geb.Morphism
morphismAbsurd =
P.label "<geb MorphismAbsurd>" $ do
kw kwGebMorphismAbsurd
morphism
morphismLeft :: ParsecS r Geb.Morphism
morphismLeft = do
P.label "<geb MorphismLeft>" $ do
kw kwGebMorphismLeft
morphism
morphismRight :: ParsecS r Geb.Morphism
morphismRight = do
P.label "<geb MorphismRight>" $ do
kw kwGebMorphismRight
morphism
morphismCase :: ParsecS r Geb.Case
morphismCase = do
P.label "<geb MorphismCase>" $ do
kw kwGebMorphismCase
_caseLeftType <- object
_caseRightType <- object
_caseCodomainType <- object
_caseOn <- morphism
_caseLeft <- morphism
_caseRight <- morphism
return Geb.Case {..}
morphismPair :: ParsecS r Geb.Pair
morphismPair = do
P.label "<geb MorphismPair>" $ do
kw kwGebMorphismPair
_pairLeftType <- object
_pairRightType <- object
_pairLeft <- morphism
_pairRight <- morphism
return Geb.Pair {..}
morphismFirst :: ParsecS r Geb.First
morphismFirst = do
P.label "<geb MorphismFirst>" $ do
kw kwGebMorphismFirst
_firstLeftType <- object
_firstRightType <- object
_firstValue <- morphism
return Geb.First {..}
morphismSecond :: ParsecS r Geb.Second
morphismSecond = do
P.label "<geb MorphismSecond>" $ do
kw kwGebMorphismSecond
_secondLeftType <- object
_secondRightType <- object
_secondValue <- morphism
return Geb.Second {..}
morphismLambda :: ParsecS r Geb.Lambda
morphismLambda = do
P.label "<geb MorphismLambda>" $ do
kw kwGebMorphismLambda
_lambdaVarType <- object
_lambdaBodyType <- object
_lambdaBody <- morphism
return Geb.Lambda {..}
morphismApplication :: ParsecS r Geb.Application
morphismApplication = do
P.label "<geb MorphismApplication>" $ do
kw kwGebMorphismApplication
_applicationDomainType <- object
_applicationCodomainType <- object
_applicationLeft <- morphism
_applicationRight <- morphism
return Geb.Application {..}
morphismVar :: ParsecS r Geb.Var
morphismVar = do
P.label "<geb MorphismVar>" $ do
kw kwGebVar <* space
_varIndex <- fromIntegral <$> parseNatural
return Geb.Var {..}
objectInitial :: ParsecS r Geb.Object
objectInitial = do
P.label "objectInitial>" $ do
kw kwGebObjectInitial
return Geb.ObjectInitial
objectTerminal :: ParsecS r Geb.Object
objectTerminal = do
P.label "objectTermina>" $ do
kw kwGebObjectTerminal
return Geb.ObjectTerminal
objectProduct :: ParsecS r Geb.Product
objectProduct = do
P.label "objectProduct>" $ do
kw kwGebObjectProduct
_productLeft <- object
_productRight <- object
return Geb.Product {..}
objectCoproduct :: ParsecS r Geb.Coproduct
objectCoproduct = do
P.label "objectCoproduct>" $ do
kw kwGebObjectCoproduct
_coproductLeft <- object
_coproductRight <- object
return Geb.Coproduct {..}
objectHom :: ParsecS r Geb.Hom
objectHom = do
P.label "objectHom >" $ do
kw kwGebObjectHom
_homDomain <- object
_homCodomain <- object
return Geb.Hom {..}

74
src/Juvix/Compiler/Backend/Geb/Translation/FromSource/Lexer.hs Normal file
View File

@ -0,0 +1,74 @@
module Juvix.Compiler.Backend.Geb.Translation.FromSource.Lexer
( module Juvix.Compiler.Backend.Geb.Translation.FromSource.Lexer,
module Juvix.Parser.Lexer,
module Juvix.Compiler.Backend.Geb.Keywords,
)
where
import Juvix.Compiler.Backend.Geb.Keywords
import Juvix.Extra.Strings qualified as Str
import Juvix.Parser.Lexer
import Juvix.Prelude
import Text.Megaparsec as P hiding (sepBy1, sepEndBy1, some)
import Text.Megaparsec.Char.Lexer qualified as L
space :: forall r. ParsecS r ()
space = L.space space1 lineCmnt blockCmnt
where
lineCmnt :: ParsecS r () = L.skipLineComment ";"
blockCmnt :: ParsecS r () = L.skipBlockComment "#|" "|#"
lexeme :: ParsecS r a -> ParsecS r a
lexeme = L.lexeme space
lexemeInterval :: ParsecS r a -> ParsecS r (a, Interval)
lexemeInterval = lexeme . interval
symbol :: Text -> ParsecS r ()
symbol = void . L.symbol space
kw :: Keyword -> ParsecS r ()
kw = void . lexeme . kw'
decimal :: (Num n) => ParsecS r (n, Interval)
decimal = lexemeInterval L.decimal
integer :: ParsecS r (Integer, Interval)
integer = integer' decimal
number :: Int -> Int -> ParsecS r (Int, Interval)
number = number' integer
string :: ParsecS r (Text, Interval)
string = lexemeInterval string'
identifier :: ParsecS r Text
identifier = lexeme bareIdentifier
identifierL :: ParsecS r (Text, Interval)
identifierL = lexemeInterval bareIdentifier
-- | Same as @identifier@ but does not consume space after it.
bareIdentifier :: ParsecS r Text
bareIdentifier = rawIdentifier allKeywordStrings
symbolAt :: ParsecS r ()
symbolAt = symbol Str.at_
lbrace :: ParsecS r ()
lbrace = symbol "{"
rbrace :: ParsecS r ()
rbrace = symbol "}"
lparen :: ParsecS r ()
lparen = symbol "("
rparen :: ParsecS r ()
rparen = symbol ")"
parens :: ParsecS r a -> ParsecS r a
parens = between lparen rparen
braces :: ParsecS r a -> ParsecS r a
braces = between (symbol "{") (symbol "}")

5
src/Juvix/Compiler/Core/Data/BinderList.hs
View File

@ -1,5 +1,6 @@
module Juvix.Compiler.Core.Data.BinderList where
import GHC.Show qualified as S
import Juvix.Compiler.Core.Language hiding (cons, drop, lookup, uncons)
import Juvix.Prelude qualified as Prelude
@ -8,6 +9,7 @@ data BinderList a = BinderList
{ _blLength :: Int,
_blMap :: [a]
}
deriving stock (Eq, Generic)
makeLenses ''BinderList
@ -45,6 +47,9 @@ instance Foldable BinderList where
toList :: BinderList a -> [a]
toList = (^. blMap)
instance Show a => Show (BinderList a) where
show = S.show . toList
-- | same as `lookupsSortedRev` but the result is in the same order as the input list.
lookupsSorted :: BinderList a -> [Var' i] -> [(Var' i, a)]
lookupsSorted bl = reverse . lookupsSortedRev bl

14
src/Juvix/Extra/Strings.hs
View File

@ -575,6 +575,15 @@ gebSnd = "snd"
gebLamb :: IsString s => s
gebLamb = "lamb"
gebValueClosure :: IsString s => s
gebValueClosure = "cls"
gebValueClosureEnv :: IsString s => s
gebValueClosureEnv = "env"
lispNil :: IsString s => s
lispNil = "nil"
gebApp :: IsString s => s
gebApp = "app"
@ -615,11 +624,14 @@ gebCoprod :: IsString s => s
gebCoprod = "coprod"
gebHom :: IsString s => s
gebHom = "hom"
gebHom = "!->"
gebInteger :: IsString s => s
gebInteger = "int"
gebTyped :: IsString s => s
gebTyped = "typed"
juvixFunctionT :: IsString s => s
juvixFunctionT = "juvix_function_t"

6
src/Juvix/Prelude/Path.hs
View File

@ -57,6 +57,12 @@ destructAbsFile x = (root, dirs, filename x)
isJuvixFile :: Path b File -> Bool
isJuvixFile = (== Just ".juvix") . fileExtension
isJuvixGebFile :: Path b File -> Bool
isJuvixGebFile = (== Just ".geb") . fileExtension
isLispFile :: Path b File -> Bool
isLispFile = (== Just ".lisp") . fileExtension
isHiddenDirectory :: Path b Dir -> Bool
isHiddenDirectory p
| toFilePath p == relRootFP = False

11
test/BackendGeb.hs Normal file
View File

@ -0,0 +1,11 @@
module BackendGeb where
import BackendGeb.Eval qualified as Eval
import Base
allTests :: TestTree
allTests =
testGroup
"BackendGeb tests"
[ Eval.allTests
]

10
test/BackendGeb/Eval.hs Normal file
View File

@ -0,0 +1,10 @@
module BackendGeb.Eval where
import BackendGeb.Eval.Positive qualified as EvalP
import Base
allTests :: TestTree
allTests =
testGroup
"JuvixGeb eval tests"
[EvalP.allTests]

59
test/BackendGeb/Eval/Base.hs Normal file
View File

@ -0,0 +1,59 @@
module BackendGeb.Eval.Base where
import Base
import Data.Text.IO qualified as TIO
import Juvix.Compiler.Backend.Geb qualified as Geb
import Juvix.Prelude.Pretty
gebEvalAssertion ::
Path Abs File ->
Path Abs File ->
(String -> IO ()) ->
Assertion
gebEvalAssertion mainFile expectedFile step = do
step "Parse"
input <- readFile (toFilePath mainFile)
case Geb.runParser mainFile input of
Left err -> assertFailure (show (pretty err))
Right (Geb.ExpressionObject _) -> do
step "No evalution for objects"
assertFailure (unpack Geb.objNoEvalMsg)
Right (Geb.ExpressionMorphism gebMorphism) -> do
let env :: Geb.Env =
Geb.Env
{ _envEvaluatorOptions = Geb.defaultEvaluatorOptions,
_envContext = mempty
}
withTempDir' $
\dirPath -> do
let outputFile = dirPath <//> $(mkRelFile "out.out")
step "Evaluate"
hout <- openFile (toFilePath outputFile) WriteMode
let result = Geb.eval' env gebMorphism
case result of
Left err -> do
hClose hout
assertFailure (show (pretty (fromJuvixError @GenericError err)))
Right value -> do
hPutStrLn hout (Geb.ppPrint value)
hClose hout
actualOutput <- TIO.readFile (toFilePath outputFile)
expected <- TIO.readFile (toFilePath expectedFile)
step "Compare expected and actual program output"
assertEqDiffText
("Check: EVAL output = " <> toFilePath expectedFile)
actualOutput
expected
gebEvalErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
gebEvalErrorAssertion mainFile step = do
step "Parse"
input <- readFile (toFilePath mainFile)
case Geb.runParser mainFile input of
Left _ -> assertBool "" True
Right (Geb.ExpressionObject _) -> assertFailure "no error"
Right (Geb.ExpressionMorphism gebMorphism) -> do
step "Evaluate"
case Geb.eval' Geb.defaultEvalEnv gebMorphism of
Left _ -> assertBool "" True
Right _ -> assertFailure "no error"

75
test/BackendGeb/Eval/Positive.hs Normal file
View File

@ -0,0 +1,75 @@
module BackendGeb.Eval.Positive where
import BackendGeb.Eval.Base
import Base
data PosTest = PosTest
{ _name :: String,
_relDir :: Path Rel Dir,
_file :: Path Rel File,
_expectedFile :: Path Rel File
}
root :: Path Abs Dir
root = relToProject $(mkRelDir "tests/Geb/positive")
testDescr :: PosTest -> TestDescr
testDescr PosTest {..} =
let tRoot = root <//> _relDir
file' = tRoot <//> _file
expected' = tRoot <//> _expectedFile
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion =
Steps $
gebEvalAssertion file' expected'
}
filterOutTests :: [String] -> [PosTest] -> [PosTest]
filterOutTests out = filter (\PosTest {..} -> _name `notElem` out)
allTests :: TestTree
allTests =
testGroup
"JuvixGeb positive tests"
(map (mkTest . testDescr) tests)
tests :: [PosTest]
tests =
[ PosTest
"App case on"
$(mkRelDir ".")
$(mkRelFile "app-case-on.geb")
$(mkRelFile "Eval/out/app-case-on.out"),
PosTest
"App fst pair"
$(mkRelDir ".")
$(mkRelFile "app-fst-pair.geb")
$(mkRelFile "Eval/out/app-fst-pair.out"),
PosTest
"lambda"
$(mkRelDir ".")
$(mkRelFile "lamb.geb")
$(mkRelFile "Eval/out/lamb.out"),
PosTest
"App lambda"
$(mkRelDir ".")
$(mkRelFile "app-lambda.geb")
$(mkRelFile "Eval/out/app-lambda.out"),
PosTest
"Double application"
$(mkRelDir ".")
$(mkRelFile "app-app-lambda.geb")
$(mkRelFile "Eval/out/app-app-lambda.out"),
PosTest
"Basic app"
$(mkRelDir ".")
$(mkRelFile "basic-app.geb")
$(mkRelFile "Eval/out/basic-app.out"),
PosTest
"case on"
$(mkRelDir ".")
$(mkRelFile "case-on.geb")
$(mkRelFile "Eval/out/case-on.out")
]

2
test/Main.hs
View File

@ -3,6 +3,7 @@ module Main (main) where
import Arity qualified
import Asm qualified
import BackendC qualified
import BackendGeb qualified
import Base
import Compilation qualified
import Core qualified
@ -20,6 +21,7 @@ slowTests =
testGroup
"Juvix slow tests"
[ BackendC.allTests,
BackendGeb.allTests,
Runtime.allTests,
Asm.allTests,
Core.allTests,

1
tests/Geb/positive/Core/out/test001.out
View File

@ -1 +0,0 @@
(right unit)

1
tests/Geb/positive/Core/out/test002.out
View File

@ -1 +0,0 @@
(left unit)

1
tests/Geb/positive/Core/out/test003.out
View File

@ -1 +0,0 @@
(left unit)

1
tests/Geb/positive/Core/out/test004.out
View File

@ -1 +0,0 @@
(left unit)

4
tests/Geb/positive/Eval/out/app-app-lambda.out Normal file
View File

@ -0,0 +1,4 @@
(cls
(env
nil)
(index 0))

2
tests/Geb/positive/Eval/out/app-case-on.out Normal file
View File

@ -0,0 +1,2 @@
(right
1)

1
tests/Geb/positive/Eval/out/app-fst-pair.out Normal file
View File

@ -0,0 +1 @@
10

7
tests/Geb/positive/Eval/out/app-lambda.out Normal file
View File

@ -0,0 +1,7 @@
(cls
(env
(cls
(env
nil)
(index 0)))
(index 1))

1
tests/Geb/positive/Eval/out/basic-app.out Normal file
View File

@ -0,0 +1 @@
3000

2
tests/Geb/positive/Eval/out/case-on.out Normal file
View File

@ -0,0 +1,2 @@
(left
unit)

7
tests/Geb/positive/Eval/out/lamb.out Normal file
View File

@ -0,0 +1,7 @@
(cls
(env
nil)
(lamb
so1
so1
(index 1)))

5
tests/Geb/positive/Eval/out/left-unit.out Normal file
View File

@ -0,0 +1,5 @@
(cls
(env
nil)
(left
unit))

2
tests/Geb/positive/Eval/out/test001.out Normal file
View File

@ -0,0 +1,2 @@
(right
unit)

2
tests/Geb/positive/Eval/out/test002.out Normal file
View File

@ -0,0 +1,2 @@
(left
unit)

2
tests/Geb/positive/Eval/out/test003.out Normal file
View File

@ -0,0 +1,2 @@
(left
unit)

2
tests/Geb/positive/Eval/out/test004.out Normal file
View File

@ -0,0 +1,2 @@
(left
unit)

0
tests/Geb/positive/Core/out/test005.out → tests/Geb/positive/Eval/out/test005.out
View File

0
tests/Geb/positive/Core/out/test006.out → tests/Geb/positive/Eval/out/test006.out
View File

1
tests/Geb/positive/Infer/out/basic-app.out Normal file
View File

@ -0,0 +1 @@
int

5
tests/Geb/positive/Infer/out/left-unit.out Normal file
View File

@ -0,0 +1,5 @@
(!->
so1
(coprod
so1
so1))

3
tests/Geb/positive/Infer/out/test001.out Normal file
View File

@ -0,0 +1,3 @@
(coprod
so1
so1)

3
tests/Geb/positive/Infer/out/test002.out Normal file
View File

@ -0,0 +1,3 @@
(coprod
so1
so1)

3
tests/Geb/positive/Infer/out/test003.out Normal file
View File

@ -0,0 +1,3 @@
(coprod
so1
so1)

3
tests/Geb/positive/Infer/out/test004.out Normal file
View File

@ -0,0 +1,3 @@
(coprod
so1
so1)

1
tests/Geb/positive/Infer/out/test005.out Normal file
View File

@ -0,0 +1 @@
int

1
tests/Geb/positive/Infer/out/test006.out Normal file
View File

@ -0,0 +1 @@
int

39
tests/Geb/positive/app-app-lambda.geb Normal file
View File

@ -0,0 +1,39 @@
;; THE following example does not typecheck on purpose
;; It's meant to be used only for the evaluator.
;; ↓ app2 fun arg, where
;; fun := cls (λ . (index 1)) with env := GlobalEnv
;; arg := cls 0 with env := GlobalEnv
;; → (eval (λ . (index 1)) with env := arg : GlobalEnv
;; → cls (arg : GlobalEnv) (index 1).
;; ↓ app1 (cls (arg : GlobalEnv) (index 1)) unit
;; → eval (index 1) with (env = unit : arg : GlobalEnv)
;; → env !! 1 → arg ≡ "cls 0 with env = GlobalEnv"
;; ≡ λ . 0
;; Nicely,
;; (((λ x λ y . x) ⬝ (λ z . z)) unit
;; ( (λ y . (λ z . z)) unit.
;; (λ z . z) ≡ λ . 0
;; ((λ λ . 1) (λ.0)) ⬝ unit
;; (( λ . (λ.0))) ⬝ unit
;; (( (λ.0)))
(app int int ;; app1
(app ;; app2
int
int
;; ↓ cls [] (lamb (index 1))
(lamb
int
int
(lamb
int
int
(index 1)))
;; ↓ cls [] (index 0)
(lamb
int
int
(index 0)))
unit)

22
tests/Geb/positive/app-case-on.geb Normal file
View File

@ -0,0 +1,22 @@
(app
(coprod int int)
(coprod so1 int)
(lamb
int int
(case-on
int
int
int
(index 0)
(lamb
int
int
(right 1))
(lamb
int
int
(left 2))
)
)
(left
3))

15
tests/Geb/positive/app-fst-pair.geb Normal file
View File

@ -0,0 +1,15 @@
(app
int
int
(lamb
int
int
(fst
int
int
(index 0)))
(pair
int
int
10
20))

25
tests/Geb/positive/app-lambda.geb Normal file
View File

@ -0,0 +1,25 @@
;; ↓ app fun arg where
;; fun := cls (λ . (index 1)) with env := []
;; arg := cls (index 0) with env := []
;; → (eval (λ . (index 1)) with env := (arg : [])
;; → cls (arg : []) (index 1).
;; λ.(λ.0)
(app
int
int
;; fun: ↓ cls [] (lamb (index 1))
;; λλ.1
(lamb
int
int
(lamb
int
int
(index 1)))
;; ↓ arg: cls [] (index 0)
;; λ.0
(lamb
int
int
(index 0)))

8
tests/Geb/positive/basic-app.geb Normal file
View File

@ -0,0 +1,8 @@
(app
int
int
(lamb
int
int
(index 0))
(add 1000 2000))

22
tests/Geb/positive/case-on.geb Normal file
View File

@ -0,0 +1,22 @@
(case-on
so1 ;left
so1 ;right
(coprod ; codomain
so1
so1)
(right 1) ; left + right
(lamb ; left -> codomain
so1
(coprod
so1
so1)
(right
unit))
(lamb ; right -> codomain
so1
(coprod
so1
so1)
(left
unit)))

9
tests/Geb/positive/lamb.geb Normal file
View File

@ -0,0 +1,9 @@
(lamb
so1
(!->
so1
so1)
(lamb
so1
so1
(index 1)))

6
tests/Geb/positive/left-unit.geb Normal file
View File

@ -0,0 +1,6 @@
(lamb
so1
(coprod
so1
so1)
(left unit))

153
tests/smoke/Commands/dev/geb.smoke.yaml Normal file
View File

@ -0,0 +1,153 @@
working-directory: ./../../../../tests
tests:
- name: geb-open
command:
- juvix
- --no-colors
- dev
- geb
- repl
stdout:
contains: "Welcome to the Juvix Geb REPL!"
exit-status: 0
- name: geb-quit
command:
- juvix
- --no-colors
- dev
- geb
- repl
stdout:
contains: "geb>"
stdin: ":quit"
exit-status: 0
- name: geb-infer-type-unit
command:
- juvix
- --no-colors
- dev
- geb
- repl
stdin: ":type unit"
stdout:
contains: "so1"
exit-status: 0
- name: geb-infer-type-object
command:
- juvix
- --no-colors
- dev
- geb
- repl
stdin: ":type so1"
stdout:
contains: "Inference only works on Geb morphisms"
exit-status: 0
- name: geb-infer-type-integer
command:
- juvix
- --no-colors
- dev
- geb
- repl
stdin: ":t (mul 2 3)"
stdout:
contains: "int"
exit-status: 0
# - name: geb-check-int
# command:
# - juvix
# - --no-colors
# - dev
# - geb
# - repl
# stdin: ":check (typed (add 1 2) so1)"
# stderr:
# contains: "so1 is not a valid object for (add 1 2)"
# exit-status: 1
- name: geb-eval-and-operations
command:
- juvix
- --no-format
- dev
- geb
- repl
stdin: "(add 2 (mul 3 4))"
stdout:
contains: |
14
exit-status: 0
- name: geb-eval-with-spaces
command:
- juvix
- dev
- geb
- repl
stdin: " unit"
stdout:
contains:
"unit"
exit-status:
- name: geb-load-and-eval-gebext
command:
shell:
- bash
script: |
cd ./Geb/positive/ && juvix dev geb repl
stdin: ":load basic-app.geb"
stdout:
contains: |
3000
exit-status: 0
- name: geb-root
command:
- juvix
- --no-colors
- dev
- geb
- repl
stdin: ":root"
stdout:
matches: |
Welcome .*
Juvix .*
Type .*
geb> .*/tests/
exit-status: 0
- name: geb-read-file
command:
- juvix
- dev
- geb
- read
args:
- Geb/positive/app-lambda.geb
stdout: |
(app
int
int
(lamb
int
int
(lamb
int
int
(index 1)))
(lamb
int
int
(index 0)))
exit-status: 0

4
tests/smoke/Commands/dev/root.smoke.yaml
View File

@ -7,8 +7,6 @@ tests:
- dev
- root
stdout:
matches: |
.*?/(juvix|main)/tests/
# contains "main" for the CI
matches: .*/tests/
exit-status: 0