From fae003313136a71022ffd04988bc422a80cd28f4 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 12 Sep 2024 19:08:21 +0200 Subject: [PATCH 1/8] ShallowFreeVarsInfo --- src/Juvix/Compiler/Core/Extra/Utils.hs | 90 +++++++++---------- .../Compiler/Core/Info/ShallowFreeVarsInfo.hs | 50 +++++++++++ .../Core/Transformation/Optimize/Inlining.hs | 2 + .../Transformation/Optimize/LetFolding.hs | 2 +- 4 files changed, 98 insertions(+), 46 deletions(-) create mode 100644 src/Juvix/Compiler/Core/Info/ShallowFreeVarsInfo.hs diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index 33756a7c8f..de26939d97 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -177,52 +177,52 @@ isFalseConstr = \case NCtr Constr {..} | _constrTag == BuiltinTag TagFalse -> True _ -> False +isDebugOp :: Node -> Bool +isDebugOp = \case + NBlt BuiltinApp {..} -> + case _builtinAppOp of + OpTrace -> True + OpFail -> True + OpSeq -> True + OpAssert -> False + OpAnomaByteArrayFromAnomaContents -> False + OpAnomaByteArrayToAnomaContents -> False + OpAnomaDecode -> False + OpAnomaEncode -> False + OpAnomaGet -> False + OpAnomaSign -> False + OpAnomaSignDetached -> False + OpAnomaVerifyDetached -> False + OpAnomaVerifyWithMessage -> False + OpEc -> False + OpFieldAdd -> False + OpFieldDiv -> False + OpFieldFromInt -> False + OpFieldMul -> False + OpFieldSub -> False + OpPoseidonHash -> False + OpRandomEcPoint -> False + OpStrConcat -> False + OpStrToInt -> False + OpUInt8FromInt -> False + OpUInt8ToInt -> False + OpByteArrayFromListByte -> False + OpByteArrayLength -> False + OpEq -> False + OpIntAdd -> False + OpIntDiv -> False + OpIntLe -> False + OpIntLt -> False + OpIntMod -> False + OpIntMul -> False + OpIntSub -> False + OpFieldToInt -> False + OpShow -> False + _ -> False + -- | Check if the node contains `trace`, `fail` or `seq` (`>->`). -containsDebugOperations :: Node -> Bool -containsDebugOperations = ufold (\x xs -> x || or xs) isDebugOp - where - isDebugOp :: Node -> Bool - isDebugOp = \case - NBlt BuiltinApp {..} -> - case _builtinAppOp of - OpTrace -> True - OpFail -> True - OpSeq -> True - OpAssert -> False - OpAnomaByteArrayFromAnomaContents -> False - OpAnomaByteArrayToAnomaContents -> False - OpAnomaDecode -> False - OpAnomaEncode -> False - OpAnomaGet -> False - OpAnomaSign -> False - OpAnomaSignDetached -> False - OpAnomaVerifyDetached -> False - OpAnomaVerifyWithMessage -> False - OpEc -> False - OpFieldAdd -> False - OpFieldDiv -> False - OpFieldFromInt -> False - OpFieldMul -> False - OpFieldSub -> False - OpPoseidonHash -> False - OpRandomEcPoint -> False - OpStrConcat -> False - OpStrToInt -> False - OpUInt8FromInt -> False - OpUInt8ToInt -> False - OpByteArrayFromListByte -> False - OpByteArrayLength -> False - OpEq -> False - OpIntAdd -> False - OpIntDiv -> False - OpIntLe -> False - OpIntLt -> False - OpIntMod -> False - OpIntMul -> False - OpIntSub -> False - OpFieldToInt -> False - OpShow -> False - _ -> False +containsDebugOps :: Node -> Bool +containsDebugOps = ufold (\x xs -> x || or xs) isDebugOp freeVarsSortedMany :: [Node] -> Set Var freeVarsSortedMany n = Set.fromList (n ^.. each . freeVars) diff --git a/src/Juvix/Compiler/Core/Info/ShallowFreeVarsInfo.hs b/src/Juvix/Compiler/Core/Info/ShallowFreeVarsInfo.hs new file mode 100644 index 0000000000..31cc9d4f62 --- /dev/null +++ b/src/Juvix/Compiler/Core/Info/ShallowFreeVarsInfo.hs @@ -0,0 +1,50 @@ +module Juvix.Compiler.Core.Info.ShallowFreeVarsInfo where + +import Data.Map qualified as Map +import Juvix.Compiler.Core.Extra +import Juvix.Compiler.Core.Info qualified as Info + +newtype ShallowFreeVarsInfo = ShallowFreeVarsInfo + { -- map free variables to the number of their shallow occurrences (not under binders) + _infoShallowFreeVars :: Map Index Int + } + +instance IsInfo ShallowFreeVarsInfo + +kShallowFreeVarsInfo :: Key ShallowFreeVarsInfo +kShallowFreeVarsInfo = Proxy + +makeLenses ''ShallowFreeVarsInfo + +-- | Computes shallow free variable info for each subnode. Assumption: no +-- subnode is a closure. +computeShallowFreeVarsInfo :: Node -> Node +computeShallowFreeVarsInfo = umap go + where + go :: Node -> Node + go node = case node of + NVar Var {..} -> + mkVar (Info.insert fvi _varInfo) _varIndex + where + fvi = ShallowFreeVarsInfo (Map.singleton _varIndex 1) + _ -> + modifyInfo (Info.insert fvi) node + where + fvi = + ShallowFreeVarsInfo $ + foldr + ( \NodeChild {..} acc -> + if + | _childBindersNum == 0 -> + Map.unionWith (+) acc (getShallowFreeVarsInfo _childNode ^. infoShallowFreeVars) + | otherwise -> + acc + ) + mempty + (children node) + +getShallowFreeVarsInfo :: Node -> ShallowFreeVarsInfo +getShallowFreeVarsInfo = fromJust . Info.lookup kShallowFreeVarsInfo . getInfo + +shallowFreeVarOccurrences :: Index -> Node -> Int +shallowFreeVarOccurrences idx n = fromMaybe 0 (Map.lookup idx (getShallowFreeVarsInfo n ^. infoShallowFreeVars)) diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs index 1dccadbff3..c2cc7c8afe 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs @@ -75,6 +75,8 @@ convertNode inlineDepth nonRecSyms md = dmapL go NIdt Ident {..} -> case pi of Just InlineCase -> NCase cs {_caseValue = mkApps def args} + Just InlineNever -> + node Nothing | HashSet.member _identSymbol nonRecSyms && isConstructorApp def diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs index a84fd6f603..87cf884eb8 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs @@ -27,7 +27,7 @@ convertNode isFoldable md = rmapL go || Info.freeVarOccurrences 0 _letBody <= 1 || isFoldable md bl (_letItem ^. letItemValue) ) - && not (containsDebugOperations _letBody) -> + && not (containsDebugOps _letBody) -> go (recur . (mkBCRemove b val' :)) (BL.cons b bl) _letBody where val' = go recur bl (_letItem ^. letItemValue) From b61044afb46d3ce72f3332eaddb41125766ad0eb Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 12 Sep 2024 19:08:38 +0200 Subject: [PATCH 2/8] test --- tests/Compilation/positive/out/test081.out | 1 + tests/Compilation/positive/test081.juvix | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+) create mode 100644 tests/Compilation/positive/out/test081.out create mode 100644 tests/Compilation/positive/test081.juvix diff --git a/tests/Compilation/positive/out/test081.out b/tests/Compilation/positive/out/test081.out new file mode 100644 index 0000000000..573541ac97 --- /dev/null +++ b/tests/Compilation/positive/out/test081.out @@ -0,0 +1 @@ +0 diff --git a/tests/Compilation/positive/test081.juvix b/tests/Compilation/positive/test081.juvix new file mode 100644 index 0000000000..73cf7255d4 --- /dev/null +++ b/tests/Compilation/positive/test081.juvix @@ -0,0 +1,18 @@ +-- Non-duplication in let-folding +module test081; + +import Stdlib.Prelude open; + +{-# inline: false #-} +g (h : Nat -> Nat) : Nat := h 0 * h 0; + +terminating +f (n : Nat) : Nat := + if + | n == 0 := 0 + | else := + let terminating x := f (sub n 1) + in + g \{_ := x}; + +main : Nat := f 10000; From a8b25d19102a9b3aaf4869e36919fa941acc3627 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 13 Sep 2024 10:19:22 +0200 Subject: [PATCH 3/8] lambdaMultiplier in FreeVarsInfo computation --- src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs | 24 ++++++--- .../Compiler/Core/Info/ShallowFreeVarsInfo.hs | 50 ------------------- .../Transformation/Optimize/LetFolding.hs | 2 +- tests/Compilation/positive/test059.juvix | 6 +-- 4 files changed, 22 insertions(+), 60 deletions(-) delete mode 100644 src/Juvix/Compiler/Core/Info/ShallowFreeVarsInfo.hs diff --git a/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs b/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs index 2a665ab4e5..b9be178967 100644 --- a/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs +++ b/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs @@ -19,7 +19,10 @@ makeLenses ''FreeVarsInfo -- | Computes free variable info for each subnode. Assumption: no subnode is a -- closure. computeFreeVarsInfo :: Node -> Node -computeFreeVarsInfo = umap go +computeFreeVarsInfo = computeFreeVarsInfo' 1 + +computeFreeVarsInfo' :: Int -> Node -> Node +computeFreeVarsInfo' lambdaMultiplier = umap go where go :: Node -> Node go node = case node of @@ -27,6 +30,15 @@ computeFreeVarsInfo = umap go mkVar (Info.insert fvi _varInfo) _varIndex where fvi = FreeVarsInfo (Map.singleton _varIndex 1) + NLam Lambda {..} -> + modifyInfo (Info.insert fvi) node + where + fvi = + FreeVarsInfo + . fmap (* lambdaMultiplier) + . Map.mapKeysMonotonic (\idx -> idx - 1) + . Map.filterWithKey (\idx _ -> idx >= 1) + $ getFreeVarsInfo _lambdaBody ^. infoFreeVars _ -> modifyInfo (Info.insert fvi) node where @@ -34,11 +46,11 @@ computeFreeVarsInfo = umap go FreeVarsInfo $ foldr ( \NodeChild {..} acc -> - Map.unionWith (+) acc $ - Map.mapKeysMonotonic (\idx -> idx - _childBindersNum) $ - Map.filterWithKey - (\idx _ -> idx >= _childBindersNum) - (getFreeVarsInfo _childNode ^. infoFreeVars) + Map.unionWith (+) acc + . Map.mapKeysMonotonic (\idx -> idx - _childBindersNum) + . Map.filterWithKey + (\idx _ -> idx >= _childBindersNum) + $ getFreeVarsInfo _childNode ^. infoFreeVars ) mempty (children node) diff --git a/src/Juvix/Compiler/Core/Info/ShallowFreeVarsInfo.hs b/src/Juvix/Compiler/Core/Info/ShallowFreeVarsInfo.hs deleted file mode 100644 index 31cc9d4f62..0000000000 --- a/src/Juvix/Compiler/Core/Info/ShallowFreeVarsInfo.hs +++ /dev/null @@ -1,50 +0,0 @@ -module Juvix.Compiler.Core.Info.ShallowFreeVarsInfo where - -import Data.Map qualified as Map -import Juvix.Compiler.Core.Extra -import Juvix.Compiler.Core.Info qualified as Info - -newtype ShallowFreeVarsInfo = ShallowFreeVarsInfo - { -- map free variables to the number of their shallow occurrences (not under binders) - _infoShallowFreeVars :: Map Index Int - } - -instance IsInfo ShallowFreeVarsInfo - -kShallowFreeVarsInfo :: Key ShallowFreeVarsInfo -kShallowFreeVarsInfo = Proxy - -makeLenses ''ShallowFreeVarsInfo - --- | Computes shallow free variable info for each subnode. Assumption: no --- subnode is a closure. -computeShallowFreeVarsInfo :: Node -> Node -computeShallowFreeVarsInfo = umap go - where - go :: Node -> Node - go node = case node of - NVar Var {..} -> - mkVar (Info.insert fvi _varInfo) _varIndex - where - fvi = ShallowFreeVarsInfo (Map.singleton _varIndex 1) - _ -> - modifyInfo (Info.insert fvi) node - where - fvi = - ShallowFreeVarsInfo $ - foldr - ( \NodeChild {..} acc -> - if - | _childBindersNum == 0 -> - Map.unionWith (+) acc (getShallowFreeVarsInfo _childNode ^. infoShallowFreeVars) - | otherwise -> - acc - ) - mempty - (children node) - -getShallowFreeVarsInfo :: Node -> ShallowFreeVarsInfo -getShallowFreeVarsInfo = fromJust . Info.lookup kShallowFreeVarsInfo . getInfo - -shallowFreeVarOccurrences :: Index -> Node -> Int -shallowFreeVarOccurrences idx n = fromMaybe 0 (Map.lookup idx (getShallowFreeVarsInfo n ^. infoShallowFreeVars)) diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs index 87cf884eb8..d95891177c 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs @@ -40,7 +40,7 @@ letFolding' isFoldable tab = mapAllNodes ( removeInfo kFreeVarsInfo . convertNode isFoldable tab - . computeFreeVarsInfo + . computeFreeVarsInfo' 2 ) tab diff --git a/tests/Compilation/positive/test059.juvix b/tests/Compilation/positive/test059.juvix index 03a5be832f..91ea8dcbce 100644 --- a/tests/Compilation/positive/test059.juvix +++ b/tests/Compilation/positive/test059.juvix @@ -1,15 +1,15 @@ -- builtin list module test059; -import Stdlib.Prelude open hiding {head}; +import Stdlib.Prelude open; mylist : List Nat := [1; 2; 3 + 1]; mylist2 : List (List Nat) := [[10]; [2]; 3 + 1 :: nil]; -head : {a : Type} -> a -> List a -> a +head' : {a : Type} -> a -> List a -> a | a [] := a | a [x; _] := x | _ (h :: _) := h; -main : Nat := head 50 mylist + head 50 (head [] mylist2); +main : Nat := head' 50 mylist + head' 50 (head' [] mylist2); From 4b39ab467af6e4c3e6afda153d4b0faad199d356 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 13 Sep 2024 10:27:10 +0200 Subject: [PATCH 4/8] enable tests --- test/Compilation/Positive.hs | 12 +++++++++++- tests/Compilation/positive/out/test080.out | 2 ++ 2 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 tests/Compilation/positive/out/test080.out diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 51fc1fb284..252f5635db 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -470,5 +470,15 @@ tests = "Test079: Let / LetRec type inference (during lambda lifting) in Core" $(mkRelDir ".") $(mkRelFile "test079.juvix") - $(mkRelFile "out/test079.out") + $(mkRelFile "out/test079.out"), + posTest + "Test080: Do notation" + $(mkRelDir ".") + $(mkRelFile "test080.juvix") + $(mkRelFile "out/test080.out"), + posTest + "Test081: Non-duplication in let-folding" + $(mkRelDir ".") + $(mkRelFile "test081.juvix") + $(mkRelFile "out/test081.out") ] diff --git a/tests/Compilation/positive/out/test080.out b/tests/Compilation/positive/out/test080.out new file mode 100644 index 0000000000..66c0e977e4 --- /dev/null +++ b/tests/Compilation/positive/out/test080.out @@ -0,0 +1,2 @@ +nothing +just 1 From 4d778dc87ff30cc1db7dca25270d219ed19b2e22 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 13 Sep 2024 14:37:14 +0200 Subject: [PATCH 5/8] fix tests --- src/Juvix/Compiler/Core/Transformation/MoveApps.hs | 2 +- test/Compilation/Positive.hs | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Core/Transformation/MoveApps.hs b/src/Juvix/Compiler/Core/Transformation/MoveApps.hs index 187d46c48e..64757d0390 100644 --- a/src/Juvix/Compiler/Core/Transformation/MoveApps.hs +++ b/src/Juvix/Compiler/Core/Transformation/MoveApps.hs @@ -77,4 +77,4 @@ convertNode = dmap go -- - https://github.com/anoma/juvix/issues/1654 -- - https://github.com/anoma/juvix/pull/1659 moveApps :: Module -> Module -moveApps = mapT (const convertNode) +moveApps = mapAllNodes convertNode diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 252f5635db..a7edbb72cc 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -451,7 +451,7 @@ tests = $(mkRelDir ".") $(mkRelFile "test075.juvix") $(mkRelFile "out/test075.out"), - posTestEval + posTest "Test076: Builtin Maybe" $(mkRelDir ".") $(mkRelFile "test076.juvix") @@ -466,12 +466,12 @@ tests = $(mkRelDir ".") $(mkRelFile "test078.juvix") $(mkRelFile "out/test078.out"), - posTestEval + posTest "Test079: Let / LetRec type inference (during lambda lifting) in Core" $(mkRelDir ".") $(mkRelFile "test079.juvix") $(mkRelFile "out/test079.out"), - posTest + posTestEval -- TODO: this test is not compiling "Test080: Do notation" $(mkRelDir ".") $(mkRelFile "test080.juvix") From d8accb3cb81e4c6ba6cff38034e536b406306b1c Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 13 Sep 2024 14:55:16 +0200 Subject: [PATCH 6/8] style changes --- src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs b/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs index b9be178967..312c6cfe61 100644 --- a/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs +++ b/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs @@ -21,6 +21,8 @@ makeLenses ''FreeVarsInfo computeFreeVarsInfo :: Node -> Node computeFreeVarsInfo = computeFreeVarsInfo' 1 +-- | `lambdaMultiplier` specifies how much to multiply the free variable count +-- for variables under lambdas computeFreeVarsInfo' :: Int -> Node -> Node computeFreeVarsInfo' lambdaMultiplier = umap go where @@ -36,9 +38,7 @@ computeFreeVarsInfo' lambdaMultiplier = umap go fvi = FreeVarsInfo . fmap (* lambdaMultiplier) - . Map.mapKeysMonotonic (\idx -> idx - 1) - . Map.filterWithKey (\idx _ -> idx >= 1) - $ getFreeVarsInfo _lambdaBody ^. infoFreeVars + $ getFreeVars 1 _lambdaBody _ -> modifyInfo (Info.insert fvi) node where @@ -46,15 +46,18 @@ computeFreeVarsInfo' lambdaMultiplier = umap go FreeVarsInfo $ foldr ( \NodeChild {..} acc -> - Map.unionWith (+) acc - . Map.mapKeysMonotonic (\idx -> idx - _childBindersNum) - . Map.filterWithKey - (\idx _ -> idx >= _childBindersNum) - $ getFreeVarsInfo _childNode ^. infoFreeVars + Map.unionWith (+) acc $ + getFreeVars _childBindersNum _childNode ) mempty (children node) + getFreeVars :: Int -> Node -> Map Index Int + getFreeVars bindersNum node = + Map.mapKeysMonotonic (\idx -> idx - bindersNum) + . Map.filterWithKey (\idx _ -> idx >= bindersNum) + $ getFreeVarsInfo node ^. infoFreeVars + getFreeVarsInfo :: Node -> FreeVarsInfo getFreeVarsInfo = fromJust . Info.lookup kFreeVarsInfo . getInfo From f2dfe48c3aeef4ca5020230b060312a7eb191245 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 13 Sep 2024 18:09:07 +0200 Subject: [PATCH 7/8] add comment --- src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs index d95891177c..7cb793dd75 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs @@ -41,6 +41,10 @@ letFolding' isFoldable tab = ( removeInfo kFreeVarsInfo . convertNode isFoldable tab . computeFreeVarsInfo' 2 + -- 2 is the lambda multiplier factor which guarantees that every free + -- variable under a lambda is counted at least twice, preventing let + -- folding for let-bound variables (with non-immediate values) that + -- occur under lambdas ) tab From 9ffbb7a781d419fcaba58eb4602e7ef8b4f87001 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 13 Sep 2024 18:15:58 +0200 Subject: [PATCH 8/8] add comment --- src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs index 7cb793dd75..c8752b1398 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/LetFolding.hs @@ -1,6 +1,7 @@ -- An optimizing transformation that folds lets whose values are immediate, -- i.e., they don't require evaluation or memory allocation (variables or --- constants), or when the bound variable occurs at most once in the body. +-- constants), or when the bound variable occurs at most once in the body but +-- not under a lambda-abstraction. -- -- For example, transforms -- ```