From 445376e338108a030595b5b131ae0418caa2e201 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Tue, 20 Dec 2022 11:17:39 +0100 Subject: [PATCH] Conversion of Nat representation to JuvixCore integers (#1661) * nat to int wip * nat to int wip * fix condition * nats in core * bugfixes * tests * make ormolu happy * fix case --- src/Juvix/Compiler/Core/Data/BinderList.hs | 12 +- src/Juvix/Compiler/Core/Data/InfoTable.hs | 16 ++- .../Compiler/Core/Data/InfoTableBuilder.hs | 15 +++ .../Compiler/Core/Data/TransformationId.hs | 1 + .../Core/Data/TransformationId/Parser.hs | 5 + src/Juvix/Compiler/Core/Evaluator.hs | 4 +- src/Juvix/Compiler/Core/Extra/Base.hs | 21 ++-- .../Compiler/Core/Extra/Recursors/Map.hs | 8 ++ .../Core/Extra/Recursors/Map/Named.hs | 58 ++++++---- .../Compiler/Core/Extra/Stripped/Base.hs | 4 +- src/Juvix/Compiler/Core/Keywords.hs | 2 + src/Juvix/Compiler/Core/Language/Nodes.hs | 3 +- src/Juvix/Compiler/Core/Pretty/Base.hs | 49 ++++++--- src/Juvix/Compiler/Core/Transformation.hs | 2 + .../Core/Transformation/LambdaLifting.hs | 6 +- .../Compiler/Core/Transformation/NatToInt.hs | 93 ++++++++++++++++ .../Core/Transformation/RemoveTypeArgs.hs | 2 +- .../Compiler/Core/Translation/FromInternal.hs | 21 ++-- .../Compiler/Core/Translation/FromSource.hs | 103 +++++++++++++----- test/Core/Eval/Positive.hs | 7 +- test/Core/Transformation.hs | 4 +- .../{RemoveTypeArgs.hs => Pipeline.hs} | 6 +- tests/Core/positive/out/test047.out | 3 + tests/Core/positive/test029.jvc | 10 +- tests/Core/positive/test046.jvc | 2 +- tests/Core/positive/test047.jvc | 38 +++++++ 26 files changed, 387 insertions(+), 108 deletions(-) create mode 100644 src/Juvix/Compiler/Core/Transformation/NatToInt.hs rename test/Core/Transformation/{RemoveTypeArgs.hs => Pipeline.hs} (64%) create mode 100644 tests/Core/positive/out/test047.out create mode 100644 tests/Core/positive/test047.jvc diff --git a/src/Juvix/Compiler/Core/Data/BinderList.hs b/src/Juvix/Compiler/Core/Data/BinderList.hs index f6722d99a..514c760f0 100644 --- a/src/Juvix/Compiler/Core/Data/BinderList.hs +++ b/src/Juvix/Compiler/Core/Data/BinderList.hs @@ -1,6 +1,6 @@ module Juvix.Compiler.Core.Data.BinderList where -import Juvix.Compiler.Core.Language hiding (cons, lookup, uncons) +import Juvix.Compiler.Core.Language hiding (cons, drop, lookup, uncons) import Juvix.Prelude qualified as Prelude -- | if we have \x\y. b, the binderlist in b is [y, x] @@ -14,11 +14,11 @@ makeLenses ''BinderList fromList :: [a] -> BinderList a fromList l = BinderList (length l) l -drop' :: Int -> BinderList a -> BinderList a -drop' k (BinderList n l) = BinderList (n - k) (dropExact k l) +drop :: Int -> BinderList a -> BinderList a +drop k (BinderList n l) = BinderList (n - k) (dropExact k l) -tail' :: BinderList a -> BinderList a -tail' = snd . fromJust . uncons +tail :: BinderList a -> BinderList a +tail = snd . fromJust . uncons uncons :: BinderList a -> Maybe (a, BinderList a) uncons l = second helper <$> Prelude.uncons (l ^. blMap) @@ -60,7 +60,7 @@ lookupsSortedRev bl = go [] 0 bl (v : vs) -> let skipped = v ^. varIndex - off off' = off + skipped - ctx' = drop' skipped ctx + ctx' = drop skipped ctx in go ((v, head' ctx') : acc) off' ctx' vs head' :: BinderList a -> a head' = lookup 0 diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs index 78954da93..79787ff5d 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs @@ -1,5 +1,10 @@ -module Juvix.Compiler.Core.Data.InfoTable where +module Juvix.Compiler.Core.Data.InfoTable + ( module Juvix.Compiler.Core.Data.InfoTable, + module Juvix.Compiler.Concrete.Data.Builtins, + ) +where +import Juvix.Compiler.Concrete.Data.Builtins import Juvix.Compiler.Core.Language type IdentContext = HashMap Symbol Node @@ -43,7 +48,8 @@ data IdentifierInfo = IdentifierInfo _identifierType :: Type, _identifierArgsNum :: Int, _identifierArgsInfo :: [ArgumentInfo], - _identifierIsExported :: Bool + _identifierIsExported :: Bool, + _identifierBuiltin :: Maybe BuiltinFunction } data ArgumentInfo = ArgumentInfo @@ -60,7 +66,8 @@ data InductiveInfo = InductiveInfo _inductiveKind :: Type, _inductiveConstructors :: [ConstructorInfo], _inductiveParams :: [ParameterInfo], - _inductivePositive :: Bool + _inductivePositive :: Bool, + _inductiveBuiltin :: Maybe BuiltinInductive } data ConstructorInfo = ConstructorInfo @@ -69,7 +76,8 @@ data ConstructorInfo = ConstructorInfo _constructorTag :: Tag, _constructorType :: Type, _constructorArgsNum :: Int, - _constructorInductive :: Symbol + _constructorInductive :: Symbol, + _constructorBuiltin :: Maybe BuiltinConstructor } data ParameterInfo = ParameterInfo diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs index d0a9dda98..8293f5aa3 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs @@ -24,6 +24,21 @@ getConstructorInfo tag = do tab <- getInfoTable return $ fromJust (HashMap.lookup tag (tab ^. infoConstructors)) +getInductiveInfo :: Member InfoTableBuilder r => Symbol -> Sem r InductiveInfo +getInductiveInfo sym = do + tab <- getInfoTable + return $ fromJust (HashMap.lookup sym (tab ^. infoInductives)) + +getIdentifierInfo :: Member InfoTableBuilder r => Symbol -> Sem r IdentifierInfo +getIdentifierInfo sym = do + tab <- getInfoTable + return $ fromJust (HashMap.lookup sym (tab ^. infoIdentifiers)) + +getBoolSymbol :: Member InfoTableBuilder r => Sem r Symbol +getBoolSymbol = do + ci <- getConstructorInfo (BuiltinTag TagTrue) + return $ ci ^. constructorInductive + checkSymbolDefined :: Member InfoTableBuilder r => Symbol -> Sem r Bool checkSymbolDefined sym = do tab <- getInfoTable diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs index ea0d2c981..6c8033b80 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs @@ -7,5 +7,6 @@ data TransformationId | TopEtaExpand | RemoveTypeArgs | MoveApps + | NatToInt | Identity deriving stock (Data) diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs index 981d61edc..668a7116c 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs @@ -46,6 +46,7 @@ pcompletions = do Identity -> strIdentity RemoveTypeArgs -> strRemoveTypeArgs MoveApps -> strMoveApps + NatToInt -> strNatToInt lexeme :: MonadParsec e Text m => m a -> m a lexeme = L.lexeme L.hspace @@ -63,6 +64,7 @@ transformation = <|> symbol strTopEtaExpand $> TopEtaExpand <|> symbol strRemoveTypeArgs $> RemoveTypeArgs <|> symbol strMoveApps $> MoveApps + <|> symbol strNatToInt $> NatToInt allStrings :: [Text] allStrings = @@ -87,3 +89,6 @@ strRemoveTypeArgs = "remove-type-args" strMoveApps :: Text strMoveApps = "move-apps" + +strNatToInt :: Text +strNatToInt = "nat-to-int" diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 58d8f6ffa..8ccdfea35 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -70,10 +70,10 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0 let !vs' = map (eval' env' . (^. letItemValue)) (toList vs) !env' = revAppend vs' env in foldr GHC.pseq (eval' env' b) vs' - NCase (Case i v bs def) -> + NCase (Case i sym v bs def) -> case eval' env v of NCtr (Constr _ tag args) -> branch n env args tag def bs - v' -> evalError "matching on non-data" (substEnv env (mkCase i v' bs def)) + v' -> evalError "matching on non-data" (substEnv env (mkCase i sym v' bs def)) NMatch (Match _ vs bs) -> let !vs' = map' (eval' env) (toList vs) in match n env vs' bs diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs index eec05574a..206d9b373 100644 --- a/src/Juvix/Compiler/Core/Extra/Base.hs +++ b/src/Juvix/Compiler/Core/Extra/Base.hs @@ -55,6 +55,9 @@ mkLambda i bi b = NLam (Lambda i bi b) mkLambda' :: Node -> Node mkLambda' = mkLambda Info.empty emptyBinder +mkLambdaTy :: Node -> Node -> Node +mkLambdaTy ty = mkLambda Info.empty (Binder "?" Nothing ty) + mkLetItem' :: Node -> LetItem mkLetItem' = LetItem emptyBinder @@ -70,10 +73,10 @@ mkLetRec i vs b = NRec (LetRec i vs b) mkLetRec' :: NonEmpty Node -> Node -> Node mkLetRec' = mkLetRec Info.empty . fmap mkLetItem' -mkCase :: Info -> Node -> [CaseBranch] -> Maybe Node -> Node -mkCase i v bs def = NCase (Case i v bs def) +mkCase :: Info -> Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node +mkCase i sym v bs def = NCase (Case i sym v bs def) -mkCase' :: Node -> [CaseBranch] -> Maybe Node -> Node +mkCase' :: Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node mkCase' = mkCase Info.empty mkMatch :: Info -> NonEmpty Node -> [MatchBranch] -> Node @@ -82,8 +85,8 @@ mkMatch i vs bs = NMatch (Match i vs bs) mkMatch' :: NonEmpty Node -> [MatchBranch] -> Node mkMatch' = mkMatch Info.empty -mkIf :: Info -> Node -> Node -> Node -> Node -mkIf i v b1 b2 = mkCase i v [br] (Just b2) +mkIf :: Info -> Symbol -> Node -> Node -> Node -> Node +mkIf i sym v b1 b2 = mkCase i sym v [br] (Just b2) where br = CaseBranch @@ -94,7 +97,7 @@ mkIf i v b1 b2 = mkCase i v [br] (Just b2) _caseBranchBody = b1 } -mkIf' :: Node -> Node -> Node -> Node +mkIf' :: Symbol -> Node -> Node -> Node -> Node mkIf' = mkIf Info.empty {------------------------------------------------------------------------} @@ -480,7 +483,7 @@ destruct = \case ] in mkLetRec i' items' (b' ^. childNode) } - NCase (Case i v brs mdef) -> + NCase (Case i sym v brs mdef) -> let branchChildren :: [([Binder], NodeChild)] branchChildren = [ (binders, manyBinders binders (br ^. caseBranchBody)) @@ -520,7 +523,7 @@ destruct = \case _nodeSubinfos = map (^. caseBranchInfo) brs, _nodeChildren = noBinders v : allNodes, _nodeReassemble = someChildrenI $ \i' is' (v' :| allNodes') -> - mkCase i' (v' ^. childNode) (mkBranches is' allNodes') Nothing + mkCase i' sym (v' ^. childNode) (mkBranches is' allNodes') Nothing } Just def -> NodeDetails @@ -528,7 +531,7 @@ destruct = \case _nodeSubinfos = map (^. caseBranchInfo) brs, _nodeChildren = noBinders v : noBinders def : allNodes, _nodeReassemble = twoManyChildrenI $ \i' is' v' def' allNodes' -> - mkCase i' (v' ^. childNode) (mkBranches is' allNodes') (Just (def' ^. childNode)) + mkCase i' sym (v' ^. childNode) (mkBranches is' allNodes') (Just (def' ^. childNode)) } NMatch (Match i vs branches) -> let allNodes :: [NodeChild] diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs index f8aee1435..c7f2bf0f6 100644 --- a/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs +++ b/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs @@ -112,6 +112,14 @@ fromRecur c = fromPair :: Functor g => d -> g (c, Node) -> g (Recur' (c, d)) fromPair d = fmap (\(c, x) -> Recur' ((c, d), x)) +fromRecur' :: Functor g => d -> g (Recur' c) -> g (Recur' (c, d)) +fromRecur' d = + fmap + ( \case + End' x -> End' x + Recur' (c, x) -> Recur' ((c, d), x) + ) + nodeMapG' :: Monad m => Sing dir -> diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs index 1ea522929..3d0ab8fe7 100644 --- a/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs +++ b/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs @@ -6,21 +6,21 @@ import Juvix.Compiler.Core.Extra.Recursors.Map import Juvix.Compiler.Core.Extra.Recursors.Parameters dmapLRM :: Monad m => (BinderList Binder -> Node -> m Recur) -> Node -> m Node -dmapLRM f = nodeMapG' STopDown binderInfoCollector (\bi -> fromRecur bi . f bi) +dmapLRM f = dmapLRM' (mempty, f) dmapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node -dmapLM f = nodeMapG' STopDown binderInfoCollector (\bi -> fromSimple bi . f bi) +dmapLM f = dmapLM' (mempty, f) umapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node umapLM f = nodeMapG' SBottomUp binderInfoCollector f -dmapNRM :: Monad m => (Index -> Node -> m Recur) -> Node -> m Node -dmapNRM f = nodeMapG' STopDown binderNumCollector (\bi -> fromRecur bi . f bi) +dmapNRM :: Monad m => (Level -> Node -> m Recur) -> Node -> m Node +dmapNRM f = dmapNRM' (0, f) -dmapNM :: Monad m => (Index -> Node -> m Node) -> Node -> m Node -dmapNM f = nodeMapG' STopDown binderNumCollector (\bi -> fromSimple bi . f bi) +dmapNM :: Monad m => (Level -> Node -> m Node) -> Node -> m Node +dmapNM f = dmapNM' (0, f) -umapNM :: Monad m => (Index -> Node -> m Node) -> Node -> m Node +umapNM :: Monad m => (Level -> Node -> m Node) -> Node -> m Node umapNM f = nodeMapG' SBottomUp binderNumCollector f dmapRM :: Monad m => (Node -> m Recur) -> Node -> m Node @@ -41,13 +41,13 @@ dmapLM' f = nodeMapG' STopDown (binderInfoCollector' (fst f)) (\bi -> fromSimple umapLM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Node) -> Node -> m Node umapLM' f = nodeMapG' SBottomUp (binderInfoCollector' (fst f)) (snd f) -dmapNRM' :: Monad m => (Index, Index -> Node -> m Recur) -> Node -> m Node +dmapNRM' :: Monad m => (Level, Level -> Node -> m Recur) -> Node -> m Node dmapNRM' f = nodeMapG' STopDown (binderNumCollector' (fst f)) (\bi -> fromRecur bi . snd f bi) -dmapNM' :: Monad m => (Index, Index -> Node -> m Node) -> Node -> m Node +dmapNM' :: Monad m => (Level, Level -> Node -> m Node) -> Node -> m Node dmapNM' f = nodeMapG' STopDown (binderNumCollector' (fst f)) (\bi -> fromSimple bi . snd f bi) -umapNM' :: Monad m => (Index, Index -> Node -> m Node) -> Node -> m Node +umapNM' :: Monad m => (Level, Level -> Node -> m Node) -> Node -> m Node umapNM' f = nodeMapG' SBottomUp (binderNumCollector' (fst f)) (snd f) dmapLR :: (BinderList Binder -> Node -> Recur) -> Node -> Node @@ -59,13 +59,13 @@ dmapL f = runIdentity . dmapLM (embedIden f) umapL :: (BinderList Binder -> Node -> Node) -> Node -> Node umapL f = runIdentity . umapLM (embedIden f) -dmapNR :: (Index -> Node -> Recur) -> Node -> Node +dmapNR :: (Level -> Node -> Recur) -> Node -> Node dmapNR f = runIdentity . dmapNRM (embedIden f) -dmapN :: (Index -> Node -> Node) -> Node -> Node +dmapN :: (Level -> Node -> Node) -> Node -> Node dmapN f = runIdentity . dmapNM (embedIden f) -umapN :: (Index -> Node -> Node) -> Node -> Node +umapN :: (Level -> Node -> Node) -> Node -> Node umapN f = runIdentity . umapNM (embedIden f) dmapR :: (Node -> Recur) -> Node -> Node @@ -86,28 +86,46 @@ dmapL' f = runIdentity . dmapLM' (embedIden f) umapL' :: (BinderList Binder, BinderList Binder -> Node -> Node) -> Node -> Node umapL' f = runIdentity . umapLM' (embedIden f) -dmapNR' :: (Index, Index -> Node -> Recur) -> Node -> Node +dmapNR' :: (Level, Level -> Node -> Recur) -> Node -> Node dmapNR' f = runIdentity . dmapNRM' (embedIden f) -dmapN' :: (Index, Index -> Node -> Node) -> Node -> Node +dmapN' :: (Level, Level -> Node -> Node) -> Node -> Node dmapN' f = runIdentity . dmapNM' (embedIden f) -umapN' :: (Index, Index -> Node -> Node) -> Node -> Node +umapN' :: (Level, Level -> Node -> Node) -> Node -> Node umapN' f = runIdentity . umapNM' (embedIden f) -dmapCLM :: Monad m => (c -> BinderList Binder -> Node -> m (c, Node)) -> c -> Node -> m Node -dmapCLM f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) binderInfoCollector) (\(c, bi) -> fromPair bi . f c bi) +dmapCLM' :: Monad m => (BinderList Binder, c -> BinderList Binder -> Node -> m (c, Node)) -> c -> Node -> m Node +dmapCLM' f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) (binderInfoCollector' (fst f))) (\(c, bi) -> fromPair bi . snd f c bi) -dmapCNM :: Monad m => (c -> Index -> Node -> m (c, Node)) -> c -> Node -> m Node +dmapCLRM' :: Monad m => (BinderList Binder, c -> BinderList Binder -> Node -> m (Recur' c)) -> c -> Node -> m Node +dmapCLRM' f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) (binderInfoCollector' (fst f))) (\(c, bi) -> fromRecur' bi . snd f c bi) + +dmapCNRM' :: Monad m => (Level, c -> Level -> Node -> m (Recur' c)) -> c -> Node -> m Node +dmapCNRM' f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) (binderNumCollector' (fst f))) (\(c, bi) -> fromRecur' bi . snd f c bi) + +dmapCLM :: Monad m => (c -> BinderList Binder -> Node -> m (c, Node)) -> c -> Node -> m Node +dmapCLM f = dmapCLM' (mempty, f) + +dmapCNM :: Monad m => (c -> Level -> Node -> m (c, Node)) -> c -> Node -> m Node dmapCNM f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) binderNumCollector) (\(c, bi) -> fromPair bi . f c bi) dmapCM :: Monad m => (c -> Node -> m (c, Node)) -> c -> Node -> m Node dmapCM f ini = nodeMapG' STopDown (identityCollector ini) (\c -> fmap Recur' . f c) +dmapCL' :: (BinderList Binder, c -> BinderList Binder -> Node -> (c, Node)) -> c -> Node -> Node +dmapCL' f ini = runIdentity . dmapCLM' (embedIden f) ini + +dmapCLR' :: (BinderList Binder, c -> BinderList Binder -> Node -> Recur' c) -> c -> Node -> Node +dmapCLR' f ini = runIdentity . dmapCLRM' (embedIden f) ini + +dmapCNR' :: (Level, c -> Level -> Node -> Recur' c) -> c -> Node -> Node +dmapCNR' f ini = runIdentity . dmapCNRM' (embedIden f) ini + dmapCL :: (c -> BinderList Binder -> Node -> (c, Node)) -> c -> Node -> Node dmapCL f ini = runIdentity . dmapCLM (embedIden f) ini -dmapCN :: (c -> Index -> Node -> (c, Node)) -> c -> Node -> Node +dmapCN :: (c -> Level -> Node -> (c, Node)) -> c -> Node -> Node dmapCN f ini = runIdentity . dmapCNM (embedIden f) ini dmapC :: (c -> Node -> (c, Node)) -> c -> Node -> Node diff --git a/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs b/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs index 60e532be4..80e9a73bf 100644 --- a/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs +++ b/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs @@ -52,5 +52,5 @@ mkLet i v b = NLet (Let i item b) mkLet' :: Node -> Node -> Node mkLet' = mkLet (LetInfo "" Nothing TyDynamic) -mkCase :: CaseInfo -> Node -> [CaseBranch] -> Maybe Node -> Node -mkCase ci v bs def = NCase (Case ci v bs def) +mkCase :: CaseInfo -> Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node +mkCase ci sym v bs def = NCase (Case ci sym v bs def) diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs index a22fcf553..e02c4e45d 100644 --- a/src/Juvix/Compiler/Core/Keywords.hs +++ b/src/Juvix/Compiler/Core/Keywords.hs @@ -10,6 +10,7 @@ import Juvix.Data.Keyword.All ( kwAny, kwAssign, kwBind, + kwBuiltin, kwCase, kwColon, kwComma, @@ -52,6 +53,7 @@ allKeywordStrings = keywordsStrings allKeywords allKeywords :: [Keyword] allKeywords = [ kwAssign, + kwBuiltin, kwLet, kwLetRec, kwIn, diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs index 54a3ba63c..93a864dcd 100644 --- a/src/Juvix/Compiler/Core/Language/Nodes.hs +++ b/src/Juvix/Compiler/Core/Language/Nodes.hs @@ -114,6 +114,7 @@ data LetRec' i a ty = LetRec -- branches default`. `Case` is lazy: only the selected branch is evaluated. data Case' i bi a = Case { _caseInfo :: i, + _caseInductive :: Symbol, _caseValue :: !a, _caseBranches :: ![CaseBranch' bi a], _caseDefault :: !(Maybe a) @@ -338,7 +339,7 @@ instance Eq a => Eq (Constr' i a) where (Constr _ tag1 args1) == (Constr _ tag2 args2) = tag1 == tag2 && args1 == args2 instance Eq a => Eq (Case' i bi a) where - (Case _ v1 bs1 def1) == (Case _ v2 bs2 def2) = v1 == v2 && bs1 == bs2 && def1 == def2 + (Case _ sym1 v1 bs1 def1) == (Case _ sym2 v2 bs2 def2) = sym1 == sym2 && v1 == v2 && bs1 == bs2 && def1 == def2 instance Eq a => Eq (CaseBranch' i a) where (==) = diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 1dac5d722..6eed97173 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -158,20 +158,32 @@ ppCodeLet' name mty lt = do return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <> line <> b' ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Text]] -> [Text] -> Case' i bi a -> Sem r (Doc Ann) -ppCodeCase' branchBinderNames branchTagNames Case {..} = do - let branchBodies = map (^. caseBranchBody) _caseBranches - bns <- mapM (mapM (ppName KNameLocal)) branchBinderNames - cns <- mapM (ppName KNameConstructor) branchTagNames - v <- ppCode _caseValue - bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwAssign <+> br') cns bns branchBodies - bs'' <- - case _caseDefault of - Just def -> do - d' <- ppCode def - return $ bs' ++ [kwDefault <+> kwAssign <+> d'] - Nothing -> return bs' - let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs'' - return $ kwCase <+> v <+> kwOf <+> bss +ppCodeCase' branchBinderNames branchTagNames Case {..} = + case _caseBranches of + [CaseBranch _ (BuiltinTag TagTrue) _ _ br1, CaseBranch _ (BuiltinTag TagTrue) _ _ br2] -> do + br1' <- ppCode br1 + br2' <- ppCode br2 + v <- ppCode _caseValue + return $ kwIf <+> v <+> kwThen <+> br1' <+> kwElse <+> br2' + [CaseBranch _ (BuiltinTag TagTrue) _ _ br1] | isJust _caseDefault -> do + br1' <- ppCode br1 + br2' <- ppCode (fromJust _caseDefault) + v <- ppCode _caseValue + return $ kwIf <+> v <+> kwThen <+> br1' <+> kwElse <+> br2' + _ -> do + let branchBodies = map (^. caseBranchBody) _caseBranches + bns <- mapM (mapM (ppName KNameLocal)) branchBinderNames + cns <- mapM (ppName KNameConstructor) branchTagNames + v <- ppCode _caseValue + bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwAssign <+> br') cns bns branchBodies + bs'' <- + case _caseDefault of + Just def -> do + d' <- ppCode def + return $ bs' ++ [kwDefault <+> kwAssign <+> d'] + Nothing -> return bs' + let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs'' + return $ kwCase <+> v <+> kwOf <+> bss instance PrettyCode PatternWildcard where ppCode _ = return kwWildcard @@ -505,6 +517,15 @@ kwMatch = keyword Str.match_ kwWith :: Doc Ann kwWith = keyword Str.with_ +kwIf :: Doc Ann +kwIf = keyword Str.if_ + +kwThen :: Doc Ann +kwThen = keyword Str.then_ + +kwElse :: Doc Ann +kwElse = keyword Str.else_ + kwDefault :: Doc Ann kwDefault = keyword Str.underscore diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index ac5e55779..b1e192844 100644 --- a/src/Juvix/Compiler/Core/Transformation.hs +++ b/src/Juvix/Compiler/Core/Transformation.hs @@ -14,6 +14,7 @@ import Juvix.Compiler.Core.Transformation.Eta import Juvix.Compiler.Core.Transformation.Identity import Juvix.Compiler.Core.Transformation.LambdaLifting import Juvix.Compiler.Core.Transformation.MoveApps +import Juvix.Compiler.Core.Transformation.NatToInt import Juvix.Compiler.Core.Transformation.RemoveTypeArgs import Juvix.Compiler.Core.Transformation.TopEtaExpand @@ -27,3 +28,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts TopEtaExpand -> topEtaExpand RemoveTypeArgs -> removeTypeArgs MoveApps -> moveApps + NatToInt -> natToInt diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs index 0d4282a53..26afc4ffd 100644 --- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs +++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs @@ -57,7 +57,8 @@ lambdaLiftNode aboveBl top = _identifierType = typeFromArgs argsInfo, _identifierArgsNum = length allfreevars, _identifierArgsInfo = argsInfo, - _identifierIsExported = False + _identifierIsExported = False, + _identifierBuiltin = Nothing } registerIdentNode f fBody' let fApp = mkApps' (mkIdent mempty f) (map NVar allfreevars) @@ -117,7 +118,8 @@ lambdaLiftNode aboveBl top = _identifierType = typeFromArgs argsInfo, _identifierArgsNum = length recItemsFreeVars, _identifierArgsInfo = argsInfo, - _identifierIsExported = False + _identifierIsExported = False, + _identifierBuiltin = Nothing } | (sym, (itemBinder, b)) <- zipExact topSyms (zipExact letRecBinders' liftedDefs) ] diff --git a/src/Juvix/Compiler/Core/Transformation/NatToInt.hs b/src/Juvix/Compiler/Core/Transformation/NatToInt.hs new file mode 100644 index 000000000..b2d9dff51 --- /dev/null +++ b/src/Juvix/Compiler/Core/Transformation/NatToInt.hs @@ -0,0 +1,93 @@ +module Juvix.Compiler.Core.Transformation.NatToInt (natToInt) where + +import Data.HashMap.Strict qualified as HashMap +import Data.List qualified as List +import Juvix.Compiler.Core.Extra +import Juvix.Compiler.Core.Info qualified as Info +import Juvix.Compiler.Core.Info.NameInfo +import Juvix.Compiler.Core.Transformation.Base + +convertNode :: InfoTable -> Node -> Node +convertNode tab = convert [] 0 + where + convert :: [Level] -> Level -> Node -> Node + convert levels bl node = dmapCNR' (bl, go) levels node + + go :: [Level] -> Level -> Node -> Recur' [Level] + go levels bl node = case node of + NVar (Var {..}) -> + End' (mkVar _varInfo (_varIndex + length (filter (\x -> x >= bl - _varIndex) levels))) + NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) -> + Recur' (levels, convertIdentApp node (\op -> mkBuiltinApp _identInfo op [l, r]) _identSymbol) + NApp (App _ (NIdt (Ident {..})) l) -> + Recur' (levels, convertIdentApp node (\op -> mkLambdaTy mkTypeInteger' $ mkBuiltinApp _identInfo op [l, mkVar' 0]) _identSymbol) + NIdt (Ident {..}) -> + Recur' + ( levels, + convertIdentApp + node + ( \op -> + mkLambdaTy mkTypeInteger' $ + mkLambdaTy mkTypeInteger' $ + mkBuiltinApp _identInfo op [mkVar' 1, mkVar' 0] + ) + _identSymbol + ) + NCtr (Constr {..}) -> + let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors) + in case ci ^. constructorBuiltin of + Just BuiltinNatZero -> + Recur' (levels, mkConstant _constrInfo (ConstInteger 0)) + Just BuiltinNatSuc -> + Recur' (levels, mkBuiltinApp _constrInfo OpIntAdd (_constrArgs ++ [mkConstant' (ConstInteger 1)])) + _ -> Recur' (levels, node) + NCase (Case {..}) -> + let ii = fromJust $ HashMap.lookup _caseInductive (tab ^. infoInductives) + in case ii ^. inductiveBuiltin of + Just BuiltinNat -> + case _caseBranches of + [br] -> makeIf br (maybeBranch _caseDefault) + [br1, br2] -> + if + | br1 ^. caseBranchBindersNum == 1 && br2 ^. caseBranchBindersNum == 0 -> + makeIf br1 (br2 ^. caseBranchBody) + | br2 ^. caseBranchBindersNum == 1 && br1 ^. caseBranchBindersNum == 0 -> + makeIf br2 (br1 ^. caseBranchBody) + | otherwise -> + impossible + [] -> Recur' (levels, fromJust _caseDefault) + _ -> impossible + _ -> Recur' (levels, node) + where + makeIf :: CaseBranch -> Node -> Recur' [Level] + makeIf CaseBranch {..} br = + let ci = fromJust $ HashMap.lookup (BuiltinTag TagTrue) (tab ^. infoConstructors) + sym = ci ^. constructorInductive + in case _caseBranchBindersNum of + 0 -> + Recur' (levels, mkIf _caseInfo sym (mkBuiltinApp' OpEq [_caseValue, mkConstant' (ConstInteger 0)]) _caseBranchBody br) + 1 -> + End' $ + mkLet mempty (emptyBinder {_binderName = name}) (mkBuiltinApp' OpIntSub [convert levels bl _caseValue, mkConstant' (ConstInteger 1)]) $ + mkIf + _caseInfo + sym + (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), mkVar (Info.singleton (NameInfo name)) 0]) + (convert levels (bl + 1) _caseBranchBody) + (convert (bl : levels) bl br) + where + name = List.head _caseBranchBinders ^. binderName + _ -> impossible + maybeBranch :: Maybe Node -> Node + maybeBranch = fromMaybe (mkBuiltinApp' OpFail [mkConstant' (ConstString "no matching branch")]) + _ -> Recur' (levels, node) + + convertIdentApp :: Node -> (BuiltinOp -> Node) -> Symbol -> Node + convertIdentApp node f sym = + let ii = fromJust $ HashMap.lookup sym (tab ^. infoIdentifiers) + in case ii ^. identifierBuiltin of + Just BuiltinNatPlus -> f OpIntAdd + _ -> node + +natToInt :: InfoTable -> InfoTable +natToInt tab = mapT (const (convertNode tab)) tab diff --git a/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs b/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs index db66166f9..f816ded69 100644 --- a/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs +++ b/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs @@ -49,7 +49,7 @@ convertNode tab = convert mempty args' = filterArgs ty _constrArgs in End (mkConstr _constrInfo _constrTag (map (convert vars) args')) NCase (Case {..}) -> - End (mkCase _caseInfo (convert vars _caseValue) (map convertBranch _caseBranches) (fmap (convert vars) _caseDefault)) + End (mkCase _caseInfo _caseInductive (convert vars _caseValue) (map convertBranch _caseBranches) (fmap (convert vars) _caseDefault)) where convertBranch :: CaseBranch -> CaseBranch convertBranch br@CaseBranch {..} = diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 35b8a106f..e973b008a 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -121,7 +121,8 @@ goInductiveDef i = do _inductiveKind = mkDynamic', _inductiveConstructors = ctorInfos, _inductiveParams = [], - _inductivePositive = i ^. Internal.inductivePositive + _inductivePositive = i ^. Internal.inductivePositive, + _inductiveBuiltin = i ^. Internal.inductiveBuiltin } registerInductive (mkIdentIndex (i ^. Internal.inductiveName)) info @@ -132,7 +133,8 @@ goConstructor :: Internal.InductiveConstructorDef -> Sem r ConstructorInfo goConstructor sym ctor = do - tag <- mBuiltin >>= ctorTag + mblt <- mBuiltin + tag <- ctorTag mblt ty <- ctorType let info = ConstructorInfo @@ -141,7 +143,8 @@ goConstructor sym ctor = do _constructorTag = tag, _constructorType = ty, _constructorArgsNum = length (ctor ^. Internal.inductiveConstructorParameters), - _constructorInductive = sym + _constructorInductive = sym, + _constructorBuiltin = mblt } registerConstructor (mkIdentIndex (ctor ^. Internal.inductiveConstructorName)) info return info @@ -198,7 +201,8 @@ goFunctionDefIden (f, sym) = do _identifierType = funTy, _identifierArgsNum = 0, _identifierArgsInfo = [], - _identifierIsExported = False + _identifierIsExported = False, + _identifierBuiltin = f ^. Internal.funDefBuiltin } registerIdent (mkIdentIndex (f ^. Internal.funDefName)) info when (f ^. Internal.funDefName . Internal.nameText == Str.main) (registerMain sym) @@ -286,7 +290,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive _inductiveKind = mkDynamic', _inductiveConstructors = [], _inductiveParams = [], - _inductivePositive = False + _inductivePositive = False, + _inductiveBuiltin = Nothing } registerInductive (mkIdentIndex (a ^. Internal.axiomName)) info @@ -307,7 +312,8 @@ goAxiomDef a = case a ^. Internal.axiomBuiltin >>= builtinBody of _identifierType = ty, _identifierArgsNum = 0, _identifierArgsInfo = [], - _identifierIsExported = False + _identifierIsExported = False, + _identifierBuiltin = Nothing } registerIdent (mkIdentIndex (a ^. Internal.axiomName)) info registerIdentNode sym body @@ -554,9 +560,10 @@ goApplication a = do funInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoFunctions) case funInfo ^. Internal.functionInfoDef . Internal.funDefBuiltin of Just Internal.BuiltinBoolIf -> do + sym <- getBoolSymbol as <- exprArgs case as of - (v : b1 : b2 : xs) -> return (mkApps' (mkIf' v b1 b2) xs) + (v : b1 : b2 : xs) -> return (mkApps' (mkIf' sym v b1 b2) xs) _ -> error "if must be called with 3 arguments" _ -> app _ -> app diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index f2c08d1c5..de8b61808 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -45,34 +45,36 @@ guardSymbolNotDefined sym err = do createBuiltinConstr :: Symbol -> - BuiltinDataTag -> + Tag -> Text -> Type -> Interval -> + Maybe BuiltinConstructor -> Sem r ConstructorInfo -createBuiltinConstr sym btag nameTxt ty i = do - let n = builtinConstrArgsNum btag +createBuiltinConstr sym tag nameTxt ty i cblt = do return $ ConstructorInfo { _constructorName = nameTxt, _constructorLocation = Just i, - _constructorTag = BuiltinTag btag, + _constructorTag = tag, _constructorType = ty, - _constructorArgsNum = n, - _constructorInductive = sym + _constructorArgsNum = length (typeArgs ty), + _constructorInductive = sym, + _constructorBuiltin = cblt } declareInductiveBuiltins :: Member InfoTableBuilder r => Text -> - [(BuiltinDataTag, Text, Type -> Type)] -> + Maybe BuiltinInductive -> + [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> ParsecS r () -declareInductiveBuiltins indName ctrs = do +declareInductiveBuiltins indName blt ctrs = do loc <- curLoc let i = mkInterval loc loc sym <- lift freshSymbol let ty = mkIdent' sym - constrs <- lift $ mapM (\(tag, name, fty) -> createBuiltinConstr sym tag name (fty ty) i) ctrs + constrs <- lift $ mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) i cblt) ctrs lift $ registerInductive indName @@ -83,7 +85,8 @@ declareInductiveBuiltins indName ctrs = do _inductiveKind = mkDynamic', _inductiveConstructors = constrs, _inductivePositive = True, - _inductiveParams = [] + _inductiveParams = [], + _inductiveBuiltin = blt } ) lift $ mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs @@ -92,18 +95,31 @@ declareIOBuiltins :: Member InfoTableBuilder r => ParsecS r () declareIOBuiltins = declareInductiveBuiltins "IO" - [ (TagReturn, "return", mkPi' mkDynamic'), - (TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty)), - (TagWrite, "write", mkPi' mkDynamic'), - (TagReadLn, "readLn", id) + Nothing + [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing), + (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing), + (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing), + (BuiltinTag TagReadLn, "readLn", id, Nothing) ] declareBoolBuiltins :: Member InfoTableBuilder r => ParsecS r () declareBoolBuiltins = declareInductiveBuiltins "bool" - [ (TagTrue, "true", id), - (TagFalse, "false", id) + (Just BuiltinBool) + [ (BuiltinTag TagTrue, "true", id, Just BuiltinBoolTrue), + (BuiltinTag TagFalse, "false", id, Just BuiltinBoolFalse) + ] + +declareNatBuiltins :: Member InfoTableBuilder r => ParsecS r () +declareNatBuiltins = do + tagZero <- lift freshTag + tagSuc <- lift freshTag + declareInductiveBuiltins + "nat" + (Just BuiltinNat) + [ (tagZero, "zero", id, Just BuiltinNatZero), + (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc) ] parseToplevel :: @@ -112,6 +128,7 @@ parseToplevel :: parseToplevel = do declareIOBuiltins declareBoolBuiltins + declareNatBuiltins space P.endBy statement (kw kwSemicolon) r <- optional expression @@ -121,11 +138,23 @@ parseToplevel = do statement :: Member InfoTableBuilder r => ParsecS r () -statement = statementDef <|> statementInductive +statement = statementBuiltin <|> void statementDef <|> statementInductive + +statementBuiltin :: + Member InfoTableBuilder r => + ParsecS r () +statementBuiltin = do + off <- P.getOffset + kw kwBuiltin + sym <- statementDef + ii <- lift $ getIdentifierInfo sym + case ii ^. identifierName of + "plus" -> lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatPlus} + _ -> parseFailure off "unrecorgnized builtin definition" statementDef :: Member InfoTableBuilder r => - ParsecS r () + ParsecS r Symbol statementDef = do kw kwDef off <- P.getOffset @@ -140,6 +169,7 @@ statementDef = do let fi = fromMaybe impossible $ HashMap.lookup sym (tab ^. infoIdentifiers) ty = fi ^. identifierType parseDefinition sym ty + return sym Just IdentInd {} -> parseFailure off ("duplicate identifier: " ++ fromText txt) Just IdentConstr {} -> @@ -156,10 +186,12 @@ statementDef = do _identifierType = ty, _identifierArgsNum = 0, _identifierArgsInfo = [], - _identifierIsExported = False + _identifierIsExported = False, + _identifierBuiltin = Nothing } lift $ registerIdent txt info void $ optional (parseDefinition sym ty) + return sym parseDefinition :: Member InfoTableBuilder r => @@ -208,7 +240,8 @@ statementInductive = do _inductiveKind = fromMaybe (mkUniv' 0) mty, _inductiveConstructors = [], _inductiveParams = [], - _inductivePositive = True + _inductivePositive = True, + _inductiveBuiltin = Nothing } lift $ registerInductive txt ii ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw kwSemicolon) @@ -233,7 +266,8 @@ constrDecl symInd = do _constructorTag = tag, _constructorArgsNum = length (typeArgs ty), _constructorType = ty, - _constructorInductive = symInd + _constructorInductive = symInd, + _constructorBuiltin = Nothing } lift $ registerConstructor txt ci return ci @@ -742,13 +776,25 @@ exprCase' off value varsNum vars = do bs <- P.sepEndBy (caseBranchP varsNum vars) (kw kwSemicolon) let bss = map fromLeft' $ filter isLeft bs let def' = map fromRight' $ filter isRight bs - case def' of - [def] -> - return $ mkCase' value bss (Just def) + case bss of + CaseBranch {..} : _ -> do + ci <- lift $ getConstructorInfo _caseBranchTag + let sym = ci ^. constructorInductive + case def' of + [def] -> + return $ mkCase' sym value bss (Just def) + [] -> + return $ mkCase' sym value bss Nothing + _ -> + parseFailure off "multiple default branches" [] -> - return $ mkCase' value bss Nothing - _ -> - parseFailure off "multiple default branches" + case def' of + [_] -> + parseFailure off "case with only the default branch not allowed" + [] -> + parseFailure off "case without branches not allowed" + _ -> + parseFailure off "multiple default branches" caseBranchP :: Member InfoTableBuilder r => @@ -818,7 +864,8 @@ exprIf varsNum vars = do br1 <- bracedExpr varsNum vars kw kwElse br2 <- bracedExpr varsNum vars - return $ mkIf Info.empty value br1 br2 + sym <- lift getBoolSymbol + return $ mkIf mempty sym value br1 br2 exprMatch :: Member InfoTableBuilder r => diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs index 87a6df0cb..7b7889d0e 100644 --- a/test/Core/Eval/Positive.hs +++ b/test/Core/Eval/Positive.hs @@ -259,5 +259,10 @@ tests = "Applications with lets and cases in function position" "." "test046.jvc" - "out/test046.out" + "out/test046.out", + PosTest + "Builtin natural numbers" + "." + "test047.jvc" + "out/test047.out" ] diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs index ab2e70b40..092e23671 100644 --- a/test/Core/Transformation.hs +++ b/test/Core/Transformation.hs @@ -3,7 +3,7 @@ module Core.Transformation where import Base import Core.Transformation.Identity qualified as Identity import Core.Transformation.Lifting qualified as Lifting -import Core.Transformation.RemoveTypeArgs qualified as RemoveTypeArgs +import Core.Transformation.Pipeline qualified as Pipeline import Core.Transformation.TopEtaExpand qualified as TopEtaExpand allTests :: TestTree @@ -13,5 +13,5 @@ allTests = [ Identity.allTests, TopEtaExpand.allTests, Lifting.allTests, - RemoveTypeArgs.allTests + Pipeline.allTests ] diff --git a/test/Core/Transformation/RemoveTypeArgs.hs b/test/Core/Transformation/Pipeline.hs similarity index 64% rename from test/Core/Transformation/RemoveTypeArgs.hs rename to test/Core/Transformation/Pipeline.hs index 51d8da70b..9238a95de 100644 --- a/test/Core/Transformation/RemoveTypeArgs.hs +++ b/test/Core/Transformation/Pipeline.hs @@ -1,4 +1,4 @@ -module Core.Transformation.RemoveTypeArgs (allTests) where +module Core.Transformation.Pipeline (allTests) where import Base import Core.Eval.Positive qualified as Eval @@ -6,10 +6,10 @@ import Core.Transformation.Base import Juvix.Compiler.Core.Transformation allTests :: TestTree -allTests = testGroup "Move applications and remove type arguments" (map liftTest Eval.tests) +allTests = testGroup "Transformation pipeline" (map liftTest Eval.tests) pipe :: [TransformationId] -pipe = [LambdaLifting, MoveApps, RemoveTypeArgs] +pipe = [NatToInt, LambdaLifting, MoveApps, RemoveTypeArgs, TopEtaExpand] liftTest :: Eval.PosTest -> TestTree liftTest _testEval = diff --git a/tests/Core/positive/out/test047.out b/tests/Core/positive/out/test047.out new file mode 100644 index 000000000..c0c7ab153 --- /dev/null +++ b/tests/Core/positive/out/test047.out @@ -0,0 +1,3 @@ +3 +136 +true diff --git a/tests/Core/positive/test029.jvc b/tests/Core/positive/test029.jvc index 97cb01e39..6d66a13c8 100644 --- a/tests/Core/positive/test029.jvc +++ b/tests/Core/positive/test029.jvc @@ -9,11 +9,11 @@ def snd := \p case p of { pair _ x := x }; def compose := \f \g \x f (g x); -def zero := \f \x x; +def czero := \f \x x; def num := \n if n = 0 then - zero + czero else \f compose f (num (n - 1) f); @@ -32,7 +32,7 @@ def pred := \n pair (fst x) (succ (snd x)) else pair (succ (fst x)) (succ (snd x))) - (pair zero zero) + (pair czero czero) ); def toInt := \n n (+ 1) 0; @@ -41,11 +41,11 @@ def writeLn := \x write x >> write "\n"; def fib := \n if isZero n then - zero + czero else let n' := pred n in if isZero n' then - succ zero + succ czero else add (fib n') (fib (pred n')); diff --git a/tests/Core/positive/test046.jvc b/tests/Core/positive/test046.jvc index 3d69e20a3..ef4057025 100644 --- a/tests/Core/positive/test046.jvc +++ b/tests/Core/positive/test046.jvc @@ -5,7 +5,7 @@ inductive list { cons : any -> list -> list; }; -def f := \l (case l of { cons x _ := x; nil := \x x } ) (let y := \x x in (let z := \x x in case l of { _ := \x x } z) y) 7; +def f := \l (case l of { cons x _ := x; nil := \x x } ) (let y := \x x in (let z := \x x in case l of { cons _ _ := \x x } z) y) 7; def main := f (cons (\x \y x y + 2) nil); diff --git a/tests/Core/positive/test047.jvc b/tests/Core/positive/test047.jvc new file mode 100644 index 000000000..d962bbaeb --- /dev/null +++ b/tests/Core/positive/test047.jvc @@ -0,0 +1,38 @@ +-- builtin natural numbers + +builtin def plus := \x \y case x of { + zero := y; + suc x' := suc (plus x' y); +}; + +def from_int := \n if n = 0 then zero else suc (from_int (n - 1)); + +def to_int := \x case x of { + suc x' := to_int x' + 1; + zero := 0; +}; + +def even := \x case x of { + suc x' := case x' of { + zero := false; + suc y := even y; + }; + _ := true; +}; + +def f := \x case x of { + suc x' := (\z case z of { + zero := even x'; + suc y := f y; + }) x'; + _ := even x; +}; + +def writeLn := \x write x >> write "\n"; + +def main := + writeLn (to_int (if even (from_int 124) then plus (suc zero) (suc (suc zero)) else zero)) >> + writeLn (to_int (plus (from_int 126) (from_int 10))) >> + writeLn (f (from_int 65)); + +main