Add Geb Backend Evaluator with some extra subcommands

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

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

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

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

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)

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

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"
+    )

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)

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 {..}

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")

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 "")

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 {..}