End-to-end Geb compilation tests (#1942)

* Adds end-to-end tests for compiling Juvix to Geb * Fixes bugs in the Core-to-Geb translation (`<=` and `let`) * Fixes a bug in the Geb evaluator (equality on integers)
anoma · Mar 29, 2023 · 3c3e442 · 3c3e442
1 parent fac6be3
commit 3c3e442
Show file tree

Hide file tree

Showing 58 changed files with 657 additions and 111 deletions.
diff --git a/app/Commands/Dev/Geb/Check.hs b/app/Commands/Dev/Geb/Check.hs
@@ -19,6 +19,6 @@ runCommand opts = do
     Right (Geb.ExpressionTypedMorphism tyMorph) -> do
       case run . runError @CheckingError $ (Geb.check' tyMorph) of
         Left err -> exitJuvixError (JuvixError err)
-        Right _ -> renderStdOut ("Well done! It typechecks" :: Text)
+        Right _ -> renderStdOut ("Well done! It typechecks\n" :: Text)
     Right _ -> exitJuvixError (error @JuvixError "Not a typed morphism")
     Left err -> exitJuvixError (JuvixError err)
diff --git a/app/Commands/Dev/Geb/Infer.hs b/app/Commands/Dev/Geb/Infer.hs
@@ -22,11 +22,12 @@ runCommand opts = do
     Right (Geb.ExpressionTypedMorphism tyMorph) -> do
       case run . runError @Geb.CheckingError $ Geb.check' tyMorph of
         Left err -> exitJuvixError (JuvixError err)
-        Right _ ->
+        Right _ -> do
           renderStdOut $
             Geb.ppOut
               opts
               (tyMorph ^. Geb.typedMorphismObject)
+          embed $ putStrLn ""
     Right (Geb.ExpressionObject _) ->
       exitJuvixError (error @JuvixError "No inference for objects")
     Left err -> exitJuvixError (JuvixError err)
diff --git a/src/Juvix/Compiler/Backend/Geb/Evaluator.hs b/src/Juvix/Compiler/Backend/Geb/Evaluator.hs
@@ -230,7 +230,7 @@ evalBinop binop = do
               | otherwise -> return valueFalse
         OpEq ->
           if
-              | l < r -> return valueTrue
+              | l == r -> return valueTrue
               | otherwise -> return valueFalse
     (m1, m2) -> case binop ^. binopOpcode of
       OpEq ->

diff --git a/src/Juvix/Compiler/Backend/Geb/Extra.hs b/src/Juvix/Compiler/Backend/Geb/Extra.hs
@@ -30,6 +30,7 @@ morphismFalse =
         _rightInjValue = MorphismUnit
       }
 
+-- | NOTE: `arg2` needs to be shifted by 1!
 mkOr :: Morphism -> Morphism -> Morphism
 mkOr arg1 arg2 =
   MorphismCase

diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs
@@ -237,8 +237,8 @@ fromCore tab = case tab ^. Core.infoMain of
                                 ( MorphismBinop
                                     Binop
                                       { _binopOpcode = OpEq,
-                                        _binopLeft = MorphismVar Var {_varIndex = 1},
-                                        _binopRight = MorphismVar Var {_varIndex = 0}
+                                        _binopLeft = MorphismVar Var {_varIndex = 2},
+                                        _binopRight = MorphismVar Var {_varIndex = 1}
                                       }
                                 )
                           }
@@ -247,29 +247,30 @@ fromCore tab = case tab ^. Core.infoMain of
               MorphismApplication
                 Application
                   { _applicationDomainType = ObjectInteger,
-                    _applicationCodomainType =
-                      ObjectHom
-                        Hom
-                          { _homDomain = ObjectInteger,
-                            _homCodomain = objectBool
-                          },
+                    _applicationCodomainType = objectBool,
                     _applicationLeft =
                       MorphismApplication
                         Application
                           { _applicationDomainType = ObjectInteger,
-                            _applicationCodomainType = objectBool,
+                            _applicationCodomainType =
+                              ObjectHom
+                                Hom
+                                  { _homDomain = ObjectInteger,
+                                    _homCodomain = objectBool
+                                  },
                             _applicationLeft = le,
-                            _applicationRight = arg2'
+                            _applicationRight = arg1'
                           },
-                    _applicationRight = arg1'
+                    _applicationRight = arg2'
                   }
       _ ->
         error "wrong builtin application argument number"
 
     convertOpEq :: [Core.Node] -> Trans Morphism
     convertOpEq args = case args of
-      arg : _
-        | Info.getNodeType arg == Core.mkTypeInteger' ->
+      arg1 : arg2 : _
+        | Info.getNodeType arg1 == Core.mkTypeInteger'
+            && Info.getNodeType arg2 == Core.mkTypeInteger' ->
             convertBinop OpEq args
       _ ->
         error "unsupported equality argument types"
@@ -360,8 +361,8 @@ fromCore tab = case tab ^. Core.infoMain of
       return $
         MorphismApplication
           Application
-            { _applicationCodomainType = domty,
-              _applicationDomainType = codty,
+            { _applicationDomainType = domty,
+              _applicationCodomainType = codty,
               _applicationLeft =
                 MorphismLambda
                   Lambda

diff --git a/src/Juvix/Compiler/Core/Transformation/CheckGeb.hs b/src/Juvix/Compiler/Core/Transformation/CheckGeb.hs
@@ -28,6 +28,12 @@ checkGeb tab =
           NLam Lambda {..}
             | isDynamic (_lambdaBinder ^. binderType) ->
                 throw (dynamicTypeError node (_lambdaBinder ^. binderLocation))
+          NLet Let {..}
+            | isDynamic (_letItem ^. letItemBinder . binderType) ->
+                throw (dynamicTypeError node (_letItem ^. letItemBinder . binderLocation))
+          NRec LetRec {..}
+            | any (isDynamic . (^. letItemBinder . binderType)) _letRecValues ->
+                throw (dynamicTypeError node (head _letRecValues ^. letItemBinder . binderLocation))
           NPi Pi {..}
             | isTypeConstr tab (_piBinder ^. binderType) ->
                 throw

diff --git a/test/BackendGeb.hs b/test/BackendGeb.hs
@@ -1,5 +1,6 @@
 module BackendGeb where
 
+import BackendGeb.Compilation qualified as Compilation
 import BackendGeb.Eval qualified as Eval
 import BackendGeb.FromCore qualified as FromCore
 import Base
@@ -9,5 +10,6 @@ allTests =
   testGroup
     "BackendGeb tests"
     [ Eval.allTests,
-      FromCore.allTests
+      FromCore.allTests,
+      Compilation.allTests
     ]
diff --git a/test/BackendGeb/Compilation.hs b/test/BackendGeb/Compilation.hs
@@ -0,0 +1,10 @@
+module BackendGeb.Compilation where
+
+import BackendGeb.Compilation.Positive qualified as P
+import Base
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Compilation to Geb"
+    [P.allTests]
diff --git a/test/BackendGeb/Compilation/Base.hs b/test/BackendGeb/Compilation/Base.hs
@@ -0,0 +1,20 @@
+module BackendGeb.Compilation.Base where
+
+import BackendGeb.FromCore.Base
+import Base
+import Juvix.Compiler.Backend (Target (TargetGeb))
+import Juvix.Compiler.Builtins (iniState)
+import Juvix.Compiler.Core qualified as Core
+import Juvix.Compiler.Pipeline
+
+gebCompilationAssertion ::
+  Path Abs File ->
+  Path Abs File ->
+  (String -> IO ()) ->
+  Assertion
+gebCompilationAssertion mainFile expectedFile step = do
+  step "Translate to JuvixCore"
+  cwd <- getCurrentDir
+  let entryPoint = (defaultEntryPoint cwd mainFile) {_entryPointTarget = TargetGeb}
+  tab <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
+  coreToGebTranslationAssertion' tab entryPoint expectedFile step
diff --git a/test/BackendGeb/Compilation/Positive.hs b/test/BackendGeb/Compilation/Positive.hs
@@ -0,0 +1,97 @@
+module BackendGeb.Compilation.Positive where
+
+import BackendGeb.Compilation.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/Compilation")
+
+testDescr :: PosTest -> TestDescr
+testDescr PosTest {..} =
+  let tRoot = root <//> _relDir
+      file' = tRoot <//> _file
+      expected' = tRoot <//> _expectedFile
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion =
+            Steps $
+              gebCompilationAssertion file' expected'
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "JuvixGeb positive compilation tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [PosTest]
+tests =
+  [ PosTest
+      "Test001: not function"
+      $(mkRelDir ".")
+      $(mkRelFile "test001.juvix")
+      $(mkRelFile "out/test001.geb"),
+    PosTest
+      "Test002: pattern matching"
+      $(mkRelDir ".")
+      $(mkRelFile "test002.juvix")
+      $(mkRelFile "out/test002.geb"),
+    PosTest
+      "Test003: inductive types"
+      $(mkRelDir ".")
+      $(mkRelFile "test003.juvix")
+      $(mkRelFile "out/test003.geb"),
+    PosTest
+      "Test004: definitions"
+      $(mkRelDir ".")
+      $(mkRelFile "test004.juvix")
+      $(mkRelFile "out/test004.geb"),
+    PosTest
+      "Test005: basic arithmetic"
+      $(mkRelDir ".")
+      $(mkRelFile "test005.juvix")
+      $(mkRelFile "out/test005.geb"),
+    PosTest
+      "Test006: arithmetic"
+      $(mkRelDir ".")
+      $(mkRelFile "test006.juvix")
+      $(mkRelFile "out/test006.geb"),
+    PosTest
+      "Test007: single-constructor inductive types"
+      $(mkRelDir ".")
+      $(mkRelFile "test007.juvix")
+      $(mkRelFile "out/test007.geb"),
+    PosTest
+      "Test008: higher-order inductive types"
+      $(mkRelDir ".")
+      $(mkRelFile "test008.juvix")
+      $(mkRelFile "out/test008.geb"),
+    PosTest
+      "Test009: let"
+      $(mkRelDir ".")
+      $(mkRelFile "test009.juvix")
+      $(mkRelFile "out/test009.geb"),
+    PosTest
+      "Test010: functions returning functions with variable capture"
+      $(mkRelDir ".")
+      $(mkRelFile "test010.juvix")
+      $(mkRelFile "out/test010.geb"),
+    PosTest
+      "Test011: applications with lets and cases in function position"
+      $(mkRelDir ".")
+      $(mkRelFile "test011.juvix")
+      $(mkRelFile "out/test011.geb"),
+    PosTest
+      "Test012: mid-square hashing (unrolled)"
+      $(mkRelDir ".")
+      $(mkRelFile "test012.juvix")
+      $(mkRelFile "out/test012.geb")
+  ]
diff --git a/test/BackendGeb/Eval/Positive.hs b/test/BackendGeb/Eval/Positive.hs
@@ -32,7 +32,7 @@ filterOutTests out = filter (\PosTest {..} -> _name `notElem` out)
 allTests :: TestTree
 allTests =
   testGroup
-    "JuvixGeb positive tests"
+    "JuvixGeb positive evaluation tests"
     (map (mkTest . testDescr) tests)
 
 tests :: [PosTest]