From 4135977a07ecdb72552ad9b98e1199b897226373 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 30 Sep 2022 19:43:33 +0200
Subject: [PATCH 01/73] implement eta expansion

---
 src/Juvix/Compiler/Core/Data/InfoTable.hs     |  4 +--
 src/Juvix/Compiler/Core/Extra.hs              | 21 ++++++++++++++
 src/Juvix/Compiler/Core/Info/TypeInfo.hs      |  8 ++----
 src/Juvix/Compiler/Core/Language.hs           |  5 +---
 src/Juvix/Compiler/Core/Language/Nodes.hs     | 28 ++++++++++++++-----
 .../Compiler/Core/Transformation/Base.hs      |  4 +--
 src/Juvix/Compiler/Core/Transformation/Eta.hs |  2 +-
 .../Core/Transformation/LambdaLifting.hs      | 16 ++---------
 .../Compiler/Core/Translation/FromSource.hs   |  2 +-
 src/Juvix/Prelude/Base.hs                     |  4 +++
 10 files changed, 58 insertions(+), 36 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs
index e643c6f0d6..15cd83afb0 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs
@@ -45,8 +45,8 @@ data IdentifierInfo = IdentifierInfo
 
 data ArgumentInfo = ArgumentInfo
   { _argumentName :: Maybe Name,
-    _argumentType :: Maybe Type,
-    _argumentIsImplicit :: Bool
+    _argumentType :: Type,
+    _argumentIsImplicit :: IsImplicit
   }
 
 data InductiveInfo = InductiveInfo
diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index 4759e1c292..d80dc18837 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -11,12 +11,16 @@ where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Extra.Base
 import Juvix.Compiler.Core.Extra.Equality
 import Juvix.Compiler.Core.Extra.Info
 import Juvix.Compiler.Core.Extra.Recursors
 import Juvix.Compiler.Core.Extra.Recursors.Fold.Named
 import Juvix.Compiler.Core.Extra.Recursors.Map.Named
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NameInfo
+import Juvix.Compiler.Core.Info.TypeInfo
 import Juvix.Compiler.Core.Language
 
 isClosed :: Node -> Bool
@@ -138,3 +142,20 @@ convertClosures = umap go
 
 convertRuntimeNodes :: Node -> Node
 convertRuntimeNodes = convertClosures
+
+argumentInfoFromInfo :: Info -> ArgumentInfo
+argumentInfoFromInfo i =
+  ArgumentInfo
+    { _argumentName = (^. infoName) <$> Info.lookup (Proxy @NameInfo) i,
+      _argumentType = getInfoType i,
+      _argumentIsImplicit = Explicit
+    }
+
+infoFromArgumentInfo :: ArgumentInfo -> Info
+infoFromArgumentInfo arg =
+  setInfoType (arg ^. argumentType) $
+    setName
+      mempty
+  where
+    setName :: Info -> Info
+    setName i = maybe i (`setInfoName` i) (arg ^. argumentName)
diff --git a/src/Juvix/Compiler/Core/Info/TypeInfo.hs b/src/Juvix/Compiler/Core/Info/TypeInfo.hs
index 6558ad85b5..fbe06622c4 100644
--- a/src/Juvix/Compiler/Core/Info/TypeInfo.hs
+++ b/src/Juvix/Compiler/Core/Info/TypeInfo.hs
@@ -1,5 +1,6 @@
 module Juvix.Compiler.Core.Info.TypeInfo where
 
+import Juvix.Compiler.Core.Extra.Base
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Language
 
@@ -12,11 +13,8 @@ kTypeInfo = Proxy
 
 makeLenses ''TypeInfo
 
-getInfoType :: Info -> Maybe Type
-getInfoType i =
-  case Info.lookup kTypeInfo i of
-    Just (TypeInfo {..}) -> Just _infoType
-    Nothing -> Nothing
+getInfoType :: Info -> Type
+getInfoType i = maybe mkDynamic' (^. infoType) (Info.lookup kTypeInfo i)
 
 setInfoType :: Type -> Info -> Info
 setInfoType = Info.insert . TypeInfo
diff --git a/src/Juvix/Compiler/Core/Language.hs b/src/Juvix/Compiler/Core/Language.hs
index 6de540dd05..ce91a28f7c 100644
--- a/src/Juvix/Compiler/Core/Language.hs
+++ b/src/Juvix/Compiler/Core/Language.hs
@@ -1,13 +1,10 @@
+-- | This file defines the tree representation of JuvixCore (Node datatype).
 module Juvix.Compiler.Core.Language
   ( module Juvix.Compiler.Core.Language,
     module Juvix.Compiler.Core.Language.Nodes,
   )
 where
 
-{-
-  This file defines the tree representation of JuvixCore (Node datatype).
--}
-
 import Juvix.Compiler.Core.Language.Nodes
 
 {---------------------------------------------------------------------------------}
diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index 1a3607a004..8e7a086e13 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -1,3 +1,4 @@
+-- | Polymorphic Node types
 module Juvix.Compiler.Core.Language.Nodes
   ( module Juvix.Compiler.Core.Language.Base,
     module Juvix.Compiler.Core.Language.Primitives,
@@ -8,9 +9,6 @@ where
 import Juvix.Compiler.Core.Language.Base
 import Juvix.Compiler.Core.Language.Primitives
 
-{-------------------------------------------------------------------}
-{- Polymorphic Node types -}
-
 -- | De Bruijn index of a locally bound variable.
 data Var' i = Var {_varInfo :: i, _varIndex :: !Index}
 
@@ -28,9 +26,17 @@ data ConstantValue
 -- Other things we might need in the future:
 -- - ConstFloat or ConstFixedPoint
 
-data App' i a = App {_appInfo :: i, _appLeft :: !a, _appRight :: !a}
+data App' i a = App
+  { _appInfo :: i,
+    _appLeft :: !a,
+    _appRight :: !a
+  }
 
-data Apps' f i a = Apps {_appsInfo :: i, _appsFun :: !f, _appsArgs :: ![a]}
+data Apps' f i a = Apps
+  { _appsInfo :: i,
+    _appsFun :: !f,
+    _appsArgs :: ![a]
+  }
 
 -- | A builtin application. A builtin has no corresponding Node. It is treated
 -- specially by the evaluator and the code generator. For example, basic
@@ -53,11 +59,18 @@ data Constr' i a = Constr
     _constrArgs :: ![a]
   }
 
-data Lambda' i a = Lambda {_lambdaInfo :: i, _lambdaBody :: !a}
+data Lambda' i a = Lambda
+  { _lambdaInfo :: i,
+    _lambdaBody :: !a
+  }
 
 -- | `let x := value in body` is not reducible to lambda + application for the
 -- purposes of ML-polymorphic / dependent type checking or code generation!
-data Let' i a = Let {_letInfo :: i, _letValue :: !a, _letBody :: !a}
+data Let' i a = Let
+  { _letInfo :: i,
+    _letValue :: !a,
+    _letBody :: !a
+  }
 
 -- | Represents a block of mutually recursive local definitions. Both in the
 -- body and in the values `length _letRecValues` implicit binders are introduced
@@ -315,6 +328,7 @@ makeLenses ''PatternWildcard'
 makeLenses ''PatternBinder'
 makeLenses ''PatternConstr'
 makeLenses ''Pi'
+makeLenses ''Lambda'
 makeLenses ''Univ'
 makeLenses ''TypeConstr'
 makeLenses ''Dynamic'
diff --git a/src/Juvix/Compiler/Core/Transformation/Base.hs b/src/Juvix/Compiler/Core/Transformation/Base.hs
index 65172aa968..26646a6dc6 100644
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@@ -12,8 +12,8 @@ import Juvix.Compiler.Core.Language
 
 type Transformation = InfoTable -> InfoTable
 
-mapT :: (Node -> Node) -> InfoTable -> InfoTable
-mapT f tab = tab {_identContext = HashMap.map f (tab ^. identContext)}
+mapT :: (Symbol -> Node -> Node) -> InfoTable -> InfoTable
+mapT f tab = tab {_identContext = HashMap.mapWithKey f (tab ^. identContext)}
 
 mapT' :: (Node -> Sem (InfoTableBuilder ': r) Node) -> InfoTable -> Sem r InfoTable
 mapT' f tab = fmap fst $ runInfoTableBuilder tab $ do
diff --git a/src/Juvix/Compiler/Core/Transformation/Eta.hs b/src/Juvix/Compiler/Core/Transformation/Eta.hs
index f20f5c8077..89c244dfb1 100644
--- a/src/Juvix/Compiler/Core/Transformation/Eta.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Eta.hs
@@ -52,4 +52,4 @@ etaExpandApps tab =
         Nothing -> 0
 
 etaExpansionApps :: Transformation
-etaExpansionApps tab = mapT (etaExpandApps tab) tab
+etaExpansionApps tab = mapT (const (etaExpandApps tab)) tab
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 7a35ef0184..42917ca6c2 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -8,9 +8,6 @@ import Juvix.Compiler.Core.Data.BinderList (BinderList)
 import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
-import Juvix.Compiler.Core.Info qualified as Info
-import Juvix.Compiler.Core.Info.NameInfo
-import Juvix.Compiler.Core.Info.TypeInfo
 import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation.Base
 
@@ -24,17 +21,8 @@ lambdaLiftNode aboveBl top =
     typeFromArgs :: [ArgumentInfo] -> Type
     typeFromArgs = \case
       [] -> mkDynamic' -- change this when we have type info about the body
-      (a : as) -> mkPi' argTy (typeFromArgs as)
-        where
-          argTy = fromMaybe mkDynamic' (a ^. argumentType)
+      (a : as) -> mkPi' (a ^. argumentType) (typeFromArgs as)
     -- extracts the argument info from the binder
-    argInfo :: Info -> ArgumentInfo
-    argInfo i =
-      ArgumentInfo
-        { _argumentName = (^. infoName) <$> Info.lookup (Proxy @NameInfo) i,
-          _argumentType = (^. infoType) <$> Info.lookup (Proxy @TypeInfo) i,
-          _argumentIsImplicit = False
-        }
     go :: BinderList Info -> Node -> Sem r Recur
     go bl = \case
       l@NLam {} -> do
@@ -44,7 +32,7 @@ lambdaLiftNode aboveBl top =
             freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
             fBody' = captureFreeVars freevarsAssocs l'
             argsInfo :: [ArgumentInfo]
-            argsInfo = map (argInfo . snd) freevarsAssocs
+            argsInfo = map (argumentInfoFromInfo . snd) freevarsAssocs
         f <- freshSymbol
         registerIdent
           IdentifierInfo
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index b34a8cd95f..eee1b744ec 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -166,7 +166,7 @@ parseDefinition sym = do
       ArgumentInfo
         { _argumentName = getInfoName bi,
           _argumentType = getInfoType bi,
-          _argumentIsImplicit = False
+          _argumentIsImplicit = Explicit
         }
       where
         bi = getInfoBinder i
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index f453067fbb..e60d208657 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -332,6 +332,10 @@ fromRightIO pp = fromRightIO' (putStrLn . pp)
 -- Misc
 --------------------------------------------------------------------------------
 
+-- | applies a function n times
+iterateN :: Int -> (a -> a) -> a -> a
+iterateN n f = (!! n) . iterate f
+
 nubHashable :: Hashable a => [a] -> [a]
 nubHashable = HashSet.toList . HashSet.fromList
 

From fcdd46c173d1d516c155912a29a3e579a993dddd Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Sat, 1 Oct 2022 01:20:35 +0200
Subject: [PATCH 02/73] add missing file

---
 .../Core/Transformation/TopEtaExpand.hs       | 26 +++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs

diff --git a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
new file mode 100644
index 0000000000..f309176200
--- /dev/null
+++ b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
@@ -0,0 +1,26 @@
+module Juvix.Compiler.Core.Transformation.TopEtaExpand where
+
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+
+topEtaExpand :: InfoTable -> InfoTable
+topEtaExpand info = mapT go info
+  where
+  go :: Symbol -> Node -> Node
+  go sym node = case info ^. infoIdentifiers . at sym of
+    Nothing -> node
+    Just idenInfo ->
+      let
+        args :: [Info]
+        args = map infoFromArgumentInfo  (idenInfo ^. identifierArgsInfo)
+      in goArgs args node
+  goArgs :: [Info] -> Node -> Node
+  goArgs args node = case args of
+    [] -> node
+    (a : as) -> case node of
+      NLam l -> NLam (over lambdaBody (goArgs as) l)
+      _ -> expand node (reverse args)
+  expand :: Node -> [Info] -> Node
+  expand n = \case
+    [] -> n
+    (a : as) -> expand (mkLambda a (mkApp' n (mkVar' 0))) as

From 13d98c985b464897d84dc54a1df06f4bc8893b03 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 3 Oct 2022 13:32:41 +0200
Subject: [PATCH 03/73] add tests

---
 .../Compiler/Core/Data/TransformationId.hs    |  1 +
 .../Core/Data/TransformationId/Parser.hs      |  1 +
 src/Juvix/Compiler/Core/Transformation.hs     |  3 ++
 .../Core/Transformation/TopEtaExpand.hs       | 35 ++++++++--------
 test/Core/Eval/Base.hs                        | 17 ++++++--
 test/Core/Eval/Positive.hs                    |  2 +-
 test/Core/Transformation.hs                   |  6 ++-
 test/Core/Transformation/Base.hs              | 42 +++++--------------
 test/Core/Transformation/TopEtaExpand.hs      | 28 +++++++++++++
 9 files changed, 80 insertions(+), 55 deletions(-)
 create mode 100644 test/Core/Transformation/TopEtaExpand.hs

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index 0415bc76d8..a6f80cb084 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -4,4 +4,5 @@ import Juvix.Prelude
 
 data TransformationId
   = LambdaLifting
+  | TopEtaExpand
   deriving stock (Data)
diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
index dac7d81b62..4c246b7ac2 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -29,3 +29,4 @@ symbol = void . lexeme . chunk
 transformation :: MonadParsec e Text m => m TransformationId
 transformation =
   symbol "lifting" $> LambdaLifting
+    <|> symbol "eta" $> TopEtaExpand
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index 69fb993abf..0087afb413 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -3,6 +3,7 @@ module Juvix.Compiler.Core.Transformation
     module Juvix.Compiler.Core.Transformation,
     module Juvix.Compiler.Core.Transformation.Eta,
     module Juvix.Compiler.Core.Transformation.LambdaLifting,
+    module Juvix.Compiler.Core.Transformation.TopEtaExpand,
     module Juvix.Compiler.Core.Data.TransformationId,
   )
 where
@@ -11,6 +12,7 @@ import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Transformation.LambdaLifting
+import Juvix.Compiler.Core.Transformation.TopEtaExpand
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
@@ -18,3 +20,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
     appTrans :: TransformationId -> InfoTable -> InfoTable
     appTrans = \case
       LambdaLifting -> lambdaLifting
+      TopEtaExpand -> topEtaExpand
diff --git a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
index f309176200..de92cff76d 100644
--- a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
+++ b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
@@ -6,21 +6,20 @@ import Juvix.Compiler.Core.Transformation.Base
 topEtaExpand :: InfoTable -> InfoTable
 topEtaExpand info = mapT go info
   where
-  go :: Symbol -> Node -> Node
-  go sym node = case info ^. infoIdentifiers . at sym of
-    Nothing -> node
-    Just idenInfo ->
-      let
-        args :: [Info]
-        args = map infoFromArgumentInfo  (idenInfo ^. identifierArgsInfo)
-      in goArgs args node
-  goArgs :: [Info] -> Node -> Node
-  goArgs args node = case args of
-    [] -> node
-    (a : as) -> case node of
-      NLam l -> NLam (over lambdaBody (goArgs as) l)
-      _ -> expand node (reverse args)
-  expand :: Node -> [Info] -> Node
-  expand n = \case
-    [] -> n
-    (a : as) -> expand (mkLambda a (mkApp' n (mkVar' 0))) as
+    go :: Symbol -> Node -> Node
+    go sym node = case info ^. infoIdentifiers . at sym of
+      Nothing -> node
+      Just idenInfo ->
+        let args :: [Info]
+            args = map infoFromArgumentInfo (idenInfo ^. identifierArgsInfo)
+         in skipLambdas args node
+    skipLambdas :: [Info] -> Node -> Node
+    skipLambdas args node = case args of
+      [] -> node
+      (_ : as) -> case node of
+        NLam l -> NLam (over lambdaBody (skipLambdas as) l)
+        _ -> expand node (reverse args)
+    expand :: Node -> [Info] -> Node
+    expand n = \case
+      [] -> n
+      (a : as) -> expand (mkLambda a (mkApp' n (mkVar' 0))) as
diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs
index 4bb0db813b..e7e61fdc75 100644
--- a/test/Core/Eval/Base.hs
+++ b/test/Core/Eval/Base.hs
@@ -10,21 +10,30 @@ import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.NoDisplayInfo
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Transformation
 import Juvix.Compiler.Core.Translation.FromSource
 import System.IO.Extra (withTempDir)
 import Text.Megaparsec.Pos qualified as M
 
-coreEvalAssertion :: FilePath -> FilePath -> (String -> IO ()) -> Assertion
-coreEvalAssertion mainFile expectedFile step = do
+coreEvalAssertion ::
+  FilePath ->
+  FilePath ->
+  [TransformationId] ->
+  (InfoTable -> Assertion) ->
+  (String -> IO ()) ->
+  Assertion
+coreEvalAssertion mainFile expectedFile trans testTrans step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
     Left err -> assertFailure (show (pretty err))
     Right (_, Nothing) -> do
-      step "Compare expected and actual program output"
+      step "Compare expected an actual program output"
       expected <- TIO.readFile expectedFile
       assertEqDiff ("Check: EVAL output = " <> expectedFile) "" expected
-    Right (tab, Just node) -> do
+    Right (tabIni, Just node) -> do
+      let tab = applyTransformations trans tabIni
+      testTrans tab
       withTempDir
         ( \dirPath -> do
             let outputFile = dirPath </> "out.out"
diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs
index f689b65ea1..e9c013a4d1 100644
--- a/test/Core/Eval/Positive.hs
+++ b/test/Core/Eval/Positive.hs
@@ -19,7 +19,7 @@ testDescr PosTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ coreEvalAssertion _file _expectedFile
+          _testAssertion = Steps $ coreEvalAssertion _file _expectedFile [] (const (return ()))
         }
 
 allTests :: TestTree
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 8d20dddcfa..68f61ae3e7 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -2,6 +2,10 @@ module Core.Transformation where
 
 import Base
 import Core.Transformation.Lifting qualified as Lifting
+import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
 
 allTests :: TestTree
-allTests = testGroup "JuvixCore transformations" [Lifting.allTests]
+allTests =
+  testGroup
+    "JuvixCore transformations"
+    [Lifting.allTests, TopEtaExpand.allTests]
diff --git a/test/Core/Transformation/Base.hs b/test/Core/Transformation/Base.hs
index 71e1092e77..2a178121ad 100644
--- a/test/Core/Transformation/Base.hs
+++ b/test/Core/Transformation/Base.hs
@@ -1,17 +1,15 @@
 module Core.Transformation.Base where
 
 import Base
+import Core.Eval.Base
+import Core.Eval.Positive qualified as Eval
 import Juvix.Compiler.Core.Data.InfoTable
-import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation
-import Juvix.Compiler.Core.Translation.FromSource
-import Prettyprinter.Render.Text qualified as Text
 
 data Test = Test
-  { _testName :: String,
-    _testCoreFile :: FilePath,
+  { _testTransformations :: [TransformationId],
     _testAssertion :: InfoTable -> Assertion,
-    _testTransformations :: [TransformationId]
+    _testEval :: Eval.PosTest
   }
 
 fromTest :: Test -> TestTree
@@ -21,29 +19,11 @@ troot :: FilePath
 troot = "tests/Core/positive/"
 
 toTestDescr :: Test -> TestDescr
-toTestDescr t@Test {..} =
-  TestDescr
-    { _testName,
-      _testRoot = troot,
-      _testAssertion = Single (coreTransAssertion t)
-    }
-
-assertExpectedOutput :: FilePath -> InfoTable -> Assertion
-assertExpectedOutput testExpectedFile r = do
-  expected <- readFile testExpectedFile
-  let actualOutput = Text.renderStrict (toTextStream (ppOut opts r))
-  assertEqDiff ("Check: output = " <> testExpectedFile) actualOutput expected
-  where
-    opts :: Options
-    opts =
-      defaultOptions
-        { _optShowDeBruijnIndices = True
+toTestDescr Test {..} =
+  let Eval.PosTest {..} = _testEval
+      tRoot = troot </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ coreEvalAssertion _file _expectedFile _testTransformations _testAssertion
         }
-
-coreTransAssertion :: Test -> Assertion
-coreTransAssertion Test {..} = do
-  r <- applyTransformations [LambdaLifting] <$> parseFile _testCoreFile
-  _testAssertion r
-
-parseFile :: FilePath -> IO InfoTable
-parseFile f = fst <$> fromRightIO show (runParser "" f emptyInfoTable <$> readFile f)
diff --git a/test/Core/Transformation/TopEtaExpand.hs b/test/Core/Transformation/TopEtaExpand.hs
new file mode 100644
index 0000000000..600a920a30
--- /dev/null
+++ b/test/Core/Transformation/TopEtaExpand.hs
@@ -0,0 +1,28 @@
+module Core.Transformation.TopEtaExpand (allTests) where
+
+import Base
+import Core.Eval.Positive qualified as Eval
+import Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation
+
+allTests :: TestTree
+allTests = testGroup "Top eta expand" (mapMaybe liftTest Eval.tests)
+
+pipe :: [TransformationId]
+pipe = [TopEtaExpand]
+
+liftTest :: Eval.PosTest -> Maybe TestTree
+liftTest _testEval@Eval.PosTest {..}
+  | _name `elem` excluded = Nothing
+  | otherwise =
+      Just $
+        fromTest
+          Test
+            { _testTransformations = pipe,
+              _testAssertion = const (return ()),
+              _testEval
+            }
+
+excluded :: [String]
+excluded =
+  []

From 8e5950b788baf49104c21e4525a9332ebac52311 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 3 Oct 2022 16:14:15 +0200
Subject: [PATCH 04/73] temporary fix for lambda

---
 test/Core/Transformation/Base.hs    | 14 ++++++++++++++
 test/Core/Transformation/Lifting.hs | 12 +++++++++---
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/test/Core/Transformation/Base.hs b/test/Core/Transformation/Base.hs
index 2a178121ad..aced2b971a 100644
--- a/test/Core/Transformation/Base.hs
+++ b/test/Core/Transformation/Base.hs
@@ -4,7 +4,9 @@ import Base
 import Core.Eval.Base
 import Core.Eval.Positive qualified as Eval
 import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation
+import Prettyprinter.Render.Text qualified as Text
 
 data Test = Test
   { _testTransformations :: [TransformationId],
@@ -27,3 +29,15 @@ toTestDescr Test {..} =
           _testRoot = tRoot,
           _testAssertion = Steps $ coreEvalAssertion _file _expectedFile _testTransformations _testAssertion
         }
+
+assertExpectedOutput :: FilePath -> InfoTable -> Assertion
+assertExpectedOutput testExpectedFile r = do
+  expected <- readFile testExpectedFile
+  let actualOutput = Text.renderStrict (toTextStream (ppOut opts r))
+  assertEqDiff ("Check: output = " <> testExpectedFile) actualOutput expected
+  where
+    opts :: Options
+    opts =
+      defaultOptions
+        { _optShowDeBruijnIndices = True
+        }
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index 514832d075..51137189f9 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -1,6 +1,7 @@
 module Core.Transformation.Lifting (allTests) where
 
 import Base
+import Core.Eval.Positive qualified as Eval
 import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
@@ -18,9 +19,14 @@ liftTest _testName _testCoreFile _testExpectedFile =
   fromTest
     Test
       { _testTransformations = pipe,
-        _testCoreFile = dir </> _testCoreFile,
-        _testName,
-        _testAssertion = assertExpectedOutput expectedFile
+        _testAssertion = assertExpectedOutput expectedFile,
+        _testEval =
+          Eval.PosTest
+            { _name = _testName,
+              _relDir = dir </> _testCoreFile,
+              _file = _testCoreFile,
+              _expectedFile = _testExpectedFile
+            }
       }
   where
     expectedFile = dir </> _testExpectedFile

From c347deb4c24fdd57264385d5c7af52962e6393fa Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 3 Oct 2022 16:25:30 +0200
Subject: [PATCH 05/73] small refactor

---
 src/Juvix/Compiler/Asm/Extra/Memory.hs   |  4 ++--
 test/Core/Transformation/TopEtaExpand.hs | 25 +++++++++---------------
 2 files changed, 11 insertions(+), 18 deletions(-)

diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs
index b1582928a5..9aec965ebc 100644
--- a/src/Juvix/Compiler/Asm/Extra/Memory.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs
@@ -38,13 +38,13 @@ pushValueStack :: Type -> Memory -> Memory
 pushValueStack ty = over memoryValueStack (Stack.push ty)
 
 popValueStack :: Int -> Memory -> Memory
-popValueStack n = (!! n) . iterate (over memoryValueStack Stack.pop)
+popValueStack n = iterateN n (over memoryValueStack Stack.pop)
 
 pushTempStack :: Type -> Memory -> Memory
 pushTempStack ty = over memoryTempStack (Stack.push ty)
 
 popTempStack :: Int -> Memory -> Memory
-popTempStack n = (!! n) . iterate (over memoryTempStack Stack.pop)
+popTempStack n = iterateN n (over memoryTempStack Stack.pop)
 
 -- | Read value stack at index `n` from the top.
 topValueStack :: Int -> Memory -> Maybe Type
diff --git a/test/Core/Transformation/TopEtaExpand.hs b/test/Core/Transformation/TopEtaExpand.hs
index 600a920a30..33f2ea3a57 100644
--- a/test/Core/Transformation/TopEtaExpand.hs
+++ b/test/Core/Transformation/TopEtaExpand.hs
@@ -6,23 +6,16 @@ import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
-allTests = testGroup "Top eta expand" (mapMaybe liftTest Eval.tests)
+allTests = testGroup "Top eta expand" (map liftTest Eval.tests)
 
 pipe :: [TransformationId]
 pipe = [TopEtaExpand]
 
-liftTest :: Eval.PosTest -> Maybe TestTree
-liftTest _testEval@Eval.PosTest {..}
-  | _name `elem` excluded = Nothing
-  | otherwise =
-      Just $
-        fromTest
-          Test
-            { _testTransformations = pipe,
-              _testAssertion = const (return ()),
-              _testEval
-            }
-
-excluded :: [String]
-excluded =
-  []
+liftTest :: Eval.PosTest -> TestTree
+liftTest _testEval =
+  fromTest
+    Test
+      { _testTransformations = pipe,
+        _testAssertion = const (return ()),
+        _testEval
+      }

From 630752901afd018104292961690e451c960b310b Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 3 Oct 2022 16:35:08 +0200
Subject: [PATCH 06/73] adapt lambda lifting tests to use evaluator

---
 .../Core/Transformation/LambdaLifting.hs      |  7 ++-
 test/Core/Transformation/Lifting.hs           | 43 ++++++++-----------
 2 files changed, 22 insertions(+), 28 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 42917ca6c2..20ed38d97b 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -52,8 +52,11 @@ lambdaLifting :: InfoTable -> InfoTable
 lambdaLifting = run . mapT' (lambdaLiftNode mempty)
 
 -- | True if lambdas are only found at the top level
-isLifted :: Node -> Bool
-isLifted = not . hasNestedLambdas
+nodeIsLifted :: Node -> Bool
+nodeIsLifted = not . hasNestedLambdas
   where
     hasNestedLambdas :: Node -> Bool
     hasNestedLambdas = has (cosmos . _NLam) . snd . unfoldLambdas'
+
+isLifted :: InfoTable -> Bool
+isLifted = all nodeIsLifted . toList . (^. identContext)
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index 51137189f9..c8b26eb990 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -6,36 +6,27 @@ import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
-allTests = testGroup "Lambda lifting" tests
+allTests = testGroup "Lambda lifting" (mapMaybe liftTest Eval.tests)
 
 pipe :: [TransformationId]
 pipe = [LambdaLifting]
 
-dir :: FilePath
-dir = "lambda-lifting"
-
-liftTest :: String -> FilePath -> FilePath -> TestTree
-liftTest _testName _testCoreFile _testExpectedFile =
-  fromTest
-    Test
-      { _testTransformations = pipe,
-        _testAssertion = assertExpectedOutput expectedFile,
-        _testEval =
-          Eval.PosTest
-            { _name = _testName,
-              _relDir = dir </> _testCoreFile,
-              _file = _testCoreFile,
-              _expectedFile = _testExpectedFile
+liftTest :: Eval.PosTest -> Maybe TestTree
+liftTest _testEval@Eval.PosTest {..}
+  | _name `elem` excluded = Nothing
+  | otherwise =
+      Just $
+        fromTest
+          Test
+            { _testTransformations = pipe,
+              _testAssertion = \i -> unless (isLifted i) (error ""),
+              _testEval
             }
-      }
-  where
-    expectedFile = dir </> _testExpectedFile
 
-tests :: [TestTree]
-tests =
-  [ liftTest
-      ("Lambda lifting without let rec " <> i)
-      ("test" <> i <> ".jvc")
-      ("test" <> i <> ".out")
-    | i <- map show [1 :: Int .. 3]
+excluded :: [String]
+excluded =
+  [ "Functions returning functions with variable capture",
+    "Higher-order recursive functions",
+    "Ackermann function (higher-order definition)",
+    "LetRec"
   ]

From 8c48b492c1fa5e2ea68ee20b874af9eaa1eda95b Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 09:22:05 +0200
Subject: [PATCH 07/73] sync

---
 src/Juvix/Compiler/Core/Language/Base.hs      |  6 +--
 .../Compiler/Core/Transformation/Base.hs      |  2 +-
 tests/Core/positive/test014.jvc               |  3 +-
 tests/Core/positive/tmp.jvc                   | 47 +++++++++++++++++++
 4 files changed, 53 insertions(+), 5 deletions(-)
 create mode 100644 tests/Core/positive/tmp.jvc

diff --git a/src/Juvix/Compiler/Core/Language/Base.hs b/src/Juvix/Compiler/Core/Language/Base.hs
index 1171399a30..8c3d1e0921 100644
--- a/src/Juvix/Compiler/Core/Language/Base.hs
+++ b/src/Juvix/Compiler/Core/Language/Base.hs
@@ -16,10 +16,10 @@ import Juvix.Prelude
 
 type Location = Interval
 
--- Consecutive symbol IDs for reachable user functions.
+-- | Consecutive symbol IDs for reachable user functions.
 type Symbol = Word
 
--- Tag of a constructor, uniquely identifying it. Tag values are consecutive and
+-- | Tag of a constructor, uniquely identifying it. Tag values are consecutive and
 -- separate from symbol IDs. We might need fixed special tags in Core for common
 -- "builtin" constructors, e.g., unit, nat, lists, pairs, so that the code
 -- generator can treat them specially.
@@ -28,5 +28,5 @@ data Tag = BuiltinTag BuiltinDataTag | UserTag Word
 
 instance Hashable Tag
 
--- de Bruijn index
+-- | de Bruijn index
 type Index = Int
diff --git a/src/Juvix/Compiler/Core/Transformation/Base.hs b/src/Juvix/Compiler/Core/Transformation/Base.hs
index 26646a6dc6..11eb6a9c2a 100644
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@@ -16,7 +16,7 @@ mapT :: (Symbol -> Node -> Node) -> InfoTable -> InfoTable
 mapT f tab = tab {_identContext = HashMap.mapWithKey f (tab ^. identContext)}
 
 mapT' :: (Node -> Sem (InfoTableBuilder ': r) Node) -> InfoTable -> Sem r InfoTable
-mapT' f tab = fmap fst $ runInfoTableBuilder tab $ do
+mapT' f tab = fmap fst $ runInfoTableBuilder tab $
   mapM_
     (\(k, v) -> f v >>= registerIdentNode k)
     (HashMap.toList (tab ^. identContext))
diff --git a/tests/Core/positive/test014.jvc b/tests/Core/positive/test014.jvc
index 635af7bc39..669671e013 100644
--- a/tests/Core/positive/test014.jvc
+++ b/tests/Core/positive/test014.jvc
@@ -13,7 +13,8 @@ def y := 17;
 def func := \x x + 4;
 def z := 0;
 
-def vx := 30; def vy := 7;
+def vx := 30;
+def vy := 7;
 
 writeLn (func (y / x)) >> -- 17 div 5 + 4 = 7
 writeLn (+ (* z x) y) >> -- 17
diff --git a/tests/Core/positive/tmp.jvc b/tests/Core/positive/tmp.jvc
new file mode 100644
index 0000000000..341d5bf3b1
--- /dev/null
+++ b/tests/Core/positive/tmp.jvc
@@ -0,0 +1,47 @@
+-- lists
+
+constr nil 0;
+constr cons 2;
+
+def head := \l case l of { cons h _ := h };
+def tail := \l case l of { cons _ t := t };
+def null := \l case l of { nil := true; cons _ _ := false };
+def map := \f \l case l of { nil := nil; cons h t := cons (f h) (map f t) };
+def foldl := \f \acc \l case l of { nil := acc; cons h t := foldl f (f acc h) t };
+def foldr := \f \acc \l case l of { nil := acc; cons h t := f h (foldr f acc t) };
+-- def filter := \f \l
+--   case l of {
+--     nil := nil;
+--     cons h t :=
+--       if f h then
+--         cons h (filter f t)
+--       else
+--         filter f t
+--   };
+def rev := foldl (\acc \x cons x acc) nil;
+
+def gen := \n if n = 0 then nil else cons n (gen (n - 1));
+
+def sum := \n foldl (+) 0 (gen n);
+def sum' := \n foldr (+) 0 (gen n);
+
+def foldl' := \f \acc \l if null l then acc else foldl' f (f acc (head l)) (tail l);
+def sum'' := \n foldl' (+) 0 (gen n);
+
+-- def writeLn := \x write x >> write "\n";
+
+-- writeLn (gen 10) >>
+-- writeLn (rev (gen 10)) >>
+-- writeLn (filter (\x x > 5) (gen 10)) >>
+-- writeLn (rev (map (\x x - 1) (gen 10))) >>
+-- writeLn (sum 10000) >>
+-- writeLn (sum 100000) >>
+-- writeLn (sum' 10000) >>
+-- writeLn (sum' 100000) >>
+-- writeLn (sum'' 10000) >>
+-- writeLn (sum'' 100000)
+
+-- case λ? + (λ? + 10 $0) $0 of {
+--                 nil := nil;
+--                 cons h t := cons ((λx - x 1) h) (map (λx - x 1) t)
+--               }

From 65bf1f75ca93dc4a5739715bf3a4d1ea7e7acfcd Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 22:06:57 +0200
Subject: [PATCH 08/73] add Identity transformation

---
 .../Compiler/Core/Data/TransformationId.hs    |  1 +
 src/Juvix/Compiler/Core/Transformation.hs     |  2 ++
 .../Compiler/Core/Transformation/Identity.hs  | 11 ++++++++++
 test/Core/Transformation.hs                   |  6 +++++-
 test/Core/Transformation/Identity.hs          | 21 +++++++++++++++++++
 5 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 src/Juvix/Compiler/Core/Transformation/Identity.hs
 create mode 100644 test/Core/Transformation/Identity.hs

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index a6f80cb084..fabcfa0cff 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -5,4 +5,5 @@ import Juvix.Prelude
 data TransformationId
   = LambdaLifting
   | TopEtaExpand
+  | Identity
   deriving stock (Data)
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index 0087afb413..c1a6681eb4 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/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.LambdaLifting
 import Juvix.Compiler.Core.Transformation.TopEtaExpand
+import Juvix.Compiler.Core.Transformation.Identity
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
@@ -21,3 +22,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
     appTrans = \case
       LambdaLifting -> lambdaLifting
       TopEtaExpand -> topEtaExpand
+      Identity -> identity
diff --git a/src/Juvix/Compiler/Core/Transformation/Identity.hs b/src/Juvix/Compiler/Core/Transformation/Identity.hs
new file mode 100644
index 0000000000..ddd807e15c
--- /dev/null
+++ b/src/Juvix/Compiler/Core/Transformation/Identity.hs
@@ -0,0 +1,11 @@
+module Juvix.Compiler.Core.Transformation.Identity
+  ( module Juvix.Compiler.Core.Transformation.Identity,
+    module Juvix.Compiler.Core.Transformation.Base,
+  )
+where
+
+import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Transformation.Base
+
+identity :: InfoTable -> InfoTable
+identity = run . mapT' return
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 68f61ae3e7..279be813cf 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -3,9 +3,13 @@ module Core.Transformation where
 import Base
 import Core.Transformation.Lifting qualified as Lifting
 import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
+import Core.Transformation.Identity qualified as Identity
 
 allTests :: TestTree
 allTests =
   testGroup
     "JuvixCore transformations"
-    [Lifting.allTests, TopEtaExpand.allTests]
+    [Lifting.allTests,
+     TopEtaExpand.allTests,
+     Identity.allTests
+    ]
diff --git a/test/Core/Transformation/Identity.hs b/test/Core/Transformation/Identity.hs
new file mode 100644
index 0000000000..28fcb2ebac
--- /dev/null
+++ b/test/Core/Transformation/Identity.hs
@@ -0,0 +1,21 @@
+module Core.Transformation.Identity (allTests) where
+
+import Base
+import Core.Eval.Positive qualified as Eval
+import Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation
+
+allTests :: TestTree
+allTests = testGroup "Identity" (map liftTest Eval.tests)
+
+pipe :: [TransformationId]
+pipe = [Identity]
+
+liftTest :: Eval.PosTest -> TestTree
+liftTest _testEval =
+        fromTest
+          Test
+            { _testTransformations = pipe,
+              _testAssertion = const (return ()),
+              _testEval
+            }

From c9d55a9e2eadc49ba66c047745e53cbb4345c368 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 22:07:13 +0200
Subject: [PATCH 09/73] primitive color

---
 src/Juvix/Compiler/Core/Pretty/Base.hs | 58 ++++++++++++++------------
 src/Juvix/Data/CodeAnn.hs              |  4 ++
 2 files changed, 36 insertions(+), 26 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 10712203bd..2e84ccd1bc 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -40,16 +40,16 @@ instance PrettyCode Name where
 
 instance PrettyCode BuiltinOp where
   ppCode = \case
-    OpIntAdd -> return kwPlus
-    OpIntSub -> return kwMinus
-    OpIntMul -> return kwMul
-    OpIntDiv -> return kwDiv
-    OpIntMod -> return kwMod
-    OpIntLt -> return kwLess
-    OpIntLe -> return kwLessEquals
-    OpEq -> return kwEquals
-    OpTrace -> return kwTrace
-    OpFail -> return kwFail
+    OpIntAdd -> return primPlus
+    OpIntSub -> return primMinus
+    OpIntMul -> return primMul
+    OpIntDiv -> return primDiv
+    OpIntMod -> return primMod
+    OpIntLt -> return primLess
+    OpIntLe -> return primLessEquals
+    OpEq -> return primEquals
+    OpTrace -> return primTrace
+    OpFail -> return primFail
 
 instance PrettyCode BuiltinDataTag where
   ppCode = \case
@@ -392,26 +392,29 @@ kwUnnamedConstr = keyword Str.exclamation
 kwQuestion :: Doc Ann
 kwQuestion = keyword Str.questionMark
 
-kwLess :: Doc Ann
-kwLess = keyword Str.less
+primLess :: Doc Ann
+primLess = primitive Str.less
 
-kwLessEquals :: Doc Ann
-kwLessEquals = keyword Str.lessEqual
+primLessEquals :: Doc Ann
+primLessEquals = primitive Str.lessEqual
 
-kwPlus :: Doc Ann
-kwPlus = keyword Str.plus
+primPlus :: Doc Ann
+primPlus = primitive Str.plus
 
-kwMinus :: Doc Ann
-kwMinus = keyword Str.minus
+primMinus :: Doc Ann
+primMinus = primitive Str.minus
 
-kwMul :: Doc Ann
-kwMul = keyword Str.mul
+primMul :: Doc Ann
+primMul = primitive Str.mul
 
-kwDiv :: Doc Ann
-kwDiv = keyword Str.div
+primDiv :: Doc Ann
+primDiv = primitive Str.div
 
-kwMod :: Doc Ann
-kwMod = keyword Str.mod
+primMod :: Doc Ann
+primMod = primitive Str.mod
+
+primEquals :: Doc Ann
+primEquals = primitive Str.equal
 
 kwLetRec :: Doc Ann
 kwLetRec = keyword Str.letrec_
@@ -437,8 +440,11 @@ kwPi = keyword Str.pi_
 kwDef :: Doc Ann
 kwDef = keyword Str.def
 
-kwTrace :: Doc Ann
-kwTrace = keyword Str.trace_
+primFail :: Doc Ann
+primFail = primitive Str.fail_
+
+primTrace :: Doc Ann
+primTrace = primitive Str.trace_
 
 kwFail :: Doc Ann
 kwFail = keyword Str.fail_
diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs
index 1216bdea0f..3ed9b0d385 100644
--- a/src/Juvix/Data/CodeAnn.hs
+++ b/src/Juvix/Data/CodeAnn.hs
@@ -42,6 +42,10 @@ stylize a = case a of
   AnnDef {} -> mempty
   AnnRef {} -> mempty
 
+-- | for builtin stuff
+primitive :: Text -> Doc Ann
+primitive = annotate (AnnKind KNameAxiom) . pretty
+
 keyword :: Text -> Doc Ann
 keyword = annotate AnnKeyword . pretty
 

From 897c8c07253ad942a3eaf78acf476df0057582ad Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 22:08:31 +0200
Subject: [PATCH 10/73] fix mkLambdas and unfoldLambdas

---
 src/Juvix/Compiler/Core/Extra/Base.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 19ebbfe50a..e49ad177fa 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -145,7 +145,7 @@ unfoldApps' :: Node -> (Node, [Node])
 unfoldApps' = second (map snd) . unfoldApps
 
 mkLambdas :: [Info] -> Node -> Node
-mkLambdas is n = foldl' (flip mkLambda) n is
+mkLambdas is n = foldl' (flip mkLambda) n (reverse is)
 
 mkLambdas' :: Int -> Node -> Node
 mkLambdas' k
@@ -158,7 +158,7 @@ unfoldLambdas = go []
     go :: [Info] -> Node -> ([Info], Node)
     go acc n = case n of
       NLam (Lambda i b) -> go (i : acc) b
-      _ -> (acc, n)
+      _ -> (reverse acc, n)
 
 unfoldLambdas' :: Node -> (Int, Node)
 unfoldLambdas' = first length . unfoldLambdas

From a3f3cd1a7437702269ad30f9b11e3b5540285a18 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 23:01:27 +0200
Subject: [PATCH 11/73] format

---
 .../Compiler/Core/Data/TransformationId/Parser.hs    |  1 +
 src/Juvix/Compiler/Core/Transformation.hs            |  2 +-
 src/Juvix/Compiler/Core/Transformation/Base.hs       | 10 ++++++----
 test/Core/Transformation.hs                          |  8 ++++----
 test/Core/Transformation/Identity.hs                 | 12 ++++++------
 5 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
index 4c246b7ac2..f20b1af682 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -30,3 +30,4 @@ transformation :: MonadParsec e Text m => m TransformationId
 transformation =
   symbol "lifting" $> LambdaLifting
     <|> symbol "eta" $> TopEtaExpand
+    <|> symbol "identity" $> Identity
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index c1a6681eb4..b0826f51aa 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -11,9 +11,9 @@ where
 import Juvix.Compiler.Core.Data.TransformationId
 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.TopEtaExpand
-import Juvix.Compiler.Core.Transformation.Identity
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
diff --git a/src/Juvix/Compiler/Core/Transformation/Base.hs b/src/Juvix/Compiler/Core/Transformation/Base.hs
index 11eb6a9c2a..94e5753d23 100644
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@@ -16,7 +16,9 @@ mapT :: (Symbol -> Node -> Node) -> InfoTable -> InfoTable
 mapT f tab = tab {_identContext = HashMap.mapWithKey f (tab ^. identContext)}
 
 mapT' :: (Node -> Sem (InfoTableBuilder ': r) Node) -> InfoTable -> Sem r InfoTable
-mapT' f tab = fmap fst $ runInfoTableBuilder tab $
-  mapM_
-    (\(k, v) -> f v >>= registerIdentNode k)
-    (HashMap.toList (tab ^. identContext))
+mapT' f tab =
+  fmap fst $
+    runInfoTableBuilder tab $
+      mapM_
+        (\(k, v) -> f v >>= registerIdentNode k)
+        (HashMap.toList (tab ^. identContext))
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 279be813cf..042eb6d997 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -1,15 +1,15 @@
 module Core.Transformation where
 
 import Base
+import Core.Transformation.Identity qualified as Identity
 import Core.Transformation.Lifting qualified as Lifting
 import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
-import Core.Transformation.Identity qualified as Identity
 
 allTests :: TestTree
 allTests =
   testGroup
     "JuvixCore transformations"
-    [Lifting.allTests,
-     TopEtaExpand.allTests,
-     Identity.allTests
+    [ Lifting.allTests,
+      TopEtaExpand.allTests,
+      Identity.allTests
     ]
diff --git a/test/Core/Transformation/Identity.hs b/test/Core/Transformation/Identity.hs
index 28fcb2ebac..bbe9a69a47 100644
--- a/test/Core/Transformation/Identity.hs
+++ b/test/Core/Transformation/Identity.hs
@@ -13,9 +13,9 @@ pipe = [Identity]
 
 liftTest :: Eval.PosTest -> TestTree
 liftTest _testEval =
-        fromTest
-          Test
-            { _testTransformations = pipe,
-              _testAssertion = const (return ()),
-              _testEval
-            }
+  fromTest
+    Test
+      { _testTransformations = pipe,
+        _testAssertion = const (return ()),
+        _testEval
+      }

From b873930adf097974f3e6321a05ac84e636b1734d Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 00:42:56 +0200
Subject: [PATCH 12/73] add reverse to fix lifting

---
 src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 20ed38d97b..f1f9c3425c 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -44,7 +44,7 @@ lambdaLiftNode aboveBl top =
               _identifierIsExported = False
             }
         registerIdentNode f fBody'
-        let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
+        let fApp = mkApps' (mkIdent mempty f) (map NVar (reverse freevars))
         return (End fApp)
       m -> return (Recur m)
 

From 8693cc944dc4a4f15dab80ead12fe468c6c6dea5 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 12:14:13 +0200
Subject: [PATCH 13/73] reverse mkApps

---
 src/Juvix/Compiler/Core/Extra.hs                        | 2 +-
 src/Juvix/Compiler/Core/Extra/Base.hs                   | 4 ++--
 src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs | 2 +-
 src/Juvix/Compiler/Core/Translation/FromSource.hs       | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index d80dc18837..95113c16c9 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -120,7 +120,7 @@ developBeta = umap go
 
 etaExpand :: Int -> Node -> Node
 etaExpand 0 n = n
-etaExpand k n = mkLambdas' k (mkApps' (shift k n) (map mkVar' (reverse [0 .. k - 1])))
+etaExpand k n = mkLambdas' k (mkApps' (shift k n) (map mkVar' [0 .. k - 1]))
 
 -- | substitution of all free variables for values in an environment
 substEnv :: Env -> Node -> Node
diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index e49ad177fa..8cf71494a6 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -128,10 +128,10 @@ unfoldType' ty = case ty of
 {- functions on Node -}
 
 mkApps :: Node -> [(Info, Node)] -> Node
-mkApps = foldl' (\acc (i, n) -> mkApp i acc n)
+mkApps m = foldl' (\acc (i, n) -> mkApp i acc n) m . reverse
 
 mkApps' :: Node -> [Node] -> Node
-mkApps' = foldl' mkApp'
+mkApps' n = foldl' mkApp' n . reverse
 
 unfoldApps :: Node -> (Node, [(Info, Node)])
 unfoldApps = go []
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index f1f9c3425c..20ed38d97b 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -44,7 +44,7 @@ lambdaLiftNode aboveBl top =
               _identifierIsExported = False
             }
         registerIdentNode f fBody'
-        let fApp = mkApps' (mkIdent mempty f) (map NVar (reverse freevars))
+        let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
         return (End fApp)
       m -> return (Recur m)
 
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index eee1b744ec..8db74ec8f4 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -463,7 +463,7 @@ atoms ::
   ParsecS r Node
 atoms varsNum vars = do
   es <- P.some (atom varsNum vars)
-  return $ mkApps' (List.head es) (List.tail es)
+  return $ mkApps' (List.head es) (reverse (List.tail es))
 
 atom ::
   Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>

From 215646bc87a0e42486a731251310c9594be910c4 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 12:16:34 +0200
Subject: [PATCH 14/73] add unfoldLambdasRev

---
 src/Juvix/Compiler/Core/Extra/Base.hs  | 9 ++++++---
 src/Juvix/Compiler/Core/Pretty/Base.hs | 2 +-
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 8cf71494a6..ad100c0203 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -152,13 +152,16 @@ mkLambdas' k
   | k < 0 = impossible
   | otherwise = mkLambdas (replicate k Info.empty)
 
-unfoldLambdas :: Node -> ([Info], Node)
-unfoldLambdas = go []
+unfoldLambdasRev :: Node -> ([Info], Node)
+unfoldLambdasRev = go []
   where
     go :: [Info] -> Node -> ([Info], Node)
     go acc n = case n of
       NLam (Lambda i b) -> go (i : acc) b
-      _ -> (reverse acc, n)
+      _ -> (acc, n)
+
+unfoldLambdas :: Node -> ([Info], Node)
+unfoldLambdas = first reverse . unfoldLambdasRev
 
 unfoldLambdas' :: Node -> (Int, Node)
 unfoldLambdas' = first length . unfoldLambdas
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 2e84ccd1bc..d86cba1e2e 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -199,7 +199,7 @@ instance PrettyCode Node where
       let name = getInfoName (x ^. constrInfo)
        in ppCodeConstr' name x
     NLam Lambda {} -> do
-      let (infos, body) = unfoldLambdas node
+      let (infos, body) = unfoldLambdasRev node
       pplams <- mapM ppLam infos
       b <- ppCode body
       return $ foldl' (flip (<+>)) b pplams

From b15166095fe6dc292673a53ff9e14c37dbabf607 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 12:25:08 +0200
Subject: [PATCH 15/73] remove topeta from branch

---
 .../Compiler/Core/Data/TransformationId.hs    |  1 -
 .../Core/Data/TransformationId/Parser.hs      |  1 -
 src/Juvix/Compiler/Core/Transformation.hs     |  3 ---
 .../Core/Transformation/TopEtaExpand.hs       | 25 -------------------
 test/Core/Transformation.hs                   |  2 --
 test/Core/Transformation/TopEtaExpand.hs      | 21 ----------------
 6 files changed, 53 deletions(-)
 delete mode 100644 src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
 delete mode 100644 test/Core/Transformation/TopEtaExpand.hs

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index fabcfa0cff..a4fddbed0e 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -4,6 +4,5 @@ import Juvix.Prelude
 
 data TransformationId
   = LambdaLifting
-  | TopEtaExpand
   | 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 f20b1af682..6a1d365908 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -29,5 +29,4 @@ symbol = void . lexeme . chunk
 transformation :: MonadParsec e Text m => m TransformationId
 transformation =
   symbol "lifting" $> LambdaLifting
-    <|> symbol "eta" $> TopEtaExpand
     <|> symbol "identity" $> Identity
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index b0826f51aa..4e8fd7c134 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -3,7 +3,6 @@ module Juvix.Compiler.Core.Transformation
     module Juvix.Compiler.Core.Transformation,
     module Juvix.Compiler.Core.Transformation.Eta,
     module Juvix.Compiler.Core.Transformation.LambdaLifting,
-    module Juvix.Compiler.Core.Transformation.TopEtaExpand,
     module Juvix.Compiler.Core.Data.TransformationId,
   )
 where
@@ -13,7 +12,6 @@ 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.TopEtaExpand
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
@@ -21,5 +19,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
     appTrans :: TransformationId -> InfoTable -> InfoTable
     appTrans = \case
       LambdaLifting -> lambdaLifting
-      TopEtaExpand -> topEtaExpand
       Identity -> identity
diff --git a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
deleted file mode 100644
index de92cff76d..0000000000
--- a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-module Juvix.Compiler.Core.Transformation.TopEtaExpand where
-
-import Juvix.Compiler.Core.Extra
-import Juvix.Compiler.Core.Transformation.Base
-
-topEtaExpand :: InfoTable -> InfoTable
-topEtaExpand info = mapT go info
-  where
-    go :: Symbol -> Node -> Node
-    go sym node = case info ^. infoIdentifiers . at sym of
-      Nothing -> node
-      Just idenInfo ->
-        let args :: [Info]
-            args = map infoFromArgumentInfo (idenInfo ^. identifierArgsInfo)
-         in skipLambdas args node
-    skipLambdas :: [Info] -> Node -> Node
-    skipLambdas args node = case args of
-      [] -> node
-      (_ : as) -> case node of
-        NLam l -> NLam (over lambdaBody (skipLambdas as) l)
-        _ -> expand node (reverse args)
-    expand :: Node -> [Info] -> Node
-    expand n = \case
-      [] -> n
-      (a : as) -> expand (mkLambda a (mkApp' n (mkVar' 0))) as
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 042eb6d997..8045947c14 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -3,13 +3,11 @@ module Core.Transformation where
 import Base
 import Core.Transformation.Identity qualified as Identity
 import Core.Transformation.Lifting qualified as Lifting
-import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
 
 allTests :: TestTree
 allTests =
   testGroup
     "JuvixCore transformations"
     [ Lifting.allTests,
-      TopEtaExpand.allTests,
       Identity.allTests
     ]
diff --git a/test/Core/Transformation/TopEtaExpand.hs b/test/Core/Transformation/TopEtaExpand.hs
deleted file mode 100644
index 33f2ea3a57..0000000000
--- a/test/Core/Transformation/TopEtaExpand.hs
+++ /dev/null
@@ -1,21 +0,0 @@
-module Core.Transformation.TopEtaExpand (allTests) where
-
-import Base
-import Core.Eval.Positive qualified as Eval
-import Core.Transformation.Base
-import Juvix.Compiler.Core.Transformation
-
-allTests :: TestTree
-allTests = testGroup "Top eta expand" (map liftTest Eval.tests)
-
-pipe :: [TransformationId]
-pipe = [TopEtaExpand]
-
-liftTest :: Eval.PosTest -> TestTree
-liftTest _testEval =
-  fromTest
-    Test
-      { _testTransformations = pipe,
-        _testAssertion = const (return ()),
-        _testEval
-      }

From cf0460b14f2c1e24b074d870b3de4cd01f3ff674 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 12:26:34 +0200
Subject: [PATCH 16/73] remove tmp file

---
 tests/Core/positive/tmp.jvc | 47 -------------------------------------
 1 file changed, 47 deletions(-)
 delete mode 100644 tests/Core/positive/tmp.jvc

diff --git a/tests/Core/positive/tmp.jvc b/tests/Core/positive/tmp.jvc
deleted file mode 100644
index 341d5bf3b1..0000000000
--- a/tests/Core/positive/tmp.jvc
+++ /dev/null
@@ -1,47 +0,0 @@
--- lists
-
-constr nil 0;
-constr cons 2;
-
-def head := \l case l of { cons h _ := h };
-def tail := \l case l of { cons _ t := t };
-def null := \l case l of { nil := true; cons _ _ := false };
-def map := \f \l case l of { nil := nil; cons h t := cons (f h) (map f t) };
-def foldl := \f \acc \l case l of { nil := acc; cons h t := foldl f (f acc h) t };
-def foldr := \f \acc \l case l of { nil := acc; cons h t := f h (foldr f acc t) };
--- def filter := \f \l
---   case l of {
---     nil := nil;
---     cons h t :=
---       if f h then
---         cons h (filter f t)
---       else
---         filter f t
---   };
-def rev := foldl (\acc \x cons x acc) nil;
-
-def gen := \n if n = 0 then nil else cons n (gen (n - 1));
-
-def sum := \n foldl (+) 0 (gen n);
-def sum' := \n foldr (+) 0 (gen n);
-
-def foldl' := \f \acc \l if null l then acc else foldl' f (f acc (head l)) (tail l);
-def sum'' := \n foldl' (+) 0 (gen n);
-
--- def writeLn := \x write x >> write "\n";
-
--- writeLn (gen 10) >>
--- writeLn (rev (gen 10)) >>
--- writeLn (filter (\x x > 5) (gen 10)) >>
--- writeLn (rev (map (\x x - 1) (gen 10))) >>
--- writeLn (sum 10000) >>
--- writeLn (sum 100000) >>
--- writeLn (sum' 10000) >>
--- writeLn (sum' 100000) >>
--- writeLn (sum'' 10000) >>
--- writeLn (sum'' 100000)
-
--- case λ? + (λ? + 10 $0) $0 of {
---                 nil := nil;
---                 cons h t := cons ((λx - x 1) h) (map (λx - x 1) t)
---               }

From dcef12ea36b7706b448f5096bad9e0884f3f6d44 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 17:45:23 +0200
Subject: [PATCH 17/73] include all test except LetRec

---
 test/Core/Transformation/Lifting.hs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index c8b26eb990..0049b37ea3 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -25,8 +25,5 @@ liftTest _testEval@Eval.PosTest {..}
 
 excluded :: [String]
 excluded =
-  [ "Functions returning functions with variable capture",
-    "Higher-order recursive functions",
-    "Ackermann function (higher-order definition)",
-    "LetRec"
+  [ "LetRec"
   ]

From e907d43fb6bd1337423b163e504a0d6c1d41d9de Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 17:46:33 +0200
Subject: [PATCH 18/73] add error message

---
 test/Core/Transformation/Lifting.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index 0049b37ea3..eb16b96af7 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -19,7 +19,7 @@ liftTest _testEval@Eval.PosTest {..}
         fromTest
           Test
             { _testTransformations = pipe,
-              _testAssertion = \i -> unless (isLifted i) (error ""),
+              _testAssertion = \i -> unless (isLifted i) (error "not lambda lifted"),
               _testEval
             }
 

From 4a413b9d98554a23ee415092d2c4b0813ff0e5f8 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 6 Oct 2022 00:18:02 +0200
Subject: [PATCH 19/73] letrec lifting wip

---
 src/Juvix/Compiler/Core/Extra.hs              | 15 +++++++-
 .../Core/Transformation/LambdaLifting.hs      | 37 +++++++++++++++++--
 2 files changed, 48 insertions(+), 4 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index 95113c16c9..fcaa363656 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -97,9 +97,21 @@ captureFreeVars fv
             | Just v <- s ^. at (u - k) -> NVar (Var i (v + k))
           m -> m
 
+-- | removes the top bindings
+substs :: [Node] -> Node -> Node
+substs t = umapN go
+  where
+    len = length t
+    go k n = case n of
+      NVar (Var i idx)
+        | idx >= k, idx - k < len -> shift k (t !! (idx - k))
+        | idx > k -> mkVar i (idx - len)
+      _ -> n
+
 -- | substitute a term t for the free variable with de Bruijn index 0, avoiding
 -- variable capture; shifts all free variabes with de Bruijn index > 0 by -1 (as
 -- if the topmost binder was removed)
+-- TODO: write in terms of substs?
 subst :: Node -> Node -> Node
 subst t = umapN go
   where
@@ -129,7 +141,8 @@ substEnv env
   | otherwise = umapN go
   where
     go k n = case n of
-      NVar (Var _ idx) | idx >= k -> env !! (idx - k)
+      NVar (Var _ idx)
+       | idx >= k -> env !! (idx - k)
       _ -> n
 
 convertClosures :: Node -> Node
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 20ed38d97b..f738fb9af2 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -25,8 +25,13 @@ lambdaLiftNode aboveBl top =
     -- extracts the argument info from the binder
     go :: BinderList Info -> Node -> Sem r Recur
     go bl = \case
-      l@NLam {} -> do
-        l' <- lambdaLiftNode bl l
+      NLam l -> goLambda l
+      NRec l -> goLetRec l
+      m -> return (Recur m)
+      where
+      goLambda :: Lambda -> Sem r Recur
+      goLambda lm = do
+        l' <- lambdaLiftNode bl (NLam lm)
         let freevars = toList (getFreeVars l')
             freevarsAssocs :: [(Index, Info)]
             freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
@@ -46,7 +51,33 @@ lambdaLiftNode aboveBl top =
         registerIdentNode f fBody'
         let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
         return (End fApp)
-      m -> return (Recur m)
+
+      goLetRec :: LetRec -> Sem r Recur
+      goLetRec letr = do
+        let defs :: NonEmpty Node
+            defs = letr ^. letRecValues
+        topSymsAssocs :: NonEmpty (Symbol, Node) <- forM defs $ \d -> do
+                                               s' <- freshSymbol
+                                               return (s', d)
+        let topSyms :: NonEmpty Symbol = fst <$> topSymsAssocs
+            freevars = toList (getFreeVars (NRec letr))
+            freevarsAssocs :: [(Index, Info)]
+            freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
+            topCall :: Symbol -> Node
+            topCall s = mkApps' (mkIdent' s) (map NVar freevars)
+            topBody :: Node -> Node
+            topBody = captureFreeVars freevarsAssocs . substs (map topCall (toList topSyms))
+            letDef :: Symbol -> Node
+            letDef s = mkApps' (mkIdent' s) (map NVar freevars)
+        body' <- lambdaLiftNode bl (letr ^. letRecBody)
+        forM_ topSymsAssocs $ \(s, a) -> do registerIdentNode s (topBody a)
+        let letdefs' :: NonEmpty Node
+            letdefs' = letDef <$> topSyms
+        let res :: Node
+            res = foldl' (flip mkLet') body' letdefs'
+        return (End res)
+
+
 
 lambdaLifting :: InfoTable -> InfoTable
 lambdaLifting = run . mapT' (lambdaLiftNode mempty)

From a286ab7ac86f56ded1bdde5d8d45771094f38756 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 6 Oct 2022 13:12:51 +0200
Subject: [PATCH 20/73] sync

---
 src/Juvix/Compiler/Core/Extra.hs                       | 10 ++--------
 .../Compiler/Core/Transformation/LambdaLifting.hs      | 10 ++++++----
 2 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index fcaa363656..10e4c9ae28 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -97,7 +97,7 @@ captureFreeVars fv
             | Just v <- s ^. at (u - k) -> NVar (Var i (v + k))
           m -> m
 
--- | removes the top bindings
+-- | subst for multiple bindings
 substs :: [Node] -> Node -> Node
 substs t = umapN go
   where
@@ -111,14 +111,8 @@ substs t = umapN go
 -- | substitute a term t for the free variable with de Bruijn index 0, avoiding
 -- variable capture; shifts all free variabes with de Bruijn index > 0 by -1 (as
 -- if the topmost binder was removed)
--- TODO: write in terms of substs?
 subst :: Node -> Node -> Node
-subst t = umapN go
-  where
-    go k n = case n of
-      NVar (Var _ idx) | idx == k -> shift k t
-      NVar (Var i idx) | idx > k -> mkVar i (idx - 1)
-      _ -> n
+subst t = substs [t]
 
 -- | reduce all beta redexes present in a term and the ones created immediately
 -- downwards (i.e., a "beta-development")
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index f738fb9af2..159bda0c18 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -65,20 +65,22 @@ lambdaLiftNode aboveBl top =
             freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
             topCall :: Symbol -> Node
             topCall s = mkApps' (mkIdent' s) (map NVar freevars)
-            topBody :: Node -> Node
-            topBody = captureFreeVars freevarsAssocs . substs (map topCall (toList topSyms))
+            topBody :: Node -> Sem r Node
+            topBody b =
+                captureFreeVars freevarsAssocs . substs (map topCall (toList topSyms))
+                <$> lambdaLiftNode bl b
             letDef :: Symbol -> Node
             letDef s = mkApps' (mkIdent' s) (map NVar freevars)
         body' <- lambdaLiftNode bl (letr ^. letRecBody)
-        forM_ topSymsAssocs $ \(s, a) -> do registerIdentNode s (topBody a)
+        forM_ topSymsAssocs $ \(s, a) -> topBody a >>= registerIdentNode s
         let letdefs' :: NonEmpty Node
             letdefs' = letDef <$> topSyms
+            -- shiftedLetDefs' = zipWith shift [0 ..] letdefs'
         let res :: Node
             res = foldl' (flip mkLet') body' letdefs'
         return (End res)
 
 
-
 lambdaLifting :: InfoTable -> InfoTable
 lambdaLifting = run . mapT' (lambdaLiftNode mempty)
 

From d4c78127d0a899c03d9d97be9aebe1144b808a4b Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 30 Sep 2022 19:43:33 +0200
Subject: [PATCH 21/73] implement eta expansion

---
 src/Juvix/Compiler/Core/Data/InfoTable.hs     |  4 +--
 src/Juvix/Compiler/Core/Extra.hs              | 21 ++++++++++++++
 src/Juvix/Compiler/Core/Info/TypeInfo.hs      |  8 ++----
 src/Juvix/Compiler/Core/Language.hs           |  5 +---
 src/Juvix/Compiler/Core/Language/Nodes.hs     | 28 ++++++++++++++-----
 .../Compiler/Core/Transformation/Base.hs      |  4 +--
 src/Juvix/Compiler/Core/Transformation/Eta.hs |  2 +-
 .../Core/Transformation/LambdaLifting.hs      | 16 ++---------
 .../Compiler/Core/Translation/FromSource.hs   |  2 +-
 src/Juvix/Prelude/Base.hs                     |  4 +++
 10 files changed, 58 insertions(+), 36 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs
index e643c6f0d6..15cd83afb0 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs
@@ -45,8 +45,8 @@ data IdentifierInfo = IdentifierInfo
 
 data ArgumentInfo = ArgumentInfo
   { _argumentName :: Maybe Name,
-    _argumentType :: Maybe Type,
-    _argumentIsImplicit :: Bool
+    _argumentType :: Type,
+    _argumentIsImplicit :: IsImplicit
   }
 
 data InductiveInfo = InductiveInfo
diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index 4759e1c292..d80dc18837 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -11,12 +11,16 @@ where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Extra.Base
 import Juvix.Compiler.Core.Extra.Equality
 import Juvix.Compiler.Core.Extra.Info
 import Juvix.Compiler.Core.Extra.Recursors
 import Juvix.Compiler.Core.Extra.Recursors.Fold.Named
 import Juvix.Compiler.Core.Extra.Recursors.Map.Named
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NameInfo
+import Juvix.Compiler.Core.Info.TypeInfo
 import Juvix.Compiler.Core.Language
 
 isClosed :: Node -> Bool
@@ -138,3 +142,20 @@ convertClosures = umap go
 
 convertRuntimeNodes :: Node -> Node
 convertRuntimeNodes = convertClosures
+
+argumentInfoFromInfo :: Info -> ArgumentInfo
+argumentInfoFromInfo i =
+  ArgumentInfo
+    { _argumentName = (^. infoName) <$> Info.lookup (Proxy @NameInfo) i,
+      _argumentType = getInfoType i,
+      _argumentIsImplicit = Explicit
+    }
+
+infoFromArgumentInfo :: ArgumentInfo -> Info
+infoFromArgumentInfo arg =
+  setInfoType (arg ^. argumentType) $
+    setName
+      mempty
+  where
+    setName :: Info -> Info
+    setName i = maybe i (`setInfoName` i) (arg ^. argumentName)
diff --git a/src/Juvix/Compiler/Core/Info/TypeInfo.hs b/src/Juvix/Compiler/Core/Info/TypeInfo.hs
index 6558ad85b5..fbe06622c4 100644
--- a/src/Juvix/Compiler/Core/Info/TypeInfo.hs
+++ b/src/Juvix/Compiler/Core/Info/TypeInfo.hs
@@ -1,5 +1,6 @@
 module Juvix.Compiler.Core.Info.TypeInfo where
 
+import Juvix.Compiler.Core.Extra.Base
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Language
 
@@ -12,11 +13,8 @@ kTypeInfo = Proxy
 
 makeLenses ''TypeInfo
 
-getInfoType :: Info -> Maybe Type
-getInfoType i =
-  case Info.lookup kTypeInfo i of
-    Just (TypeInfo {..}) -> Just _infoType
-    Nothing -> Nothing
+getInfoType :: Info -> Type
+getInfoType i = maybe mkDynamic' (^. infoType) (Info.lookup kTypeInfo i)
 
 setInfoType :: Type -> Info -> Info
 setInfoType = Info.insert . TypeInfo
diff --git a/src/Juvix/Compiler/Core/Language.hs b/src/Juvix/Compiler/Core/Language.hs
index 6de540dd05..ce91a28f7c 100644
--- a/src/Juvix/Compiler/Core/Language.hs
+++ b/src/Juvix/Compiler/Core/Language.hs
@@ -1,13 +1,10 @@
+-- | This file defines the tree representation of JuvixCore (Node datatype).
 module Juvix.Compiler.Core.Language
   ( module Juvix.Compiler.Core.Language,
     module Juvix.Compiler.Core.Language.Nodes,
   )
 where
 
-{-
-  This file defines the tree representation of JuvixCore (Node datatype).
--}
-
 import Juvix.Compiler.Core.Language.Nodes
 
 {---------------------------------------------------------------------------------}
diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index 1a3607a004..8e7a086e13 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -1,3 +1,4 @@
+-- | Polymorphic Node types
 module Juvix.Compiler.Core.Language.Nodes
   ( module Juvix.Compiler.Core.Language.Base,
     module Juvix.Compiler.Core.Language.Primitives,
@@ -8,9 +9,6 @@ where
 import Juvix.Compiler.Core.Language.Base
 import Juvix.Compiler.Core.Language.Primitives
 
-{-------------------------------------------------------------------}
-{- Polymorphic Node types -}
-
 -- | De Bruijn index of a locally bound variable.
 data Var' i = Var {_varInfo :: i, _varIndex :: !Index}
 
@@ -28,9 +26,17 @@ data ConstantValue
 -- Other things we might need in the future:
 -- - ConstFloat or ConstFixedPoint
 
-data App' i a = App {_appInfo :: i, _appLeft :: !a, _appRight :: !a}
+data App' i a = App
+  { _appInfo :: i,
+    _appLeft :: !a,
+    _appRight :: !a
+  }
 
-data Apps' f i a = Apps {_appsInfo :: i, _appsFun :: !f, _appsArgs :: ![a]}
+data Apps' f i a = Apps
+  { _appsInfo :: i,
+    _appsFun :: !f,
+    _appsArgs :: ![a]
+  }
 
 -- | A builtin application. A builtin has no corresponding Node. It is treated
 -- specially by the evaluator and the code generator. For example, basic
@@ -53,11 +59,18 @@ data Constr' i a = Constr
     _constrArgs :: ![a]
   }
 
-data Lambda' i a = Lambda {_lambdaInfo :: i, _lambdaBody :: !a}
+data Lambda' i a = Lambda
+  { _lambdaInfo :: i,
+    _lambdaBody :: !a
+  }
 
 -- | `let x := value in body` is not reducible to lambda + application for the
 -- purposes of ML-polymorphic / dependent type checking or code generation!
-data Let' i a = Let {_letInfo :: i, _letValue :: !a, _letBody :: !a}
+data Let' i a = Let
+  { _letInfo :: i,
+    _letValue :: !a,
+    _letBody :: !a
+  }
 
 -- | Represents a block of mutually recursive local definitions. Both in the
 -- body and in the values `length _letRecValues` implicit binders are introduced
@@ -315,6 +328,7 @@ makeLenses ''PatternWildcard'
 makeLenses ''PatternBinder'
 makeLenses ''PatternConstr'
 makeLenses ''Pi'
+makeLenses ''Lambda'
 makeLenses ''Univ'
 makeLenses ''TypeConstr'
 makeLenses ''Dynamic'
diff --git a/src/Juvix/Compiler/Core/Transformation/Base.hs b/src/Juvix/Compiler/Core/Transformation/Base.hs
index 65172aa968..26646a6dc6 100644
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@@ -12,8 +12,8 @@ import Juvix.Compiler.Core.Language
 
 type Transformation = InfoTable -> InfoTable
 
-mapT :: (Node -> Node) -> InfoTable -> InfoTable
-mapT f tab = tab {_identContext = HashMap.map f (tab ^. identContext)}
+mapT :: (Symbol -> Node -> Node) -> InfoTable -> InfoTable
+mapT f tab = tab {_identContext = HashMap.mapWithKey f (tab ^. identContext)}
 
 mapT' :: (Node -> Sem (InfoTableBuilder ': r) Node) -> InfoTable -> Sem r InfoTable
 mapT' f tab = fmap fst $ runInfoTableBuilder tab $ do
diff --git a/src/Juvix/Compiler/Core/Transformation/Eta.hs b/src/Juvix/Compiler/Core/Transformation/Eta.hs
index f20f5c8077..89c244dfb1 100644
--- a/src/Juvix/Compiler/Core/Transformation/Eta.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Eta.hs
@@ -52,4 +52,4 @@ etaExpandApps tab =
         Nothing -> 0
 
 etaExpansionApps :: Transformation
-etaExpansionApps tab = mapT (etaExpandApps tab) tab
+etaExpansionApps tab = mapT (const (etaExpandApps tab)) tab
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 7a35ef0184..42917ca6c2 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -8,9 +8,6 @@ import Juvix.Compiler.Core.Data.BinderList (BinderList)
 import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
-import Juvix.Compiler.Core.Info qualified as Info
-import Juvix.Compiler.Core.Info.NameInfo
-import Juvix.Compiler.Core.Info.TypeInfo
 import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation.Base
 
@@ -24,17 +21,8 @@ lambdaLiftNode aboveBl top =
     typeFromArgs :: [ArgumentInfo] -> Type
     typeFromArgs = \case
       [] -> mkDynamic' -- change this when we have type info about the body
-      (a : as) -> mkPi' argTy (typeFromArgs as)
-        where
-          argTy = fromMaybe mkDynamic' (a ^. argumentType)
+      (a : as) -> mkPi' (a ^. argumentType) (typeFromArgs as)
     -- extracts the argument info from the binder
-    argInfo :: Info -> ArgumentInfo
-    argInfo i =
-      ArgumentInfo
-        { _argumentName = (^. infoName) <$> Info.lookup (Proxy @NameInfo) i,
-          _argumentType = (^. infoType) <$> Info.lookup (Proxy @TypeInfo) i,
-          _argumentIsImplicit = False
-        }
     go :: BinderList Info -> Node -> Sem r Recur
     go bl = \case
       l@NLam {} -> do
@@ -44,7 +32,7 @@ lambdaLiftNode aboveBl top =
             freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
             fBody' = captureFreeVars freevarsAssocs l'
             argsInfo :: [ArgumentInfo]
-            argsInfo = map (argInfo . snd) freevarsAssocs
+            argsInfo = map (argumentInfoFromInfo . snd) freevarsAssocs
         f <- freshSymbol
         registerIdent
           IdentifierInfo
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index b34a8cd95f..eee1b744ec 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -166,7 +166,7 @@ parseDefinition sym = do
       ArgumentInfo
         { _argumentName = getInfoName bi,
           _argumentType = getInfoType bi,
-          _argumentIsImplicit = False
+          _argumentIsImplicit = Explicit
         }
       where
         bi = getInfoBinder i
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index f453067fbb..e60d208657 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -332,6 +332,10 @@ fromRightIO pp = fromRightIO' (putStrLn . pp)
 -- Misc
 --------------------------------------------------------------------------------
 
+-- | applies a function n times
+iterateN :: Int -> (a -> a) -> a -> a
+iterateN n f = (!! n) . iterate f
+
 nubHashable :: Hashable a => [a] -> [a]
 nubHashable = HashSet.toList . HashSet.fromList
 

From 05b61da54185cbc209aeb0e5bfa95413b44e387d Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Sat, 1 Oct 2022 01:20:35 +0200
Subject: [PATCH 22/73] add missing file

---
 .../Core/Transformation/TopEtaExpand.hs       | 26 +++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs

diff --git a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
new file mode 100644
index 0000000000..f309176200
--- /dev/null
+++ b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
@@ -0,0 +1,26 @@
+module Juvix.Compiler.Core.Transformation.TopEtaExpand where
+
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+
+topEtaExpand :: InfoTable -> InfoTable
+topEtaExpand info = mapT go info
+  where
+  go :: Symbol -> Node -> Node
+  go sym node = case info ^. infoIdentifiers . at sym of
+    Nothing -> node
+    Just idenInfo ->
+      let
+        args :: [Info]
+        args = map infoFromArgumentInfo  (idenInfo ^. identifierArgsInfo)
+      in goArgs args node
+  goArgs :: [Info] -> Node -> Node
+  goArgs args node = case args of
+    [] -> node
+    (a : as) -> case node of
+      NLam l -> NLam (over lambdaBody (goArgs as) l)
+      _ -> expand node (reverse args)
+  expand :: Node -> [Info] -> Node
+  expand n = \case
+    [] -> n
+    (a : as) -> expand (mkLambda a (mkApp' n (mkVar' 0))) as

From 1bfeaa241ab6b458332bbce06e2f0bccd1606267 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 3 Oct 2022 13:32:41 +0200
Subject: [PATCH 23/73] add tests

---
 .../Compiler/Core/Data/TransformationId.hs    |  1 +
 .../Core/Data/TransformationId/Parser.hs      |  1 +
 src/Juvix/Compiler/Core/Transformation.hs     |  3 ++
 .../Core/Transformation/TopEtaExpand.hs       | 35 ++++++++--------
 test/Core/Eval/Base.hs                        | 17 ++++++--
 test/Core/Eval/Positive.hs                    |  2 +-
 test/Core/Transformation.hs                   |  6 ++-
 test/Core/Transformation/Base.hs              | 42 +++++--------------
 test/Core/Transformation/TopEtaExpand.hs      | 28 +++++++++++++
 9 files changed, 80 insertions(+), 55 deletions(-)
 create mode 100644 test/Core/Transformation/TopEtaExpand.hs

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index 0415bc76d8..a6f80cb084 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -4,4 +4,5 @@ import Juvix.Prelude
 
 data TransformationId
   = LambdaLifting
+  | TopEtaExpand
   deriving stock (Data)
diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
index dac7d81b62..4c246b7ac2 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -29,3 +29,4 @@ symbol = void . lexeme . chunk
 transformation :: MonadParsec e Text m => m TransformationId
 transformation =
   symbol "lifting" $> LambdaLifting
+    <|> symbol "eta" $> TopEtaExpand
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index 69fb993abf..0087afb413 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -3,6 +3,7 @@ module Juvix.Compiler.Core.Transformation
     module Juvix.Compiler.Core.Transformation,
     module Juvix.Compiler.Core.Transformation.Eta,
     module Juvix.Compiler.Core.Transformation.LambdaLifting,
+    module Juvix.Compiler.Core.Transformation.TopEtaExpand,
     module Juvix.Compiler.Core.Data.TransformationId,
   )
 where
@@ -11,6 +12,7 @@ import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Transformation.LambdaLifting
+import Juvix.Compiler.Core.Transformation.TopEtaExpand
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
@@ -18,3 +20,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
     appTrans :: TransformationId -> InfoTable -> InfoTable
     appTrans = \case
       LambdaLifting -> lambdaLifting
+      TopEtaExpand -> topEtaExpand
diff --git a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
index f309176200..de92cff76d 100644
--- a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
+++ b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
@@ -6,21 +6,20 @@ import Juvix.Compiler.Core.Transformation.Base
 topEtaExpand :: InfoTable -> InfoTable
 topEtaExpand info = mapT go info
   where
-  go :: Symbol -> Node -> Node
-  go sym node = case info ^. infoIdentifiers . at sym of
-    Nothing -> node
-    Just idenInfo ->
-      let
-        args :: [Info]
-        args = map infoFromArgumentInfo  (idenInfo ^. identifierArgsInfo)
-      in goArgs args node
-  goArgs :: [Info] -> Node -> Node
-  goArgs args node = case args of
-    [] -> node
-    (a : as) -> case node of
-      NLam l -> NLam (over lambdaBody (goArgs as) l)
-      _ -> expand node (reverse args)
-  expand :: Node -> [Info] -> Node
-  expand n = \case
-    [] -> n
-    (a : as) -> expand (mkLambda a (mkApp' n (mkVar' 0))) as
+    go :: Symbol -> Node -> Node
+    go sym node = case info ^. infoIdentifiers . at sym of
+      Nothing -> node
+      Just idenInfo ->
+        let args :: [Info]
+            args = map infoFromArgumentInfo (idenInfo ^. identifierArgsInfo)
+         in skipLambdas args node
+    skipLambdas :: [Info] -> Node -> Node
+    skipLambdas args node = case args of
+      [] -> node
+      (_ : as) -> case node of
+        NLam l -> NLam (over lambdaBody (skipLambdas as) l)
+        _ -> expand node (reverse args)
+    expand :: Node -> [Info] -> Node
+    expand n = \case
+      [] -> n
+      (a : as) -> expand (mkLambda a (mkApp' n (mkVar' 0))) as
diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs
index 4bb0db813b..e7e61fdc75 100644
--- a/test/Core/Eval/Base.hs
+++ b/test/Core/Eval/Base.hs
@@ -10,21 +10,30 @@ import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.NoDisplayInfo
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Transformation
 import Juvix.Compiler.Core.Translation.FromSource
 import System.IO.Extra (withTempDir)
 import Text.Megaparsec.Pos qualified as M
 
-coreEvalAssertion :: FilePath -> FilePath -> (String -> IO ()) -> Assertion
-coreEvalAssertion mainFile expectedFile step = do
+coreEvalAssertion ::
+  FilePath ->
+  FilePath ->
+  [TransformationId] ->
+  (InfoTable -> Assertion) ->
+  (String -> IO ()) ->
+  Assertion
+coreEvalAssertion mainFile expectedFile trans testTrans step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
     Left err -> assertFailure (show (pretty err))
     Right (_, Nothing) -> do
-      step "Compare expected and actual program output"
+      step "Compare expected an actual program output"
       expected <- TIO.readFile expectedFile
       assertEqDiff ("Check: EVAL output = " <> expectedFile) "" expected
-    Right (tab, Just node) -> do
+    Right (tabIni, Just node) -> do
+      let tab = applyTransformations trans tabIni
+      testTrans tab
       withTempDir
         ( \dirPath -> do
             let outputFile = dirPath </> "out.out"
diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs
index f689b65ea1..e9c013a4d1 100644
--- a/test/Core/Eval/Positive.hs
+++ b/test/Core/Eval/Positive.hs
@@ -19,7 +19,7 @@ testDescr PosTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ coreEvalAssertion _file _expectedFile
+          _testAssertion = Steps $ coreEvalAssertion _file _expectedFile [] (const (return ()))
         }
 
 allTests :: TestTree
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 8d20dddcfa..68f61ae3e7 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -2,6 +2,10 @@ module Core.Transformation where
 
 import Base
 import Core.Transformation.Lifting qualified as Lifting
+import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
 
 allTests :: TestTree
-allTests = testGroup "JuvixCore transformations" [Lifting.allTests]
+allTests =
+  testGroup
+    "JuvixCore transformations"
+    [Lifting.allTests, TopEtaExpand.allTests]
diff --git a/test/Core/Transformation/Base.hs b/test/Core/Transformation/Base.hs
index 71e1092e77..2a178121ad 100644
--- a/test/Core/Transformation/Base.hs
+++ b/test/Core/Transformation/Base.hs
@@ -1,17 +1,15 @@
 module Core.Transformation.Base where
 
 import Base
+import Core.Eval.Base
+import Core.Eval.Positive qualified as Eval
 import Juvix.Compiler.Core.Data.InfoTable
-import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation
-import Juvix.Compiler.Core.Translation.FromSource
-import Prettyprinter.Render.Text qualified as Text
 
 data Test = Test
-  { _testName :: String,
-    _testCoreFile :: FilePath,
+  { _testTransformations :: [TransformationId],
     _testAssertion :: InfoTable -> Assertion,
-    _testTransformations :: [TransformationId]
+    _testEval :: Eval.PosTest
   }
 
 fromTest :: Test -> TestTree
@@ -21,29 +19,11 @@ troot :: FilePath
 troot = "tests/Core/positive/"
 
 toTestDescr :: Test -> TestDescr
-toTestDescr t@Test {..} =
-  TestDescr
-    { _testName,
-      _testRoot = troot,
-      _testAssertion = Single (coreTransAssertion t)
-    }
-
-assertExpectedOutput :: FilePath -> InfoTable -> Assertion
-assertExpectedOutput testExpectedFile r = do
-  expected <- readFile testExpectedFile
-  let actualOutput = Text.renderStrict (toTextStream (ppOut opts r))
-  assertEqDiff ("Check: output = " <> testExpectedFile) actualOutput expected
-  where
-    opts :: Options
-    opts =
-      defaultOptions
-        { _optShowDeBruijnIndices = True
+toTestDescr Test {..} =
+  let Eval.PosTest {..} = _testEval
+      tRoot = troot </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ coreEvalAssertion _file _expectedFile _testTransformations _testAssertion
         }
-
-coreTransAssertion :: Test -> Assertion
-coreTransAssertion Test {..} = do
-  r <- applyTransformations [LambdaLifting] <$> parseFile _testCoreFile
-  _testAssertion r
-
-parseFile :: FilePath -> IO InfoTable
-parseFile f = fst <$> fromRightIO show (runParser "" f emptyInfoTable <$> readFile f)
diff --git a/test/Core/Transformation/TopEtaExpand.hs b/test/Core/Transformation/TopEtaExpand.hs
new file mode 100644
index 0000000000..600a920a30
--- /dev/null
+++ b/test/Core/Transformation/TopEtaExpand.hs
@@ -0,0 +1,28 @@
+module Core.Transformation.TopEtaExpand (allTests) where
+
+import Base
+import Core.Eval.Positive qualified as Eval
+import Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation
+
+allTests :: TestTree
+allTests = testGroup "Top eta expand" (mapMaybe liftTest Eval.tests)
+
+pipe :: [TransformationId]
+pipe = [TopEtaExpand]
+
+liftTest :: Eval.PosTest -> Maybe TestTree
+liftTest _testEval@Eval.PosTest {..}
+  | _name `elem` excluded = Nothing
+  | otherwise =
+      Just $
+        fromTest
+          Test
+            { _testTransformations = pipe,
+              _testAssertion = const (return ()),
+              _testEval
+            }
+
+excluded :: [String]
+excluded =
+  []

From efcc0b51c0f68355e9c1ee2b893a2fcb4f2c85c1 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 3 Oct 2022 16:14:15 +0200
Subject: [PATCH 24/73] temporary fix for lambda

---
 test/Core/Transformation/Base.hs    | 14 ++++++++++++++
 test/Core/Transformation/Lifting.hs | 12 +++++++++---
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/test/Core/Transformation/Base.hs b/test/Core/Transformation/Base.hs
index 2a178121ad..aced2b971a 100644
--- a/test/Core/Transformation/Base.hs
+++ b/test/Core/Transformation/Base.hs
@@ -4,7 +4,9 @@ import Base
 import Core.Eval.Base
 import Core.Eval.Positive qualified as Eval
 import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation
+import Prettyprinter.Render.Text qualified as Text
 
 data Test = Test
   { _testTransformations :: [TransformationId],
@@ -27,3 +29,15 @@ toTestDescr Test {..} =
           _testRoot = tRoot,
           _testAssertion = Steps $ coreEvalAssertion _file _expectedFile _testTransformations _testAssertion
         }
+
+assertExpectedOutput :: FilePath -> InfoTable -> Assertion
+assertExpectedOutput testExpectedFile r = do
+  expected <- readFile testExpectedFile
+  let actualOutput = Text.renderStrict (toTextStream (ppOut opts r))
+  assertEqDiff ("Check: output = " <> testExpectedFile) actualOutput expected
+  where
+    opts :: Options
+    opts =
+      defaultOptions
+        { _optShowDeBruijnIndices = True
+        }
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index 514832d075..51137189f9 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -1,6 +1,7 @@
 module Core.Transformation.Lifting (allTests) where
 
 import Base
+import Core.Eval.Positive qualified as Eval
 import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
@@ -18,9 +19,14 @@ liftTest _testName _testCoreFile _testExpectedFile =
   fromTest
     Test
       { _testTransformations = pipe,
-        _testCoreFile = dir </> _testCoreFile,
-        _testName,
-        _testAssertion = assertExpectedOutput expectedFile
+        _testAssertion = assertExpectedOutput expectedFile,
+        _testEval =
+          Eval.PosTest
+            { _name = _testName,
+              _relDir = dir </> _testCoreFile,
+              _file = _testCoreFile,
+              _expectedFile = _testExpectedFile
+            }
       }
   where
     expectedFile = dir </> _testExpectedFile

From 9851854e1309a05d07cd3869ec70555f746f0c28 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 3 Oct 2022 16:25:30 +0200
Subject: [PATCH 25/73] small refactor

---
 src/Juvix/Compiler/Asm/Extra/Memory.hs   |  4 ++--
 test/Core/Transformation/TopEtaExpand.hs | 25 +++++++++---------------
 2 files changed, 11 insertions(+), 18 deletions(-)

diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs
index b1582928a5..9aec965ebc 100644
--- a/src/Juvix/Compiler/Asm/Extra/Memory.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs
@@ -38,13 +38,13 @@ pushValueStack :: Type -> Memory -> Memory
 pushValueStack ty = over memoryValueStack (Stack.push ty)
 
 popValueStack :: Int -> Memory -> Memory
-popValueStack n = (!! n) . iterate (over memoryValueStack Stack.pop)
+popValueStack n = iterateN n (over memoryValueStack Stack.pop)
 
 pushTempStack :: Type -> Memory -> Memory
 pushTempStack ty = over memoryTempStack (Stack.push ty)
 
 popTempStack :: Int -> Memory -> Memory
-popTempStack n = (!! n) . iterate (over memoryTempStack Stack.pop)
+popTempStack n = iterateN n (over memoryTempStack Stack.pop)
 
 -- | Read value stack at index `n` from the top.
 topValueStack :: Int -> Memory -> Maybe Type
diff --git a/test/Core/Transformation/TopEtaExpand.hs b/test/Core/Transformation/TopEtaExpand.hs
index 600a920a30..33f2ea3a57 100644
--- a/test/Core/Transformation/TopEtaExpand.hs
+++ b/test/Core/Transformation/TopEtaExpand.hs
@@ -6,23 +6,16 @@ import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
-allTests = testGroup "Top eta expand" (mapMaybe liftTest Eval.tests)
+allTests = testGroup "Top eta expand" (map liftTest Eval.tests)
 
 pipe :: [TransformationId]
 pipe = [TopEtaExpand]
 
-liftTest :: Eval.PosTest -> Maybe TestTree
-liftTest _testEval@Eval.PosTest {..}
-  | _name `elem` excluded = Nothing
-  | otherwise =
-      Just $
-        fromTest
-          Test
-            { _testTransformations = pipe,
-              _testAssertion = const (return ()),
-              _testEval
-            }
-
-excluded :: [String]
-excluded =
-  []
+liftTest :: Eval.PosTest -> TestTree
+liftTest _testEval =
+  fromTest
+    Test
+      { _testTransformations = pipe,
+        _testAssertion = const (return ()),
+        _testEval
+      }

From afe19ac10847833a1ea1699883b17c791ab79866 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 3 Oct 2022 16:35:08 +0200
Subject: [PATCH 26/73] adapt lambda lifting tests to use evaluator

---
 .../Core/Transformation/LambdaLifting.hs      |  7 ++-
 test/Core/Transformation/Lifting.hs           | 43 ++++++++-----------
 2 files changed, 22 insertions(+), 28 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 42917ca6c2..20ed38d97b 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -52,8 +52,11 @@ lambdaLifting :: InfoTable -> InfoTable
 lambdaLifting = run . mapT' (lambdaLiftNode mempty)
 
 -- | True if lambdas are only found at the top level
-isLifted :: Node -> Bool
-isLifted = not . hasNestedLambdas
+nodeIsLifted :: Node -> Bool
+nodeIsLifted = not . hasNestedLambdas
   where
     hasNestedLambdas :: Node -> Bool
     hasNestedLambdas = has (cosmos . _NLam) . snd . unfoldLambdas'
+
+isLifted :: InfoTable -> Bool
+isLifted = all nodeIsLifted . toList . (^. identContext)
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index 51137189f9..c8b26eb990 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -6,36 +6,27 @@ import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
-allTests = testGroup "Lambda lifting" tests
+allTests = testGroup "Lambda lifting" (mapMaybe liftTest Eval.tests)
 
 pipe :: [TransformationId]
 pipe = [LambdaLifting]
 
-dir :: FilePath
-dir = "lambda-lifting"
-
-liftTest :: String -> FilePath -> FilePath -> TestTree
-liftTest _testName _testCoreFile _testExpectedFile =
-  fromTest
-    Test
-      { _testTransformations = pipe,
-        _testAssertion = assertExpectedOutput expectedFile,
-        _testEval =
-          Eval.PosTest
-            { _name = _testName,
-              _relDir = dir </> _testCoreFile,
-              _file = _testCoreFile,
-              _expectedFile = _testExpectedFile
+liftTest :: Eval.PosTest -> Maybe TestTree
+liftTest _testEval@Eval.PosTest {..}
+  | _name `elem` excluded = Nothing
+  | otherwise =
+      Just $
+        fromTest
+          Test
+            { _testTransformations = pipe,
+              _testAssertion = \i -> unless (isLifted i) (error ""),
+              _testEval
             }
-      }
-  where
-    expectedFile = dir </> _testExpectedFile
 
-tests :: [TestTree]
-tests =
-  [ liftTest
-      ("Lambda lifting without let rec " <> i)
-      ("test" <> i <> ".jvc")
-      ("test" <> i <> ".out")
-    | i <- map show [1 :: Int .. 3]
+excluded :: [String]
+excluded =
+  [ "Functions returning functions with variable capture",
+    "Higher-order recursive functions",
+    "Ackermann function (higher-order definition)",
+    "LetRec"
   ]

From c89cfdb0db9bc041d514dcfe6bbd8fdd286381fb Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 09:22:05 +0200
Subject: [PATCH 27/73] sync

---
 src/Juvix/Compiler/Core/Language/Base.hs      |  6 +--
 .../Compiler/Core/Transformation/Base.hs      |  2 +-
 tests/Core/positive/test014.jvc               |  3 +-
 tests/Core/positive/tmp.jvc                   | 47 +++++++++++++++++++
 4 files changed, 53 insertions(+), 5 deletions(-)
 create mode 100644 tests/Core/positive/tmp.jvc

diff --git a/src/Juvix/Compiler/Core/Language/Base.hs b/src/Juvix/Compiler/Core/Language/Base.hs
index 1171399a30..8c3d1e0921 100644
--- a/src/Juvix/Compiler/Core/Language/Base.hs
+++ b/src/Juvix/Compiler/Core/Language/Base.hs
@@ -16,10 +16,10 @@ import Juvix.Prelude
 
 type Location = Interval
 
--- Consecutive symbol IDs for reachable user functions.
+-- | Consecutive symbol IDs for reachable user functions.
 type Symbol = Word
 
--- Tag of a constructor, uniquely identifying it. Tag values are consecutive and
+-- | Tag of a constructor, uniquely identifying it. Tag values are consecutive and
 -- separate from symbol IDs. We might need fixed special tags in Core for common
 -- "builtin" constructors, e.g., unit, nat, lists, pairs, so that the code
 -- generator can treat them specially.
@@ -28,5 +28,5 @@ data Tag = BuiltinTag BuiltinDataTag | UserTag Word
 
 instance Hashable Tag
 
--- de Bruijn index
+-- | de Bruijn index
 type Index = Int
diff --git a/src/Juvix/Compiler/Core/Transformation/Base.hs b/src/Juvix/Compiler/Core/Transformation/Base.hs
index 26646a6dc6..11eb6a9c2a 100644
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@@ -16,7 +16,7 @@ mapT :: (Symbol -> Node -> Node) -> InfoTable -> InfoTable
 mapT f tab = tab {_identContext = HashMap.mapWithKey f (tab ^. identContext)}
 
 mapT' :: (Node -> Sem (InfoTableBuilder ': r) Node) -> InfoTable -> Sem r InfoTable
-mapT' f tab = fmap fst $ runInfoTableBuilder tab $ do
+mapT' f tab = fmap fst $ runInfoTableBuilder tab $
   mapM_
     (\(k, v) -> f v >>= registerIdentNode k)
     (HashMap.toList (tab ^. identContext))
diff --git a/tests/Core/positive/test014.jvc b/tests/Core/positive/test014.jvc
index 635af7bc39..669671e013 100644
--- a/tests/Core/positive/test014.jvc
+++ b/tests/Core/positive/test014.jvc
@@ -13,7 +13,8 @@ def y := 17;
 def func := \x x + 4;
 def z := 0;
 
-def vx := 30; def vy := 7;
+def vx := 30;
+def vy := 7;
 
 writeLn (func (y / x)) >> -- 17 div 5 + 4 = 7
 writeLn (+ (* z x) y) >> -- 17
diff --git a/tests/Core/positive/tmp.jvc b/tests/Core/positive/tmp.jvc
new file mode 100644
index 0000000000..341d5bf3b1
--- /dev/null
+++ b/tests/Core/positive/tmp.jvc
@@ -0,0 +1,47 @@
+-- lists
+
+constr nil 0;
+constr cons 2;
+
+def head := \l case l of { cons h _ := h };
+def tail := \l case l of { cons _ t := t };
+def null := \l case l of { nil := true; cons _ _ := false };
+def map := \f \l case l of { nil := nil; cons h t := cons (f h) (map f t) };
+def foldl := \f \acc \l case l of { nil := acc; cons h t := foldl f (f acc h) t };
+def foldr := \f \acc \l case l of { nil := acc; cons h t := f h (foldr f acc t) };
+-- def filter := \f \l
+--   case l of {
+--     nil := nil;
+--     cons h t :=
+--       if f h then
+--         cons h (filter f t)
+--       else
+--         filter f t
+--   };
+def rev := foldl (\acc \x cons x acc) nil;
+
+def gen := \n if n = 0 then nil else cons n (gen (n - 1));
+
+def sum := \n foldl (+) 0 (gen n);
+def sum' := \n foldr (+) 0 (gen n);
+
+def foldl' := \f \acc \l if null l then acc else foldl' f (f acc (head l)) (tail l);
+def sum'' := \n foldl' (+) 0 (gen n);
+
+-- def writeLn := \x write x >> write "\n";
+
+-- writeLn (gen 10) >>
+-- writeLn (rev (gen 10)) >>
+-- writeLn (filter (\x x > 5) (gen 10)) >>
+-- writeLn (rev (map (\x x - 1) (gen 10))) >>
+-- writeLn (sum 10000) >>
+-- writeLn (sum 100000) >>
+-- writeLn (sum' 10000) >>
+-- writeLn (sum' 100000) >>
+-- writeLn (sum'' 10000) >>
+-- writeLn (sum'' 100000)
+
+-- case λ? + (λ? + 10 $0) $0 of {
+--                 nil := nil;
+--                 cons h t := cons ((λx - x 1) h) (map (λx - x 1) t)
+--               }

From 4fe6c475ac73ad9dca495806f5b6e85e77ca0d02 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 22:06:57 +0200
Subject: [PATCH 28/73] add Identity transformation

---
 .../Compiler/Core/Data/TransformationId.hs    |  1 +
 src/Juvix/Compiler/Core/Transformation.hs     |  2 ++
 .../Compiler/Core/Transformation/Identity.hs  | 11 ++++++++++
 test/Core/Transformation.hs                   |  6 +++++-
 test/Core/Transformation/Identity.hs          | 21 +++++++++++++++++++
 5 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 src/Juvix/Compiler/Core/Transformation/Identity.hs
 create mode 100644 test/Core/Transformation/Identity.hs

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index a6f80cb084..fabcfa0cff 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -5,4 +5,5 @@ import Juvix.Prelude
 data TransformationId
   = LambdaLifting
   | TopEtaExpand
+  | Identity
   deriving stock (Data)
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index 0087afb413..c1a6681eb4 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/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.LambdaLifting
 import Juvix.Compiler.Core.Transformation.TopEtaExpand
+import Juvix.Compiler.Core.Transformation.Identity
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
@@ -21,3 +22,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
     appTrans = \case
       LambdaLifting -> lambdaLifting
       TopEtaExpand -> topEtaExpand
+      Identity -> identity
diff --git a/src/Juvix/Compiler/Core/Transformation/Identity.hs b/src/Juvix/Compiler/Core/Transformation/Identity.hs
new file mode 100644
index 0000000000..ddd807e15c
--- /dev/null
+++ b/src/Juvix/Compiler/Core/Transformation/Identity.hs
@@ -0,0 +1,11 @@
+module Juvix.Compiler.Core.Transformation.Identity
+  ( module Juvix.Compiler.Core.Transformation.Identity,
+    module Juvix.Compiler.Core.Transformation.Base,
+  )
+where
+
+import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Transformation.Base
+
+identity :: InfoTable -> InfoTable
+identity = run . mapT' return
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 68f61ae3e7..279be813cf 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -3,9 +3,13 @@ module Core.Transformation where
 import Base
 import Core.Transformation.Lifting qualified as Lifting
 import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
+import Core.Transformation.Identity qualified as Identity
 
 allTests :: TestTree
 allTests =
   testGroup
     "JuvixCore transformations"
-    [Lifting.allTests, TopEtaExpand.allTests]
+    [Lifting.allTests,
+     TopEtaExpand.allTests,
+     Identity.allTests
+    ]
diff --git a/test/Core/Transformation/Identity.hs b/test/Core/Transformation/Identity.hs
new file mode 100644
index 0000000000..28fcb2ebac
--- /dev/null
+++ b/test/Core/Transformation/Identity.hs
@@ -0,0 +1,21 @@
+module Core.Transformation.Identity (allTests) where
+
+import Base
+import Core.Eval.Positive qualified as Eval
+import Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation
+
+allTests :: TestTree
+allTests = testGroup "Identity" (map liftTest Eval.tests)
+
+pipe :: [TransformationId]
+pipe = [Identity]
+
+liftTest :: Eval.PosTest -> TestTree
+liftTest _testEval =
+        fromTest
+          Test
+            { _testTransformations = pipe,
+              _testAssertion = const (return ()),
+              _testEval
+            }

From 743ce0658a21f56b9e1fa48ea654160ea913c3bd Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 22:07:13 +0200
Subject: [PATCH 29/73] primitive color

---
 src/Juvix/Compiler/Core/Pretty/Base.hs | 58 ++++++++++++++------------
 src/Juvix/Data/CodeAnn.hs              |  4 ++
 2 files changed, 36 insertions(+), 26 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 10712203bd..2e84ccd1bc 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -40,16 +40,16 @@ instance PrettyCode Name where
 
 instance PrettyCode BuiltinOp where
   ppCode = \case
-    OpIntAdd -> return kwPlus
-    OpIntSub -> return kwMinus
-    OpIntMul -> return kwMul
-    OpIntDiv -> return kwDiv
-    OpIntMod -> return kwMod
-    OpIntLt -> return kwLess
-    OpIntLe -> return kwLessEquals
-    OpEq -> return kwEquals
-    OpTrace -> return kwTrace
-    OpFail -> return kwFail
+    OpIntAdd -> return primPlus
+    OpIntSub -> return primMinus
+    OpIntMul -> return primMul
+    OpIntDiv -> return primDiv
+    OpIntMod -> return primMod
+    OpIntLt -> return primLess
+    OpIntLe -> return primLessEquals
+    OpEq -> return primEquals
+    OpTrace -> return primTrace
+    OpFail -> return primFail
 
 instance PrettyCode BuiltinDataTag where
   ppCode = \case
@@ -392,26 +392,29 @@ kwUnnamedConstr = keyword Str.exclamation
 kwQuestion :: Doc Ann
 kwQuestion = keyword Str.questionMark
 
-kwLess :: Doc Ann
-kwLess = keyword Str.less
+primLess :: Doc Ann
+primLess = primitive Str.less
 
-kwLessEquals :: Doc Ann
-kwLessEquals = keyword Str.lessEqual
+primLessEquals :: Doc Ann
+primLessEquals = primitive Str.lessEqual
 
-kwPlus :: Doc Ann
-kwPlus = keyword Str.plus
+primPlus :: Doc Ann
+primPlus = primitive Str.plus
 
-kwMinus :: Doc Ann
-kwMinus = keyword Str.minus
+primMinus :: Doc Ann
+primMinus = primitive Str.minus
 
-kwMul :: Doc Ann
-kwMul = keyword Str.mul
+primMul :: Doc Ann
+primMul = primitive Str.mul
 
-kwDiv :: Doc Ann
-kwDiv = keyword Str.div
+primDiv :: Doc Ann
+primDiv = primitive Str.div
 
-kwMod :: Doc Ann
-kwMod = keyword Str.mod
+primMod :: Doc Ann
+primMod = primitive Str.mod
+
+primEquals :: Doc Ann
+primEquals = primitive Str.equal
 
 kwLetRec :: Doc Ann
 kwLetRec = keyword Str.letrec_
@@ -437,8 +440,11 @@ kwPi = keyword Str.pi_
 kwDef :: Doc Ann
 kwDef = keyword Str.def
 
-kwTrace :: Doc Ann
-kwTrace = keyword Str.trace_
+primFail :: Doc Ann
+primFail = primitive Str.fail_
+
+primTrace :: Doc Ann
+primTrace = primitive Str.trace_
 
 kwFail :: Doc Ann
 kwFail = keyword Str.fail_
diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs
index 1216bdea0f..3ed9b0d385 100644
--- a/src/Juvix/Data/CodeAnn.hs
+++ b/src/Juvix/Data/CodeAnn.hs
@@ -42,6 +42,10 @@ stylize a = case a of
   AnnDef {} -> mempty
   AnnRef {} -> mempty
 
+-- | for builtin stuff
+primitive :: Text -> Doc Ann
+primitive = annotate (AnnKind KNameAxiom) . pretty
+
 keyword :: Text -> Doc Ann
 keyword = annotate AnnKeyword . pretty
 

From 75269cae46474448764d7f657e1ec95245f4a4e6 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 22:08:31 +0200
Subject: [PATCH 30/73] fix mkLambdas and unfoldLambdas

---
 src/Juvix/Compiler/Core/Extra/Base.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 19ebbfe50a..e49ad177fa 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -145,7 +145,7 @@ unfoldApps' :: Node -> (Node, [Node])
 unfoldApps' = second (map snd) . unfoldApps
 
 mkLambdas :: [Info] -> Node -> Node
-mkLambdas is n = foldl' (flip mkLambda) n is
+mkLambdas is n = foldl' (flip mkLambda) n (reverse is)
 
 mkLambdas' :: Int -> Node -> Node
 mkLambdas' k
@@ -158,7 +158,7 @@ unfoldLambdas = go []
     go :: [Info] -> Node -> ([Info], Node)
     go acc n = case n of
       NLam (Lambda i b) -> go (i : acc) b
-      _ -> (acc, n)
+      _ -> (reverse acc, n)
 
 unfoldLambdas' :: Node -> (Int, Node)
 unfoldLambdas' = first length . unfoldLambdas

From 53af15b9938b48144708bce97a4a14bd54161cef Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 4 Oct 2022 23:01:27 +0200
Subject: [PATCH 31/73] format

---
 .../Compiler/Core/Data/TransformationId/Parser.hs    |  1 +
 src/Juvix/Compiler/Core/Transformation.hs            |  2 +-
 src/Juvix/Compiler/Core/Transformation/Base.hs       | 10 ++++++----
 test/Core/Transformation.hs                          |  8 ++++----
 test/Core/Transformation/Identity.hs                 | 12 ++++++------
 5 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
index 4c246b7ac2..f20b1af682 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -30,3 +30,4 @@ transformation :: MonadParsec e Text m => m TransformationId
 transformation =
   symbol "lifting" $> LambdaLifting
     <|> symbol "eta" $> TopEtaExpand
+    <|> symbol "identity" $> Identity
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index c1a6681eb4..b0826f51aa 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -11,9 +11,9 @@ where
 import Juvix.Compiler.Core.Data.TransformationId
 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.TopEtaExpand
-import Juvix.Compiler.Core.Transformation.Identity
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
diff --git a/src/Juvix/Compiler/Core/Transformation/Base.hs b/src/Juvix/Compiler/Core/Transformation/Base.hs
index 11eb6a9c2a..94e5753d23 100644
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@@ -16,7 +16,9 @@ mapT :: (Symbol -> Node -> Node) -> InfoTable -> InfoTable
 mapT f tab = tab {_identContext = HashMap.mapWithKey f (tab ^. identContext)}
 
 mapT' :: (Node -> Sem (InfoTableBuilder ': r) Node) -> InfoTable -> Sem r InfoTable
-mapT' f tab = fmap fst $ runInfoTableBuilder tab $
-  mapM_
-    (\(k, v) -> f v >>= registerIdentNode k)
-    (HashMap.toList (tab ^. identContext))
+mapT' f tab =
+  fmap fst $
+    runInfoTableBuilder tab $
+      mapM_
+        (\(k, v) -> f v >>= registerIdentNode k)
+        (HashMap.toList (tab ^. identContext))
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 279be813cf..042eb6d997 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -1,15 +1,15 @@
 module Core.Transformation where
 
 import Base
+import Core.Transformation.Identity qualified as Identity
 import Core.Transformation.Lifting qualified as Lifting
 import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
-import Core.Transformation.Identity qualified as Identity
 
 allTests :: TestTree
 allTests =
   testGroup
     "JuvixCore transformations"
-    [Lifting.allTests,
-     TopEtaExpand.allTests,
-     Identity.allTests
+    [ Lifting.allTests,
+      TopEtaExpand.allTests,
+      Identity.allTests
     ]
diff --git a/test/Core/Transformation/Identity.hs b/test/Core/Transformation/Identity.hs
index 28fcb2ebac..bbe9a69a47 100644
--- a/test/Core/Transformation/Identity.hs
+++ b/test/Core/Transformation/Identity.hs
@@ -13,9 +13,9 @@ pipe = [Identity]
 
 liftTest :: Eval.PosTest -> TestTree
 liftTest _testEval =
-        fromTest
-          Test
-            { _testTransformations = pipe,
-              _testAssertion = const (return ()),
-              _testEval
-            }
+  fromTest
+    Test
+      { _testTransformations = pipe,
+        _testAssertion = const (return ()),
+        _testEval
+      }

From 102b1d3248e12b7c0a42d45425477b5bc24353dc Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 00:42:56 +0200
Subject: [PATCH 32/73] add reverse to fix lifting

---
 src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 20ed38d97b..f1f9c3425c 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -44,7 +44,7 @@ lambdaLiftNode aboveBl top =
               _identifierIsExported = False
             }
         registerIdentNode f fBody'
-        let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
+        let fApp = mkApps' (mkIdent mempty f) (map NVar (reverse freevars))
         return (End fApp)
       m -> return (Recur m)
 

From 6dd40914a21eaa978b2b3d860cc7b93156fe7276 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 12:14:13 +0200
Subject: [PATCH 33/73] reverse mkApps

---
 src/Juvix/Compiler/Core/Extra.hs                        | 2 +-
 src/Juvix/Compiler/Core/Extra/Base.hs                   | 4 ++--
 src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs | 2 +-
 src/Juvix/Compiler/Core/Translation/FromSource.hs       | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index d80dc18837..95113c16c9 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -120,7 +120,7 @@ developBeta = umap go
 
 etaExpand :: Int -> Node -> Node
 etaExpand 0 n = n
-etaExpand k n = mkLambdas' k (mkApps' (shift k n) (map mkVar' (reverse [0 .. k - 1])))
+etaExpand k n = mkLambdas' k (mkApps' (shift k n) (map mkVar' [0 .. k - 1]))
 
 -- | substitution of all free variables for values in an environment
 substEnv :: Env -> Node -> Node
diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index e49ad177fa..8cf71494a6 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -128,10 +128,10 @@ unfoldType' ty = case ty of
 {- functions on Node -}
 
 mkApps :: Node -> [(Info, Node)] -> Node
-mkApps = foldl' (\acc (i, n) -> mkApp i acc n)
+mkApps m = foldl' (\acc (i, n) -> mkApp i acc n) m . reverse
 
 mkApps' :: Node -> [Node] -> Node
-mkApps' = foldl' mkApp'
+mkApps' n = foldl' mkApp' n . reverse
 
 unfoldApps :: Node -> (Node, [(Info, Node)])
 unfoldApps = go []
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index f1f9c3425c..20ed38d97b 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -44,7 +44,7 @@ lambdaLiftNode aboveBl top =
               _identifierIsExported = False
             }
         registerIdentNode f fBody'
-        let fApp = mkApps' (mkIdent mempty f) (map NVar (reverse freevars))
+        let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
         return (End fApp)
       m -> return (Recur m)
 
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index eee1b744ec..8db74ec8f4 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -463,7 +463,7 @@ atoms ::
   ParsecS r Node
 atoms varsNum vars = do
   es <- P.some (atom varsNum vars)
-  return $ mkApps' (List.head es) (List.tail es)
+  return $ mkApps' (List.head es) (reverse (List.tail es))
 
 atom ::
   Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>

From 135a0fb0d060c3d3ee2586b5315f97aa7a72144e Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 12:16:34 +0200
Subject: [PATCH 34/73] add unfoldLambdasRev

---
 src/Juvix/Compiler/Core/Extra/Base.hs  | 9 ++++++---
 src/Juvix/Compiler/Core/Pretty/Base.hs | 2 +-
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 8cf71494a6..ad100c0203 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -152,13 +152,16 @@ mkLambdas' k
   | k < 0 = impossible
   | otherwise = mkLambdas (replicate k Info.empty)
 
-unfoldLambdas :: Node -> ([Info], Node)
-unfoldLambdas = go []
+unfoldLambdasRev :: Node -> ([Info], Node)
+unfoldLambdasRev = go []
   where
     go :: [Info] -> Node -> ([Info], Node)
     go acc n = case n of
       NLam (Lambda i b) -> go (i : acc) b
-      _ -> (reverse acc, n)
+      _ -> (acc, n)
+
+unfoldLambdas :: Node -> ([Info], Node)
+unfoldLambdas = first reverse . unfoldLambdasRev
 
 unfoldLambdas' :: Node -> (Int, Node)
 unfoldLambdas' = first length . unfoldLambdas
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 2e84ccd1bc..d86cba1e2e 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -199,7 +199,7 @@ instance PrettyCode Node where
       let name = getInfoName (x ^. constrInfo)
        in ppCodeConstr' name x
     NLam Lambda {} -> do
-      let (infos, body) = unfoldLambdas node
+      let (infos, body) = unfoldLambdasRev node
       pplams <- mapM ppLam infos
       b <- ppCode body
       return $ foldl' (flip (<+>)) b pplams

From c47d6c91915e8ecea995ff68842f91057938eeaf Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 12:25:08 +0200
Subject: [PATCH 35/73] remove topeta from branch

---
 .../Compiler/Core/Data/TransformationId.hs    |  1 -
 .../Core/Data/TransformationId/Parser.hs      |  1 -
 src/Juvix/Compiler/Core/Transformation.hs     |  3 ---
 .../Core/Transformation/TopEtaExpand.hs       | 25 -------------------
 test/Core/Transformation.hs                   |  2 --
 test/Core/Transformation/TopEtaExpand.hs      | 21 ----------------
 6 files changed, 53 deletions(-)
 delete mode 100644 src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
 delete mode 100644 test/Core/Transformation/TopEtaExpand.hs

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index fabcfa0cff..a4fddbed0e 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -4,6 +4,5 @@ import Juvix.Prelude
 
 data TransformationId
   = LambdaLifting
-  | TopEtaExpand
   | 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 f20b1af682..6a1d365908 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -29,5 +29,4 @@ symbol = void . lexeme . chunk
 transformation :: MonadParsec e Text m => m TransformationId
 transformation =
   symbol "lifting" $> LambdaLifting
-    <|> symbol "eta" $> TopEtaExpand
     <|> symbol "identity" $> Identity
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index b0826f51aa..4e8fd7c134 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -3,7 +3,6 @@ module Juvix.Compiler.Core.Transformation
     module Juvix.Compiler.Core.Transformation,
     module Juvix.Compiler.Core.Transformation.Eta,
     module Juvix.Compiler.Core.Transformation.LambdaLifting,
-    module Juvix.Compiler.Core.Transformation.TopEtaExpand,
     module Juvix.Compiler.Core.Data.TransformationId,
   )
 where
@@ -13,7 +12,6 @@ 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.TopEtaExpand
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
@@ -21,5 +19,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
     appTrans :: TransformationId -> InfoTable -> InfoTable
     appTrans = \case
       LambdaLifting -> lambdaLifting
-      TopEtaExpand -> topEtaExpand
       Identity -> identity
diff --git a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
deleted file mode 100644
index de92cff76d..0000000000
--- a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-module Juvix.Compiler.Core.Transformation.TopEtaExpand where
-
-import Juvix.Compiler.Core.Extra
-import Juvix.Compiler.Core.Transformation.Base
-
-topEtaExpand :: InfoTable -> InfoTable
-topEtaExpand info = mapT go info
-  where
-    go :: Symbol -> Node -> Node
-    go sym node = case info ^. infoIdentifiers . at sym of
-      Nothing -> node
-      Just idenInfo ->
-        let args :: [Info]
-            args = map infoFromArgumentInfo (idenInfo ^. identifierArgsInfo)
-         in skipLambdas args node
-    skipLambdas :: [Info] -> Node -> Node
-    skipLambdas args node = case args of
-      [] -> node
-      (_ : as) -> case node of
-        NLam l -> NLam (over lambdaBody (skipLambdas as) l)
-        _ -> expand node (reverse args)
-    expand :: Node -> [Info] -> Node
-    expand n = \case
-      [] -> n
-      (a : as) -> expand (mkLambda a (mkApp' n (mkVar' 0))) as
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 042eb6d997..8045947c14 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -3,13 +3,11 @@ module Core.Transformation where
 import Base
 import Core.Transformation.Identity qualified as Identity
 import Core.Transformation.Lifting qualified as Lifting
-import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
 
 allTests :: TestTree
 allTests =
   testGroup
     "JuvixCore transformations"
     [ Lifting.allTests,
-      TopEtaExpand.allTests,
       Identity.allTests
     ]
diff --git a/test/Core/Transformation/TopEtaExpand.hs b/test/Core/Transformation/TopEtaExpand.hs
deleted file mode 100644
index 33f2ea3a57..0000000000
--- a/test/Core/Transformation/TopEtaExpand.hs
+++ /dev/null
@@ -1,21 +0,0 @@
-module Core.Transformation.TopEtaExpand (allTests) where
-
-import Base
-import Core.Eval.Positive qualified as Eval
-import Core.Transformation.Base
-import Juvix.Compiler.Core.Transformation
-
-allTests :: TestTree
-allTests = testGroup "Top eta expand" (map liftTest Eval.tests)
-
-pipe :: [TransformationId]
-pipe = [TopEtaExpand]
-
-liftTest :: Eval.PosTest -> TestTree
-liftTest _testEval =
-  fromTest
-    Test
-      { _testTransformations = pipe,
-        _testAssertion = const (return ()),
-        _testEval
-      }

From a43680c14b9a94325760074d0cb44d8c31bc9676 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 12:26:34 +0200
Subject: [PATCH 36/73] remove tmp file

---
 tests/Core/positive/tmp.jvc | 47 -------------------------------------
 1 file changed, 47 deletions(-)
 delete mode 100644 tests/Core/positive/tmp.jvc

diff --git a/tests/Core/positive/tmp.jvc b/tests/Core/positive/tmp.jvc
deleted file mode 100644
index 341d5bf3b1..0000000000
--- a/tests/Core/positive/tmp.jvc
+++ /dev/null
@@ -1,47 +0,0 @@
--- lists
-
-constr nil 0;
-constr cons 2;
-
-def head := \l case l of { cons h _ := h };
-def tail := \l case l of { cons _ t := t };
-def null := \l case l of { nil := true; cons _ _ := false };
-def map := \f \l case l of { nil := nil; cons h t := cons (f h) (map f t) };
-def foldl := \f \acc \l case l of { nil := acc; cons h t := foldl f (f acc h) t };
-def foldr := \f \acc \l case l of { nil := acc; cons h t := f h (foldr f acc t) };
--- def filter := \f \l
---   case l of {
---     nil := nil;
---     cons h t :=
---       if f h then
---         cons h (filter f t)
---       else
---         filter f t
---   };
-def rev := foldl (\acc \x cons x acc) nil;
-
-def gen := \n if n = 0 then nil else cons n (gen (n - 1));
-
-def sum := \n foldl (+) 0 (gen n);
-def sum' := \n foldr (+) 0 (gen n);
-
-def foldl' := \f \acc \l if null l then acc else foldl' f (f acc (head l)) (tail l);
-def sum'' := \n foldl' (+) 0 (gen n);
-
--- def writeLn := \x write x >> write "\n";
-
--- writeLn (gen 10) >>
--- writeLn (rev (gen 10)) >>
--- writeLn (filter (\x x > 5) (gen 10)) >>
--- writeLn (rev (map (\x x - 1) (gen 10))) >>
--- writeLn (sum 10000) >>
--- writeLn (sum 100000) >>
--- writeLn (sum' 10000) >>
--- writeLn (sum' 100000) >>
--- writeLn (sum'' 10000) >>
--- writeLn (sum'' 100000)
-
--- case λ? + (λ? + 10 $0) $0 of {
---                 nil := nil;
---                 cons h t := cons ((λx - x 1) h) (map (λx - x 1) t)
---               }

From 110a90c1a2ea2a88716f4c652ac0d684dc0bba5d Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 17:45:23 +0200
Subject: [PATCH 37/73] include all test except LetRec

---
 test/Core/Transformation/Lifting.hs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index c8b26eb990..0049b37ea3 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -25,8 +25,5 @@ liftTest _testEval@Eval.PosTest {..}
 
 excluded :: [String]
 excluded =
-  [ "Functions returning functions with variable capture",
-    "Higher-order recursive functions",
-    "Ackermann function (higher-order definition)",
-    "LetRec"
+  [ "LetRec"
   ]

From b3c9cce19771733c49494725a92fc0eaaaafd545 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 5 Oct 2022 17:46:33 +0200
Subject: [PATCH 38/73] add error message

---
 test/Core/Transformation/Lifting.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index 0049b37ea3..eb16b96af7 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -19,7 +19,7 @@ liftTest _testEval@Eval.PosTest {..}
         fromTest
           Test
             { _testTransformations = pipe,
-              _testAssertion = \i -> unless (isLifted i) (error ""),
+              _testAssertion = \i -> unless (isLifted i) (error "not lambda lifted"),
               _testEval
             }
 

From ed14c96dc939c2cbc1a912456a07e51a0f849497 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 6 Oct 2022 13:19:00 +0200
Subject: [PATCH 39/73] revert mkApps change

---
 src/Juvix/Compiler/Core/Extra/Base.hs                   | 4 ++--
 src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs | 2 +-
 src/Juvix/Compiler/Core/Translation/FromSource.hs       | 2 +-
 test/Core/Eval/Base.hs                                  | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index ad100c0203..102b682c87 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -128,10 +128,10 @@ unfoldType' ty = case ty of
 {- functions on Node -}
 
 mkApps :: Node -> [(Info, Node)] -> Node
-mkApps m = foldl' (\acc (i, n) -> mkApp i acc n) m . reverse
+mkApps m = foldl' (\acc (i, n) -> mkApp i acc n) m
 
 mkApps' :: Node -> [Node] -> Node
-mkApps' n = foldl' mkApp' n . reverse
+mkApps' n = foldl' mkApp' n
 
 unfoldApps :: Node -> (Node, [(Info, Node)])
 unfoldApps = go []
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 20ed38d97b..9351460361 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -44,7 +44,7 @@ lambdaLiftNode aboveBl top =
               _identifierIsExported = False
             }
         registerIdentNode f fBody'
-        let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
+        let fApp = mkApps' (mkIdent mempty f) (reverse (map NVar freevars)) -- TODO suspicious reverse
         return (End fApp)
       m -> return (Recur m)
 
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 8db74ec8f4..eee1b744ec 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -463,7 +463,7 @@ atoms ::
   ParsecS r Node
 atoms varsNum vars = do
   es <- P.some (atom varsNum vars)
-  return $ mkApps' (List.head es) (reverse (List.tail es))
+  return $ mkApps' (List.head es) (List.tail es)
 
 atom ::
   Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs
index e7e61fdc75..39b1e17529 100644
--- a/test/Core/Eval/Base.hs
+++ b/test/Core/Eval/Base.hs
@@ -28,7 +28,7 @@ coreEvalAssertion mainFile expectedFile trans testTrans step = do
   case r of
     Left err -> assertFailure (show (pretty err))
     Right (_, Nothing) -> do
-      step "Compare expected an actual program output"
+      step "Compare expected and actual program output"
       expected <- TIO.readFile expectedFile
       assertEqDiff ("Check: EVAL output = " <> expectedFile) "" expected
     Right (tabIni, Just node) -> do

From 76dd396c804c9fa76405d8e1dabd60785ec761c0 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 6 Oct 2022 17:13:36 +0200
Subject: [PATCH 40/73] fix captureFreeVars

---
 src/Juvix/Compiler/Core/Extra.hs              |  6 ++-
 src/Juvix/Compiler/Core/Extra/Base.hs         |  8 ++++
 src/Juvix/Compiler/Core/Info/BinderInfo.hs    |  6 +++
 src/Juvix/Compiler/Core/Info/NameInfo.hs      |  2 +-
 src/Juvix/Compiler/Core/Pretty/Base.hs        | 19 +++-----
 .../Core/Transformation/LambdaLifting.hs      | 45 ++++++++++---------
 6 files changed, 50 insertions(+), 36 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index 95113c16c9..1e7a9dde5a 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -79,15 +79,17 @@ cosmos f = ufoldA reassemble f
 
 -- | The list should not contain repeated indices. The 'Info' corresponds to the
 -- binder of the variable.
+-- if fv = x1, x2, .., xn
+-- the result is of the form λx1 λx2 .. λ xn b
 captureFreeVars :: [(Index, Info)] -> Node -> Node
 captureFreeVars fv
   | n == 0 = id
-  | otherwise = mkLambdas infos . mapFreeVars
+  | otherwise = mkLambdasB infos . mapFreeVars
   where
     (indices, infos) = unzip fv
     n = length fv
     s :: HashMap Index Index
-    s = HashMap.fromList (zip indices [0 ..])
+    s = HashMap.fromList (zip (reverse indices) [0 ..])
     mapFreeVars :: Node -> Node
     mapFreeVars = dmapN go
       where
diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 102b682c87..6b153b1cce 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -147,6 +147,14 @@ unfoldApps' = second (map snd) . unfoldApps
 mkLambdas :: [Info] -> Node -> Node
 mkLambdas is n = foldl' (flip mkLambda) n (reverse is)
 
+-- | the given info corresponds to the binder info
+mkLambdaB :: Info -> Node -> Node
+mkLambdaB = mkLambda . singletonInfoBinder
+
+-- | the given infos correspond to the binder infos
+mkLambdasB :: [Info] -> Node -> Node
+mkLambdasB is n = foldl' (flip mkLambdaB) n (reverse is)
+
 mkLambdas' :: Int -> Node -> Node
 mkLambdas' k
   | k < 0 = impossible
diff --git a/src/Juvix/Compiler/Core/Info/BinderInfo.hs b/src/Juvix/Compiler/Core/Info/BinderInfo.hs
index 605c1b0f20..98717952f5 100644
--- a/src/Juvix/Compiler/Core/Info/BinderInfo.hs
+++ b/src/Juvix/Compiler/Core/Info/BinderInfo.hs
@@ -36,3 +36,9 @@ getInfoBinders n i =
 
 setInfoBinders :: [Info] -> Info -> Info
 setInfoBinders = Info.insert . BindersInfo
+
+setInfoBinder :: Info -> Info -> Info
+setInfoBinder = Info.insert . BinderInfo
+
+singletonInfoBinder :: Info -> Info
+singletonInfoBinder i = setInfoBinder i mempty
diff --git a/src/Juvix/Compiler/Core/Info/NameInfo.hs b/src/Juvix/Compiler/Core/Info/NameInfo.hs
index d1ba92308c..36b360d77f 100644
--- a/src/Juvix/Compiler/Core/Info/NameInfo.hs
+++ b/src/Juvix/Compiler/Core/Info/NameInfo.hs
@@ -15,7 +15,7 @@ makeLenses ''NameInfo
 getInfoName :: Info -> Maybe Name
 getInfoName i =
   case Info.lookup kNameInfo i of
-    Just (NameInfo {..}) -> Just _infoName
+    Just NameInfo {..} -> Just _infoName
     Nothing -> Nothing
 
 setInfoName :: Name -> Info -> Info
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index d86cba1e2e..8c69c34bd7 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -198,19 +198,14 @@ instance PrettyCode Node where
     NCtr x ->
       let name = getInfoName (x ^. constrInfo)
        in ppCodeConstr' name x
-    NLam Lambda {} -> do
-      let (infos, body) = unfoldLambdasRev node
-      pplams <- mapM ppLam infos
+    NLam (Lambda i body) -> do
       b <- ppCode body
-      return $ foldl' (flip (<+>)) b pplams
-      where
-        ppLam :: Info -> Sem r (Doc Ann)
-        ppLam i =
-          case getInfoName (getInfoBinder i) of
-            Just name -> do
-              n <- ppCode name
-              return $ kwLambda <> n
-            Nothing -> return $ kwLambda <> kwQuestion
+      lam <- case getInfoName (getInfoBinder i) of
+        Just name -> do
+          n <- ppCode name
+          return $ kwLambda <> n
+        Nothing -> return $ kwLambda <> kwQuestion
+      return (lam <+> b)
     NLet x ->
       let name = getInfoName (getInfoBinder (x ^. letInfo))
        in ppCodeLet' name x
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 9351460361..73d0441fbd 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -25,28 +25,31 @@ lambdaLiftNode aboveBl top =
     -- extracts the argument info from the binder
     go :: BinderList Info -> Node -> Sem r Recur
     go bl = \case
-      l@NLam {} -> do
-        l' <- lambdaLiftNode bl l
-        let freevars = toList (getFreeVars l')
-            freevarsAssocs :: [(Index, Info)]
-            freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
-            fBody' = captureFreeVars freevarsAssocs l'
-            argsInfo :: [ArgumentInfo]
-            argsInfo = map (argumentInfoFromInfo . snd) freevarsAssocs
-        f <- freshSymbol
-        registerIdent
-          IdentifierInfo
-            { _identifierSymbol = f,
-              _identifierName = Nothing,
-              _identifierType = typeFromArgs argsInfo,
-              _identifierArgsNum = length freevars,
-              _identifierArgsInfo = argsInfo,
-              _identifierIsExported = False
-            }
-        registerIdentNode f fBody'
-        let fApp = mkApps' (mkIdent mempty f) (reverse (map NVar freevars)) -- TODO suspicious reverse
-        return (End fApp)
+      NLam l -> goLambda l
       m -> return (Recur m)
+      where
+        goLambda :: Lambda -> Sem r Recur
+        goLambda lm = do
+          l' <- lambdaLiftNode bl (NLam lm)
+          let freevars = toList (getFreeVars l')
+              freevarsAssocs :: [(Index, Info)]
+              freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
+              fBody' = captureFreeVars freevarsAssocs l'
+              argsInfo :: [ArgumentInfo]
+              argsInfo = map (argumentInfoFromInfo . snd) freevarsAssocs
+          f <- freshSymbol
+          registerIdent
+            IdentifierInfo
+              { _identifierSymbol = f,
+                _identifierName = Nothing,
+                _identifierType = typeFromArgs argsInfo,
+                _identifierArgsNum = length freevars,
+                _identifierArgsInfo = argsInfo,
+                _identifierIsExported = False
+              }
+          registerIdentNode f fBody'
+          let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
+          return (End fApp)
 
 lambdaLifting :: InfoTable -> InfoTable
 lambdaLifting = run . mapT' (lambdaLiftNode mempty)

From 4be475f9e5831a5d5132c43418569c85e40b7d08 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 6 Oct 2022 18:09:05 +0200
Subject: [PATCH 41/73] add shiftHelper

---
 .../Core/Transformation/LambdaLifting.hs         | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 159bda0c18..13deb2eb57 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -75,9 +75,21 @@ lambdaLiftNode aboveBl top =
         forM_ topSymsAssocs $ \(s, a) -> topBody a >>= registerIdentNode s
         let letdefs' :: NonEmpty Node
             letdefs' = letDef <$> topSyms
-            -- shiftedLetDefs' = zipWith shift [0 ..] letdefs'
+            -- free variables in the lets and the body need to be shifted
+            -- because we are introducing binders.
+            -- the topmost let is shifted 0
+            -- the lowermost is shifted (len - 1)
+            -- the final body is shifted len
+            shiftHelper :: Node -> NonEmpty Node -> Node
+            shiftHelper b = goShift 0
+              where
+              goShift :: Int -> NonEmpty Node -> Node
+              goShift k = \case
+                x :| yys -> case yys of
+                  [] -> shift k (mkLet' x b)
+                  (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys))
         let res :: Node
-            res = foldl' (flip mkLet') body' letdefs'
+            res = shiftHelper body' letdefs'
         return (End res)
 
 

From 1f5f950793a1e6842860e388d41ab4b9a1bbd161 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 6 Oct 2022 18:36:07 +0200
Subject: [PATCH 42/73] format

---
 src/Juvix/Compiler/Core/Extra.hs              |   2 +-
 .../Core/Transformation/LambdaLifting.hs      | 121 +++++++++---------
 .../Compiler/Core/Translation/FromSource.hs   |   2 +-
 test/Core/Transformation/Lifting.hs           |   3 +-
 4 files changed, 64 insertions(+), 64 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index 0be9ec30a8..0ed807b49d 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -138,7 +138,7 @@ substEnv env
   where
     go k n = case n of
       NVar (Var _ idx)
-       | idx >= k -> env !! (idx - k)
+        | idx >= k -> env !! (idx - k)
       _ -> n
 
 convertClosures :: Node -> Node
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 13deb2eb57..932e41937c 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -29,69 +29,68 @@ lambdaLiftNode aboveBl top =
       NRec l -> goLetRec l
       m -> return (Recur m)
       where
-      goLambda :: Lambda -> Sem r Recur
-      goLambda lm = do
-        l' <- lambdaLiftNode bl (NLam lm)
-        let freevars = toList (getFreeVars l')
-            freevarsAssocs :: [(Index, Info)]
-            freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
-            fBody' = captureFreeVars freevarsAssocs l'
-            argsInfo :: [ArgumentInfo]
-            argsInfo = map (argumentInfoFromInfo . snd) freevarsAssocs
-        f <- freshSymbol
-        registerIdent
-          IdentifierInfo
-            { _identifierSymbol = f,
-              _identifierName = Nothing,
-              _identifierType = typeFromArgs argsInfo,
-              _identifierArgsNum = length freevars,
-              _identifierArgsInfo = argsInfo,
-              _identifierIsExported = False
-            }
-        registerIdentNode f fBody'
-        let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
-        return (End fApp)
+        goLambda :: Lambda -> Sem r Recur
+        goLambda lm = do
+          l' <- lambdaLiftNode bl (NLam lm)
+          let freevars = toList (getFreeVars l')
+              freevarsAssocs :: [(Index, Info)]
+              freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
+              fBody' = captureFreeVars freevarsAssocs l'
+              argsInfo :: [ArgumentInfo]
+              argsInfo = map (argumentInfoFromInfo . snd) freevarsAssocs
+          f <- freshSymbol
+          registerIdent
+            IdentifierInfo
+              { _identifierSymbol = f,
+                _identifierName = Nothing,
+                _identifierType = typeFromArgs argsInfo,
+                _identifierArgsNum = length freevars,
+                _identifierArgsInfo = argsInfo,
+                _identifierIsExported = False
+              }
+          registerIdentNode f fBody'
+          let fApp = mkApps' (mkIdent mempty f) (map NVar freevars)
+          return (End fApp)
 
-      goLetRec :: LetRec -> Sem r Recur
-      goLetRec letr = do
-        let defs :: NonEmpty Node
-            defs = letr ^. letRecValues
-        topSymsAssocs :: NonEmpty (Symbol, Node) <- forM defs $ \d -> do
-                                               s' <- freshSymbol
-                                               return (s', d)
-        let topSyms :: NonEmpty Symbol = fst <$> topSymsAssocs
-            freevars = toList (getFreeVars (NRec letr))
-            freevarsAssocs :: [(Index, Info)]
-            freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
-            topCall :: Symbol -> Node
-            topCall s = mkApps' (mkIdent' s) (map NVar freevars)
-            topBody :: Node -> Sem r Node
-            topBody b =
+        goLetRec :: LetRec -> Sem r Recur
+        goLetRec letr = do
+          let defs :: NonEmpty Node
+              defs = letr ^. letRecValues
+          topSymsAssocs :: NonEmpty (Symbol, Node) <- forM defs $ \d -> do
+            s' <- freshSymbol
+            return (s', d)
+          let topSyms :: NonEmpty Symbol = fst <$> topSymsAssocs
+              freevars = toList (getFreeVars (NRec letr))
+              freevarsAssocs :: [(Index, Info)]
+              freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
+              topCall :: Symbol -> Node
+              topCall s = mkApps' (mkIdent' s) (map NVar freevars)
+              topBody :: Node -> Sem r Node
+              topBody b =
                 captureFreeVars freevarsAssocs . substs (map topCall (toList topSyms))
-                <$> lambdaLiftNode bl b
-            letDef :: Symbol -> Node
-            letDef s = mkApps' (mkIdent' s) (map NVar freevars)
-        body' <- lambdaLiftNode bl (letr ^. letRecBody)
-        forM_ topSymsAssocs $ \(s, a) -> topBody a >>= registerIdentNode s
-        let letdefs' :: NonEmpty Node
-            letdefs' = letDef <$> topSyms
-            -- free variables in the lets and the body need to be shifted
-            -- because we are introducing binders.
-            -- the topmost let is shifted 0
-            -- the lowermost is shifted (len - 1)
-            -- the final body is shifted len
-            shiftHelper :: Node -> NonEmpty Node -> Node
-            shiftHelper b = goShift 0
-              where
-              goShift :: Int -> NonEmpty Node -> Node
-              goShift k = \case
-                x :| yys -> case yys of
-                  [] -> shift k (mkLet' x b)
-                  (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys))
-        let res :: Node
-            res = shiftHelper body' letdefs'
-        return (End res)
-
+                  <$> lambdaLiftNode bl b
+              letDef :: Symbol -> Node
+              letDef s = mkApps' (mkIdent' s) (map NVar freevars)
+          body' <- lambdaLiftNode bl (letr ^. letRecBody)
+          forM_ topSymsAssocs $ \(s, a) -> topBody a >>= registerIdentNode s
+          let letdefs' :: NonEmpty Node
+              letdefs' = letDef <$> topSyms
+              -- free variables in the lets and the body need to be shifted
+              -- because we are introducing binders.
+              -- the topmost let is shifted 0
+              -- the lowermost is shifted (len - 1)
+              -- the final body is shifted len
+              shiftHelper :: Node -> NonEmpty Node -> Node
+              shiftHelper b = goShift 0
+                where
+                  goShift :: Int -> NonEmpty Node -> Node
+                  goShift k = \case
+                    x :| yys -> case yys of
+                      [] -> shift k (mkLet' x b)
+                      (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys))
+          let res :: Node
+              res = shiftHelper body' letdefs'
+          return (End res)
 
 lambdaLifting :: InfoTable -> InfoTable
 lambdaLifting = run . mapT' (lambdaLiftNode mempty)
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 8db74ec8f4..eee1b744ec 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -463,7 +463,7 @@ atoms ::
   ParsecS r Node
 atoms varsNum vars = do
   es <- P.some (atom varsNum vars)
-  return $ mkApps' (List.head es) (reverse (List.tail es))
+  return $ mkApps' (List.head es) (List.tail es)
 
 atom ::
   Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index eb16b96af7..a57d9fc059 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -25,5 +25,6 @@ liftTest _testEval@Eval.PosTest {..}
 
 excluded :: [String]
 excluded =
-  [ "LetRec"
+  [
+    -- "LetRec"
   ]

From 608f0ce542f794e3f03b04b392053404a80f772a Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 6 Oct 2022 23:38:12 +0200
Subject: [PATCH 43/73] letrec wip

---
 .../Compiler/Core/Transformation/LambdaLifting.hs | 15 +++++++++++----
 test/Core/Transformation/Lifting.hs               |  4 +---
 2 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 932e41937c..9e0319ff78 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -8,6 +8,7 @@ import Juvix.Compiler.Core.Data.BinderList (BinderList)
 import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info.BinderInfo qualified as Info
 import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation.Base
 
@@ -31,7 +32,9 @@ lambdaLiftNode aboveBl top =
       where
         goLambda :: Lambda -> Sem r Recur
         goLambda lm = do
-          l' <- lambdaLiftNode bl (NLam lm)
+          let lambdaBinder :: Info
+              lambdaBinder = Info.getInfoBinder (lm ^. lambdaInfo)
+          l' <- lambdaLiftNode (BL.extend lambdaBinder bl) (NLam lm)
           let freevars = toList (getFreeVars l')
               freevarsAssocs :: [(Index, Info)]
               freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
@@ -56,6 +59,10 @@ lambdaLiftNode aboveBl top =
         goLetRec letr = do
           let defs :: NonEmpty Node
               defs = letr ^. letRecValues
+              letRecBinders :: [Info]
+              letRecBinders = Info.getInfoBinders (length defs) (letr ^. letRecInfo)
+              bl' :: BinderList Info
+              bl' = BL.prepend letRecBinders bl
           topSymsAssocs :: NonEmpty (Symbol, Node) <- forM defs $ \d -> do
             s' <- freshSymbol
             return (s', d)
@@ -68,10 +75,10 @@ lambdaLiftNode aboveBl top =
               topBody :: Node -> Sem r Node
               topBody b =
                 captureFreeVars freevarsAssocs . substs (map topCall (toList topSyms))
-                  <$> lambdaLiftNode bl b
+                  <$> lambdaLiftNode bl' b
               letDef :: Symbol -> Node
               letDef s = mkApps' (mkIdent' s) (map NVar freevars)
-          body' <- lambdaLiftNode bl (letr ^. letRecBody)
+          body' <- lambdaLiftNode bl' (letr ^. letRecBody)
           forM_ topSymsAssocs $ \(s, a) -> topBody a >>= registerIdentNode s
           let letdefs' :: NonEmpty Node
               letdefs' = letDef <$> topSyms
@@ -90,7 +97,7 @@ lambdaLiftNode aboveBl top =
                       (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys))
           let res :: Node
               res = shiftHelper body' letdefs'
-          return (End res)
+          return (Recur res)
 
 lambdaLifting :: InfoTable -> InfoTable
 lambdaLifting = run . mapT' (lambdaLiftNode mempty)
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index a57d9fc059..afd2f7af1a 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -25,6 +25,4 @@ liftTest _testEval@Eval.PosTest {..}
 
 excluded :: [String]
 excluded =
-  [
-    -- "LetRec"
-  ]
+  []

From a8f8f3f2f9f82f9b9db67a6343fe8b1c142fe5f9 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 7 Oct 2022 09:19:12 +0200
Subject: [PATCH 44/73] add --eval and --no-print

---
 app/Commands/Dev/Core/Read.hs                 | 10 ++++++++-
 app/Commands/Dev/Core/Read/Options.hs         | 21 +++++++++++++++++++
 .../Core/Transformation/LambdaLifting.hs      |  3 ++-
 test/Core/Transformation.hs                   |  4 ++--
 4 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/app/Commands/Dev/Core/Read.hs b/app/Commands/Dev/Core/Read.hs
index 9c1ba62bf1..4fa2057da0 100644
--- a/app/Commands/Dev/Core/Read.hs
+++ b/app/Commands/Dev/Core/Read.hs
@@ -1,6 +1,7 @@
 module Commands.Dev.Core.Read where
 
 import Commands.Base
+import Commands.Dev.Core.Eval qualified as Eval
 import Commands.Dev.Core.Read.Options
 import Juvix.Compiler.Core.Pretty qualified as Core
 import Juvix.Compiler.Core.Transformation qualified as Core
@@ -11,7 +12,14 @@ runCommand opts = do
   s' <- embed (readFile f)
   tab <- getRight (fst <$> mapLeft JuvixError (Core.runParser "" f Core.emptyInfoTable s'))
   let tab' = Core.applyTransformations (opts ^. coreReadTransformations) tab
-  renderStdOut (Core.ppOut opts tab')
+  unless (opts ^. coreReadNoPrint) (renderStdOut (Core.ppOut opts tab'))
+  doEval
   where
+    doEval :: Sem r ()
+    doEval = when (opts ^. coreReadEval) $ do
+      embed (putStrLn "--------------------------------")
+      embed (putStrLn "|            Eval              |")
+      embed (putStrLn "--------------------------------")
+      Eval.runCommand (project opts)
     f :: FilePath
     f = opts ^. coreReadInputFile . pathPath
diff --git a/app/Commands/Dev/Core/Read/Options.hs b/app/Commands/Dev/Core/Read/Options.hs
index 4fcd766ee7..1466be16db 100644
--- a/app/Commands/Dev/Core/Read/Options.hs
+++ b/app/Commands/Dev/Core/Read/Options.hs
@@ -1,5 +1,6 @@
 module Commands.Dev.Core.Read.Options where
 
+import Commands.Dev.Core.Eval.Options qualified as Eval
 import CommonOptions
 import Juvix.Compiler.Core.Data.TransformationId.Parser
 import Juvix.Compiler.Core.Pretty.Options qualified as Core
@@ -7,6 +8,8 @@ import Juvix.Compiler.Core.Pretty.Options qualified as Core
 data CoreReadOptions = CoreReadOptions
   { _coreReadTransformations :: [TransformationId],
     _coreReadShowDeBruijn :: Bool,
+    _coreReadEval :: Bool,
+    _coreReadNoPrint :: Bool,
     _coreReadInputFile :: Path
   }
   deriving stock (Data)
@@ -19,9 +22,27 @@ instance CanonicalProjection CoreReadOptions Core.Options where
       { Core._optShowDeBruijnIndices = c ^. coreReadShowDeBruijn
       }
 
+instance CanonicalProjection CoreReadOptions Eval.CoreEvalOptions where
+  project c =
+    Eval.CoreEvalOptions
+      { _coreEvalNoIO = False,
+        _coreEvalInputFile = c ^. coreReadInputFile,
+        _coreEvalShowDeBruijn = c ^. coreReadShowDeBruijn
+      }
+
 parseCoreReadOptions :: Parser CoreReadOptions
 parseCoreReadOptions = do
   _coreReadShowDeBruijn <- optDeBruijn
+  _coreReadNoPrint <-
+    switch
+      ( long "no-print"
+          <> help "do not print the transformed code"
+      )
+  _coreReadEval <-
+    switch
+      ( long "eval"
+          <> help "evaluate after the transformation"
+      )
   _coreReadTransformations <-
     option
       (eitherReader parseTransf)
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 9e0319ff78..31b758002b 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -66,7 +66,8 @@ lambdaLiftNode aboveBl top =
           topSymsAssocs :: NonEmpty (Symbol, Node) <- forM defs $ \d -> do
             s' <- freshSymbol
             return (s', d)
-          let topSyms :: NonEmpty Symbol = fst <$> topSymsAssocs
+          let topSyms :: NonEmpty Symbol
+              topSyms = fst <$> topSymsAssocs
               freevars = toList (getFreeVars (NRec letr))
               freevarsAssocs :: [(Index, Info)]
               freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
diff --git a/test/Core/Transformation.hs b/test/Core/Transformation.hs
index 8045947c14..5f7a1d0b5c 100644
--- a/test/Core/Transformation.hs
+++ b/test/Core/Transformation.hs
@@ -8,6 +8,6 @@ allTests :: TestTree
 allTests =
   testGroup
     "JuvixCore transformations"
-    [ Lifting.allTests,
-      Identity.allTests
+    [ Identity.allTests,
+      Lifting.allTests
     ]

From 7dc93446a7a418b5958ddd88de68103c76421cb7 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 7 Oct 2022 09:49:34 +0200
Subject: [PATCH 45/73] remove dead code

---
 test/Core/Transformation/Base.hs | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/test/Core/Transformation/Base.hs b/test/Core/Transformation/Base.hs
index aced2b971a..2a178121ad 100644
--- a/test/Core/Transformation/Base.hs
+++ b/test/Core/Transformation/Base.hs
@@ -4,9 +4,7 @@ import Base
 import Core.Eval.Base
 import Core.Eval.Positive qualified as Eval
 import Juvix.Compiler.Core.Data.InfoTable
-import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation
-import Prettyprinter.Render.Text qualified as Text
 
 data Test = Test
   { _testTransformations :: [TransformationId],
@@ -29,15 +27,3 @@ toTestDescr Test {..} =
           _testRoot = tRoot,
           _testAssertion = Steps $ coreEvalAssertion _file _expectedFile _testTransformations _testAssertion
         }
-
-assertExpectedOutput :: FilePath -> InfoTable -> Assertion
-assertExpectedOutput testExpectedFile r = do
-  expected <- readFile testExpectedFile
-  let actualOutput = Text.renderStrict (toTextStream (ppOut opts r))
-  assertEqDiff ("Check: output = " <> testExpectedFile) actualOutput expected
-  where
-    opts :: Options
-    opts =
-      defaultOptions
-        { _optShowDeBruijnIndices = True
-        }

From 3f26c13c3f533d806770b01dc3419d214a544e90 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 7 Oct 2022 12:49:59 +0200
Subject: [PATCH 46/73] add debug !!

---
 src/Juvix/Prelude/Base.hs           | 10 +++++++++-
 test/Core/Transformation/Lifting.hs |  3 ++-
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index e60d208657..58b62b32ff 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -93,7 +93,7 @@ import Data.HashSet (HashSet)
 import Data.HashSet qualified as HashSet
 import Data.Hashable
 import Data.Int
-import Data.List.Extra hiding (groupSortOn, head, last, mconcatMap)
+import Data.List.Extra hiding (groupSortOn, head, last, mconcatMap, (!!))
 import Data.List.Extra qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty.Extra
@@ -228,6 +228,14 @@ tableNestedInsert k1 k2 = tableInsert (HashMap.singleton k2) (HashMap.insert k2)
 -- List
 --------------------------------------------------------------------------------
 
+(!!) :: HasCallStack => [a] -> Int -> a
+(!!) l n = case l of
+  [] -> error "out of bounds"
+  (x : xs)
+    | 0 < n -> error "negative index"
+    | 0 == n -> x
+    | otherwise -> xs !! (n - 1)
+
 revAppend :: [a] -> [a] -> [a]
 revAppend [] !ys = ys
 revAppend (x : xs) !ys = revAppend xs (x : ys)
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index afd2f7af1a..4199c8ed17 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -19,7 +19,8 @@ liftTest _testEval@Eval.PosTest {..}
         fromTest
           Test
             { _testTransformations = pipe,
-              _testAssertion = \i -> unless (isLifted i) (error "not lambda lifted"),
+              -- _testAssertion = \i -> unless (isLifted i) (error "not lambda lifted"),
+              _testAssertion = const (return ()),
               _testEval
             }
 

From 163764e14e605f97e9553b0f19e44102045b68f4 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Sat, 8 Oct 2022 16:10:45 +0200
Subject: [PATCH 47/73] properly eval transformed info table

---
 app/Commands/Dev/Core/Eval.hs | 36 +++++++++++++++++++++++------------
 app/Commands/Dev/Core/Read.hs | 10 +++++-----
 2 files changed, 29 insertions(+), 17 deletions(-)

diff --git a/app/Commands/Dev/Core/Eval.hs b/app/Commands/Dev/Core/Eval.hs
index 6bc776ec2b..84567cbf37 100644
--- a/app/Commands/Dev/Core/Eval.hs
+++ b/app/Commands/Dev/Core/Eval.hs
@@ -25,24 +25,36 @@ doEval noIO loc tab node
   | noIO = embed $ Core.catchEvalError loc (Core.eval (tab ^. Core.identContext) [] node)
   | otherwise = embed $ Core.catchEvalErrorIO loc (Core.evalIO (tab ^. Core.identContext) [] node)
 
+evalAndPrint ::
+  forall r.
+  Members '[Embed IO, App] r =>
+  CoreEvalOptions ->
+  Core.InfoTable ->
+  Core.Node ->
+  Sem r ()
+evalAndPrint opts tab node = do
+  r <- doEval (opts ^. coreEvalNoIO) defaultLoc tab node
+  case r of
+    Left err -> exitJuvixError (JuvixError err)
+    Right node'
+      | Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
+          return ()
+    Right node' -> do
+      renderStdOut (Core.ppOut opts node')
+      embed (putStrLn "")
+  where
+    defaultLoc :: Interval
+    defaultLoc = singletonInterval (mkLoc f 0 (M.initialPos f))
+    f :: FilePath
+    f = opts ^. coreEvalInputFile . pathPath
+
 runCommand :: forall r. Members '[Embed IO, App] r => CoreEvalOptions -> Sem r ()
 runCommand opts = do
   s <- embed (readFile f)
   case Core.runParser "" f Core.emptyInfoTable s of
     Left err -> exitJuvixError (JuvixError err)
-    Right (tab, Just node) -> do
-      r <- doEval (opts ^. coreEvalNoIO) defaultLoc tab node
-      case r of
-        Left err -> exitJuvixError (JuvixError err)
-        Right node'
-          | Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
-              return ()
-        Right node' -> do
-          renderStdOut (Core.ppOut opts node')
-          embed (putStrLn "")
+    Right (tab, Just node) -> do evalAndPrint opts tab node
     Right (_, Nothing) -> return ()
   where
-    defaultLoc :: Interval
-    defaultLoc = singletonInterval (mkLoc f 0 (M.initialPos f))
     f :: FilePath
     f = opts ^. coreEvalInputFile . pathPath
diff --git a/app/Commands/Dev/Core/Read.hs b/app/Commands/Dev/Core/Read.hs
index 4fa2057da0..28567d2896 100644
--- a/app/Commands/Dev/Core/Read.hs
+++ b/app/Commands/Dev/Core/Read.hs
@@ -10,16 +10,16 @@ import Juvix.Compiler.Core.Translation.FromSource qualified as Core
 runCommand :: forall r. Members '[Embed IO, App] r => CoreReadOptions -> Sem r ()
 runCommand opts = do
   s' <- embed (readFile f)
-  tab <- getRight (fst <$> mapLeft JuvixError (Core.runParser "" f Core.emptyInfoTable s'))
+  (tab, mnode) <- getRight (mapLeft JuvixError (Core.runParser "" f Core.emptyInfoTable s'))
   let tab' = Core.applyTransformations (opts ^. coreReadTransformations) tab
   unless (opts ^. coreReadNoPrint) (renderStdOut (Core.ppOut opts tab'))
-  doEval
+  whenJust mnode $ doEval tab'
   where
-    doEval :: Sem r ()
-    doEval = when (opts ^. coreReadEval) $ do
+    doEval :: Core.InfoTable -> Core.Node -> Sem r ()
+    doEval tab' node = when (opts ^. coreReadEval) $ do
       embed (putStrLn "--------------------------------")
       embed (putStrLn "|            Eval              |")
       embed (putStrLn "--------------------------------")
-      Eval.runCommand (project opts)
+      Eval.evalAndPrint (project opts) tab' node
     f :: FilePath
     f = opts ^. coreReadInputFile . pathPath

From a02515e0c53970201b0e60f9588948d68ee4907b Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Sat, 8 Oct 2022 16:19:40 +0200
Subject: [PATCH 48/73] fix !! in prelude

---
 src/Juvix/Prelude/Base.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index 58b62b32ff..89afe914f3 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -232,7 +232,7 @@ tableNestedInsert k1 k2 = tableInsert (HashMap.singleton k2) (HashMap.insert k2)
 (!!) l n = case l of
   [] -> error "out of bounds"
   (x : xs)
-    | 0 < n -> error "negative index"
+    | n < 0 -> error "negative index"
     | 0 == n -> x
     | otherwise -> xs !! (n - 1)
 

From f7d4f3437dd9f16534fa8983978ad142be8e4478 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Sat, 8 Oct 2022 16:33:31 +0200
Subject: [PATCH 49/73] change !!

---
 src/Juvix/Prelude/Base.hs | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index 89afe914f3..2d223568c3 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -229,12 +229,10 @@ tableNestedInsert k1 k2 = tableInsert (HashMap.singleton k2) (HashMap.insert k2)
 --------------------------------------------------------------------------------
 
 (!!) :: HasCallStack => [a] -> Int -> a
-(!!) l n = case l of
-  [] -> error "out of bounds"
-  (x : xs)
-    | n < 0 -> error "negative index"
-    | 0 == n -> x
-    | otherwise -> xs !! (n - 1)
+(!!) l n
+  | n < 0 = error ("negative index: " <> show n)
+  | length l <= n = error ("out of bounds: length " <> show (length l) <> "; index " <> show n)
+  | otherwise = l List.!! n
 
 revAppend :: [a] -> [a] -> [a]
 revAppend [] !ys = ys

From e8ee4c0eae567f0cd938b2417ce8c23fcd2fc7ae Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 10 Oct 2022 18:33:52 +0200
Subject: [PATCH 50/73] fix and optimize letrec lifting

---
 src/Juvix/Compiler/Core/Extra.hs              | 13 ++-
 src/Juvix/Compiler/Core/Language/Nodes.hs     |  1 +
 .../Core/Transformation/LambdaLifting.hs      | 80 +++++++++++++------
 src/Juvix/Prelude/Base.hs                     |  9 +++
 4 files changed, 76 insertions(+), 27 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index 0ed807b49d..d5e182f5e2 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -11,6 +11,8 @@ where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Core.Data.BinderList (BinderList)
+import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Extra.Base
 import Juvix.Compiler.Core.Extra.Equality
@@ -26,8 +28,15 @@ import Juvix.Compiler.Core.Language
 isClosed :: Node -> Bool
 isClosed = not . has freeVars
 
-getFreeVars :: Node -> HashSet Var
-getFreeVars n = HashSet.fromList (n ^.. freeVars)
+freeVarsSet :: Node -> HashSet Var
+freeVarsSet n = HashSet.fromList (n ^.. freeVars)
+
+freeVarsWithInfo :: BinderList Info -> Node -> [(Index, Info)]
+freeVarsWithInfo bl n =
+  [ (i, BL.lookup i bl)
+    | v <- toList (freeVarsSet n),
+      let i = v ^. varIndex
+  ]
 
 freeVars :: SimpleFold Node Var
 freeVars f = ufoldNA reassemble go
diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index 8e7a086e13..a52bd5e4a9 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -75,6 +75,7 @@ data Let' i a = Let
 -- | Represents a block of mutually recursive local definitions. Both in the
 -- body and in the values `length _letRecValues` implicit binders are introduced
 -- which hold the functions/values being defined.
+-- the last item _letRecValues will have have index $0 in the body.
 data LetRec' i a = LetRec
   { _letRecInfo :: i,
     _letRecValues :: !(NonEmpty a),
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 31b758002b..4a9fd6e05c 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -35,7 +35,7 @@ lambdaLiftNode aboveBl top =
           let lambdaBinder :: Info
               lambdaBinder = Info.getInfoBinder (lm ^. lambdaInfo)
           l' <- lambdaLiftNode (BL.extend lambdaBinder bl) (NLam lm)
-          let freevars = toList (getFreeVars l')
+          let freevars = toList (freeVarsSet l')
               freevarsAssocs :: [(Index, Info)]
               freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
               fBody' = captureFreeVars freevarsAssocs l'
@@ -57,47 +57,77 @@ lambdaLiftNode aboveBl top =
 
         goLetRec :: LetRec -> Sem r Recur
         goLetRec letr = do
-          let defs :: NonEmpty Node
-              defs = letr ^. letRecValues
+          let defs :: [Node]
+              defs = toList (letr ^. letRecValues)
+              ndefs :: Int
+              ndefs = length defs
               letRecBinders :: [Info]
-              letRecBinders = Info.getInfoBinders (length defs) (letr ^. letRecInfo)
+              letRecBinders = Info.getInfoBinders ndefs (letr ^. letRecInfo)
               bl' :: BinderList Info
               bl' = BL.prepend letRecBinders bl
-          topSymsAssocs :: NonEmpty (Symbol, Node) <- forM defs $ \d -> do
+          topSymsAssocs :: [(Symbol, Node)] <- forM defs $ \d -> do
             s' <- freshSymbol
             return (s', d)
-          let topSyms :: NonEmpty Symbol
-              topSyms = fst <$> topSymsAssocs
-              freevars = toList (getFreeVars (NRec letr))
-              freevarsAssocs :: [(Index, Info)]
-              freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
-              topCall :: Symbol -> Node
-              topCall s = mkApps' (mkIdent' s) (map NVar freevars)
-              topBody :: Node -> Sem r Node
-              topBody b =
-                captureFreeVars freevarsAssocs . substs (map topCall (toList topSyms))
-                  <$> lambdaLiftNode bl' b
-              letDef :: Symbol -> Node
-              letDef s = mkApps' (mkIdent' s) (map NVar freevars)
+          let topSyms :: [Symbol]
+              topSyms = map fst topSymsAssocs
+              -- free vars in each let
+              recItemsFreeVars :: [[(Index, Info)]]
+              recItemsFreeVars = mapMaybe helper . toList . freeVarsSet <$> defs
+                where
+                  -- throw away variables bound in the letrec and shift others
+                  helper :: Var -> Maybe (Index, Info)
+                  helper v
+                    | idx < ndefs = Nothing
+                    | otherwise =
+                        let idx' = idx - ndefs
+                         in Just (idx', BL.lookup idx' bl)
+                    where
+                      idx = v ^. varIndex
+              -- replace calls to letrec items to a calls to the fresh top symbols
+              subsCalls :: Node -> Node
+              subsCalls =
+                substs
+                  ( reverse
+                      [ mkApps' (mkIdent' sym) (map (mkVar' . fst) fv)
+                        | (sym, fv) <- zipExact topSyms recItemsFreeVars
+                      ]
+                  )
+              declareTopSyms :: Sem r ()
+              declareTopSyms = do
+                tbs <- topBodies
+                zipWithExactM_ registerIdentNode topSyms tbs
+                where
+                  topBodies :: Sem r [Node]
+                  topBodies =
+                    sequence
+                      [ captureFreeVars fv . subsCalls
+                          <$> lambdaLiftNode bl' b
+                        | (b, fv) <- zipExact defs recItemsFreeVars
+                      ]
+              letItems :: [Node]
+              letItems =
+                [ mkApps' (mkIdent' s) (map (mkVar' . fst) fv)
+                  | (s, fv) <- zipExact topSyms recItemsFreeVars
+                ]
+          declareTopSyms
           body' <- lambdaLiftNode bl' (letr ^. letRecBody)
-          forM_ topSymsAssocs $ \(s, a) -> topBody a >>= registerIdentNode s
-          let letdefs' :: NonEmpty Node
-              letdefs' = letDef <$> topSyms
-              -- free variables in the lets and the body need to be shifted
+          let -- free variables in the lets and the body need to be shifted
               -- because we are introducing binders.
               -- the topmost let is shifted 0
               -- the lowermost is shifted (len - 1)
-              -- the final body is shifted len
+              -- the final body is not shifted
               shiftHelper :: Node -> NonEmpty Node -> Node
               shiftHelper b = goShift 0
                 where
                   goShift :: Int -> NonEmpty Node -> Node
                   goShift k = \case
                     x :| yys -> case yys of
-                      [] -> shift k (mkLet' x b)
+                      [] -> mkLet' (shift k x) b
                       (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys))
           let res :: Node
-              res = shiftHelper body' letdefs'
+              res = shiftHelper body' (nonEmpty' letItems)
+          -- TODO: if there is a lambda on top of body', I think it is possible to just move it up instead of recursing.
+          -- However, recursing should be ok
           return (Recur res)
 
 lambdaLifting :: InfoTable -> InfoTable
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index 2d223568c3..f1be6c7e32 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -256,6 +256,12 @@ commonPrefix a b = reverse (go [] a b)
         | x' == y' -> go (x' : ac) xs ys
       _ -> ac
 
+zipWithExactM :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m [c]
+zipWithExactM f a b = mapM (uncurry f) (zipExact a b)
+
+zipWithExactM_ :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m ()
+zipWithExactM_ f a b = void (zipWithExactM f a b)
+
 --------------------------------------------------------------------------------
 -- NonEmpty
 --------------------------------------------------------------------------------
@@ -263,6 +269,9 @@ commonPrefix a b = reverse (go [] a b)
 nonEmptyUnsnoc :: NonEmpty a -> (Maybe (NonEmpty a), a)
 nonEmptyUnsnoc e = (NonEmpty.nonEmpty (NonEmpty.init e), NonEmpty.last e)
 
+nonEmpty' :: HasCallStack => [a] -> NonEmpty a
+nonEmpty' = fromJust . nonEmpty
+
 _nonEmpty :: Lens' [a] (Maybe (NonEmpty a))
 _nonEmpty f x = maybe [] toList <$> f (nonEmpty x)
 

From 88353e663c7f3caa576073b9c06ae4a55ef3872c Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 10 Oct 2022 19:27:48 +0200
Subject: [PATCH 51/73] revert !!

---
 src/Juvix/Prelude/Base.hs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index f1be6c7e32..cfe760c823 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -93,7 +93,7 @@ import Data.HashSet (HashSet)
 import Data.HashSet qualified as HashSet
 import Data.Hashable
 import Data.Int
-import Data.List.Extra hiding (groupSortOn, head, last, mconcatMap, (!!))
+import Data.List.Extra hiding (groupSortOn, head, last, mconcatMap)
 import Data.List.Extra qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty.Extra
@@ -228,11 +228,11 @@ tableNestedInsert k1 k2 = tableInsert (HashMap.singleton k2) (HashMap.insert k2)
 -- List
 --------------------------------------------------------------------------------
 
-(!!) :: HasCallStack => [a] -> Int -> a
-(!!) l n
-  | n < 0 = error ("negative index: " <> show n)
-  | length l <= n = error ("out of bounds: length " <> show (length l) <> "; index " <> show n)
-  | otherwise = l List.!! n
+-- (!!) :: HasCallStack => [a] -> Int -> a
+-- (!!) l n
+--   | n < 0 = error ("negative index: " <> show n)
+--   | length l <= n = error ("out of bounds: length " <> show (length l) <> "; index " <> show n)
+--   | otherwise = l List.!! n
 
 revAppend :: [a] -> [a] -> [a]
 revAppend [] !ys = ys

From 5d7ee4efd67ad821e5d096636e4001268c636a6d Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 10 Oct 2022 23:56:38 +0200
Subject: [PATCH 52/73] restore test check

---
 src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs | 8 ++------
 test/Core/Transformation/Lifting.hs                     | 3 +--
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 4a9fd6e05c..2b527c9030 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -65,12 +65,8 @@ lambdaLiftNode aboveBl top =
               letRecBinders = Info.getInfoBinders ndefs (letr ^. letRecInfo)
               bl' :: BinderList Info
               bl' = BL.prepend letRecBinders bl
-          topSymsAssocs :: [(Symbol, Node)] <- forM defs $ \d -> do
-            s' <- freshSymbol
-            return (s', d)
-          let topSyms :: [Symbol]
-              topSyms = map fst topSymsAssocs
-              -- free vars in each let
+          topSyms :: [Symbol] <- forM defs (const freshSymbol)
+          let -- free vars in each let
               recItemsFreeVars :: [[(Index, Info)]]
               recItemsFreeVars = mapMaybe helper . toList . freeVarsSet <$> defs
                 where
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index 4199c8ed17..afd2f7af1a 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -19,8 +19,7 @@ liftTest _testEval@Eval.PosTest {..}
         fromTest
           Test
             { _testTransformations = pipe,
-              -- _testAssertion = \i -> unless (isLifted i) (error "not lambda lifted"),
-              _testAssertion = const (return ()),
+              _testAssertion = \i -> unless (isLifted i) (error "not lambda lifted"),
               _testEval
             }
 

From c530f6ebe55ca33df716149badd5a272a0e3d7ce Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 11 Oct 2022 09:36:11 +0200
Subject: [PATCH 53/73] remove comment

---
 src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 2b527c9030..6a05ab104d 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -122,8 +122,6 @@ lambdaLiftNode aboveBl top =
                       (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys))
           let res :: Node
               res = shiftHelper body' (nonEmpty' letItems)
-          -- TODO: if there is a lambda on top of body', I think it is possible to just move it up instead of recursing.
-          -- However, recursing should be ok
           return (Recur res)
 
 lambdaLifting :: InfoTable -> InfoTable

From 5bccb5b6491cedf366cfa5a2e0b2f4e7304e7988 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 11 Oct 2022 10:18:58 +0200
Subject: [PATCH 54/73] rename sum function to avoid shadowing

---
 tests/Core/positive/test040.jvc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/Core/positive/test040.jvc b/tests/Core/positive/test040.jvc
index 6cc205a8c4..4e107d34bc 100644
--- a/tests/Core/positive/test040.jvc
+++ b/tests/Core/positive/test040.jvc
@@ -1,6 +1,6 @@
 -- letrec
 
-def sum := letrec sum := \x if x = 0 then 0 else x + sum (x - 1) in sum;
+def sum := letrec sum' := \x if x = 0 then 0 else x + sum' (x - 1) in sum';
 
 def fact := \x
   letrec fact' := \x \acc if x = 0 then acc else fact' (x - 1) (acc * x)

From e873ec5ee613cc4a0a28ffb57f2e9d5ad067c677 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 11 Oct 2022 13:12:25 +0200
Subject: [PATCH 55/73] get free variables after lifting

---
 .../Core/Transformation/LambdaLifting.hs       | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 6a05ab104d..f9b6306833 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -66,9 +66,10 @@ lambdaLiftNode aboveBl top =
               bl' :: BinderList Info
               bl' = BL.prepend letRecBinders bl
           topSyms :: [Symbol] <- forM defs (const freshSymbol)
+          liftedDefs <- mapM (lambdaLiftNode bl') defs
           let -- free vars in each let
               recItemsFreeVars :: [[(Index, Info)]]
-              recItemsFreeVars = mapMaybe helper . toList . freeVarsSet <$> defs
+              recItemsFreeVars = mapMaybe helper . toList . freeVarsSet <$> liftedDefs
                 where
                   -- throw away variables bound in the letrec and shift others
                   helper :: Var -> Maybe (Index, Info)
@@ -89,17 +90,14 @@ lambdaLiftNode aboveBl top =
                       ]
                   )
               declareTopSyms :: Sem r ()
-              declareTopSyms = do
-                tbs <- topBodies
-                zipWithExactM_ registerIdentNode topSyms tbs
+              declareTopSyms =
+                zipWithExactM_ registerIdentNode topSyms topBodies
                 where
-                  topBodies :: Sem r [Node]
+                  topBodies :: [Node]
                   topBodies =
-                    sequence
-                      [ captureFreeVars fv . subsCalls
-                          <$> lambdaLiftNode bl' b
-                        | (b, fv) <- zipExact defs recItemsFreeVars
-                      ]
+                    [ captureFreeVars fv (subsCalls b)
+                      | (b, fv) <- zipExact liftedDefs recItemsFreeVars
+                    ]
               letItems :: [Node]
               letItems =
                 [ mkApps' (mkIdent' s) (map (mkVar' . fst) fv)

From a6fb7acd1f653c87b738233978397648f7fe8a38 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 11 Oct 2022 13:13:01 +0200
Subject: [PATCH 56/73] move line

---
 src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index f9b6306833..57ad63d432 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -67,6 +67,7 @@ lambdaLiftNode aboveBl top =
               bl' = BL.prepend letRecBinders bl
           topSyms :: [Symbol] <- forM defs (const freshSymbol)
           liftedDefs <- mapM (lambdaLiftNode bl') defs
+          body' <- lambdaLiftNode bl' (letr ^. letRecBody)
           let -- free vars in each let
               recItemsFreeVars :: [[(Index, Info)]]
               recItemsFreeVars = mapMaybe helper . toList . freeVarsSet <$> liftedDefs
@@ -104,7 +105,6 @@ lambdaLiftNode aboveBl top =
                   | (s, fv) <- zipExact topSyms recItemsFreeVars
                 ]
           declareTopSyms
-          body' <- lambdaLiftNode bl' (letr ^. letRecBody)
           let -- free variables in the lets and the body need to be shifted
               -- because we are introducing binders.
               -- the topmost let is shifted 0

From e880e9b758a0950e0719df80833e1236d6c588e6 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 11 Oct 2022 18:55:38 +0200
Subject: [PATCH 57/73] add type info

---
 .../Core/Transformation/LambdaLifting.hs      | 24 +++++++++++++------
 1 file changed, 17 insertions(+), 7 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 57ad63d432..7540191425 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -92,13 +92,23 @@ lambdaLiftNode aboveBl top =
                   )
               declareTopSyms :: Sem r ()
               declareTopSyms =
-                zipWithExactM_ registerIdentNode topSyms topBodies
-                where
-                  topBodies :: [Node]
-                  topBodies =
-                    [ captureFreeVars fv (subsCalls b)
-                      | (b, fv) <- zipExact liftedDefs recItemsFreeVars
-                    ]
+                sequence_
+                  [ do
+                      let topBody = captureFreeVars fv (subsCalls b)
+                          argsInfo :: [ArgumentInfo]
+                          argsInfo = map (argumentInfoFromInfo . snd) fv
+                      registerIdentNode sym topBody
+                      registerIdent
+                        IdentifierInfo
+                          { _identifierSymbol = sym,
+                            _identifierName = Nothing,
+                            _identifierType = typeFromArgs argsInfo,
+                            _identifierArgsNum = length fv,
+                            _identifierArgsInfo = argsInfo,
+                            _identifierIsExported = False
+                          }
+                    | (sym, b, fv) <- zip3Exact topSyms liftedDefs recItemsFreeVars
+                  ]
               letItems :: [Node]
               letItems =
                 [ mkApps' (mkIdent' s) (map (mkVar' . fst) fv)

From f61d29f635c2c92b3e9c0162376f5366c214294f Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 13 Oct 2022 14:18:44 +0200
Subject: [PATCH 58/73] change letrec test

---
 tests/Core/positive/test040.jvc | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/tests/Core/positive/test040.jvc b/tests/Core/positive/test040.jvc
index 4e107d34bc..cba61a55da 100644
--- a/tests/Core/positive/test040.jvc
+++ b/tests/Core/positive/test040.jvc
@@ -13,24 +13,26 @@ def fib :=
 def writeLn := \x write x >> write "\n";
 
 def mutrec :=
+  let two := 2 in
+  let one := 1 in
   letrec[f g h]
     f := \x {
-      if x < 1 then
-        1
+      if x < one then
+        one
       else
-        g (x - 1) + 2 * x
+        g (x - one) + two * x
     };
     g := \x {
-      if x < 1 then
-        1
+      if x < one then
+        one
       else
-        x + h (x - 1)
+        x + h (x - one)
     };
     h := \x letrec z := {
-      if x < 1 then
-        1
+      if x < one then
+        one
       else
-        x * f (x - 1)
+        x * f (x - one)
     } in z
   in writeLn (f 5) >> writeLn (f 10) >> writeLn (f 100) >> writeLn (g 5) >> writeLn (h 5);
 

From 88f0d974ac99bb85bbf819b841d7c3417adae132 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 13 Oct 2022 15:19:56 +0200
Subject: [PATCH 59/73] the notorious reverse

---
 src/Juvix/Compiler/Core/Extra.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index d5e182f5e2..26ca8033dc 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -137,7 +137,7 @@ developBeta = umap go
 
 etaExpand :: Int -> Node -> Node
 etaExpand 0 n = n
-etaExpand k n = mkLambdas' k (mkApps' (shift k n) (map mkVar' [0 .. k - 1]))
+etaExpand k n = mkLambdas' k (mkApps' (shift k n) (map mkVar' (reverse [0 .. k - 1])))
 
 -- | substitution of all free variables for values in an environment
 substEnv :: Env -> Node -> Node

From f32b4ff6480e4ce1930ac353774d9e91176a62c9 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 13 Oct 2022 15:22:22 +0200
Subject: [PATCH 60/73] typo

---
 test/Core/Eval/Base.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs
index e7e61fdc75..39b1e17529 100644
--- a/test/Core/Eval/Base.hs
+++ b/test/Core/Eval/Base.hs
@@ -28,7 +28,7 @@ coreEvalAssertion mainFile expectedFile trans testTrans step = do
   case r of
     Left err -> assertFailure (show (pretty err))
     Right (_, Nothing) -> do
-      step "Compare expected an actual program output"
+      step "Compare expected and actual program output"
       expected <- TIO.readFile expectedFile
       assertEqDiff ("Check: EVAL output = " <> expectedFile) "" expected
     Right (tabIni, Just node) -> do

From d2bb2b9016ac25eae1577c891085015eed2ae9f2 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 13 Oct 2022 15:23:37 +0200
Subject: [PATCH 61/73] shadowing in test

---
 tests/Core/positive/test040.jvc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/Core/positive/test040.jvc b/tests/Core/positive/test040.jvc
index cba61a55da..e778949eca 100644
--- a/tests/Core/positive/test040.jvc
+++ b/tests/Core/positive/test040.jvc
@@ -1,6 +1,6 @@
 -- letrec
 
-def sum := letrec sum' := \x if x = 0 then 0 else x + sum' (x - 1) in sum';
+def sum := letrec sum := \x if x = 0 then 0 else x + sum (x - 1) in sum;
 
 def fact := \x
   letrec fact' := \x \acc if x = 0 then acc else fact' (x - 1) (acc * x)

From 8644c36d00cf2ccd61c2752bf16e244b74115dfc Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 13 Oct 2022 15:31:02 +0200
Subject: [PATCH 62/73] cleanup

---
 src/Juvix/Prelude/Base.hs           |  6 ------
 test/Core/Transformation/Lifting.hs | 23 ++++++++---------------
 2 files changed, 8 insertions(+), 21 deletions(-)

diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index cfe760c823..f523b246a6 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -228,12 +228,6 @@ tableNestedInsert k1 k2 = tableInsert (HashMap.singleton k2) (HashMap.insert k2)
 -- List
 --------------------------------------------------------------------------------
 
--- (!!) :: HasCallStack => [a] -> Int -> a
--- (!!) l n
---   | n < 0 = error ("negative index: " <> show n)
---   | length l <= n = error ("out of bounds: length " <> show (length l) <> "; index " <> show n)
---   | otherwise = l List.!! n
-
 revAppend :: [a] -> [a] -> [a]
 revAppend [] !ys = ys
 revAppend (x : xs) !ys = revAppend xs (x : ys)
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index afd2f7af1a..81a7f7387b 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -11,18 +11,11 @@ allTests = testGroup "Lambda lifting" (mapMaybe liftTest Eval.tests)
 pipe :: [TransformationId]
 pipe = [LambdaLifting]
 
-liftTest :: Eval.PosTest -> Maybe TestTree
-liftTest _testEval@Eval.PosTest {..}
-  | _name `elem` excluded = Nothing
-  | otherwise =
-      Just $
-        fromTest
-          Test
-            { _testTransformations = pipe,
-              _testAssertion = \i -> unless (isLifted i) (error "not lambda lifted"),
-              _testEval
-            }
-
-excluded :: [String]
-excluded =
-  []
+liftTest :: Eval.PosTest -> TestTree
+liftTest _testEval@Eval.PosTest {..} =
+  fromTest
+    Test
+      { _testTransformations = pipe,
+        _testAssertion = \i -> unless (isLifted i) (error "not lambda lifted"),
+        _testEval
+      }

From 1b0448bc56fb3e2771017fcedfe1136fdd84cb2b Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 17 Oct 2022 22:10:57 +0200
Subject: [PATCH 63/73] fix mapMaybe -> map

---
 test/Core/Transformation/Lifting.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index 81a7f7387b..c0f61a712c 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -6,7 +6,7 @@ import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
-allTests = testGroup "Lambda lifting" (mapMaybe liftTest Eval.tests)
+allTests = testGroup "Lambda lifting" (map liftTest Eval.tests)
 
 pipe :: [TransformationId]
 pipe = [LambdaLifting]

From 0db9153d3ab4694ed9266ce371276c607147b333 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 18 Oct 2022 00:35:34 +0200
Subject: [PATCH 64/73] add simple scope checker for Core

---
 app/Commands/Dev/Core/Read.hs                 |  2 ++
 src/Juvix/Compiler/Core/Evaluator.hs          |  6 ++--
 src/Juvix/Compiler/Core/Scoper.hs             | 31 +++++++++++++++++++
 .../Compiler/Core/Transformation/Base.hs      |  3 ++
 src/Juvix/Prelude/Base.hs                     |  3 ++
 5 files changed, 43 insertions(+), 2 deletions(-)
 create mode 100644 src/Juvix/Compiler/Core/Scoper.hs

diff --git a/app/Commands/Dev/Core/Read.hs b/app/Commands/Dev/Core/Read.hs
index 28567d2896..ec233b5cb8 100644
--- a/app/Commands/Dev/Core/Read.hs
+++ b/app/Commands/Dev/Core/Read.hs
@@ -4,6 +4,7 @@ import Commands.Base
 import Commands.Dev.Core.Eval qualified as Eval
 import Commands.Dev.Core.Read.Options
 import Juvix.Compiler.Core.Pretty qualified as Core
+import Juvix.Compiler.Core.Scoper qualified as Scoper
 import Juvix.Compiler.Core.Transformation qualified as Core
 import Juvix.Compiler.Core.Translation.FromSource qualified as Core
 
@@ -12,6 +13,7 @@ runCommand opts = do
   s' <- embed (readFile f)
   (tab, mnode) <- getRight (mapLeft JuvixError (Core.runParser "" f Core.emptyInfoTable s'))
   let tab' = Core.applyTransformations (opts ^. coreReadTransformations) tab
+  embed (Scoper.scopeTrace tab')
   unless (opts ^. coreReadNoPrint) (renderStdOut (Core.ppOut opts tab'))
   whenJust mnode $ doEval tab'
   where
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 0e2e9e1fca..3ab7294ed6 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -10,7 +10,7 @@ import Control.Exception qualified as Exception
 import Data.HashMap.Strict qualified as HashMap
 import Debug.Trace qualified as Debug
 import GHC.Conc qualified as GHC
-import GHC.Show as S
+import GHC.Show qualified as S
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Error (CoreError (..))
 import Juvix.Compiler.Core.Extra
@@ -55,7 +55,9 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
 
     eval' :: Env -> Node -> Node
     eval' !env !n = case n of
-      NVar (Var _ idx) -> env !! idx
+      NVar (Var _ idx)
+        | idx < length env -> env !! idx
+        | otherwise -> error ("invalid index: " <> show idx <> " (length: " <> show (length env) <> ")")
       NIdt (Ident _ sym) -> eval' [] (lookupContext n sym)
       NCst {} -> n
       NApp (App i l r) ->
diff --git a/src/Juvix/Compiler/Core/Scoper.hs b/src/Juvix/Compiler/Core/Scoper.hs
new file mode 100644
index 0000000000..ae2e2b856f
--- /dev/null
+++ b/src/Juvix/Compiler/Core/Scoper.hs
@@ -0,0 +1,31 @@
+module Juvix.Compiler.Core.Scoper where
+
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Transformation.Base
+
+type ScopeError = Text
+
+scopeCheck :: InfoTable -> Maybe ScopeError
+scopeCheck = either Just (const Nothing) . run . runError . walkT goTopNode
+
+goTopNode :: Members '[Error ScopeError] r => Symbol -> Node -> Sem r ()
+goTopNode sym = runReader sym . walkN check
+
+check :: Members '[Reader Symbol, Error ScopeError] r => Index -> Node -> Sem r ()
+check k = \case
+  NVar v
+    | v ^. varIndex < k -> return ()
+    | otherwise -> scopeErr ("variable " <> ppTrace (NVar v) <> " is out of scope")
+  _ -> return ()
+
+scopeErr :: Members '[Reader Symbol, Error ScopeError] r => Text -> Sem r a
+scopeErr msg = do
+  sym <- ask @Symbol
+  throw @ScopeError ("Scope error in the definition of " <> show sym <> "\n" <> msg)
+
+-- | prints the scope error without exiting
+scopeTrace :: InfoTable -> IO ()
+scopeTrace i = whenJust (scopeCheck i) putStrLn
diff --git a/src/Juvix/Compiler/Core/Transformation/Base.hs b/src/Juvix/Compiler/Core/Transformation/Base.hs
index 94e5753d23..0312370425 100644
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@@ -22,3 +22,6 @@ mapT' f tab =
       mapM_
         (\(k, v) -> f v >>= registerIdentNode k)
         (HashMap.toList (tab ^. identContext))
+
+walkT :: Applicative f => (Symbol -> Node -> f ()) -> InfoTable -> f ()
+walkT f tab = for_ (HashMap.toList (tab ^. identContext)) (uncurry f)
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index f523b246a6..26434aec88 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -337,6 +337,9 @@ fromRightIO' pp = do
 fromRightIO :: (e -> Text) -> IO (Either e r) -> IO r
 fromRightIO pp = fromRightIO' (putStrLn . pp)
 
+leftToMaybe :: Either l r -> Maybe l
+leftToMaybe = either Just (const Nothing)
+
 --------------------------------------------------------------------------------
 -- Misc
 --------------------------------------------------------------------------------

From 871f7debd011d1978f2e077854634d1c8975006d Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 18 Oct 2022 11:55:52 +0200
Subject: [PATCH 65/73] fix letrec printing

---
 src/Juvix/Compiler/Core/Pretty/Base.hs | 70 ++++++++++++++------------
 1 file changed, 39 insertions(+), 31 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 8c83036056..9eb0977c96 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -138,7 +138,7 @@ ppCodeLet' name mty lt = do
           mempty <+> kwColon <+> ty
         Nothing ->
           mempty
-  return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <+> b'
+  return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <> line <> b'
 
 ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Maybe Name]] -> [Maybe Name] -> Case' i bi a -> Sem r (Doc Ann)
 ppCodeCase' branchBinderNames branchTagNames Case {..} = do
@@ -188,6 +188,41 @@ ppPatterns pats = do
   ps' <- mapM ppCode pats
   return $ hsep (punctuate comma (toList ps'))
 
+instance PrettyCode Let where
+  ppCode :: forall r. Member (Reader Options) r => Let -> Sem r (Doc Ann)
+  ppCode x = do
+    let name = getInfoName (getInfoBinder (x ^. letInfo))
+        ty = getInfoType (getInfoBinder (x ^. letInfo))
+     in do
+          mty <- case ty of
+            NDyn {} -> return Nothing
+            _ -> Just <$> ppCode ty
+          ppCodeLet' name mty x
+
+instance PrettyCode LetRec where
+  ppCode :: forall r. Member (Reader Options) r => LetRec -> Sem r (Doc Ann)
+  ppCode LetRec {..} = do
+    let n = length _letRecValues
+    ns <- mapM getName (getInfoBinders n _letRecInfo)
+    vs <- mapM ppCode _letRecValues
+    b' <- ppCode _letRecBody
+    return $ case ns of
+      [hns] -> kwLetRec <+> hns <+> kwAssign <+> head vs <+> kwIn <+> b'
+      _ ->
+        let bss =
+              indent' $
+                align $
+                  concatWith (\a b -> a <> kwSemicolon <> line <> b) $
+                    zipWithExact (\name val -> name <+> kwAssign <+> val) ns (toList vs)
+            nss = enclose kwSquareL kwSquareR (concatWith (<+>) ns)
+         in kwLetRec <> nss <> line <> bss <> line <> kwIn <> line <> b'
+    where
+      getName :: Info -> Sem r (Doc Ann)
+      getName i =
+        case getInfoName i of
+          Just name -> ppCode name
+          Nothing -> return kwQuestion
+
 instance PrettyCode Node where
   ppCode :: forall r. Member (Reader Options) r => Node -> Sem r (Doc Ann)
   ppCode node = case node of
@@ -216,35 +251,8 @@ instance PrettyCode Node where
               return $ kwLambda <> parens (n <+> kwColon <+> tty)
         Nothing -> return $ kwLambda <> kwQuestion
       return (lam <+> b)
-    NLet x ->
-      let name = getInfoName (getInfoBinder (x ^. letInfo))
-          ty = getInfoType (getInfoBinder (x ^. letInfo))
-       in do
-            mty <- case ty of
-              NDyn {} -> return Nothing
-              _ -> Just <$> ppCode ty
-            ppCodeLet' name mty x
-    NRec LetRec {..} -> do
-      let n = length _letRecValues
-      ns <- mapM getName (getInfoBinders n _letRecInfo)
-      vs <- mapM ppCode _letRecValues
-      b' <- ppCode _letRecBody
-      case listToMaybe ns of
-        Just hns -> return $ kwLetRec <+> hns <+> kwAssign <+> head vs <+> kwIn <+> b'
-        Nothing ->
-          let bss =
-                indent' $
-                  align $
-                    concatWith (\a b -> a <> kwSemicolon <> line <> b) $
-                      zipWithExact (\name val -> name <+> kwAssign <+> val) ns (toList vs)
-              nss = enclose kwSquareL kwSquareR (concatWith (<+>) ns)
-           in return $ kwLetRec <> nss <> line <> bss <> line <> kwIn <> line <> b'
-      where
-        getName :: Info -> Sem r (Doc Ann)
-        getName i =
-          case getInfoName i of
-            Just name -> ppCode name
-            Nothing -> return kwQuestion
+    NLet x -> ppCode x
+    NRec l -> ppCode l
     NCase x@Case {..} ->
       let branchBinderNames = map (\(CaseBranch {..}) -> map getInfoName (getInfoBinders _caseBranchBindersNum _caseBranchInfo)) _caseBranches
           branchTagNames = map (\(CaseBranch {..}) -> getInfoName _caseBranchInfo) _caseBranches
@@ -341,7 +349,7 @@ instance PrettyCode InfoTable where
           ppDef s n = do
             sym' <- maybe (return (pretty s)) ppCode (tbl ^? infoIdentifiers . at s . _Just . identifierName . _Just)
             body' <- ppCode n
-            return (kwDef <+> sym' <+> kwAssign <+> body')
+            return (kwDef <+> sym' <+> kwAssign <+> nest 2 body')
 
 instance PrettyCode Stripped.InfoTable where
   ppCode :: forall r. Member (Reader Options) r => Stripped.InfoTable -> Sem r (Doc Ann)

From 1433f5ed6c21ae990cfdef0b33a5bd0cd7075c85 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 18 Oct 2022 20:30:20 +0200
Subject: [PATCH 66/73] fix shifting

---
 src/Juvix/Compiler/Core/Pretty/Base.hs        |  5 ++-
 .../Core/Transformation/LambdaLifting.hs      | 44 ++++++++++---------
 tests/Core/positive/test040-bis.jvc           | 15 +++++++
 tests/Core/positive/test040-bis2.jvc          | 18 ++++++++
 4 files changed, 61 insertions(+), 21 deletions(-)
 create mode 100644 tests/Core/positive/test040-bis.jvc
 create mode 100644 tests/Core/positive/test040-bis2.jvc

diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 9eb0977c96..fdf9ac509a 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -347,7 +347,10 @@ instance PrettyCode InfoTable where
         where
           ppDef :: Symbol -> Node -> Sem r (Doc Ann)
           ppDef s n = do
-            sym' <- maybe (return (pretty s)) ppCode (tbl ^? infoIdentifiers . at s . _Just . identifierName . _Just)
+            let mname :: Maybe Name
+                mname = tbl ^? infoIdentifiers . at s . _Just . identifierName . _Just
+                mname' = over (_Just . namePretty) (\nm -> nm <> "!" <> prettyText s) mname
+            sym' <- maybe (return (pretty s)) ppCode mname'
             body' <- ppCode n
             return (kwDef <+> sym' <+> kwAssign <+> nest 2 body')
 
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 7540191425..7a4f47fc0b 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -9,6 +9,7 @@ import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info.BinderInfo qualified as Info
+import Juvix.Compiler.Core.Info.NameInfo
 import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation.Base
 
@@ -69,64 +70,67 @@ lambdaLiftNode aboveBl top =
           liftedDefs <- mapM (lambdaLiftNode bl') defs
           body' <- lambdaLiftNode bl' (letr ^. letRecBody)
           let -- free vars in each let
-              recItemsFreeVars :: [[(Index, Info)]]
-              recItemsFreeVars = mapMaybe helper . toList . freeVarsSet <$> liftedDefs
+              recItemsFreeVars :: [(Var, Info)]
+              recItemsFreeVars = mapMaybe helper (toList (mconcatMap freeVarsSet liftedDefs))
                 where
                   -- throw away variables bound in the letrec and shift others
-                  helper :: Var -> Maybe (Index, Info)
+                  helper :: Var -> Maybe (Var, Info)
                   helper v
                     | idx < ndefs = Nothing
                     | otherwise =
                         let idx' = idx - ndefs
-                         in Just (idx', BL.lookup idx' bl)
+                         in Just (v, BL.lookup idx' bl)
                     where
                       idx = v ^. varIndex
-              -- replace calls to letrec items to a calls to the fresh top symbols
+              -- replace calls to letrec items to a calls to the fresh top
+              -- symbols TODO note that these calls can appear in the
+              -- dynamically created top level nodes created during lambda
+              -- lifting
               subsCalls :: Node -> Node
               subsCalls =
                 substs
                   ( reverse
-                      [ mkApps' (mkIdent' sym) (map (mkVar' . fst) fv)
-                        | (sym, fv) <- zipExact topSyms recItemsFreeVars
+                      [ mkApps' (mkIdent' sym) (map (NVar . fst) fv)
+                        | let fv = recItemsFreeVars, sym <- topSyms
                       ]
                   )
               declareTopSyms :: Sem r ()
               declareTopSyms =
                 sequence_
                   [ do
-                      let topBody = captureFreeVars fv (subsCalls b)
+                      let
+                          fv = recItemsFreeVars
+                          topBody = captureFreeVars (map (first (^. varIndex)) fv) (subsCalls b)
                           argsInfo :: [ArgumentInfo]
                           argsInfo = map (argumentInfoFromInfo . snd) fv
                       registerIdentNode sym topBody
                       registerIdent
                         IdentifierInfo
                           { _identifierSymbol = sym,
-                            _identifierName = Nothing,
+                            _identifierName = getInfoName itemInfo,
                             _identifierType = typeFromArgs argsInfo,
                             _identifierArgsNum = length fv,
                             _identifierArgsInfo = argsInfo,
                             _identifierIsExported = False
                           }
-                    | (sym, b, fv) <- zip3Exact topSyms liftedDefs recItemsFreeVars
+                    | (sym, (itemInfo, b)) <- zipExact topSyms (zipExact letRecBinders liftedDefs)
                   ]
               letItems :: [Node]
-              letItems =
-                [ mkApps' (mkIdent' s) (map (mkVar' . fst) fv)
-                  | (s, fv) <- zipExact topSyms recItemsFreeVars
+              letItems = let fv = recItemsFreeVars in
+                [ mkApps' (mkIdent' s) (map (NVar . fst) fv)
+                  | s <- topSyms
                 ]
           declareTopSyms
-          let -- free variables in the lets and the body need to be shifted
-              -- because we are introducing binders.
-              -- the topmost let is shifted 0
-              -- the lowermost is shifted (len - 1)
-              -- the final body is not shifted
+          let -- TODO it can probably be simplified
               shiftHelper :: Node -> NonEmpty Node -> Node
-              shiftHelper b = goShift 0
+              shiftHelper b = goShift (- ndefs)
                 where
                   goShift :: Int -> NonEmpty Node -> Node
                   goShift k = \case
                     x :| yys -> case yys of
-                      [] -> mkLet' (shift k x) b
+                      []
+                        | k == - 1 -> mkLet' (shift k x) b
+                        | otherwise -> impossible
                       (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys))
           let res :: Node
               res = shiftHelper body' (nonEmpty' letItems)
diff --git a/tests/Core/positive/test040-bis.jvc b/tests/Core/positive/test040-bis.jvc
new file mode 100644
index 0000000000..ea1b8d455b
--- /dev/null
+++ b/tests/Core/positive/test040-bis.jvc
@@ -0,0 +1,15 @@
+-- letrec 2
+
+def writeLn := \x write x >> write "\n";
+
+def mutrec :=
+  let one := 1 in
+  let two := 2 in
+  let three := 3 in
+  letrec[a b c]
+    a := \x b one;
+    b := \x c two;
+    c := \x three
+  in writeLn (a 5);
+
+letrec x := 3 in mutrec
diff --git a/tests/Core/positive/test040-bis2.jvc b/tests/Core/positive/test040-bis2.jvc
new file mode 100644
index 0000000000..c413926912
--- /dev/null
+++ b/tests/Core/positive/test040-bis2.jvc
@@ -0,0 +1,18 @@
+-- letrec
+
+def writeLn := \x write x >> write "\n";
+
+def mutrec :=
+  let one := 1 in
+  let two := 2 in
+  letrec[f h]
+    f := h one;
+    h := \x letrec z := {
+       f two
+    } in z
+  in writeLn (f 5);
+  -- >> writeLn (f 10) >> writeLn (f 100) >> writeLn (g 5) >> writeLn (h 5);
+
+letrec x := 3
+in
+mutrec

From e614a6356fea785d2cc1b281815b466a3c9add84 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 19 Oct 2022 13:49:46 +0200
Subject: [PATCH 67/73] fix recursive call

---
 src/Juvix/Compiler/Core/Pretty.hs             |  2 +-
 .../Core/Transformation/LambdaLifting.hs      | 78 +++++++++++++------
 tests/Core/positive/test040-bis.jvc           |  5 ++
 tests/Core/positive/test040-bis2.jvc          | 22 +++---
 4 files changed, 71 insertions(+), 36 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Pretty.hs b/src/Juvix/Compiler/Core/Pretty.hs
index 6dbadfec3d..c635002cbc 100644
--- a/src/Juvix/Compiler/Core/Pretty.hs
+++ b/src/Juvix/Compiler/Core/Pretty.hs
@@ -22,7 +22,7 @@ ppTrace' :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> Text
 ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts)
 
 ppTrace :: PrettyCode c => c -> Text
-ppTrace = ppTrace' defaultOptions
+ppTrace = ppTrace' traceOptions
 
 ppPrint :: PrettyCode c => c -> Text
 ppPrint = show . ppOutDefault
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 7a4f47fc0b..800eb01506 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -58,6 +58,7 @@ lambdaLiftNode aboveBl top =
 
         goLetRec :: LetRec -> Sem r Recur
         goLetRec letr = do
+          -- getInfoTable >>= traceM . ppTrace
           let defs :: [Node]
               defs = toList (letr ^. letRecValues)
               ndefs :: Int
@@ -67,40 +68,64 @@ lambdaLiftNode aboveBl top =
               bl' :: BinderList Info
               bl' = BL.prepend letRecBinders bl
           topSyms :: [Symbol] <- forM defs (const freshSymbol)
-          liftedDefs <- mapM (lambdaLiftNode bl') defs
-          body' <- lambdaLiftNode bl' (letr ^. letRecBody)
-          let -- free vars in each let
-              recItemsFreeVars :: [(Var, Info)]
-              recItemsFreeVars = mapMaybe helper (toList (mconcatMap freeVarsSet liftedDefs))
+          let recItemsFreeVars :: [(Var, Info)]
+              recItemsFreeVars = mapMaybe helper (toList (mconcatMap freeVarsSet defs))
                 where
+                  -- free vars in each let
                   -- throw away variables bound in the letrec and shift others
                   helper :: Var -> Maybe (Var, Info)
                   helper v
-                    | idx < ndefs = Nothing
-                    | otherwise =
-                        let idx' = idx - ndefs
-                         in Just (v, BL.lookup idx' bl)
+                    | v ^. varIndex < ndefs = Nothing
+                    | otherwise = Just (set varIndex idx' v, BL.lookup idx' bl)
                     where
-                      idx = v ^. varIndex
-              -- replace calls to letrec items to a calls to the fresh top
-              -- symbols TODO note that these calls can appear in the
-              -- dynamically created top level nodes created during lambda
-              -- lifting
+                      idx' = (v ^. varIndex) - ndefs
+
+              -- FIXME
               subsCalls :: Node -> Node
               subsCalls =
                 substs
                   ( reverse
-                      [ mkApps' (mkIdent' sym) (map (NVar . fst) fv)
-                        | let fv = recItemsFreeVars, sym <- topSyms
+                      [ mkApps' (mkIdent' sym) (map (NVar . fst) recItemsFreeVars)
+                        | sym <- topSyms
                       ]
                   )
+          let fv = recItemsFreeVars
+          -- traceM ("freevars " <> show (length fv) <> " " <> show (map (pretty . getInfoName . snd) fv))
+          liftedDefs <- mapM (lambdaLiftNode bl . subsCalls) defs
+          body' <- lambdaLiftNode bl' (letr ^. letRecBody)
+          let -- free vars in each let
+              -- recItemsFreeVars' :: [(Var, Info)]
+              -- recItemsFreeVars' = mapMaybe helper (toList (mconcatMap freeVarsSet liftedDefs))
+              --   where
+              --     -- throw away variables bound in the letrec and shift others
+
+              --     helper :: Var -> Maybe (Var, Info)
+              --     helper v
+              --       | idx < ndefs = Nothing
+              --       | otherwise =
+              --           let idx' = idx - ndefs
+              --            in Just (v, BL.lookup idx' bl)
+              --       where
+              --         idx = v ^. varIndex
+              -- -- replace calls to letrec items to a calls to the fresh top
+              -- -- symbols.
+              -- -- FIXME note that these calls can appear in the
+              -- -- dynamically created top level nodes in recursive calls to
+              -- -- lambda lifting
+              -- subsCalls' :: Node -> Node
+              -- subsCalls' =
+              --   substs
+              --     ( reverse
+              --         [ mkApps' (mkIdent' sym) (map (NVar . fst) recItemsFreeVars)
+              --           | sym <- topSyms
+              --         ]
+              --     )
               declareTopSyms :: Sem r ()
               declareTopSyms =
                 sequence_
                   [ do
-                      let
-                          fv = recItemsFreeVars
-                          topBody = captureFreeVars (map (first (^. varIndex)) fv) (subsCalls b)
+                      let fv = recItemsFreeVars
+                          topBody = captureFreeVars (map (first (^. varIndex)) fv) b
                           argsInfo :: [ArgumentInfo]
                           argsInfo = map (argumentInfoFromInfo . snd) fv
                       registerIdentNode sym topBody
@@ -116,20 +141,23 @@ lambdaLiftNode aboveBl top =
                     | (sym, (itemInfo, b)) <- zipExact topSyms (zipExact letRecBinders liftedDefs)
                   ]
               letItems :: [Node]
-              letItems = let fv = recItemsFreeVars in
-                [ mkApps' (mkIdent' s) (map (NVar . fst) fv)
-                  | s <- topSyms
-                ]
+              letItems =
+                let fv = recItemsFreeVars
+                 in [ mkApps' (mkIdent' s) (map (NVar . fst) fv)
+                      | s <- topSyms
+                    ]
           declareTopSyms
+
+          -- getInfoTable >>= traceM . ppTrace
           let -- TODO it can probably be simplified
               shiftHelper :: Node -> NonEmpty Node -> Node
-              shiftHelper b = goShift (- ndefs)
+              shiftHelper b = goShift 0
                 where
                   goShift :: Int -> NonEmpty Node -> Node
                   goShift k = \case
                     x :| yys -> case yys of
                       []
-                        | k == - 1 -> mkLet' (shift k x) b
+                        | k == ndefs - 1 -> mkLet' (shift k x) b
                         | otherwise -> impossible
                       (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys))
           let res :: Node
diff --git a/tests/Core/positive/test040-bis.jvc b/tests/Core/positive/test040-bis.jvc
index ea1b8d455b..d134fe5135 100644
--- a/tests/Core/positive/test040-bis.jvc
+++ b/tests/Core/positive/test040-bis.jvc
@@ -12,4 +12,9 @@ def mutrec :=
     c := \x three
   in writeLn (a 5);
 
+-- bl = [three, two, one]
+-- unfiltered free vars of defs = {one$5, two$4, three$3, b$2, c$1}
+-- filtered free vars of defs = {one$2, two$1, three$0}
+
+
 letrec x := 3 in mutrec
diff --git a/tests/Core/positive/test040-bis2.jvc b/tests/Core/positive/test040-bis2.jvc
index c413926912..81a5a9abe6 100644
--- a/tests/Core/positive/test040-bis2.jvc
+++ b/tests/Core/positive/test040-bis2.jvc
@@ -2,17 +2,19 @@
 
 def writeLn := \x write x >> write "\n";
 
+-- def mutrec2 :=
+--   let two := 2 in
+--    letrec z2 := {
+--        two
+--     } in z2 + two;
+
 def mutrec :=
-  let one := 1 in
   let two := 2 in
   letrec[f h]
-    f := h one;
-    h := \x letrec z := {
-       f two
-    } in z
-  in writeLn (f 5);
-  -- >> writeLn (f 10) >> writeLn (f 100) >> writeLn (g 5) >> writeLn (h 5);
+    f := h;
+    h := letrec z := {
+       f + two
+    } in z + two
+  in writeLn f;
 
-letrec x := 3
-in
-mutrec
+letrec x := 3 in mutrec

From beb489d28b0bf515e017e820a9eb538139b2e059 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 20 Oct 2022 10:48:58 +0200
Subject: [PATCH 68/73] polish

---
 .../Core/Transformation/LambdaLifting.hs      | 45 ++++---------------
 test/Core/Transformation/Lifting.hs           |  2 +-
 2 files changed, 9 insertions(+), 38 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 800eb01506..6ef8700289 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -58,7 +58,6 @@ lambdaLiftNode aboveBl top =
 
         goLetRec :: LetRec -> Sem r Recur
         goLetRec letr = do
-          -- getInfoTable >>= traceM . ppTrace
           let defs :: [Node]
               defs = toList (letr ^. letRecValues)
               ndefs :: Int
@@ -80,7 +79,6 @@ lambdaLiftNode aboveBl top =
                     where
                       idx' = (v ^. varIndex) - ndefs
 
-              -- FIXME
               subsCalls :: Node -> Node
               subsCalls =
                 substs
@@ -89,52 +87,26 @@ lambdaLiftNode aboveBl top =
                         | sym <- topSyms
                       ]
                   )
-          let fv = recItemsFreeVars
-          -- traceM ("freevars " <> show (length fv) <> " " <> show (map (pretty . getInfoName . snd) fv))
+          -- NOTE that we are first substituting the calls and then performing
+          -- lambda lifting. This is a tradeoff. We have slower compilation but
+          -- slightly faster execution time, since it minimizes the number of
+          -- free variables that need to be passed around.
           liftedDefs <- mapM (lambdaLiftNode bl . subsCalls) defs
           body' <- lambdaLiftNode bl' (letr ^. letRecBody)
-          let -- free vars in each let
-              -- recItemsFreeVars' :: [(Var, Info)]
-              -- recItemsFreeVars' = mapMaybe helper (toList (mconcatMap freeVarsSet liftedDefs))
-              --   where
-              --     -- throw away variables bound in the letrec and shift others
-
-              --     helper :: Var -> Maybe (Var, Info)
-              --     helper v
-              --       | idx < ndefs = Nothing
-              --       | otherwise =
-              --           let idx' = idx - ndefs
-              --            in Just (v, BL.lookup idx' bl)
-              --       where
-              --         idx = v ^. varIndex
-              -- -- replace calls to letrec items to a calls to the fresh top
-              -- -- symbols.
-              -- -- FIXME note that these calls can appear in the
-              -- -- dynamically created top level nodes in recursive calls to
-              -- -- lambda lifting
-              -- subsCalls' :: Node -> Node
-              -- subsCalls' =
-              --   substs
-              --     ( reverse
-              --         [ mkApps' (mkIdent' sym) (map (NVar . fst) recItemsFreeVars)
-              --           | sym <- topSyms
-              --         ]
-              --     )
-              declareTopSyms :: Sem r ()
+          let declareTopSyms :: Sem r ()
               declareTopSyms =
                 sequence_
                   [ do
-                      let fv = recItemsFreeVars
-                          topBody = captureFreeVars (map (first (^. varIndex)) fv) b
+                      let topBody = captureFreeVars (map (first (^. varIndex)) recItemsFreeVars) b
                           argsInfo :: [ArgumentInfo]
-                          argsInfo = map (argumentInfoFromInfo . snd) fv
+                          argsInfo = map (argumentInfoFromInfo . snd) recItemsFreeVars
                       registerIdentNode sym topBody
                       registerIdent
                         IdentifierInfo
                           { _identifierSymbol = sym,
                             _identifierName = getInfoName itemInfo,
                             _identifierType = typeFromArgs argsInfo,
-                            _identifierArgsNum = length fv,
+                            _identifierArgsNum = length recItemsFreeVars,
                             _identifierArgsInfo = argsInfo,
                             _identifierIsExported = False
                           }
@@ -148,7 +120,6 @@ lambdaLiftNode aboveBl top =
                     ]
           declareTopSyms
 
-          -- getInfoTable >>= traceM . ppTrace
           let -- TODO it can probably be simplified
               shiftHelper :: Node -> NonEmpty Node -> Node
               shiftHelper b = goShift 0
diff --git a/test/Core/Transformation/Lifting.hs b/test/Core/Transformation/Lifting.hs
index c0f61a712c..87f187c68c 100644
--- a/test/Core/Transformation/Lifting.hs
+++ b/test/Core/Transformation/Lifting.hs
@@ -12,7 +12,7 @@ pipe :: [TransformationId]
 pipe = [LambdaLifting]
 
 liftTest :: Eval.PosTest -> TestTree
-liftTest _testEval@Eval.PosTest {..} =
+liftTest _testEval =
   fromTest
     Test
       { _testTransformations = pipe,

From 7f009cf8b636476fd9fe3868bbe8b492a6330d33 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 20 Oct 2022 10:54:01 +0200
Subject: [PATCH 69/73] remove dead code

---
 src/Juvix/Compiler/Core/Extra.hs     |  9 ---------
 src/Juvix/Prelude/Base.hs            |  9 ---------
 tests/Core/positive/test040-bis.jvc  | 20 --------------------
 tests/Core/positive/test040-bis2.jvc | 20 --------------------
 tests/Core/positive/test040.jvc      | 20 +++++++++-----------
 5 files changed, 9 insertions(+), 69 deletions(-)
 delete mode 100644 tests/Core/positive/test040-bis.jvc
 delete mode 100644 tests/Core/positive/test040-bis2.jvc

diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index fb646e2f6b..7dfa79707f 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -11,8 +11,6 @@ where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
-import Juvix.Compiler.Core.Data.BinderList (BinderList)
-import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Extra.Base
 import Juvix.Compiler.Core.Extra.Equality
@@ -30,13 +28,6 @@ isClosed = not . has freeVars
 freeVarsSet :: Node -> HashSet Var
 freeVarsSet n = HashSet.fromList (n ^.. freeVars)
 
-freeVarsWithInfo :: BinderList Info -> Node -> [(Index, Info)]
-freeVarsWithInfo bl n =
-  [ (i, BL.lookup i bl)
-    | v <- toList (freeVarsSet n),
-      let i = v ^. varIndex
-  ]
-
 freeVars :: SimpleFold Node Var
 freeVars f = ufoldNA reassemble go
   where
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index 6f5d90b14b..ff67d01596 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -252,12 +252,6 @@ commonPrefix a b = reverse (go [] a b)
         | x' == y' -> go (x' : ac) xs ys
       _ -> ac
 
-zipWithExactM :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m [c]
-zipWithExactM f a b = mapM (uncurry f) (zipExact a b)
-
-zipWithExactM_ :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m ()
-zipWithExactM_ f a b = void (zipWithExactM f a b)
-
 --------------------------------------------------------------------------------
 -- NonEmpty
 --------------------------------------------------------------------------------
@@ -339,9 +333,6 @@ fromRightIO' pp = do
 fromRightIO :: (e -> Text) -> IO (Either e r) -> IO r
 fromRightIO pp = fromRightIO' (putStrLn . pp)
 
-leftToMaybe :: Either l r -> Maybe l
-leftToMaybe = either Just (const Nothing)
-
 --------------------------------------------------------------------------------
 -- Files
 --------------------------------------------------------------------------------
diff --git a/tests/Core/positive/test040-bis.jvc b/tests/Core/positive/test040-bis.jvc
deleted file mode 100644
index d134fe5135..0000000000
--- a/tests/Core/positive/test040-bis.jvc
+++ /dev/null
@@ -1,20 +0,0 @@
--- letrec 2
-
-def writeLn := \x write x >> write "\n";
-
-def mutrec :=
-  let one := 1 in
-  let two := 2 in
-  let three := 3 in
-  letrec[a b c]
-    a := \x b one;
-    b := \x c two;
-    c := \x three
-  in writeLn (a 5);
-
--- bl = [three, two, one]
--- unfiltered free vars of defs = {one$5, two$4, three$3, b$2, c$1}
--- filtered free vars of defs = {one$2, two$1, three$0}
-
-
-letrec x := 3 in mutrec
diff --git a/tests/Core/positive/test040-bis2.jvc b/tests/Core/positive/test040-bis2.jvc
deleted file mode 100644
index 81a5a9abe6..0000000000
--- a/tests/Core/positive/test040-bis2.jvc
+++ /dev/null
@@ -1,20 +0,0 @@
--- letrec
-
-def writeLn := \x write x >> write "\n";
-
--- def mutrec2 :=
---   let two := 2 in
---    letrec z2 := {
---        two
---     } in z2 + two;
-
-def mutrec :=
-  let two := 2 in
-  letrec[f h]
-    f := h;
-    h := letrec z := {
-       f + two
-    } in z + two
-  in writeLn f;
-
-letrec x := 3 in mutrec
diff --git a/tests/Core/positive/test040.jvc b/tests/Core/positive/test040.jvc
index e778949eca..6cc205a8c4 100644
--- a/tests/Core/positive/test040.jvc
+++ b/tests/Core/positive/test040.jvc
@@ -13,26 +13,24 @@ def fib :=
 def writeLn := \x write x >> write "\n";
 
 def mutrec :=
-  let two := 2 in
-  let one := 1 in
   letrec[f g h]
     f := \x {
-      if x < one then
-        one
+      if x < 1 then
+        1
       else
-        g (x - one) + two * x
+        g (x - 1) + 2 * x
     };
     g := \x {
-      if x < one then
-        one
+      if x < 1 then
+        1
       else
-        x + h (x - one)
+        x + h (x - 1)
     };
     h := \x letrec z := {
-      if x < one then
-        one
+      if x < 1 then
+        1
       else
-        x * f (x - one)
+        x * f (x - 1)
     } in z
   in writeLn (f 5) >> writeLn (f 10) >> writeLn (f 100) >> writeLn (g 5) >> writeLn (h 5);
 

From 27cc5dbfc0b2b582f8c51ab376da68b870bb0efc Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 21 Oct 2022 16:50:44 +0200
Subject: [PATCH 70/73] remove length from the evaluator

---
 src/Juvix/Compiler/Core/Evaluator.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 3ab7294ed6..99b0c6a8eb 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -56,8 +56,8 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
     eval' :: Env -> Node -> Node
     eval' !env !n = case n of
       NVar (Var _ idx)
-        | idx < length env -> env !! idx
-        | otherwise -> error ("invalid index: " <> show idx <> " (length: " <> show (length env) <> ")")
+        | null (drop idx env) -> error ("invalid index: " <> show idx <> " (length: " <> show (length env) <> ")")
+        | otherwise -> env !! idx
       NIdt (Ident _ sym) -> eval' [] (lookupContext n sym)
       NCst {} -> n
       NApp (App i l r) ->

From d774d9cbca29029d917fc4ee86fb65f8ac431dab Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 21 Oct 2022 16:55:05 +0200
Subject: [PATCH 71/73] small improvement

---
 src/Juvix/Compiler/Core/Evaluator.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 99b0c6a8eb..e4e62bc499 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -55,9 +55,9 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
 
     eval' :: Env -> Node -> Node
     eval' !env !n = case n of
-      NVar (Var _ idx)
-        | null (drop idx env) -> error ("invalid index: " <> show idx <> " (length: " <> show (length env) <> ")")
-        | otherwise -> env !! idx
+      NVar (Var _ idx) -> fromMaybe err (listToMaybe (drop idx env))
+        where
+          err = error ("invalid index: " <> show idx <> " (length: " <> show (length env) <> ")")
       NIdt (Ident _ sym) -> eval' [] (lookupContext n sym)
       NCst {} -> n
       NApp (App i l r) ->

From b89632ed117bbc3854c6167f73865cd60d433d1b Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 21 Oct 2022 17:01:04 +0200
Subject: [PATCH 72/73] use strict

---
 package.yaml                         | 1 +
 src/Juvix/Compiler/Core/Evaluator.hs | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/package.yaml b/package.yaml
index 1757468449..71007f30b1 100644
--- a/package.yaml
+++ b/package.yaml
@@ -49,6 +49,7 @@ dependencies:
 - singletons == 3.0.*
 - singletons-th == 3.1.*
 - Stream == 0.4.*
+- strict == 0.4.*
 - time == 1.11.*
 - template-haskell == 2.18.*
 - text == 1.2.*
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index e4e62bc499..46219da23a 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -8,6 +8,7 @@ module Juvix.Compiler.Core.Evaluator where
 
 import Control.Exception qualified as Exception
 import Data.HashMap.Strict qualified as HashMap
+import Data.Strict.Maybe qualified as Strict
 import Debug.Trace qualified as Debug
 import GHC.Conc qualified as GHC
 import GHC.Show qualified as S
@@ -55,7 +56,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
 
     eval' :: Env -> Node -> Node
     eval' !env !n = case n of
-      NVar (Var _ idx) -> fromMaybe err (listToMaybe (drop idx env))
+      NVar (Var _ idx) -> Strict.fromMaybe err (Strict.listToMaybe (drop idx env))
         where
           err = error ("invalid index: " <> show idx <> " (length: " <> show (length env) <> ")")
       NIdt (Ident _ sym) -> eval' [] (lookupContext n sym)

From 116f51387772e0dc35e3796abf6b1eb0c275fa9c Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 21 Oct 2022 18:37:40 +0200
Subject: [PATCH 73/73] use Prelude's !!

---
 package.yaml                         | 1 -
 src/Juvix/Compiler/Core/Evaluator.hs | 5 +----
 2 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/package.yaml b/package.yaml
index 71007f30b1..1757468449 100644
--- a/package.yaml
+++ b/package.yaml
@@ -49,7 +49,6 @@ dependencies:
 - singletons == 3.0.*
 - singletons-th == 3.1.*
 - Stream == 0.4.*
-- strict == 0.4.*
 - time == 1.11.*
 - template-haskell == 2.18.*
 - text == 1.2.*
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 46219da23a..d6adb31219 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -8,7 +8,6 @@ module Juvix.Compiler.Core.Evaluator where
 
 import Control.Exception qualified as Exception
 import Data.HashMap.Strict qualified as HashMap
-import Data.Strict.Maybe qualified as Strict
 import Debug.Trace qualified as Debug
 import GHC.Conc qualified as GHC
 import GHC.Show qualified as S
@@ -56,9 +55,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
 
     eval' :: Env -> Node -> Node
     eval' !env !n = case n of
-      NVar (Var _ idx) -> Strict.fromMaybe err (Strict.listToMaybe (drop idx env))
-        where
-          err = error ("invalid index: " <> show idx <> " (length: " <> show (length env) <> ")")
+      NVar (Var _ idx) -> env !! idx
       NIdt (Ident _ sym) -> eval' [] (lookupContext n sym)
       NCst {} -> n
       NApp (App i l r) ->