diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index c8d2700f76..db3b9d7f6a 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -62,10 +62,16 @@ data NockmaMemRepListConstr | NockmaMemRepListConstrCons deriving stock (Eq) +data NockmaMemRepMaybeConstr + = NockmaMemRepMaybeConstrNothing + | NockmaMemRepMaybeConstrJust + deriving stock (Eq) + data NockmaMemRep = NockmaMemRepConstr | NockmaMemRepTuple | NockmaMemRepList NockmaMemRepListConstr + | NockmaMemRepMaybe NockmaMemRepMaybeConstr newtype NockmaBuiltinTag = NockmaBuiltinBool Bool @@ -224,15 +230,27 @@ allConstructors Tree.InfoTable {..} ci = getConstructorInfo'' :: Tree.Tag -> Tree.ConstructorInfo getConstructorInfo'' t = _infoConstrs ^?! at t . _Just -supportsListNockmaRep :: Tree.InfoTable -> Tree.ConstructorInfo -> Maybe NockmaMemRepListConstr -supportsListNockmaRep tab ci = case allConstructors tab ci of - c1 :| [c2] - | [0, 2] `elem` permutations ((^. Tree.constructorArgsNum) <$> [c1, c2]) -> Just $ case ci ^. Tree.constructorArgsNum of - 0 -> NockmaMemRepListConstrNil - 2 -> NockmaMemRepListConstrCons - _ -> impossible - | otherwise -> Nothing - _ -> Nothing +supportsListNockmaRep :: Tree.InfoTable -> Tree.ConstructorInfo -> Maybe NockmaMemRep +supportsListNockmaRep tab ci = + NockmaMemRepList <$> case allConstructors tab ci of + c1 :| [c2] + | [0, 2] `elem` permutations ((^. Tree.constructorArgsNum) <$> [c1, c2]) -> Just $ case ci ^. Tree.constructorArgsNum of + 0 -> NockmaMemRepListConstrNil + 2 -> NockmaMemRepListConstrCons + _ -> impossible + | otherwise -> Nothing + _ -> Nothing + +supportsMaybeNockmaRep :: Tree.InfoTable -> Tree.ConstructorInfo -> Maybe NockmaMemRep +supportsMaybeNockmaRep tab ci = + NockmaMemRepMaybe <$> case allConstructors tab ci of + c1 :| [c2] + | [0, 1] `elem` permutations ((^. Tree.constructorArgsNum) <$> [c1, c2]) -> Just $ case ci ^. Tree.constructorArgsNum of + 0 -> NockmaMemRepMaybeConstrNothing + 1 -> NockmaMemRepMaybeConstrJust + _ -> impossible + | otherwise -> Nothing + _ -> Nothing -- | Use `Tree.toNockma` before calling this function fromTreeTable :: (Members '[Error JuvixError, Reader CompilerOptions] r) => Tree.InfoTable -> Sem r AnomaResult @@ -253,7 +271,7 @@ fromTreeTable t = case t ^. Tree.infoMainFunction of } where rep :: NockmaMemRep - rep = maybe r NockmaMemRepList (supportsListNockmaRep tab ci) + rep = fromMaybe r (supportsListNockmaRep tab ci <|> supportsMaybeNockmaRep tab ci) where r = nockmaMemRep (memRep ci (getInductiveInfo (ci ^. Tree.constructorInductive))) @@ -372,6 +390,10 @@ compile = \case NockmaMemRepList constr -> case constr of NockmaMemRepListConstrNil -> impossible NockmaMemRepListConstrCons -> fr ++ indexTuple 2 argIx + NockmaMemRepMaybe constr -> case constr of + NockmaMemRepMaybeConstrNothing -> impossible + -- just x is represented as [0 x] so argument index is offset by 1. + NockmaMemRepMaybeConstrJust -> fr ++ indexTuple 2 (argIx + 1) (opAddress "constrRef") <$> path where goDirectRef :: Tree.DirectRef -> Sem r (Term Natural) @@ -729,6 +751,13 @@ goConstructor mr t args = case t of NockmaMemRepListConstrCons -> case args of [l, r] -> TCell l r _ -> impossible + NockmaMemRepMaybe constr -> case constr of + NockmaMemRepMaybeConstrNothing + | null args -> (OpQuote # nockNilTagged "maybe-constr-nothing") + | otherwise -> impossible + NockmaMemRepMaybeConstrJust -> case args of + [x] -> TCell (OpQuote # nockNilTagged "maybe-constr-just-head") x + _ -> impossible unsupported :: Text -> a unsupported thing = error ("The Nockma backend does not support " <> thing) @@ -965,6 +994,9 @@ caseCmd arg defaultBranch = \case NockmaMemRepList constr -> do bs' <- mapM (firstM asNockmaMemRepListConstr) bs return (goRepList ((constr, b) :| bs')) + NockmaMemRepMaybe constr -> do + bs' <- mapM (firstM asNockmaMemRepMaybeConstr) bs + return (goRepMaybe ((constr, b) :| bs')) where goRepConstr :: Tree.Tag -> @@ -993,6 +1025,15 @@ caseCmd arg defaultBranch = \case _ -> impossible Tree.BuiltinTag {} -> impossible + asNockmaMemRepMaybeConstr :: Tree.Tag -> Sem r NockmaMemRepMaybeConstr + asNockmaMemRepMaybeConstr tag = case tag of + Tree.UserTag {} -> do + rep <- getConstructorMemRep tag + case rep of + NockmaMemRepMaybe constr -> return constr + _ -> impossible + Tree.BuiltinTag {} -> impossible + goBoolTag :: Bool -> Term Natural -> @@ -1021,6 +1062,17 @@ caseCmd arg defaultBranch = \case f :: (NockmaMemRepListConstr, Term Natural) -> Maybe (Term Natural) f (c', br) = guard (c /= c') $> br + goRepMaybe :: NonEmpty (NockmaMemRepMaybeConstr, Term Natural) -> Term Natural + goRepMaybe ((c, b) :| bs) = + let cond = OpIsCell # arg + otherBranch = fromMaybe crash (firstJust f bs <|> defaultBranch) + in case c of + NockmaMemRepMaybeConstrJust -> branch cond b otherBranch + NockmaMemRepMaybeConstrNothing -> branch cond otherBranch b + where + f :: (NockmaMemRepMaybeConstr, Term Natural) -> Maybe (Term Natural) + f (c', br) = guard (c /= c') $> br + branch :: Term Natural -> Term Natural -> diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index c6a395868a..3843af88ba 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -583,5 +583,16 @@ allTests = $(mkRelDir ".") $(mkRelFile "test079.juvix") [OpQuote # inputStr] - $ checkOutput [[nock| "Juvix! ✨ héllo world ✨" |]] + $ checkOutput [[nock| "Juvix! ✨ héllo world ✨" |]], + mkAnomaCallTest + "Test080: Maybe" + $(mkRelDir ".") + $(mkRelFile "test080.juvix") + [] + $ checkOutput + [ [nock| [nil 1] |], + [nock| 2 |], + [nock| 3 |], + [nock| nil |] + ] ] diff --git a/tests/Anoma/Compilation/positive/test080.juvix b/tests/Anoma/Compilation/positive/test080.juvix new file mode 100644 index 0000000000..bf39ebf72f --- /dev/null +++ b/tests/Anoma/Compilation/positive/test080.juvix @@ -0,0 +1,20 @@ +module test080; + +import Stdlib.Prelude open; +import Stdlib.Debug.Trace open; + +main : Maybe Nat := + trace (just 1) + >-> trace + {Nat} + case just 2 of { + | just x := x + | nothing := 0 + } + >-> trace + {Nat} + case nothing {Nat} of { + | just x := 0 + | nothing := 3 + } + >-> nothing;