1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-03 09:41:10 +03:00

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 https://github.com/anoma/juvix/issues/2670

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
This commit is contained in:
Jan Mas Rovira 2024-02-26 11:19:29 +01:00 committed by GitHub
parent be24abb0ca
commit 1413f8f9c4
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 13 additions and 3 deletions

View File

@ -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

View File

@ -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 {..}