diff --git a/Makefile b/Makefile index 87c246701..5941ed2cd 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/app/Commands/Dev.hs b/app/Commands/Dev.hs index 81cb6b954..7d9e1128f 100644 --- a/app/Commands/Dev.hs +++ b/app/Commands/Dev.hs @@ -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 diff --git a/app/Commands/Dev/Core/Read.hs b/app/Commands/Dev/Core/Read.hs index 36299094f..c677298d5 100644 --- a/app/Commands/Dev/Core/Read.hs +++ b/app/Commands/Dev/Core/Read.hs @@ -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 diff --git a/app/Commands/Dev/Geb.hs b/app/Commands/Dev/Geb.hs new file mode 100644 index 000000000..4fcd06ffe --- /dev/null +++ b/app/Commands/Dev/Geb.hs @@ -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 diff --git a/app/Commands/Dev/Geb/Check.hs b/app/Commands/Dev/Geb/Check.hs new file mode 100644 index 000000000..f28e53cbb --- /dev/null +++ b/app/Commands/Dev/Geb/Check.hs @@ -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) diff --git a/app/Commands/Dev/Geb/Eval.hs b/app/Commands/Dev/Geb/Eval.hs new file mode 100644 index 000000000..f809e4032 --- /dev/null +++ b/app/Commands/Dev/Geb/Eval.hs @@ -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 diff --git a/app/Commands/Dev/Geb/Eval/Options.hs b/app/Commands/Dev/Geb/Eval/Options.hs new file mode 100644 index 000000000..6a6b03689 --- /dev/null +++ b/app/Commands/Dev/Geb/Eval/Options.hs @@ -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" + ) diff --git a/app/Commands/Dev/Geb/Infer.hs b/app/Commands/Dev/Geb/Infer.hs new file mode 100644 index 000000000..af4c66d5f --- /dev/null +++ b/app/Commands/Dev/Geb/Infer.hs @@ -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) diff --git a/app/Commands/Dev/Geb/Infer/Options.hs b/app/Commands/Dev/Geb/Infer/Options.hs new file mode 100644 index 000000000..06c2831ed --- /dev/null +++ b/app/Commands/Dev/Geb/Infer/Options.hs @@ -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 {..} diff --git a/app/Commands/Dev/Geb/Options.hs b/app/Commands/Dev/Geb/Options.hs new file mode 100644 index 000000000..91831e668 --- /dev/null +++ b/app/Commands/Dev/Geb/Options.hs @@ -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") diff --git a/app/Commands/Dev/Geb/Read.hs b/app/Commands/Dev/Geb/Read.hs new file mode 100644 index 000000000..f36b98c05 --- /dev/null +++ b/app/Commands/Dev/Geb/Read.hs @@ -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 "") diff --git a/app/Commands/Dev/Geb/Read/Options.hs b/app/Commands/Dev/Geb/Read/Options.hs new file mode 100644 index 000000000..63877cfaa --- /dev/null +++ b/app/Commands/Dev/Geb/Read/Options.hs @@ -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 {..} diff --git a/app/Commands/Dev/Geb/Repl.hs b/app/Commands/Dev/Geb/Repl.hs new file mode 100644 index 000000000..20754a55b --- /dev/null +++ b/app/Commands/Dev/Geb/Repl.hs @@ -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) diff --git a/app/Commands/Dev/Geb/Repl/Format.hs b/app/Commands/Dev/Geb/Repl/Format.hs new file mode 100644 index 000000000..49ec38638 --- /dev/null +++ b/app/Commands/Dev/Geb/Repl/Format.hs @@ -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 diff --git a/app/Commands/Dev/Geb/Repl/Options.hs b/app/Commands/Dev/Geb/Repl/Options.hs new file mode 100644 index 000000000..db1d2f3b9 --- /dev/null +++ b/app/Commands/Dev/Geb/Repl/Options.hs @@ -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 {..} diff --git a/app/Commands/Dev/Options.hs b/app/Commands/Dev/Options.hs index 6f6e801ab..4aca25ff9 100644 --- a/app/Commands/Dev/Options.hs +++ b/app/Commands/Dev/Options.hs @@ -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" $ diff --git a/app/Commands/Extra/Compile/Options.hs b/app/Commands/Extra/Compile/Options.hs index d8caf54c4..f8e580bda 100644 --- a/app/Commands/Extra/Compile/Options.hs +++ b/app/Commands/Extra/Compile/Options.hs @@ -57,7 +57,7 @@ parseCompileOptions = do ) _compileTerm <- switch - ( short 'T' + ( short 'G' <> long "only-term" <> help "Produce term output only (for targets: geb)" ) diff --git a/app/CommonOptions.hs b/app/CommonOptions.hs index 19b293d50..dafa6cee3 100644 --- a/app/CommonOptions.hs +++ b/app/CommonOptions.hs @@ -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" diff --git a/juvix-stdlib b/juvix-stdlib index 6f77cb925..3a7d37feb 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 6f77cb9251e5f2eeccf650e77e572c1261c28f00 +Subproject commit 3a7d37febd078380032d409531123c9436256b86 diff --git a/src/Juvix/Compiler/Backend/Geb.hs b/src/Juvix/Compiler/Backend/Geb.hs index 321aed451..f1ba8205c 100644 --- a/src/Juvix/Compiler/Backend/Geb.hs +++ b/src/Juvix/Compiler/Backend/Geb.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking.hs b/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking.hs new file mode 100644 index 000000000..37564e67c --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking.hs @@ -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" + } diff --git a/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Data/Types.hs b/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Data/Types.hs new file mode 100644 index 000000000..db4ab3b9c --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Data/Types.hs @@ -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 + } diff --git a/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Error.hs new file mode 100644 index 000000000..8d2590bd1 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Error.hs @@ -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) diff --git a/src/Juvix/Compiler/Backend/Geb/Data/Context.hs b/src/Juvix/Compiler/Backend/Geb/Data/Context.hs new file mode 100644 index 000000000..e81f20827 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Data/Context.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Evaluator.hs b/src/Juvix/Compiler/Backend/Geb/Evaluator.hs new file mode 100644 index 000000000..ff99220d0 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Evaluator.hs @@ -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 + } diff --git a/src/Juvix/Compiler/Backend/Geb/Evaluator/Data.hs b/src/Juvix/Compiler/Backend/Geb/Evaluator/Data.hs new file mode 100644 index 000000000..ca8a90b09 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Evaluator/Data.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/Env.hs b/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/Env.hs new file mode 100644 index 000000000..a8e8ab9d5 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/Env.hs @@ -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 + } diff --git a/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/RunEvalResult.hs b/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/RunEvalResult.hs new file mode 100644 index 000000000..393094dfd --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/RunEvalResult.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/Values.hs b/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/Values.hs new file mode 100644 index 000000000..7449f896b --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Evaluator/Data/Values.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Evaluator/Error.hs b/src/Juvix/Compiler/Backend/Geb/Evaluator/Error.hs new file mode 100644 index 000000000..9c6da4e17 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Evaluator/Error.hs @@ -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) diff --git a/src/Juvix/Compiler/Backend/Geb/Evaluator/Options.hs b/src/Juvix/Compiler/Backend/Geb/Evaluator/Options.hs new file mode 100644 index 000000000..4c4b05bca --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Evaluator/Options.hs @@ -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 + } diff --git a/src/Juvix/Compiler/Backend/Geb/Extra.hs b/src/Juvix/Compiler/Backend/Geb/Extra.hs index f16c3ec56..6243240a1 100644 --- a/src/Juvix/Compiler/Backend/Geb/Extra.hs +++ b/src/Juvix/Compiler/Backend/Geb/Extra.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Keywords.hs b/src/Juvix/Compiler/Backend/Geb/Keywords.hs new file mode 100644 index 000000000..b3f7ae161 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Keywords.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Language.hs b/src/Juvix/Compiler/Backend/Geb/Language.hs index d395cdcd3..590f4b479 100644 --- a/src/Juvix/Compiler/Backend/Geb/Language.hs +++ b/src/Juvix/Compiler/Backend/Geb/Language.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs index 1a6ff6295..182f2680c 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Keywords.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Keywords.hs new file mode 100644 index 000000000..b9cbcfcf3 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Keywords.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs index b6123a31a..e8464008c 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs @@ -12,7 +12,7 @@ defaultOptions :: Options defaultOptions = Options traceOptions :: Options -traceOptions = Options +traceOptions = defaultOptions fromGenericOptions :: GenericOptions -> Options fromGenericOptions _ = defaultOptions diff --git a/src/Juvix/Compiler/Backend/Geb/Translation.hs b/src/Juvix/Compiler/Backend/Geb/Translation.hs index 6c7473feb..92c45ae03 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation.hs @@ -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 diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromSource.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromSource.hs new file mode 100644 index 000000000..94f21f6f6 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromSource.hs @@ -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 "" $ do + lexeme $ + P.takeWhile1P Nothing validChars + where + validChars :: Char -> Bool + validChars = (`notElem` ("() " :: String)) + +parseLispList :: ParsecS r () +parseLispList = + P.label "" $ + 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 "" $ 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 "" parseLispExpr + P.label "" 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 "" $ + space *> parseGebExpression <* P.eof + +morphism :: ParsecS r Geb.Morphism +morphism = + P.label "" $ 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.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 "" $ do + op <- opcode + m1 <- morphism + m2 <- morphism + return + Geb.Binop + { _binopOpcode = op, + _binopLeft = m1, + _binopRight = m2 + } + +object :: ParsecS r Geb.Object +object = + P.label "" $ 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 "" $ do + kw kwGebMorphismUnit + return Geb.MorphismUnit + +morphismAbsurd :: ParsecS r Geb.Morphism +morphismAbsurd = + P.label "" $ do + kw kwGebMorphismAbsurd + morphism + +morphismLeft :: ParsecS r Geb.Morphism +morphismLeft = do + P.label "" $ do + kw kwGebMorphismLeft + morphism + +morphismRight :: ParsecS r Geb.Morphism +morphismRight = do + P.label "" $ do + kw kwGebMorphismRight + morphism + +morphismCase :: ParsecS r Geb.Case +morphismCase = do + P.label "" $ 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 "" $ do + kw kwGebMorphismPair + _pairLeftType <- object + _pairRightType <- object + _pairLeft <- morphism + _pairRight <- morphism + return Geb.Pair {..} + +morphismFirst :: ParsecS r Geb.First +morphismFirst = do + P.label "" $ do + kw kwGebMorphismFirst + _firstLeftType <- object + _firstRightType <- object + _firstValue <- morphism + return Geb.First {..} + +morphismSecond :: ParsecS r Geb.Second +morphismSecond = do + P.label "" $ do + kw kwGebMorphismSecond + _secondLeftType <- object + _secondRightType <- object + _secondValue <- morphism + return Geb.Second {..} + +morphismLambda :: ParsecS r Geb.Lambda +morphismLambda = do + P.label "" $ do + kw kwGebMorphismLambda + _lambdaVarType <- object + _lambdaBodyType <- object + _lambdaBody <- morphism + return Geb.Lambda {..} + +morphismApplication :: ParsecS r Geb.Application +morphismApplication = do + P.label "" $ do + kw kwGebMorphismApplication + _applicationDomainType <- object + _applicationCodomainType <- object + _applicationLeft <- morphism + _applicationRight <- morphism + return Geb.Application {..} + +morphismVar :: ParsecS r Geb.Var +morphismVar = do + P.label "" $ 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 {..} diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromSource/Lexer.hs new file mode 100644 index 000000000..d78531988 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromSource/Lexer.hs @@ -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 "}") diff --git a/src/Juvix/Compiler/Core/Data/BinderList.hs b/src/Juvix/Compiler/Core/Data/BinderList.hs index 102992b4b..b43ba16fd 100644 --- a/src/Juvix/Compiler/Core/Data/BinderList.hs +++ b/src/Juvix/Compiler/Core/Data/BinderList.hs @@ -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 diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 25a596110..00d925acd 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -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" diff --git a/src/Juvix/Prelude/Path.hs b/src/Juvix/Prelude/Path.hs index be87eec5d..8bdf0424a 100644 --- a/src/Juvix/Prelude/Path.hs +++ b/src/Juvix/Prelude/Path.hs @@ -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 diff --git a/test/BackendGeb.hs b/test/BackendGeb.hs new file mode 100644 index 000000000..3158f9373 --- /dev/null +++ b/test/BackendGeb.hs @@ -0,0 +1,11 @@ +module BackendGeb where + +import BackendGeb.Eval qualified as Eval +import Base + +allTests :: TestTree +allTests = + testGroup + "BackendGeb tests" + [ Eval.allTests + ] diff --git a/test/BackendGeb/Eval.hs b/test/BackendGeb/Eval.hs new file mode 100644 index 000000000..ced72d77c --- /dev/null +++ b/test/BackendGeb/Eval.hs @@ -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] diff --git a/test/BackendGeb/Eval/Base.hs b/test/BackendGeb/Eval/Base.hs new file mode 100644 index 000000000..981cef262 --- /dev/null +++ b/test/BackendGeb/Eval/Base.hs @@ -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" diff --git a/test/BackendGeb/Eval/Positive.hs b/test/BackendGeb/Eval/Positive.hs new file mode 100644 index 000000000..0d0ec8a1a --- /dev/null +++ b/test/BackendGeb/Eval/Positive.hs @@ -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") + ] diff --git a/test/Main.hs b/test/Main.hs index 110969e15..0c5fdb379 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -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, diff --git a/tests/Geb/positive/Core/out/test001.out b/tests/Geb/positive/Core/out/test001.out deleted file mode 100644 index f3c260ef6..000000000 --- a/tests/Geb/positive/Core/out/test001.out +++ /dev/null @@ -1 +0,0 @@ -(right unit) diff --git a/tests/Geb/positive/Core/out/test002.out b/tests/Geb/positive/Core/out/test002.out deleted file mode 100644 index a0a32923d..000000000 --- a/tests/Geb/positive/Core/out/test002.out +++ /dev/null @@ -1 +0,0 @@ -(left unit) diff --git a/tests/Geb/positive/Core/out/test003.out b/tests/Geb/positive/Core/out/test003.out deleted file mode 100644 index a0a32923d..000000000 --- a/tests/Geb/positive/Core/out/test003.out +++ /dev/null @@ -1 +0,0 @@ -(left unit) diff --git a/tests/Geb/positive/Core/out/test004.out b/tests/Geb/positive/Core/out/test004.out deleted file mode 100644 index a0a32923d..000000000 --- a/tests/Geb/positive/Core/out/test004.out +++ /dev/null @@ -1 +0,0 @@ -(left unit) diff --git a/tests/Geb/positive/Eval/out/app-app-lambda.out b/tests/Geb/positive/Eval/out/app-app-lambda.out new file mode 100644 index 000000000..4a22a3e92 --- /dev/null +++ b/tests/Geb/positive/Eval/out/app-app-lambda.out @@ -0,0 +1,4 @@ +(cls + (env + nil) + (index 0)) diff --git a/tests/Geb/positive/Eval/out/app-case-on.out b/tests/Geb/positive/Eval/out/app-case-on.out new file mode 100644 index 000000000..be90d296e --- /dev/null +++ b/tests/Geb/positive/Eval/out/app-case-on.out @@ -0,0 +1,2 @@ +(right + 1) diff --git a/tests/Geb/positive/Eval/out/app-fst-pair.out b/tests/Geb/positive/Eval/out/app-fst-pair.out new file mode 100644 index 000000000..f599e28b8 --- /dev/null +++ b/tests/Geb/positive/Eval/out/app-fst-pair.out @@ -0,0 +1 @@ +10 diff --git a/tests/Geb/positive/Eval/out/app-lambda.out b/tests/Geb/positive/Eval/out/app-lambda.out new file mode 100644 index 000000000..7536096fd --- /dev/null +++ b/tests/Geb/positive/Eval/out/app-lambda.out @@ -0,0 +1,7 @@ +(cls + (env + (cls + (env + nil) + (index 0))) + (index 1)) diff --git a/tests/Geb/positive/Eval/out/basic-app.out b/tests/Geb/positive/Eval/out/basic-app.out new file mode 100644 index 000000000..13de30f45 --- /dev/null +++ b/tests/Geb/positive/Eval/out/basic-app.out @@ -0,0 +1 @@ +3000 diff --git a/tests/Geb/positive/Eval/out/case-on.out b/tests/Geb/positive/Eval/out/case-on.out new file mode 100644 index 000000000..d2367deac --- /dev/null +++ b/tests/Geb/positive/Eval/out/case-on.out @@ -0,0 +1,2 @@ +(left + unit) diff --git a/tests/Geb/positive/Eval/out/lamb.out b/tests/Geb/positive/Eval/out/lamb.out new file mode 100644 index 000000000..6f09ff5b8 --- /dev/null +++ b/tests/Geb/positive/Eval/out/lamb.out @@ -0,0 +1,7 @@ +(cls + (env + nil) + (lamb + so1 + so1 + (index 1))) diff --git a/tests/Geb/positive/Eval/out/left-unit.out b/tests/Geb/positive/Eval/out/left-unit.out new file mode 100644 index 000000000..8dfbe3a42 --- /dev/null +++ b/tests/Geb/positive/Eval/out/left-unit.out @@ -0,0 +1,5 @@ +(cls + (env + nil) + (left + unit)) diff --git a/tests/Geb/positive/Eval/out/test001.out b/tests/Geb/positive/Eval/out/test001.out new file mode 100644 index 000000000..475071f33 --- /dev/null +++ b/tests/Geb/positive/Eval/out/test001.out @@ -0,0 +1,2 @@ +(right + unit) diff --git a/tests/Geb/positive/Eval/out/test002.out b/tests/Geb/positive/Eval/out/test002.out new file mode 100644 index 000000000..d2367deac --- /dev/null +++ b/tests/Geb/positive/Eval/out/test002.out @@ -0,0 +1,2 @@ +(left + unit) diff --git a/tests/Geb/positive/Eval/out/test003.out b/tests/Geb/positive/Eval/out/test003.out new file mode 100644 index 000000000..d2367deac --- /dev/null +++ b/tests/Geb/positive/Eval/out/test003.out @@ -0,0 +1,2 @@ +(left + unit) diff --git a/tests/Geb/positive/Eval/out/test004.out b/tests/Geb/positive/Eval/out/test004.out new file mode 100644 index 000000000..d2367deac --- /dev/null +++ b/tests/Geb/positive/Eval/out/test004.out @@ -0,0 +1,2 @@ +(left + unit) diff --git a/tests/Geb/positive/Core/out/test005.out b/tests/Geb/positive/Eval/out/test005.out similarity index 100% rename from tests/Geb/positive/Core/out/test005.out rename to tests/Geb/positive/Eval/out/test005.out diff --git a/tests/Geb/positive/Core/out/test006.out b/tests/Geb/positive/Eval/out/test006.out similarity index 100% rename from tests/Geb/positive/Core/out/test006.out rename to tests/Geb/positive/Eval/out/test006.out diff --git a/tests/Geb/positive/Infer/out/basic-app.out b/tests/Geb/positive/Infer/out/basic-app.out new file mode 100644 index 000000000..4e0b2da04 --- /dev/null +++ b/tests/Geb/positive/Infer/out/basic-app.out @@ -0,0 +1 @@ +int \ No newline at end of file diff --git a/tests/Geb/positive/Infer/out/left-unit.out b/tests/Geb/positive/Infer/out/left-unit.out new file mode 100644 index 000000000..7b2fc48c1 --- /dev/null +++ b/tests/Geb/positive/Infer/out/left-unit.out @@ -0,0 +1,5 @@ +(!-> + so1 + (coprod + so1 + so1)) \ No newline at end of file diff --git a/tests/Geb/positive/Infer/out/test001.out b/tests/Geb/positive/Infer/out/test001.out new file mode 100644 index 000000000..c57a92e85 --- /dev/null +++ b/tests/Geb/positive/Infer/out/test001.out @@ -0,0 +1,3 @@ +(coprod + so1 + so1) \ No newline at end of file diff --git a/tests/Geb/positive/Infer/out/test002.out b/tests/Geb/positive/Infer/out/test002.out new file mode 100644 index 000000000..c57a92e85 --- /dev/null +++ b/tests/Geb/positive/Infer/out/test002.out @@ -0,0 +1,3 @@ +(coprod + so1 + so1) \ No newline at end of file diff --git a/tests/Geb/positive/Infer/out/test003.out b/tests/Geb/positive/Infer/out/test003.out new file mode 100644 index 000000000..c57a92e85 --- /dev/null +++ b/tests/Geb/positive/Infer/out/test003.out @@ -0,0 +1,3 @@ +(coprod + so1 + so1) \ No newline at end of file diff --git a/tests/Geb/positive/Infer/out/test004.out b/tests/Geb/positive/Infer/out/test004.out new file mode 100644 index 000000000..c57a92e85 --- /dev/null +++ b/tests/Geb/positive/Infer/out/test004.out @@ -0,0 +1,3 @@ +(coprod + so1 + so1) \ No newline at end of file diff --git a/tests/Geb/positive/Infer/out/test005.out b/tests/Geb/positive/Infer/out/test005.out new file mode 100644 index 000000000..4e0b2da04 --- /dev/null +++ b/tests/Geb/positive/Infer/out/test005.out @@ -0,0 +1 @@ +int \ No newline at end of file diff --git a/tests/Geb/positive/Infer/out/test006.out b/tests/Geb/positive/Infer/out/test006.out new file mode 100644 index 000000000..4e0b2da04 --- /dev/null +++ b/tests/Geb/positive/Infer/out/test006.out @@ -0,0 +1 @@ +int \ No newline at end of file diff --git a/tests/Geb/positive/app-app-lambda.geb b/tests/Geb/positive/app-app-lambda.geb new file mode 100644 index 000000000..a859e1e66 --- /dev/null +++ b/tests/Geb/positive/app-app-lambda.geb @@ -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) \ No newline at end of file diff --git a/tests/Geb/positive/app-case-on.geb b/tests/Geb/positive/app-case-on.geb new file mode 100644 index 000000000..f755547a6 --- /dev/null +++ b/tests/Geb/positive/app-case-on.geb @@ -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)) \ No newline at end of file diff --git a/tests/Geb/positive/app-fst-pair.geb b/tests/Geb/positive/app-fst-pair.geb new file mode 100644 index 000000000..afed41109 --- /dev/null +++ b/tests/Geb/positive/app-fst-pair.geb @@ -0,0 +1,15 @@ +(app + int + int + (lamb + int + int + (fst + int + int + (index 0))) + (pair + int + int + 10 + 20)) diff --git a/tests/Geb/positive/app-lambda.geb b/tests/Geb/positive/app-lambda.geb new file mode 100644 index 000000000..c04bb4c43 --- /dev/null +++ b/tests/Geb/positive/app-lambda.geb @@ -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))) diff --git a/tests/Geb/positive/basic-app.geb b/tests/Geb/positive/basic-app.geb new file mode 100644 index 000000000..cd27f4d62 --- /dev/null +++ b/tests/Geb/positive/basic-app.geb @@ -0,0 +1,8 @@ +(app + int + int + (lamb + int + int + (index 0)) + (add 1000 2000)) diff --git a/tests/Geb/positive/case-on.geb b/tests/Geb/positive/case-on.geb new file mode 100644 index 000000000..ac456a7b3 --- /dev/null +++ b/tests/Geb/positive/case-on.geb @@ -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))) \ No newline at end of file diff --git a/tests/Geb/positive/lamb.geb b/tests/Geb/positive/lamb.geb new file mode 100644 index 000000000..e196b1a1e --- /dev/null +++ b/tests/Geb/positive/lamb.geb @@ -0,0 +1,9 @@ +(lamb + so1 + (!-> + so1 + so1) + (lamb + so1 + so1 + (index 1))) \ No newline at end of file diff --git a/tests/Geb/positive/left-unit.geb b/tests/Geb/positive/left-unit.geb new file mode 100644 index 000000000..3c2122944 --- /dev/null +++ b/tests/Geb/positive/left-unit.geb @@ -0,0 +1,6 @@ +(lamb + so1 + (coprod + so1 + so1) + (left unit)) diff --git a/tests/smoke/Commands/dev/geb.smoke.yaml b/tests/smoke/Commands/dev/geb.smoke.yaml new file mode 100644 index 000000000..5a8a44b82 --- /dev/null +++ b/tests/smoke/Commands/dev/geb.smoke.yaml @@ -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 diff --git a/tests/smoke/Commands/dev/root.smoke.yaml b/tests/smoke/Commands/dev/root.smoke.yaml index 5b59c9bc6..9f3459981 100644 --- a/tests/smoke/Commands/dev/root.smoke.yaml +++ b/tests/smoke/Commands/dev/root.smoke.yaml @@ -7,8 +7,6 @@ tests: - dev - root stdout: - matches: | - .*?/(juvix|main)/tests/ - # contains "main" for the CI + matches: .*/tests/ exit-status: 0 \ No newline at end of file