--unroll option

app/App.hs

@@ -3,7 +3,6 @@ module App where
 import CommonOptions
 import Data.ByteString qualified as ByteString
 import GlobalOptions
-import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Pipeline
 import Juvix.Data.Error qualified as Error
@@ -79,21 +78,11 @@ getEntryPoint' RunAppIOArgs {..} inputFile = do
     if
         | opts ^. globalStdin -> Just <$> getContents
         | otherwise -> return Nothing
-  return
-    EntryPoint
-      { _entryPointRoot = root,
-        _entryPointResolverRoot = root,
-        _entryPointBuildDir = _runAppIOArgsBuildDir,
-        _entryPointNoTermination = opts ^. globalNoTermination,
-        _entryPointNoPositivity = opts ^. globalNoPositivity,
-        _entryPointNoCoverage = opts ^. globalNoCoverage,
-        _entryPointNoStdlib = opts ^. globalNoStdlib,
+  return $
+    (entryPointFromGlobalOptions root (someBaseToAbs _runAppIOArgsInvokeDir (inputFile ^. pathPath)) opts)
+      { _entryPointBuildDir = _runAppIOArgsBuildDir,
         _entryPointPackage = _runAppIOArgsPkg,
-        _entryPointModulePaths = pure (someBaseToAbs _runAppIOArgsInvokeDir (inputFile ^. pathPath)),
-        _entryPointGenericOptions = project opts,
-        _entryPointStdin = estdin,
-        _entryPointDebug = False,
-        _entryPointTarget = Backend.TargetCore
+        _entryPointStdin = estdin
       }
 
 someBaseToAbs' :: (Members '[App] r) => SomeBase a -> Sem r (Path Abs a)

app/Commands/Dev/Geb/Repl.hs

@@ -43,20 +43,10 @@ runCommand replOpts = do
         gopts <- State.gets (^. replStateGlobalOptions)
         absInputFile :: Path Abs File <- replMakeAbsolute inputFile
         return $
-          EntryPoint
-            { _entryPointRoot = root,
-              _entryPointBuildDir = buildDir,
-              _entryPointResolverRoot = root,
-              _entryPointNoTermination = gopts ^. globalNoTermination,
-              _entryPointNoPositivity = gopts ^. globalNoPositivity,
-              _entryPointNoCoverage = gopts ^. globalNoCoverage,
-              _entryPointNoStdlib = gopts ^. globalNoStdlib,
+          (entryPointFromGlobalOptions root absInputFile gopts)
+            { _entryPointBuildDir = buildDir,
               _entryPointPackage = package,
-              _entryPointModulePaths = pure absInputFile,
-              _entryPointGenericOptions = project gopts,
-              _entryPointStdin = Nothing,
-              _entryPointTarget = Backend.TargetGeb,
-              _entryPointDebug = False
+              _entryPointTarget = Backend.TargetGeb
             }
   embed
     ( State.evalStateT

app/Commands/Repl.hs

@@ -9,7 +9,6 @@ import Control.Exception (throwIO)
 import Control.Monad.State.Strict qualified as State
 import Data.String.Interpolate (i, __i)
 import Evaluator
-import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Core.Error qualified as Core
 import Juvix.Compiler.Core.Extra qualified as Core
@@ -85,20 +84,9 @@ runCommand opts = do
         gopts <- State.gets (^. replStateGlobalOptions)
         absInputFile :: Path Abs File <- replMakeAbsolute inputFile
         return $
-          EntryPoint
-            { _entryPointRoot = root,
-              _entryPointBuildDir = buildDir,
-              _entryPointResolverRoot = root,
-              _entryPointNoTermination = gopts ^. globalNoTermination,
-              _entryPointNoPositivity = gopts ^. globalNoPositivity,
-              _entryPointNoCoverage = gopts ^. globalNoCoverage,
-              _entryPointNoStdlib = gopts ^. globalNoStdlib,
-              _entryPointPackage = package,
-              _entryPointModulePaths = pure absInputFile,
-              _entryPointGenericOptions = project gopts,
-              _entryPointStdin = Nothing,
-              _entryPointTarget = Backend.TargetCore,
-              _entryPointDebug = False
+          (entryPointFromGlobalOptions root absInputFile gopts)
+            { _entryPointBuildDir = buildDir,
+              _entryPointPackage = package
             }
 
       printHelpTxt :: String -> Repl ()
@@ -306,23 +294,10 @@ defaultPreludeEntryPoint :: Repl EntryPoint
 defaultPreludeEntryPoint = do
   opts <- State.gets (^. replStateGlobalOptions)
   root <- State.gets (^. replStatePkgDir)
-  let buildDir = rootBuildDir root
-      defStdlibDir = defaultStdlibPath buildDir
+  let defStdlibDir = defaultStdlibPath (rootBuildDir root)
   return $
-    EntryPoint
-      { _entryPointRoot = root,
-        _entryPointResolverRoot = defStdlibDir,
-        _entryPointBuildDir = buildDir,
-        _entryPointNoTermination = opts ^. globalNoTermination,
-        _entryPointNoPositivity = opts ^. globalNoPositivity,
-        _entryPointNoCoverage = opts ^. globalNoCoverage,
-        _entryPointNoStdlib = opts ^. globalNoStdlib,
-        _entryPointPackage = defaultPackage root buildDir,
-        _entryPointModulePaths = pure (defStdlibDir <//> preludePath),
-        _entryPointGenericOptions = project opts,
-        _entryPointStdin = Nothing,
-        _entryPointTarget = Backend.TargetCore,
-        _entryPointDebug = False
+    (entryPointFromGlobalOptions root (defStdlibDir <//> preludePath) opts)
+      { _entryPointResolverRoot = defStdlibDir
       }
 
 replMakeAbsolute :: SomeBase b -> Repl (Path Abs b)

app/CommonOptions.hs

@@ -11,6 +11,7 @@ import Juvix.Compiler.Core.Data.TransformationId.Parser
 import Juvix.Prelude
 import Options.Applicative
 import System.Process
+import Text.Read (readMaybe)
 import Prelude (show)
 
 -- | Paths that are input are used to detect the root of the project.
@@ -130,6 +131,12 @@ someDirOpt = eitherReader aux
     aux :: String -> Either String (SomeBase Dir)
     aux s = maybe (Left $ s <> " is not a directory path") Right (parseSomeDir s)
 
+naturalNumberOpt :: ReadM Word
+naturalNumberOpt = eitherReader aux
+  where
+    aux :: String -> Either String Word
+    aux s = maybe (Left $ s <> " is not a nonnegative number") Right (readMaybe s :: Maybe Word)
+
 extCompleter :: String -> Completer
 extCompleter ext = mkCompleter $ \word -> do
   let cmd = unwords ["compgen", "-o", "plusdirs", "-f", "-X", "!*." <> ext, "--", requote word]

app/GlobalOptions.hs

@@ -7,6 +7,7 @@ import CommonOptions
 import Juvix.Compiler.Abstract.Pretty.Options qualified as Abstract
 import Juvix.Compiler.Core.Options qualified as Core
 import Juvix.Compiler.Internal.Pretty.Options qualified as Internal
+import Juvix.Compiler.Pipeline (EntryPoint (..), defaultEntryPoint)
 import Juvix.Data.Error.GenericError qualified as E
 import Juvix.Extra.Paths
 
@@ -20,7 +21,8 @@ data GlobalOptions = GlobalOptions
     _globalNoTermination :: Bool,
     _globalNoPositivity :: Bool,
     _globalNoCoverage :: Bool,
-    _globalNoStdlib :: Bool
+    _globalNoStdlib :: Bool,
+    _globalUnrollLimit :: Word
   }
   deriving stock (Eq, Show)
 
@@ -48,7 +50,8 @@ instance CanonicalProjection GlobalOptions E.GenericOptions where
 instance CanonicalProjection GlobalOptions Core.CoreOptions where
   project GlobalOptions {..} =
     Core.CoreOptions
-      { Core._optCheckCoverage = not _globalNoCoverage
+      { Core._optCheckCoverage = not _globalNoCoverage,
+        Core._optUnrollLimit = fromIntegral _globalUnrollLimit
       }
 
 defaultGlobalOptions :: GlobalOptions
@@ -63,7 +66,8 @@ defaultGlobalOptions =
       _globalStdin = False,
       _globalNoPositivity = False,
       _globalNoCoverage = False,
-      _globalNoStdlib = False
+      _globalNoStdlib = False,
+      _globalUnrollLimit = 140
     }
 
 -- | Get a parser for global flags which can be hidden or not depending on
@@ -122,6 +126,10 @@ parseGlobalFlags = do
       ( long "no-stdlib"
           <> help "Do not use the standard library"
       )
+  _globalUnrollLimit <-
+    option
+      naturalNumberOpt
+      (long "unroll" <> value 140 <> help "Recursion unrolling limit (default: 140)")
   return GlobalOptions {..}
 
 parseBuildDir :: Mod OptionFields (SomeBase Dir) -> Parser (AppPath Dir)
@@ -136,3 +144,14 @@ parseBuildDir m = do
           <> m
       )
   pure AppPath {_pathIsInput = False, ..}
+
+entryPointFromGlobalOptions :: Path Abs Dir -> Path Abs File -> GlobalOptions -> EntryPoint
+entryPointFromGlobalOptions root mainFile opts =
+  (defaultEntryPoint root mainFile)
+    { _entryPointNoTermination = opts ^. globalNoTermination,
+      _entryPointNoPositivity = opts ^. globalNoPositivity,
+      _entryPointNoCoverage = opts ^. globalNoCoverage,
+      _entryPointNoStdlib = opts ^. globalNoStdlib,
+      _entryPointUnrollLimit = fromIntegral $ opts ^. globalUnrollLimit,
+      _entryPointGenericOptions = project opts
+    }

src/Juvix/Compiler/Core/Options.hs

@@ -3,20 +3,23 @@ module Juvix.Compiler.Core.Options where
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Prelude
 
-newtype CoreOptions = CoreOptions
-  { _optCheckCoverage :: Bool
+data CoreOptions = CoreOptions
+  { _optCheckCoverage :: Bool,
+    _optUnrollLimit :: Int
   }
 
 makeLenses ''CoreOptions
 
 defaultCoreOptions :: CoreOptions
 defaultCoreOptions =
   CoreOptions
-    { _optCheckCoverage = True
+    { _optCheckCoverage = True,
+      _optUnrollLimit = 140
     }
 
 fromEntryPoint :: EntryPoint -> CoreOptions
 fromEntryPoint EntryPoint {..} =
   CoreOptions
-    { _optCheckCoverage = not _entryPointNoCoverage
+    { _optCheckCoverage = not _entryPointNoCoverage,
+      _optUnrollLimit = _entryPointUnrollLimit
     }

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -425,7 +425,7 @@ instance PrettyCode InfoTable where
   ppCode :: forall r. (Member (Reader Options) r) => InfoTable -> Sem r (Doc Ann)
   ppCode tbl = do
     tys <- ppInductives (toList (tbl ^. infoInductives))
-    sigs <- ppSigs (toList (tbl ^. infoIdentifiers))
+    sigs <- ppSigs (sortOn (^. identifierSymbol) $ toList (tbl ^. infoIdentifiers))
     ctx' <- ppContext (tbl ^. identContext)
     main <- maybe (return "") (\s -> (<> line) . (line <>) <$> ppName KNameFunction (fromJust (HashMap.lookup s (tbl ^. infoIdentifiers)) ^. identifierName)) (tbl ^. infoMain)
     return (tys <> line <> line <> sigs <> line <> ctx' <> line <> main)
@@ -458,7 +458,7 @@ instance PrettyCode InfoTable where
 
       ppContext :: IdentContext -> Sem r (Doc Ann)
       ppContext ctx = do
-        defs <- mapM (uncurry ppDef) (HashMap.toList ctx)
+        defs <- mapM (uncurry ppDef) (sortOn fst (HashMap.toList ctx))
         return (vsep (catMaybes defs))
         where
           ppDef :: Symbol -> Node -> Sem r (Maybe (Doc Ann))

src/Juvix/Compiler/Core/Transformation.hs

@@ -42,7 +42,7 @@ applyTransformations ts tbl = foldl' (\acc tid -> acc >>= appTrans tid) (return
       NatToInt -> return . natToInt
       ConvertBuiltinTypes -> return . convertBuiltinTypes
       ComputeTypeInfo -> return . computeTypeInfo
-      UnrollRecursion -> return . unrollRecursion
+      UnrollRecursion -> unrollRecursion
       MatchToCase -> mapError (JuvixError @CoreError) . matchToCase
       NaiveMatchToCase -> return . Naive.matchToCase
       EtaExpandApps -> return . etaExpansionApps

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

@@ -4,16 +4,16 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Data.IdentDependencyInfo
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base
 
-unrollRecursion :: InfoTable -> InfoTable
-unrollRecursion tab =
-  let (mp, tab') =
-        run $
-          runState @(HashMap Symbol Symbol) mempty $
-            execInfoTableBuilder tab $
-              forM_ (buildSCCs (createIdentDependencyInfo tab)) goSCC
-   in mapIdentSymbols mp $ pruneInfoTable tab'
+unrollRecursion :: Member (Reader CoreOptions) r => InfoTable -> Sem r InfoTable
+unrollRecursion tab = do
+  (mp, tab') <-
+    runState @(HashMap Symbol Symbol) mempty $
+      execInfoTableBuilder tab $
+        forM_ (buildSCCs (createIdentDependencyInfo tab)) goSCC
+  return $ mapIdentSymbols mp $ pruneInfoTable tab'
   where
     mapIdentSymbols :: HashMap Symbol Symbol -> InfoTable -> InfoTable
     mapIdentSymbols mp = over infoMain adjustMain . mapAllNodes (umap go)
@@ -29,25 +29,23 @@ unrollRecursion tab =
         adjustMain :: Maybe Symbol -> Maybe Symbol
         adjustMain = fmap $ \sym -> fromMaybe sym (HashMap.lookup sym mp)
 
-    goSCC :: Members '[InfoTableBuilder, State (HashMap Symbol Symbol)] r => SCC Symbol -> Sem r ()
+    goSCC :: Members '[InfoTableBuilder, State (HashMap Symbol Symbol), Reader CoreOptions] r => SCC Symbol -> Sem r ()
     goSCC = \case
       CyclicSCC syms -> unrollSCC syms
       AcyclicSCC _ -> return ()
 
-    unrollSCC :: Members '[InfoTableBuilder, State (HashMap Symbol Symbol)] r => [Symbol] -> Sem r ()
+    unrollSCC :: Members '[InfoTableBuilder, State (HashMap Symbol Symbol), Reader CoreOptions] r => [Symbol] -> Sem r ()
     unrollSCC syms = do
-      freshSyms <- genSyms syms
-      forM_ syms (unroll freshSyms)
-      modify (\mp -> foldr (mapSymbol freshSyms) mp syms)
+      unrollLimit <- asks (^. optUnrollLimit)
+      freshSyms <- genSyms unrollLimit syms
+      forM_ syms (unroll unrollLimit freshSyms)
+      modify (\mp -> foldr (mapSymbol unrollLimit freshSyms) mp syms)
       where
-        unrollLimit :: Int
-        unrollLimit = 140
+        mapSymbol :: Int -> HashMap (Indexed Symbol) Symbol -> Symbol -> HashMap Symbol Symbol -> HashMap Symbol Symbol
+        mapSymbol unrollLimit freshSyms sym = HashMap.insert sym (fromJust $ HashMap.lookup (Indexed unrollLimit sym) freshSyms)
 
-        mapSymbol :: HashMap (Indexed Symbol) Symbol -> Symbol -> HashMap Symbol Symbol -> HashMap Symbol Symbol
-        mapSymbol freshSyms sym = HashMap.insert sym (fromJust $ HashMap.lookup (Indexed unrollLimit sym) freshSyms)
-
-        genSyms :: forall r. Member InfoTableBuilder r => [Symbol] -> Sem r (HashMap (Indexed Symbol) Symbol)
-        genSyms = foldr go (return mempty)
+        genSyms :: forall r. Member InfoTableBuilder r => Int -> [Symbol] -> Sem r (HashMap (Indexed Symbol) Symbol)
+        genSyms unrollLimit = foldr go (return mempty)
           where
             go :: Symbol -> Sem r (HashMap (Indexed Symbol) Symbol) -> Sem r (HashMap (Indexed Symbol) Symbol)
             go sym m = foldr (go' sym) m [0 .. unrollLimit]
@@ -58,8 +56,8 @@ unrollRecursion tab =
               sym' <- freshSymbol
               return $ HashMap.insert (Indexed limit sym) sym' mp
 
-        unroll :: forall r. Member InfoTableBuilder r => HashMap (Indexed Symbol) Symbol -> Symbol -> Sem r ()
-        unroll freshSyms sym = do
+        unroll :: forall r. Member InfoTableBuilder r => Int -> HashMap (Indexed Symbol) Symbol -> Symbol -> Sem r ()
+        unroll unrollLimit freshSyms sym = do
           forM_ [0 .. unrollLimit] goUnroll
           removeSymbol sym
           where

src/Juvix/Compiler/Pipeline/EntryPoint.hs

@@ -24,6 +24,7 @@ data EntryPoint = EntryPoint
     _entryPointStdin :: Maybe Text,
     _entryPointTarget :: Target,
     _entryPointDebug :: Bool,
+    _entryPointUnrollLimit :: Int,
     _entryPointGenericOptions :: GenericOptions,
     _entryPointModulePaths :: NonEmpty (Path Abs File)
   }
@@ -44,8 +45,9 @@ defaultEntryPoint root mainFile =
       _entryPointStdin = Nothing,
       _entryPointPackage = defaultPackage root buildDir,
       _entryPointGenericOptions = defaultGenericOptions,
-      _entryPointTarget = TargetCNative64,
+      _entryPointTarget = TargetCore,
       _entryPointDebug = False,
+      _entryPointUnrollLimit = 140,
       _entryPointModulePaths = pure mainFile
     }
   where