Fix bug in computeTypeInfo (#2234)

* Closes #2233

src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs

@@ -33,13 +33,13 @@ ufoldA uplus f = ufoldG unitCollector uplus (const f)
 ufoldLA :: (Applicative f) => (a -> [a] -> a) -> (BinderList Binder -> Node -> f a) -> Node -> f a
 ufoldLA uplus f = ufoldG binderInfoCollector uplus f
 
-ufoldNA :: (Applicative f) => (a -> [a] -> a) -> (Index -> Node -> f a) -> Node -> f a
+ufoldNA :: (Applicative f) => (a -> [a] -> a) -> (Level -> Node -> f a) -> Node -> f a
 ufoldNA uplus f = ufoldG binderNumCollector uplus f
 
 walk :: (Applicative f) => (Node -> f ()) -> Node -> f ()
 walk = ufoldA (foldr mappend)
 
-walkN :: (Applicative f) => (Index -> Node -> f ()) -> Node -> f ()
+walkN :: (Applicative f) => (Level -> Node -> f ()) -> Node -> f ()
 walkN = ufoldNA (foldr mappend)
 
 walkL :: (Applicative f) => (BinderList Binder -> Node -> f ()) -> Node -> f ()
@@ -51,7 +51,7 @@ ufold uplus f = runIdentity . ufoldA uplus (return . f)
 ufoldL :: (a -> [a] -> a) -> (BinderList Binder -> Node -> a) -> Node -> a
 ufoldL uplus f = runIdentity . ufoldLA uplus (\is -> return . f is)
 
-ufoldN :: (a -> [a] -> a) -> (Index -> Node -> a) -> Node -> a
+ufoldN :: (a -> [a] -> a) -> (Level -> Node -> a) -> Node -> a
 ufoldN uplus f = runIdentity . ufoldNA uplus (\idx -> return . f idx)
 
 gather :: (a -> Node -> a) -> a -> Node -> a

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -369,3 +369,9 @@ isCaseBoolean = \case
         True
   _ ->
     False
+
+checkInfoTable :: InfoTable -> Bool
+checkInfoTable tab =
+  all isClosed (tab ^. identContext)
+    && all isClosed (fmap (^. identifierType) (tab ^. infoIdentifiers))
+    && all isClosed (fmap (^. constructorType) (tab ^. infoConstructors))

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -75,7 +75,7 @@ computeNodeTypeInfo tab = umapL go
         Just nd -> Info.getNodeType nd
         Nothing -> case _caseBranches of
           CaseBranch {..} : _ ->
-            Info.getNodeType _caseBranchBody
+            shift (-_caseBranchBindersNum) (Info.getNodeType _caseBranchBody)
           [] -> error "case with no branches"
       NMatch Match {} ->
         error "match unsupported"

test/Core/Compile/Base.hs

@@ -8,6 +8,7 @@ import Data.Text.IO qualified as TIO
 import GHC.Base (seq)
 import Juvix.Compiler.Asm.Pretty qualified as Asm
 import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm
+import Juvix.Compiler.Core.Extra.Utils
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Pipeline
 import Juvix.Compiler.Core.Translation.FromSource
@@ -48,6 +49,7 @@ coreCompileAssertion' tab mainFile expectedFile stdinText step = do
   case run $ runReader defaultCoreOptions $ runError $ toStripped' tab of
     Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
     Right tab0 -> do
+      assertBool "Check info table" (checkInfoTable tab0)
       let tab' = Asm.fromCore $ Stripped.fromCore $ tab0
       length (fromText (Asm.ppPrint tab' tab') :: String) `seq`
         Asm.asmCompileAssertion' tab' mainFile expectedFile stdinText step

test/Core/Eval/Base.hs

@@ -153,6 +153,7 @@ coreEvalAssertion mainFile expectedFile trans testTrans step = do
       case run $ runReader defaultCoreOptions $ runError $ applyTransformations trans (setupMainFunction tabIni node) of
         Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
         Right tab -> do
+          assertBool "Check info table" (checkInfoTable tab)
           testTrans tab
           coreEvalAssertion' EvalModePlain tab mainFile expectedFile step