Skip to content

Commit

Permalink
Support Anoma representation of Maybe
Browse files Browse the repository at this point in the history
  • Loading branch information
paulcadman committed Jun 25, 2024
1 parent 6d24d71 commit 8f0a665
Show file tree
Hide file tree
Showing 3 changed files with 94 additions and 11 deletions.
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;

0 comments on commit 8f0a665

Please sign in to comment.