Move applications inside Lets and Cases (#1659)

* Move applications inside lets and cases

* make ormolu happy

src/Juvix/Compiler/Core/Data/TransformationId.hs

@@ -6,5 +6,6 @@ data TransformationId
   = LambdaLifting
   | TopEtaExpand
   | RemoveTypeArgs
+  | MoveApps
   | Identity
   deriving stock (Data)

src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs

@@ -45,6 +45,7 @@ pcompletions = do
       TopEtaExpand -> strTopEtaExpand
       Identity -> strIdentity
       RemoveTypeArgs -> strRemoveTypeArgs
+      MoveApps -> strMoveApps
 
 lexeme :: MonadParsec e Text m => m a -> m a
 lexeme = L.lexeme L.hspace
@@ -61,13 +62,15 @@ transformation =
     <|> symbol strIdentity $> Identity
     <|> symbol strTopEtaExpand $> TopEtaExpand
     <|> symbol strRemoveTypeArgs $> RemoveTypeArgs
+    <|> symbol strMoveApps $> MoveApps
 
 allStrings :: [Text]
 allStrings =
   [ strLifting,
     strTopEtaExpand,
     strIdentity,
-    strRemoveTypeArgs
+    strRemoveTypeArgs,
+    strMoveApps
   ]
 
 strLifting :: Text
@@ -81,3 +84,6 @@ strIdentity = "identity"
 
 strRemoveTypeArgs :: Text
 strRemoveTypeArgs = "remove-type-args"
+
+strMoveApps :: Text
+strMoveApps = "move-apps"

src/Juvix/Compiler/Core/Transformation.hs

@@ -13,6 +13,7 @@ import Juvix.Compiler.Core.Transformation.Base
 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.RemoveTypeArgs
 import Juvix.Compiler.Core.Transformation.TopEtaExpand
 
@@ -25,3 +26,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
       Identity -> identity
       TopEtaExpand -> topEtaExpand
       RemoveTypeArgs -> removeTypeArgs
+      MoveApps -> moveApps

src/Juvix/Compiler/Core/Transformation/MoveApps.hs

@@ -0,0 +1,37 @@
+module Juvix.Compiler.Core.Transformation.MoveApps
+  ( moveApps,
+    module Juvix.Compiler.Core.Transformation.Base,
+  )
+where
+
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+
+convertNode :: Node -> Node
+convertNode = dmap go
+  where
+    go :: Node -> Node
+    go node = case node of
+      NApp {} ->
+        let (tgt, args) = unfoldApps node
+         in case tgt of
+              NLet lt@(Let {..}) ->
+                NLet lt {_letBody = mkApps _letBody (map (second (shift 1)) args)}
+              NCase cs@(Case {..}) ->
+                NCase
+                  cs
+                    { _caseBranches =
+                        map
+                          ( \br@CaseBranch {..} ->
+                              br
+                                { _caseBranchBody = mkApps _caseBranchBody (map (second (shift _caseBranchBindersNum)) args)
+                                }
+                          )
+                          _caseBranches,
+                      _caseDefault = fmap (`mkApps` args) _caseDefault
+                    }
+              _ -> node
+      _ -> node
+
+moveApps :: InfoTable -> InfoTable
+moveApps tab = mapT (const convertNode) tab

test/Core/Eval/Positive.hs

@@ -254,5 +254,10 @@ tests =
       "Type application and abstraction"
       "."
       "test045.jvc"
-      "out/test045.out"
+      "out/test045.out",
+    PosTest
+      "Applications with lets and cases in function position"
+      "."
+      "test046.jvc"
+      "out/test046.out"
   ]

test/Core/Transformation/RemoveTypeArgs.hs

@@ -6,10 +6,10 @@ import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
-allTests = testGroup "Remove type arguments" (map liftTest Eval.tests)
+allTests = testGroup "Move applications and remove type arguments" (map liftTest Eval.tests)
 
 pipe :: [TransformationId]
-pipe = [LambdaLifting, RemoveTypeArgs]
+pipe = [LambdaLifting, MoveApps, RemoveTypeArgs]
 
 liftTest :: Eval.PosTest -> TestTree
 liftTest _testEval =

tests/Core/positive/out/test046.out

@@ -0,0 +1 @@
+9

tests/Core/positive/test046.jvc

@@ -0,0 +1,12 @@
+-- applications with lets and cases in function position
+
+inductive list {
+  nil : 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 main := f (cons (\x \y x y + 2) nil);
+
+main