Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support Anoma representation of Maybe #2856

Merged
merged 2 commits into from
Jun 26, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
72 changes: 62 additions & 10 deletions src/Juvix/Compiler/Nockma/Translation/FromTree.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)))

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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 ->
Expand Down
13 changes: 12 additions & 1 deletion test/Anoma/Compilation/Positive.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 |]
]
]
20 changes: 20 additions & 0 deletions tests/Anoma/Compilation/positive/test080.juvix
Original file line number Diff line number Diff line change
@@ -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;
Loading