Fix caseCmd for RepConstr (#2666)

See #2670 for an example which triggers the bug. The nockma case compilation did not correctly compile case expressions for standard (i.e not list or tuple) constructors. Existing compilation tests (e.g Tree, Lambda Calculus) did not fail due to the relevant `fromJust` never being evaluated due to lazy evaluation. The tests now write out the resulting nockma file to force full evaluation. * Closes #2670 --------- Co-authored-by: Paul Cadman <[email protected]>
anoma · Feb 26, 2024 · 1413f8f · 1413f8f
1 parent be24abb
commit 1413f8f
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 3 deletions.
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
@@ -753,8 +753,13 @@ caseCmd arg defaultBranch = \case
             OpEq
               # constructorTagToTerm tag
               # (getConstructorField ConstructorTag arg)
-      elseBr <- caseCmd arg defaultBranch bs
-      return (branch cond b elseBr)
+      case nonEmpty bs of
+        Nothing -> case defaultBranch of
+          Nothing -> return b
+          Just defbr -> return (branch cond b defbr)
+        Just ((t', b') :| bs') -> do
+          elseBr <- goRepConstr t' b' bs'
+          return (branch cond b elseBr)
 
     asNockmaMemRepListConstr :: Tree.Tag -> Sem r NockmaMemRepListConstr
     asNockmaMemRepListConstr tag = case tag of

diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
@@ -4,6 +4,7 @@ import Base
 import Juvix.Compiler.Backend (Target (TargetAnoma))
 import Juvix.Compiler.Nockma.Evaluator
 import Juvix.Compiler.Nockma.Language
+import Juvix.Compiler.Nockma.Pretty
 import Juvix.Compiler.Nockma.Translation.FromSource.QQ
 import Juvix.Compiler.Nockma.Translation.FromTree
 import Juvix.Prelude qualified as Prelude
@@ -19,7 +20,11 @@ mkAnomaCallTest' enableDebug _testName relRoot mainFile args _testCheck =
   where
     mkTestIO :: IO Test
     mkTestIO = do
-      _testProgramSubject <- withRootCopy compileMain
+      _testProgramSubject <- withRootCopy $ \tmpDir -> do
+        compiledMain <- compileMain tmpDir
+        -- Write out the nockma function to force full evaluation of the compiler
+        writeFileEnsureLn (tmpDir <//> $(mkRelFile "test.nockma")) (ppSerialize compiledMain)
+        return compiledMain
       let _testProgramFormula = anomaCall args
           _testEvalOptions = defaultEvalOptions
       return Test {..}