Test core to geb translation (#1865)

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

app/Commands/Compile.hs

@@ -6,7 +6,6 @@ import Commands.Dev.Core.Compile.Base qualified as Compile
 import Commands.Extra.Compile qualified as Compile
 import Data.Text.IO qualified as TIO
 import Juvix.Compiler.Core qualified as Core
-import Juvix.Compiler.Core.Pipeline qualified as Core
 import Juvix.Compiler.Core.Pretty qualified as Core
 import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core
 

app/Commands/Dev/Geb/Eval.hs

@@ -35,6 +35,7 @@ evalAndPrint ::
   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 =
@@ -51,7 +52,6 @@ evalAndPrint opts = \case
             case Geb.eval' env morphism of
               Left err -> exitJuvixError err
               Right m -> renderStdOut (Geb.ppOut opts' m)
-  Geb.ExpressionObject _ -> error Geb.objNoEvalMsg
   Geb.ExpressionTypedMorphism tyMorph ->
     evalAndPrint
       opts

app/Commands/Eval.hs

@@ -4,10 +4,6 @@ import Commands.Base
 import Commands.Eval.Options
 import Evaluator qualified as Eval
 import Juvix.Compiler.Core qualified as Core
-import Juvix.Compiler.Core.Data.InfoTable qualified as Core
-import Juvix.Compiler.Core.Language qualified as Core
-import Juvix.Compiler.Core.Options qualified as Core
-import Juvix.Compiler.Core.Pipeline qualified as Core
 
 runCommand :: (Members '[Embed IO, App] r) => EvalOptions -> Sem r ()
 runCommand opts@EvalOptions {..} = do

examples/midsquare/MidSquareHash.juvix

@@ -3,9 +3,8 @@
 --- https://research.cs.vt.edu/AVresearch/hashing/midsquare.php
 
 --- The implementation is for hashing natural numbers with maximum 16 bits into 6
---- bits.
----
 
+--- bits.
 module MidSquareHash;
 
 open import Stdlib.Prelude;
@@ -17,12 +16,14 @@ pow zero := 1;
 pow (suc n) := 2 * pow n;
 
 --- `hash' N` hashes a number with max N bits (i.e. smaller than 2^N) into 6 bits
+
 --- (i.e. smaller than 64) using the mid-square algorithm.
 hash' : Nat -> Nat -> Nat;
 hash' (suc n@(suc (suc m))) x :=
-  if (x < pow n)
-     (hash' n x)
-     (mod (div (x * x) (pow m)) (pow 6));
+  if
+    (x < pow n)
+    (hash' n x)
+    (mod (div (x * x) (pow m)) (pow 6));
 hash' _ x := x * x;
 
 hash : Nat -> Nat := hash' 16;

examples/midsquare/MidSquareHashUnrolled.juvix

@@ -1,10 +1,12 @@
 --- This file implements the mid-square hashing function in Juvix. See:
+
 --- https://research.cs.vt.edu/AVresearch/hashing/midsquare.php
----
+
 --- The implementation is for hashing natural numbers with maximum 16 bits into 6
+
 --- bits. In order to facilitate the translation to the current version of the
+
 --- GEB backend, no recursion is used (it is manually unrolled).
----
 module MidSquareHashUnrolled;
 
 open import Stdlib.Prelude;
@@ -12,24 +14,41 @@ open import Stdlib.Data.Nat.Ord;
 
 --- `powN` is 2 ^ N
 pow0 : Nat := 1;
+
 pow1 : Nat := 2 * pow0;
+
 pow2 : Nat := 2 * pow1;
+
 pow3 : Nat := 2 * pow2;
+
 pow4 : Nat := 2 * pow3;
+
 pow5 : Nat := 2 * pow4;
+
 pow6 : Nat := 2 * pow5;
+
 pow7 : Nat := 2 * pow6;
+
 pow8 : Nat := 2 * pow7;
+
 pow9 : Nat := 2 * pow8;
+
 pow10 : Nat := 2 * pow9;
+
 pow11 : Nat := 2 * pow10;
+
 pow12 : Nat := 2 * pow11;
+
 pow13 : Nat := 2 * pow12;
+
 pow14 : Nat := 2 * pow13;
+
 pow15 : Nat := 2 * pow14;
+
 pow16 : Nat := 2 * pow15;
 
 --- `hashN` hashes a number with max N bits (i.e. smaller than 2^N) into 6 bits
+
 --- (i.e. smaller than 64) using the mid-square algorithm.
 hash0 : Nat -> Nat;
 hash0 x := 0;
@@ -44,48 +63,59 @@ hash3 : Nat -> Nat;
 hash3 x := x * x;
 
 hash4 : Nat -> Nat;
-hash4 x := if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+hash4 x :=
+  if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
 
 hash5 : Nat -> Nat;
-hash5 x := if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+hash5 x :=
+  if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
 
 hash6 : Nat -> Nat;
-hash6 x := if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+hash6 x :=
+  if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
 
 hash7 : Nat -> Nat;
-hash7 x := if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+hash7 x :=
+  if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
 
 hash8 : Nat -> Nat;
-hash8 x := if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+hash8 x :=
+  if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
 
 hash9 : Nat -> Nat;
-hash9 x := if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+hash9 x :=
+  if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
 
 hash10 : Nat -> Nat;
-hash10 x := if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+hash10 x :=
+  if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
 
 hash11 : Nat -> Nat;
-hash11 x := if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+hash11 x :=
+  if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
 
 hash12 : Nat -> Nat;
-hash12 x := if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+hash12 x :=
+  if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
 
 hash13 : Nat -> Nat;
-hash13 x := if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+hash13 x :=
+  if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
 
 hash14 : Nat -> Nat;
-hash14 x := if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+hash14 x :=
+  if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
 
 hash15 : Nat -> Nat;
-hash15 x := if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+hash15 x :=
+  if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
 
 hash16 : Nat -> Nat;
-hash16 x := if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+hash16 x :=
+  if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
 
 hash : Nat -> Nat := hash16;
 
 main : Nat;
 main := hash 1367;
 -- result: 3
-
-end;

src/Juvix/Compiler/Core.hs

@@ -1,3 +1,20 @@
-module Juvix.Compiler.Core (module Juvix.Compiler.Core.Translation) where
+module Juvix.Compiler.Core
+  ( module Juvix.Compiler.Core.Translation,
+    module Juvix.Compiler.Core.Pipeline,
+    module Juvix.Compiler.Core.Language,
+    module Juvix.Compiler.Core.Evaluator,
+    module Juvix.Compiler.Core.Data,
+    module Juvix.Compiler.Core.Extra,
+    module Juvix.Compiler.Core.Error,
+    module Juvix.Compiler.Core.Options,
+  )
+where
 
+import Juvix.Compiler.Core.Data
+import Juvix.Compiler.Core.Error
+import Juvix.Compiler.Core.Evaluator
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Options
+import Juvix.Compiler.Core.Pipeline
 import Juvix.Compiler.Core.Translation

src/Juvix/Compiler/Core/Data/InfoTable.hs

@@ -41,6 +41,13 @@ emptyInfoTable =
       _infoBuiltins = mempty
     }
 
+emptyInfoTable' :: Node -> InfoTable
+emptyInfoTable' mainNode =
+  emptyInfoTable
+    { _identContext = HashMap.singleton 0 mainNode,
+      _infoMain = Just 0
+    }
+
 data IdentKind
   = IdentFun Symbol
   | IdentInd Symbol

src/Juvix/Compiler/Core/Evaluator.hs

@@ -45,6 +45,13 @@ instance Show EvalError where
 
 instance Exception.Exception EvalError
 
+evalInfoTable :: Handle -> InfoTable -> Node
+evalInfoTable herr info = eval herr idenCtxt [] mainNode
+  where
+    idenCtxt = info ^. identContext
+    mainSym = fromJust (info ^. infoMain)
+    mainNode = fromJust (HashMap.lookup mainSym idenCtxt)
+
 -- | `eval ctx env n` evalues a node `n` whose all free variables point into
 -- `env`. All nodes in `ctx` must be closed. All nodes in `env` must be values.
 -- Invariant for values v: eval ctx env v = v

src/Juvix/Compiler/Core/Translation.hs

@@ -1,8 +1,10 @@
 module Juvix.Compiler.Core.Translation
   ( module Juvix.Compiler.Core.Translation.FromInternal,
     module Juvix.Compiler.Core.Translation.FromInternal.Data,
+    module Juvix.Compiler.Core.Translation.FromSource,
   )
 where
 
 import Juvix.Compiler.Core.Translation.FromInternal
 import Juvix.Compiler.Core.Translation.FromInternal.Data
+import Juvix.Compiler.Core.Translation.FromSource

test/BackendGeb.hs

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

test/BackendGeb/FromCore.hs

@@ -0,0 +1,10 @@
+module BackendGeb.FromCore where
+
+import BackendGeb.FromCore.Positive qualified as FromCoreP
+import Base
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Translation from Juvix Core to Geb"
+    [FromCoreP.allTests]

test/BackendGeb/FromCore/Base.hs

@@ -0,0 +1,85 @@
+module BackendGeb.FromCore.Base where
+
+import Base
+import Data.Text.IO qualified as TIO
+import Juvix.Compiler.Backend.Geb qualified as Geb
+import Juvix.Compiler.Core qualified as Core
+import Juvix.Compiler.Pipeline
+import Juvix.Prelude.Pretty
+
+coreToGebtranslationAssertion ::
+  Path Abs File ->
+  Path Abs File ->
+  (String -> IO ()) ->
+  Assertion
+coreToGebtranslationAssertion mainFile expectedFile step = do
+  step "Parse Juvix Core file"
+  input <- readFile . toFilePath $ mainFile
+  cwd <- getCurrentDir
+  let entryPoint = defaultEntryPoint cwd mainFile
+  case Core.runParserMain mainFile Core.emptyInfoTable input of
+    Left err -> assertFailure . show . pretty $ err
+    Right coreInfoTable -> do
+      step "Prepare the Juvix Core node for translation to Geb"
+      case run . runReader entryPoint . runError @Geb.JuvixError $
+        Core.toGeb coreInfoTable of
+        Left err ->
+          assertFailure . show . pretty $
+            fromJuvixError @GenericError err
+        Right readyCoreInfoTable -> do
+          step "Translate the Juvix Core node to Geb"
+          let (translatedMorphism, translatedObj) = Geb.fromCore readyCoreInfoTable
+          step "Typecheck the translated Geb node"
+          let typeMorph =
+                Geb.TypedMorphism
+                  { _typedMorphism = translatedMorphism,
+                    _typedMorphismObject = translatedObj
+                  }
+          case run . runError @Geb.CheckingError $ Geb.check' typeMorph of
+            Left err ->
+              assertFailure . show . pretty $
+                fromJuvixError @GenericError (JuvixError err)
+            Right _ -> do
+              step "Try evaluating the JuvixCore node"
+              let resultCoreEval :: Core.Node = Core.evalInfoTable stderr readyCoreInfoTable
+              step "Translate the result of the evaluated JuvixCore node to Geb"
+              let (gebCoreEvalResult, _) = Geb.fromCore $ Core.setupMainFunction readyCoreInfoTable resultCoreEval
+              case ( Geb.eval' Geb.defaultEvalEnv translatedMorphism,
+                     Geb.eval' Geb.defaultEvalEnv gebCoreEvalResult
+                   ) of
+                (Left err, _) -> do
+                  step "The evaluation of the translated Geb node failed"
+                  assertFailure . show . pretty $
+                    fromJuvixError @GenericError (JuvixError err)
+                (_, Left err) -> do
+                  step "The evaluation of gebCoreEvalResult failed"
+                  assertFailure . show . pretty $ fromJuvixError @GenericError (JuvixError err)
+                ( Right resEvalTranslatedMorph,
+                  Right resEvalGebCoreEvalResult
+                  ) -> do
+                    step "Compare the geb value of the Core eval output and the Geb eval output"
+                    if
+                        | resEvalTranslatedMorph /= resEvalGebCoreEvalResult ->
+                            assertFailure "The evaluation for the Core node and the Geb node are not equal"
+                        | otherwise -> do
+                            let fpath = toFilePath expectedFile
+                            expectedInput <- TIO.readFile fpath
+                            step "Compare expected and actual program output"
+                            let compareEvalOutput morph =
+                                  case Geb.eval' Geb.defaultEvalEnv morph of
+                                    Left err ->
+                                      assertFailure . show . pretty $
+                                        fromJuvixError @GenericError (JuvixError err)
+                                    Right resEvalExpected -> do
+                                      if
+                                          | resEvalTranslatedMorph /= resEvalExpected ->
+                                              assertFailure $
+                                                "The result of evaluating the translated Geb"
+                                                  <> "node is not equal to the expected output"
+                                          | otherwise -> assertBool "" True
+                            case Geb.runParser expectedFile expectedInput of
+                              Left parseErr -> assertFailure . show . pretty $ parseErr
+                              Right (Geb.ExpressionMorphism m) -> compareEvalOutput m
+                              Right (Geb.ExpressionTypedMorphism m) -> compareEvalOutput (m ^. Geb.typedMorphism)
+                              Right (Geb.ExpressionObject _) ->
+                                assertFailure "Expected a morphism, but got an object for the expected output"

test/BackendGeb/FromCore/Positive.hs

@@ -0,0 +1,80 @@
+module BackendGeb.FromCore.Positive where
+
+import BackendGeb.FromCore.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 $
+              coreToGebtranslationAssertion 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
+      "Test001"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test001.jvc")
+      $(mkRelFile "Eval/out/test001.geb"),
+    PosTest
+      "Test002"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test002.jvc")
+      $(mkRelFile "Eval/out/test002.geb"),
+    PosTest
+      "Test003"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test003.jvc")
+      $(mkRelFile "Eval/out/test003.geb"),
+    PosTest
+      "Test004"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test004.jvc")
+      $(mkRelFile "Eval/out/test004.geb"),
+    PosTest
+      "Test005"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test005.jvc")
+      $(mkRelFile "Eval/out/test005.geb"),
+    PosTest
+      "Test006"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test006.jvc")
+      $(mkRelFile "Eval/out/test006.geb"),
+    PosTest
+      "Test007"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test007.jvc")
+      $(mkRelFile "Eval/out/test007.geb"),
+    PosTest
+      "Test008"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test008.jvc")
+      $(mkRelFile "Eval/out/test008.geb")
+  ]

tests/Geb/positive/Core/test001.jvc

@@ -1,2 +1,2 @@
 
-(\(x : bool) if x then false else true) true
+(\(x : Bool) if x then false else true) true

tests/Geb/positive/Core/test002.jvc

@@ -1,7 +1,7 @@
 
 type optbool {
-  Just : bool -> optbool;
+  Just : Bool -> optbool;
   Nothing : optbool;
 };
 
-(\(x : bool) \(o : optbool) { case o of { Just b := if x then true else b; Nothing := false } }) false (Just true)
+(\(x : Bool) \(o : optbool) { case o of { Just b := if x then true else b; Nothing := false } }) false (Just true)

tests/Geb/positive/Core/test003.jvc

@@ -2,8 +2,8 @@
 
 type enum {
   opt0 : enum;
-  opt1 : bool -> enum;
-  opt2 : bool -> bool -> enum;
+  opt1 : Bool -> enum;
+  opt2 : Bool -> Bool -> enum;
 };
 
 (\(e : enum) case e of {

tests/Geb/positive/Core/test004.jvc

@@ -1,6 +1,6 @@
 -- definitions
 
-def not : bool -> bool := \(x : bool) if x then false else true;
-def and : bool -> bool -> bool := \(x : bool) \(y : bool) if x then y else false;
+def not : Bool -> Bool := \(x : Bool) if x then false else true;
+def and : Bool -> Bool -> Bool := \(x : Bool) \(y : Bool) if x then y else false;
 
 and (not false) (not (not true))

tests/Geb/positive/Core/test006.jvc

@@ -1,18 +1,18 @@
 -- arithmetic
 
-def f : int -> int -> int := \(x : int) \(y : int) x + y;
+def f : Int -> Int -> Int := \(x : Int) \(y : Int) x + y;
 
-def g : int -> int -> int := \(x : int) \(y : int) (x + 1) - (y * 7);
+def g : Int -> Int -> Int := \(x : Int) \(y : Int) (x + 1) - (y * 7);
 
-def h : (int -> int -> int) -> int -> int -> int := \(f : int -> int -> int) \(y : int) \(z : int) f y y * z;
+def h : (Int -> Int -> Int) -> Int -> Int -> Int := \(f : Int -> Int -> Int) \(y : Int) \(z : Int) f y y * z;
 
-def x : int := 5;
-def y : int := 17;
-def func : int -> int := \(x : int) x + 4;
-def z : int := 0;
+def x : Int := 5;
+def y : Int := 17;
+def func : Int -> Int := \(x : Int) x + 4;
+def z : Int := 0;
 
-def vx : int := 30;
-def vy : int := 7;
+def vx : Int := 30;
+def vy : Int := 7;
 
 func (y / x) + -- 17 div 5 + 4 = 7
 (z * x + y) + -- 17

tests/Geb/positive/Core/test007.jvc

@@ -1,7 +1,7 @@
 -- single-constructor inductive types
 
 type Box2 {
-    box2 : int -> int -> Box2;
+    box2 : Int -> Int -> Box2;
 };
 
 type Box {

tests/Geb/positive/Core/test008.jvc

@@ -2,9 +2,9 @@
 
 type enum {
   opt0 : enum;
-  opt1 : bool -> enum;
-  opt2 : bool -> (bool -> bool) -> enum;
-  opt3 : bool -> (bool -> bool -> bool) -> bool -> enum;
+  opt1 : Bool -> enum;
+  opt2 : Bool -> (Bool -> Bool) -> enum;
+  opt3 : Bool -> (Bool -> Bool -> Bool) -> Bool -> enum;
 };
 
 (\(e : enum) case e of {
@@ -12,4 +12,4 @@ type enum {
   opt1 b := b;
   opt2 b f := f b;
   opt3 b1 f b2 := f b1 b2;
-}) (opt3 true (\(x : bool) \(y : bool) if y then false else x) false)
+}) (opt3 true (\(x : Bool) \(y : Bool) if y then false else x) false)

tests/Geb/positive/Eval/out/test001.geb

@@ -1,2 +1,4 @@
 (right
+  so1
+  so1
   unit)

tests/Geb/positive/Eval/out/test002.geb

@@ -1,2 +1,4 @@
 (left
+  so1
+  so1
   unit)

tests/Geb/positive/Eval/out/test003.geb

@@ -1,2 +1,4 @@
 (left
+  so1
+  so1
   unit)

tests/Geb/positive/Eval/out/test004.geb

@@ -1,2 +1,4 @@
 (left
+  so1
+  so1
   unit)

tests/Geb/positive/Eval/out/test008.geb

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

tests/Geb/positive/Eval/out/test008.out

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