mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
9f22eaa1cf
This PR adds testing for the core-to-geb translation.
It works as follows:
1. Parse the Juvix Core file.
2. Prepare the Juvix Core node for translation to Geb.
3. Translate the Juvix Core node to Geb.
5. Perform type checking on the translated Geb node to ensure that the
types
from the core node make sense in the Geb context and avoid any Geb
runtime
errors.
6. Evaluate the Juvix Core node to see if it produces the expected
result.
7. Translate the result of the evaluated Juvix Core node to Geb for
comparison
with the expected output later.
8. Compare the result of the evaluation of the Geb term produced in step
3
with the result of the evaluation of the Geb term produced in step 6 to
ensure consistency.
9. If step 8 succeeds, then compare the output of step 6 (the evaluation
of the core
node) with the expected output (given in Geb format) to ensure that
the program is functioning as intended.
This PR goes after:
- https://github.com/anoma/juvix/pull/1863
and
https://github.com/anoma/juvix/pull/1832
59 lines
1.8 KiB
Haskell
59 lines
1.8 KiB
Haskell
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.ExpressionObject _ -> error Geb.objNoEvalMsg
|
|
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.ExpressionTypedMorphism tyMorph ->
|
|
evalAndPrint
|
|
opts
|
|
(Geb.ExpressionMorphism (tyMorph ^. Geb.typedMorphism))
|