Add translation from Internal to Core (#1567)

2024-10-05 20:47:36 +03:00 · 2022-11-07 13:47:56 +00:00 · 2022-11-07 13:47:56 +00:00 · a3b2aa6940
commit a3b2aa6940
parent 6adf5ed20a
127 changed files with 2042 additions and 155 deletions
--- a/app/App.hs
+++ b/app/App.hs
@ -3,6 +3,7 @@ module App where
 import CommonOptions
 import Data.ByteString qualified as ByteString
 import GlobalOptions
+import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Pipeline
 import Juvix.Data.Error qualified as Error
 import Juvix.Prelude.Pretty hiding (Doc)
@ -16,7 +17,7 @@ data App m a where
  AskPackage :: App m Package
  AskGlobalOptions :: App m GlobalOptions
  RenderStdOut :: (HasAnsiBackend a, HasTextBackend a) => a -> App m ()
-  RunPipelineEither :: Path -> Sem PipelineEff a -> App m (Either JuvixError a)
+  RunPipelineEither :: Path -> Sem PipelineEff a -> App m (Either JuvixError (BuiltinsState, a))
  Say :: Text -> App m ()
  Raw :: ByteString -> App m ()

@ -34,7 +35,7 @@ runAppIO g root pkg = interpret $ \case
  AskRoot -> return root
  RunPipelineEither input p -> do
    entry <- embed (getEntryPoint' g root pkg input)
-    embed (runIOEither entry p)
+    embed (runIOEither iniState entry p)
  Say t
    | g ^. globalOnlyErrors -> return ()
    | otherwise -> embed (putStrLn t)
@ -83,7 +84,7 @@ runPipeline input p = do
  r <- runPipelineEither input p
  case r of
    Left err -> exitJuvixError err
-    Right res -> return res
+    Right res -> return (snd res)

 newline :: Member App r => Sem r ()
 newline = say ""
--- a/app/Commands/Dev/Core/Eval.hs
+++ b/app/Commands/Dev/Core/Eval.hs
@ -2,51 +2,9 @@ module Commands.Dev.Core.Eval where

 import Commands.Base
 import Commands.Dev.Core.Eval.Options
+import Evaluator
 import Juvix.Compiler.Core.Data.InfoTable qualified as Core
-import Juvix.Compiler.Core.Error qualified as Core
-import Juvix.Compiler.Core.Evaluator qualified as Core
-import Juvix.Compiler.Core.Extra.Base qualified as Core
-import Juvix.Compiler.Core.Info qualified as Info
-import Juvix.Compiler.Core.Info.NoDisplayInfo qualified as Info
-import Juvix.Compiler.Core.Language qualified as Core
-import Juvix.Compiler.Core.Pretty qualified as Core
 import Juvix.Compiler.Core.Translation.FromSource qualified as Core
-import Text.Megaparsec.Pos qualified as M
-
-doEval ::
-  forall r.
-  Members '[Embed IO, App] r =>
-  Bool ->
-  Interval ->
-  Core.InfoTable ->
-  Core.Node ->
-  Sem r (Either Core.CoreError Core.Node)
-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 0 (M.initialPos f))
-    f :: FilePath
-    f = opts ^. coreEvalInputFile . pathPath

 runCommand :: forall r. Members '[Embed IO, App] r => CoreEvalOptions -> Sem r ()
 runCommand opts = do
--- a/app/Commands/Dev/Core/Eval/Options.hs
+++ b/app/Commands/Dev/Core/Eval/Options.hs
@ -1,6 +1,7 @@
 module Commands.Dev.Core.Eval.Options where

 import CommonOptions
+import Evaluator qualified as Eval
 import Juvix.Compiler.Core.Pretty.Options qualified as Core

 data CoreEvalOptions = CoreEvalOptions
@ -18,6 +19,13 @@ instance CanonicalProjection CoreEvalOptions Core.Options where
      { Core._optShowDeBruijnIndices = c ^. coreEvalShowDeBruijn
      }

+instance CanonicalProjection CoreEvalOptions Eval.EvalOptions where
+  project c =
+    Eval.EvalOptions
+      { _evalInputFile = c ^. coreEvalInputFile,
+        _evalNoIO = c ^. coreEvalNoIO
+      }
+
 parseCoreEvalOptions :: Parser CoreEvalOptions
 parseCoreEvalOptions = do
  _coreEvalNoIO <-
--- a/app/Commands/Dev/Core/Read.hs
+++ b/app/Commands/Dev/Core/Read.hs
@ -1,27 +1,27 @@
 module Commands.Dev.Core.Read where

 import Commands.Base
-import Commands.Dev.Core.Eval qualified as Eval
 import Commands.Dev.Core.Read.Options
+import Evaluator qualified as Eval
 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

-runCommand :: forall r. Members '[Embed IO, App] r => CoreReadOptions -> Sem r ()
+runCommand :: forall r a. (Members '[Embed IO, App] r, CanonicalProjection a Eval.EvalOptions, CanonicalProjection a Core.Options, CanonicalProjection a CoreReadOptions) => a -> Sem r ()
 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
+  let tab' = Core.applyTransformations (project opts ^. coreReadTransformations) tab
  embed (Scoper.scopeTrace tab')
-  unless (opts ^. coreReadNoPrint) (renderStdOut (Core.ppOut opts tab'))
+  unless (project opts ^. coreReadNoPrint) (renderStdOut (Core.ppOut opts tab'))
  whenJust mnode $ doEval tab'
  where
    doEval :: Core.InfoTable -> Core.Node -> Sem r ()
-    doEval tab' node = when (opts ^. coreReadEval) $ do
+    doEval tab' node = when (project opts ^. coreReadEval) $ do
      embed (putStrLn "--------------------------------")
      embed (putStrLn "|            Eval              |")
      embed (putStrLn "--------------------------------")
-      Eval.evalAndPrint (project opts) tab' node
+      Eval.evalAndPrint opts tab' node
    f :: FilePath
-    f = opts ^. coreReadInputFile . pathPath
+    f = project opts ^. coreReadInputFile . pathPath
--- a/app/Commands/Dev/Core/Read/Options.hs
+++ b/app/Commands/Dev/Core/Read/Options.hs
@ -2,6 +2,7 @@ module Commands.Dev.Core.Read.Options where

 import Commands.Dev.Core.Eval.Options qualified as Eval
 import CommonOptions
+import Evaluator qualified as Evaluator
 import Juvix.Compiler.Core.Data.TransformationId.Parser
 import Juvix.Compiler.Core.Pretty.Options qualified as Core

@ -30,6 +31,13 @@ instance CanonicalProjection CoreReadOptions Eval.CoreEvalOptions where
        _coreEvalShowDeBruijn = c ^. coreReadShowDeBruijn
      }

+instance CanonicalProjection CoreReadOptions Evaluator.EvalOptions where
+  project x =
+    Evaluator.EvalOptions
+      { _evalNoIO = False,
+        _evalInputFile = x ^. coreReadInputFile
+      }
+
 parseCoreReadOptions :: Parser CoreReadOptions
 parseCoreReadOptions = do
  _coreReadShowDeBruijn <- optDeBruijn
--- a/app/Commands/Dev/Core/Repl.hs
+++ b/app/Commands/Dev/Core/Repl.hs
@ -1,8 +1,8 @@
 module Commands.Dev.Core.Repl where

 import Commands.Base
-import Commands.Dev.Core.Eval (doEval)
 import Commands.Dev.Core.Repl.Options
+import Evaluator
 import Juvix.Compiler.Core.Data.InfoTable qualified as Core
 import Juvix.Compiler.Core.Extra.Base qualified as Core
 import Juvix.Compiler.Core.Info qualified as Info
--- a/app/Commands/Dev/Highlight.hs
+++ b/app/Commands/Dev/Highlight.hs
@ -15,9 +15,9 @@ runCommand HighlightOptions {..} = do
      genOpts <- askGenericOptions
      say (Highlight.goError (run $ runReader genOpts $ errorIntervals err))
    Right r -> do
-      let tbl = r ^. Scoper.resultParserTable
+      let tbl = r ^. _2 . Scoper.resultParserTable
          items = tbl ^. Parser.infoParsedItems
-          names = r ^. (Scoper.resultScoperTable . Scoper.infoNames)
+          names = r ^. _2 . (Scoper.resultScoperTable . Scoper.infoNames)
          inputFile = _highlightInputFile ^. pathPath
          hinput =
            Highlight.filterInput
--- a/app/Commands/Dev/Internal.hs
+++ b/app/Commands/Dev/Internal.hs
@ -2,6 +2,7 @@ module Commands.Dev.Internal where

 import Commands.Base
 import Commands.Dev.Internal.Arity qualified as Arity
+import Commands.Dev.Internal.CoreEval qualified as InternalCoreEval
 import Commands.Dev.Internal.Options
 import Commands.Dev.Internal.Pretty qualified as InternalPretty
 import Commands.Dev.Internal.Typecheck qualified as InternalTypecheck
@ -11,3 +12,4 @@ runCommand = \case
  Pretty opts -> InternalPretty.runCommand opts
  Arity opts -> Arity.runCommand opts
  TypeCheck opts -> InternalTypecheck.runCommand opts
+  CoreEval opts -> InternalCoreEval.runCommand opts
--- a/app/Commands/Dev/Internal/CoreEval.hs
+++ b/app/Commands/Dev/Internal/CoreEval.hs
@ -0,0 +1,13 @@
+module Commands.Dev.Internal.CoreEval where
+
+import Commands.Base
+import Commands.Dev.Internal.CoreEval.Options
+import Data.HashMap.Strict qualified as HashMap
+import Evaluator
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Translation
+
+runCommand :: Members '[Embed IO, App] r => InternalCoreEvalOptions -> Sem r ()
+runCommand localOpts = do
+  tab <- (^. coreResultTable) <$> runPipeline (localOpts ^. internalCoreEvalInputFile) upToCore
+  forM_ ((tab ^. infoMain) >>= ((tab ^. identContext) HashMap.!?)) (evalAndPrint localOpts tab)
--- a/app/Commands/Dev/Internal/CoreEval/Options.hs
+++ b/app/Commands/Dev/Internal/CoreEval/Options.hs
@ -0,0 +1,42 @@
+module Commands.Dev.Internal.CoreEval.Options where
+
+import CommonOptions
+import Evaluator qualified as Eval
+import Juvix.Compiler.Core.Pretty.Options qualified as Core
+
+data InternalCoreEvalOptions = InternalCoreEvalOptions
+  { _internalCoreEvalShowDeBruijn :: Bool,
+    _internalCoreEvalNoIO :: Bool,
+    _internalCoreEvalInputFile :: Path
+  }
+  deriving stock (Data)
+
+makeLenses ''InternalCoreEvalOptions
+
+instance CanonicalProjection InternalCoreEvalOptions Core.Options where
+  project c =
+    Core.defaultOptions
+      { Core._optShowDeBruijnIndices = c ^. internalCoreEvalShowDeBruijn
+      }
+
+instance CanonicalProjection InternalCoreEvalOptions Eval.EvalOptions where
+  project c =
+    Eval.EvalOptions
+      { _evalInputFile = c ^. internalCoreEvalInputFile,
+        _evalNoIO = c ^. internalCoreEvalNoIO
+      }
+
+parseInternalCoreEval :: Parser InternalCoreEvalOptions
+parseInternalCoreEval = do
+  _internalCoreEvalShowDeBruijn <-
+    switch
+      ( long "show-de-bruijn"
+          <> help "Show variable de Bruijn indices"
+      )
+  _internalCoreEvalNoIO <-
+    switch
+      ( long "no-io"
+          <> help "Don't interpret the IO effects"
+      )
+  _internalCoreEvalInputFile <- parseInputJuvixFile
+  pure InternalCoreEvalOptions {..}
--- a/app/Commands/Dev/Internal/Options.hs
+++ b/app/Commands/Dev/Internal/Options.hs
@ -1,6 +1,7 @@
 module Commands.Dev.Internal.Options where

 import Commands.Dev.Internal.Arity.Options
+import Commands.Dev.Internal.CoreEval.Options
 import Commands.Dev.Internal.Pretty.Options
 import Commands.Dev.Internal.Typecheck.Options
 import CommonOptions
@ -9,6 +10,7 @@ data InternalCommand
  = Pretty InternalPrettyOptions
  | TypeCheck InternalTypeOptions
  | Arity InternalArityOptions
+  | CoreEval InternalCoreEvalOptions
  deriving stock (Data)

 parseInternalCommand :: Parser InternalCommand
@ -17,7 +19,8 @@ parseInternalCommand =
    mconcat
      [ commandPretty,
        commandArity,
-        commandTypeCheck
+        commandTypeCheck,
+        commandCoreEval
      ]
  where
    commandArity :: Mod CommandFields InternalCommand
@ -29,6 +32,9 @@ parseInternalCommand =
    commandTypeCheck :: Mod CommandFields InternalCommand
    commandTypeCheck = command "typecheck" typeCheckInfo

+    commandCoreEval :: Mod CommandFields InternalCommand
+    commandCoreEval = command "core-eval" coreEvalInfo
+
    arityInfo :: ParserInfo InternalCommand
    arityInfo =
      info
@ -46,3 +52,9 @@ parseInternalCommand =
      info
        (TypeCheck <$> parseInternalType)
        (progDesc "Translate a Juvix file to Internal and typecheck the result")
+
+    coreEvalInfo :: ParserInfo InternalCommand
+    coreEvalInfo =
+      info
+        (CoreEval <$> parseInternalCoreEval)
+        (progDesc "Translate a Juvix file to Core and evaluate the result")
--- a/app/Commands/Repl.hs
+++ b/app/Commands/Repl.hs
@ -0,0 +1,266 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Commands.Repl where
+
+import Commands.Base hiding (command)
+import Commands.Repl.Options
+import Control.Exception (throwIO)
+import Control.Monad.IO.Class
+import Control.Monad.State.Strict qualified as State
+import Data.String.Interpolate (i, __i)
+import Evaluator
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Core.Error qualified as Core
+import Juvix.Compiler.Core.Extra qualified as Core
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NoDisplayInfo qualified as Info
+import Juvix.Compiler.Core.Language qualified as Core
+import Juvix.Compiler.Core.Pretty qualified as Core
+import Juvix.Compiler.Core.Translation.FromInternal.Data as Core
+import Juvix.Compiler.Internal.Language qualified as Internal
+import Juvix.Compiler.Internal.Pretty qualified as Internal
+import Juvix.Data.Error.GenericError qualified as Error
+import Juvix.Extra.Version
+import Juvix.Prelude.Pretty qualified as P
+import System.Console.ANSI qualified as Ansi
+import System.Console.Haskeline
+import System.Console.Repline
+import System.Console.Repline qualified as Repline
+import Text.Megaparsec qualified as M
+
+data ReplContext = ReplContext
+  { _replContextBuiltins :: BuiltinsState,
+    _replContextExpContext :: ExpressionContext,
+    _replContextEntryPoint :: EntryPoint
+  }
+
+data ReplState = ReplState
+  { _replStateRoot :: FilePath,
+    _replStateContext :: Maybe ReplContext,
+    _replStateGlobalOptions :: GlobalOptions,
+    _replStateMkEntryPoint :: FilePath -> EntryPoint
+  }
+
+makeLenses ''ReplState
+makeLenses ''ReplContext
+
+type ReplS = State.StateT ReplState IO
+
+type Repl a = HaskelineT ReplS a
+
+helpTxt :: MonadIO m => m ()
+helpTxt =
+  liftIO
+    ( putStrLn
+        [__i|
+  Type any expression to evaluate it in the context of the currently loaded module or use one of the following commands:
+  :help
+         Print help text and describe options
+  :load FILE
+         Load a file into the REPL
+  :type EXPRESSION
+         Infer the type of an expression
+  :core EXPRESSION
+         Translate the expression to JuvixCore
+  :idents
+         List the identifiers in the environment
+  :multiline
+         Start a multi-line input. Submit with <Ctrl-D>
+  :root
+         Print the current project root
+  :quit
+         Exit the REPL
+  |]
+    )
+
+noFileLoadedMsg :: MonadIO m => m ()
+noFileLoadedMsg = liftIO (putStrLn "No file loaded. Load a file using the `:load FILE` command.")
+
+welcomeMsg :: MonadIO m => m ()
+welcomeMsg = liftIO (putStrLn [i|Juvix REPL version #{versionTag}: https://juvix.org. Run :help for help|])
+
+runCommand :: Members '[Embed IO, App] r => ReplOptions -> Sem r ()
+runCommand opts = do
+  let printHelpTxt :: String -> Repl ()
+      printHelpTxt _ = helpTxt
+
+      multilineCmd :: String
+      multilineCmd = "multiline"
+
+      quit :: String -> Repl ()
+      quit _ = liftIO (throwIO Interrupt)
+
+      loadFile :: String -> Repl ()
+      loadFile args = do
+        mkEntryPoint <- State.gets (^. replStateMkEntryPoint)
+        let f = unpack (strip (pack args))
+            entryPoint = mkEntryPoint f
+        (bs, res) <- liftIO (runIO' iniState entryPoint upToCore)
+        State.modify
+          ( set
+              replStateContext
+              ( Just
+                  ( ReplContext
+                      { _replContextBuiltins = bs,
+                        _replContextExpContext = expressionContext res,
+                        _replContextEntryPoint = entryPoint
+                      }
+                  )
+              )
+          )
+        liftIO (putStrLn [i|OK loaded: #{f}|])
+
+      printRoot :: String -> Repl ()
+      printRoot _ = do
+        r <- State.gets (^. replStateRoot)
+        liftIO $ putStrLn (pack r)
+
+      command :: String -> Repl ()
+      command input = Repline.dontCrash $ do
+        ctx <- State.gets (^. replStateContext)
+        gopts <- State.gets (^. replStateGlobalOptions)
+        case ctx of
+          Just ctx' -> do
+            evalRes <- compileThenEval ctx' input
+            case evalRes of
+              Left err -> printError gopts err
+              Right n
+                | Info.member Info.kNoDisplayInfo (Core.getInfo n) -> return ()
+              Right n -> renderOut gopts (Core.ppOut (ctx' ^. replContextEntryPoint . entryPointGenericOptions) n)
+          Nothing -> noFileLoadedMsg
+        where
+          defaultLoc :: Interval
+          defaultLoc = singletonInterval (mkLoc 0 (M.initialPos ""))
+
+          compileThenEval :: ReplContext -> String -> Repl (Either JuvixError Core.Node)
+          compileThenEval ctx s = bindEither compileString eval
+            where
+              eval :: Core.Node -> Repl (Either JuvixError Core.Node)
+              eval n =
+                liftIO $
+                  mapLeft
+                    (JuvixError @Core.CoreError)
+                    <$> doEvalIO False defaultLoc (ctx ^. replContextExpContext . contextCoreResult . Core.coreResultTable) n
+
+              compileString :: Repl (Either JuvixError Core.Node)
+              compileString = liftIO $ compileExpressionIO' ctx (pack s)
+
+              bindEither :: Monad m => m (Either e a) -> (a -> m (Either e b)) -> m (Either e b)
+              bindEither x f = join <$> (x >>= mapM f)
+
+      core :: String -> Repl ()
+      core input = Repline.dontCrash $ do
+        ctx <- State.gets (^. replStateContext)
+        gopts <- State.gets (^. replStateGlobalOptions)
+        case ctx of
+          Just ctx' -> do
+            compileRes <- liftIO (compileExpressionIO' ctx' (pack input))
+            case compileRes of
+              Left err -> printError gopts err
+              Right n -> renderOut gopts (Core.ppOut (project' @GenericOptions gopts) n)
+          Nothing -> noFileLoadedMsg
+
+      inferType :: String -> Repl ()
+      inferType input = Repline.dontCrash $ do
+        ctx <- State.gets (^. replStateContext)
+        gopts <- State.gets (^. replStateGlobalOptions)
+        case ctx of
+          Just ctx' -> do
+            compileRes <- liftIO (inferExpressionIO' ctx' (pack input))
+            case compileRes of
+              Left err -> printError gopts err
+              Right n -> renderOut gopts (Internal.ppOut (project' @GenericOptions gopts) n)
+          Nothing -> noFileLoadedMsg
+
+      options :: [(String, String -> Repl ())]
+      options =
+        [ ("help", Repline.dontCrash . printHelpTxt),
+          -- `multiline` is included here for auto-completion purposes only.
+          -- `repline`'s `multilineCommand` logic overrides this no-op.
+          (multilineCmd, Repline.dontCrash . \_ -> return ()),
+          ("quit", quit),
+          ("load", Repline.dontCrash . loadFile),
+          ("root", printRoot),
+          ("type", inferType),
+          ("core", core)
+        ]
+
+      defaultMatcher :: [(String, CompletionFunc ReplS)]
+      defaultMatcher = [(":load", fileCompleter)]
+
+      optsCompleter :: WordCompleter ReplS
+      optsCompleter n = do
+        let names = (":" <>) . fst <$> options
+        return (filter (isPrefixOf n) names)
+
+      banner :: MultiLine -> Repl String
+      banner = \case
+        MultiLine -> return "... "
+        SingleLine -> return "juvix> "
+
+      prefix :: Maybe Char
+      prefix = Just ':'
+
+      multilineCommand :: Maybe String
+      multilineCommand = Just multilineCmd
+
+      initialiser :: Repl ()
+      initialiser = do
+        welcomeMsg
+        whenJust ((^. pathPath) <$> (opts ^. replInputFile)) loadFile
+
+      finaliser :: Repl ExitDecision
+      finaliser = return Exit
+
+      tabComplete :: CompleterStyle ReplS
+      tabComplete = Prefix (wordCompleter optsCompleter) defaultMatcher
+
+      replAction :: ReplS ()
+      replAction = evalReplOpts ReplOpts {..}
+
+  root <- askRoot
+  globalOptions <- askGlobalOptions
+  embed
+    ( State.evalStateT
+        replAction
+        ( ReplState
+            { _replStateRoot = root,
+              _replStateContext = Nothing,
+              _replStateGlobalOptions = globalOptions,
+              _replStateMkEntryPoint = getReplEntryPoint globalOptions root
+            }
+        )
+    )
+
+getReplEntryPoint :: GlobalOptions -> FilePath -> FilePath -> EntryPoint
+getReplEntryPoint opts root inputFile =
+  EntryPoint
+    { _entryPointRoot = root,
+      _entryPointNoTermination = opts ^. globalNoTermination,
+      _entryPointNoPositivity = opts ^. globalNoPositivity,
+      _entryPointNoStdlib = opts ^. globalNoStdlib,
+      _entryPointStdlibPath = opts ^. globalStdlibPath,
+      _entryPointPackage = emptyPackage,
+      _entryPointModulePaths = pure inputFile,
+      _entryPointGenericOptions = project opts,
+      _entryPointStdin = Nothing
+    }
+
+inferExpressionIO' :: ReplContext -> Text -> IO (Either JuvixError Internal.Expression)
+inferExpressionIO' ctx = inferExpressionIO "" (ctx ^. replContextExpContext) (ctx ^. replContextBuiltins)
+
+compileExpressionIO' :: ReplContext -> Text -> IO (Either JuvixError Core.Node)
+compileExpressionIO' ctx = compileExpressionIO "" (ctx ^. replContextExpContext) (ctx ^. replContextBuiltins)
+
+render' :: (MonadIO m, P.HasAnsiBackend a, P.HasTextBackend a) => GlobalOptions -> a -> m ()
+render' g t = liftIO $ do
+  hasAnsi <- Ansi.hSupportsANSI stdout
+  P.renderIO (not (g ^. globalNoColors) && hasAnsi) t
+
+renderOut :: (MonadIO m, P.HasAnsiBackend a, P.HasTextBackend a) => GlobalOptions -> a -> m ()
+renderOut g t = render' g t >> liftIO (putStrLn "")
+
+printError :: MonadIO m => GlobalOptions -> JuvixError -> m ()
+printError opts e = liftIO $ do
+  hasAnsi <- Ansi.hSupportsANSI stderr
+  liftIO $ hPutStrLn stderr $ run (runReader (project' @GenericOptions opts) (Error.render (not (opts ^. globalNoColors) && hasAnsi) False e))
--- a/app/Commands/Repl/Options.hs
+++ b/app/Commands/Repl/Options.hs
@ -0,0 +1,14 @@
+module Commands.Repl.Options where
+
+import CommonOptions
+
+newtype ReplOptions = ReplOptions
+  {_replInputFile :: Maybe Path}
+  deriving stock (Data)
+
+makeLenses ''ReplOptions
+
+parseRepl :: Parser ReplOptions
+parseRepl = do
+  _replInputFile <- optional parseInputJuvixFile
+  pure ReplOptions {..}
--- a/app/Evaluator.hs
+++ b/app/Evaluator.hs
@ -0,0 +1,63 @@
+module Evaluator where
+
+import App
+import CommonOptions
+import Juvix.Compiler.Core.Data.InfoTable qualified as Core
+import Juvix.Compiler.Core.Error qualified as Core
+import Juvix.Compiler.Core.Evaluator qualified as Core
+import Juvix.Compiler.Core.Extra.Base qualified as Core
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NoDisplayInfo qualified as Info
+import Juvix.Compiler.Core.Language qualified as Core
+import Juvix.Compiler.Core.Pretty qualified as Core
+import Text.Megaparsec.Pos qualified as M
+
+data EvalOptions = EvalOptions
+  { _evalInputFile :: Path,
+    _evalNoIO :: Bool
+  }
+
+makeLenses ''EvalOptions
+
+doEval ::
+  forall r.
+  Members '[Embed IO] r =>
+  Bool ->
+  Interval ->
+  Core.InfoTable ->
+  Core.Node ->
+  Sem r (Either Core.CoreError Core.Node)
+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)
+
+doEvalIO ::
+  Bool ->
+  Interval ->
+  Core.InfoTable ->
+  Core.Node ->
+  IO (Either Core.CoreError Core.Node)
+doEvalIO noIO i tab node = runM (doEval noIO i tab node)
+
+evalAndPrint ::
+  forall r a.
+  (Members '[Embed IO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection a Core.Options) =>
+  a ->
+  Core.InfoTable ->
+  Core.Node ->
+  Sem r ()
+evalAndPrint opts tab node = do
+  r <- doEval (project opts ^. evalNoIO) 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 0 (M.initialPos f))
+    f :: FilePath
+    f = project opts ^. evalInputFile . pathPath
--- a/app/TopCommand.hs
+++ b/app/TopCommand.hs
@ -6,6 +6,7 @@ import Commands.Dev qualified as Dev
 import Commands.Doctor qualified as Doctor
 import Commands.Html qualified as Html
 import Commands.Init qualified as Init
+import Commands.Repl qualified as Repl
 import Commands.Typecheck qualified as Typecheck
 import Juvix.Extra.Version
 import System.Environment (getProgName)
@ -29,3 +30,4 @@ runTopCommand = \case
  Typecheck opts -> Typecheck.runCommand opts
  Compile opts -> Compile.runCommand opts
  Html opts -> Html.runCommand opts
+  JuvixRepl opts -> Repl.runCommand opts
--- a/app/TopCommand/Options.hs
+++ b/app/TopCommand/Options.hs
@ -4,6 +4,7 @@ import Commands.Compile.Options
 import Commands.Dev.Options
 import Commands.Doctor.Options
 import Commands.Html.Options
+import Commands.Repl.Options
 import Commands.Typecheck.Options
 import CommonOptions hiding (Doc)
 import Data.Generics.Uniplate.Data
@ -19,6 +20,7 @@ data TopCommand
  | Dev DevCommand
  | Doctor DoctorOptions
  | Init
+  | JuvixRepl ReplOptions
  deriving stock (Data)

 topCommandInputFile :: TopCommand -> Maybe FilePath
@ -55,7 +57,8 @@ parseUtility =
          metavar "UTILITY_CMD",
          commandDoctor,
          commandInit,
-          commandDev
+          commandDev,
+          commandRepl
        ]
    )
  where
@ -75,6 +78,14 @@ parseUtility =
            (Doctor <$> parseDoctorOptions)
            (progDesc "Perform checks on your Juvix development environment")
        )
+    commandRepl :: Mod CommandFields TopCommand
+    commandRepl =
+      command
+        "repl"
+        ( info
+            (JuvixRepl <$> parseRepl)
+            (progDesc "Run the Juvix REPL")
+        )

 commandCheck :: Mod CommandFields TopCommand
 commandCheck =
--- a/c-runtime/builtins/juvix_string.h
+++ b/c-runtime/builtins/juvix_string.h
@ -0,0 +1,6 @@
+#ifndef STRING_H_
+#define STRING_H_
+
+typedef char* prim_string;
+
+#endif // STRING_H_
--- a/c-runtime/standalone/c-runtime.h
+++ b/c-runtime/standalone/c-runtime.h
@ -4,6 +4,7 @@
 #include "bool.h"
 #include "nat.h"
 #include "io.h"
+#include "juvix_string.h"

 typedef __SIZE_TYPE__ size_t;
 typedef __UINT8_TYPE__ uint8_t;
--- a/c-runtime/wasi-libc/c-runtime.h
+++ b/c-runtime/wasi-libc/c-runtime.h
@ -9,6 +9,7 @@
 #include "bool.h"
 #include "nat.h"
 #include "io.h"
+#include "juvix_string.h"

 typedef struct juvix_function {
    uintptr_t fun;
--- a/c-runtime/wasi-standalone/c-runtime.h
+++ b/c-runtime/wasi-standalone/c-runtime.h
@ -4,6 +4,7 @@
 #include "bool.h"
 #include "nat.h"
 #include "io.h"
+#include "juvix_string.h"

 typedef __SIZE_TYPE__ size_t;
 typedef __UINT8_TYPE__ uint8_t;
--- a/2
+++ b/2
@ -1 +1 @@
-Subproject commit 572580b3184fc74254bf76f95af997fef2638aeb
+Subproject commit c91ec2eb6daf49c993a1f55673e75d97cb8dada3
--- a/package.yaml
+++ b/package.yaml
@ -108,8 +108,12 @@ executables:
    source-dirs: app
    dependencies:
    - juvix
+    - haskeline == 0.8.*
    - http-conduit == 2.3.*
+    - mtl == 2.2.*
    - optparse-applicative == 0.17.*
+    - repline == 0.4.*
+    - string-interpolate == 0.3.*
    - uniplate == 1.6.*
    verbatim:
      default-language: GHC2021
--- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs
@ -34,6 +34,9 @@ fromConcrete _resultScoper =
  where
    ms = _resultScoper ^. Scoper.resultModules

+fromConcreteExpression :: Members '[Error JuvixError, NameIdGen] r => Scoper.Expression -> Sem r Abstract.Expression
+fromConcreteExpression = mapError (JuvixError @ScoperError) . goExpression
+
 goTopModule ::
  Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r =>
  Module 'Scoped 'ModuleTop ->
@ -264,6 +267,9 @@ registerBuiltinAxiom d = \case
  BuiltinIO -> registerIO d
  BuiltinIOSequence -> registerIOSequence d
  BuiltinNatPrint -> registerNatPrint d
+  BuiltinString -> registerString d
+  BuiltinStringPrint -> registerStringPrint d
+  BuiltinBoolPrint -> registerBoolPrint d

 goInductive ::
  Members '[InfoTableBuilder, Builtins, Error ScoperError] r =>
--- a/src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs
+++ b/src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs
@ -21,6 +21,9 @@ builtinAxiomName = \case
  BuiltinNatPrint -> Just printNat
  BuiltinIO -> Just io
  BuiltinIOSequence -> Just ioseq
+  BuiltinString -> Just string_
+  BuiltinStringPrint -> Just printString
+  BuiltinBoolPrint -> Just printBool

 builtinFunctionName :: BuiltinFunction -> Maybe Text
 builtinFunctionName = \case
--- a/src/Juvix/Compiler/Backend/C/Data/CNames.hs
+++ b/src/Juvix/Compiler/Backend/C/Data/CNames.hs
@ -14,9 +14,15 @@ suc = primPrefix "suc"
 printNat :: Text
 printNat = primPrefix "printNat"

+printString :: Text
+printString = primPrefix "printString"
+
 io :: Text
 io = primPrefix "io"

+string_ :: Text
+string_ = primPrefix "string"
+
 nat :: Text
 nat = primPrefix "nat"

@ -29,6 +35,9 @@ true_ = primPrefix "true"
 false_ :: Text
 false_ = primPrefix "false"

+printBool :: Text
+printBool = primPrefix "printBool"
+
 int_ :: Text
 int_ = "int"

--- a/src/Juvix/Compiler/Backend/C/Data/Closure.hs
+++ b/src/Juvix/Compiler/Backend/C/Data/Closure.hs
@ -5,6 +5,7 @@ import Juvix.Compiler.Backend.C.Language
 import Juvix.Compiler.Concrete.Data.Builtins (IsBuiltin (toBuiltinPrim))
 import Juvix.Compiler.Internal.Extra (mkPolyType')
 import Juvix.Compiler.Internal.Extra qualified as Micro
+import Juvix.Compiler.Internal.Translation.Extra qualified as Micro
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Micro
 import Juvix.Prelude

@ -79,7 +80,7 @@ genClosureExpression funArgTyps = \case
  where
    exprApplication :: Micro.Application -> Sem r [ClosureInfo]
    exprApplication a = do
-      (f0, appArgs) <- unfoldPolyApp a
+      (f0, appArgs) <- Micro.unfoldPolyApplication a
      if
          | null appArgs -> genClosureExpression funArgTyps f0
          | otherwise -> case f0 of
--- a/src/Juvix/Compiler/Backend/C/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Backend/C/Translation/FromInternal.hs
@ -20,6 +20,7 @@ import Juvix.Compiler.Concrete.Language qualified as C
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Internal.Extra (mkPolyType')
 import Juvix.Compiler.Internal.Extra qualified as Micro
+import Juvix.Compiler.Internal.Translation.Extra qualified as Trans
 import Juvix.Compiler.Internal.Translation.FromAbstract qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as Micro1
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Micro
@ -400,7 +401,7 @@ goIden = \case

 goApplication :: forall r. Members '[Reader PatternInfoTable, Reader Micro.TypesTable, Builtins, Reader Micro.InfoTable] r => Micro.Application -> Sem r Expression
 goApplication a = do
-  (f, args0) <- unfoldPolyApp a
+  (f, args0) <- Trans.unfoldPolyApplication a
  if
      | null args0 -> goExpression f
      | otherwise -> case f of
--- a/src/Juvix/Compiler/Builtins.hs
+++ b/src/Juvix/Compiler/Builtins.hs
@ -3,6 +3,7 @@ module Juvix.Compiler.Builtins
    module Juvix.Compiler.Builtins.Nat,
    module Juvix.Compiler.Builtins.IO,
    module Juvix.Compiler.Builtins.Bool,
+    module Juvix.Compiler.Builtins.String,
  )
 where

@ -10,3 +11,4 @@ import Juvix.Compiler.Builtins.Bool
 import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Nat
+import Juvix.Compiler.Builtins.String
--- a/src/Juvix/Compiler/Builtins/Bool.hs
+++ b/src/Juvix/Compiler/Builtins/Bool.hs
@ -64,3 +64,10 @@ registerIf f = do
    Just z -> forM_ z $ \((exLhs, exBody), (lhs, body)) -> do
      unless (exLhs =% lhs) (error "clause lhs does not match")
      unless (exBody =% body) (error $ "clause body does not match " <> ppTrace exBody <> " | " <> ppTrace body)
+
+registerBoolPrint :: Members '[Builtins] r => AxiomDef -> Sem r ()
+registerBoolPrint f = do
+  bool_ <- getBuiltinName (getLoc f) BuiltinBool
+  io <- getBuiltinName (getLoc f) BuiltinIO
+  unless (f ^. axiomType === (bool_ --> io)) (error "Bool print has the wrong type signature")
+  registerBuiltin BuiltinBoolPrint (f ^. axiomName)
--- a/src/Juvix/Compiler/Builtins/Effect.hs
+++ b/src/Juvix/Compiler/Builtins/Effect.hs
@ -59,5 +59,5 @@ re = reinterpret $ \case
                _alreadyDefinedLoc = getLoc n
              }

-runBuiltins :: Member (Error JuvixError) r => Sem (Builtins ': r) a -> Sem r a
-runBuiltins = evalState iniState . re
+runBuiltins :: Member (Error JuvixError) r => BuiltinsState -> Sem (Builtins ': r) a -> Sem r (BuiltinsState, a)
+runBuiltins s = runState s . re
--- a/src/Juvix/Compiler/Builtins/String.hs
+++ b/src/Juvix/Compiler/Builtins/String.hs
@ -0,0 +1,17 @@
+module Juvix.Compiler.Builtins.String where
+
+import Juvix.Compiler.Abstract.Extra
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Prelude
+
+registerString :: Member Builtins r => AxiomDef -> Sem r ()
+registerString d = do
+  unless (isSmallUniverse' (d ^. axiomType)) (error "String should be in the small universe")
+  registerBuiltin BuiltinString (d ^. axiomName)
+
+registerStringPrint :: Member Builtins r => AxiomDef -> Sem r ()
+registerStringPrint f = do
+  string_ <- getBuiltinName (getLoc f) BuiltinString
+  io <- getBuiltinName (getLoc f) BuiltinIO
+  unless (f ^. axiomType === (string_ --> io)) (error "String print has the wrong type signature")
+  registerBuiltin BuiltinStringPrint (f ^. axiomName)
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@ -75,6 +75,9 @@ instance Pretty BuiltinFunction where

 data BuiltinAxiom
  = BuiltinNatPrint
+  | BuiltinStringPrint
+  | BuiltinBoolPrint
+  | BuiltinString
  | BuiltinIO
  | BuiltinIOSequence
  deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
@ -84,5 +87,8 @@ instance Hashable BuiltinAxiom
 instance Pretty BuiltinAxiom where
  pretty = \case
    BuiltinNatPrint -> Str.natPrint
+    BuiltinStringPrint -> Str.stringPrint
+    BuiltinBoolPrint -> Str.boolPrint
    BuiltinIO -> Str.io
+    BuiltinString -> Str.string
    BuiltinIOSequence -> Str.ioSequence
--- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
@ -91,8 +91,8 @@ toState = reinterpret $ \case
     in modify (over infoFunctionClauses (HashMap.insert key value))
  RegisterName n -> modify (over infoNames (cons (S.AName n)))

-runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
-runInfoTableBuilder = runState emptyInfoTable . toState
+runInfoTableBuilder :: InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
+runInfoTableBuilder tab = runState tab . toState

 ignoreInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r a
 ignoreInfoTableBuilder = evalState emptyInfoTable . toState
--- a/src/Juvix/Compiler/Concrete/Data/Scope.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Scope.hs
@ -63,7 +63,8 @@ makeLenses ''ScopeParameters

 data ScoperState = ScoperState
  { _scoperModulesCache :: ModulesCache,
-    _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete)
+    _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete),
+    _scoperScope :: HashMap TopModulePath Scope
  }

 makeLenses ''ScoperState
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed.hs
@ -5,6 +5,7 @@ module Juvix.Compiler.Concrete.Translation.FromParsed
  )
 where

+import Juvix.Compiler.Concrete.Data.InfoTable
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context
@ -18,4 +19,4 @@ fromParsed ::
  Sem r ScoperResult
 fromParsed pr = mapError (JuvixError @ScoperError) $ do
  let modules = pr ^. Parser.resultModules
-  scopeCheck pr modules
+  scopeCheck pr emptyInfoTable modules
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@ -16,6 +16,7 @@ import Juvix.Compiler.Concrete.Data.Name qualified as N
 import Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder (mergeTable)
 import Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder qualified as Parser
 import Juvix.Compiler.Concrete.Data.Scope
+import Juvix.Compiler.Concrete.Data.Scope qualified as S
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Compiler.Concrete.Language
@ -26,42 +27,70 @@ import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context (ParserResult)
 import Juvix.Prelude

+iniScoperState :: ScoperState
+iniScoperState =
+  ScoperState
+    { _scoperModulesCache = ModulesCache mempty,
+      _scoperModules = mempty,
+      _scoperScope = mempty
+    }
+
+iniScopeParameters :: ScopeParameters
+iniScopeParameters =
+  ScopeParameters
+    { _scopeFileExtension = ".juvix",
+      _scopeTopParents = mempty
+    }
+
 scopeCheck ::
  Members '[Files, Error ScoperError, NameIdGen] r =>
  ParserResult ->
+  InfoTable ->
  NonEmpty (Module 'Parsed 'ModuleTop) ->
  Sem r ScoperResult
-scopeCheck pr modules =
+scopeCheck pr tab modules =
  fmap mkResult $
    Parser.runInfoTableBuilder $
-      runInfoTableBuilder $
-        runReader scopeParameters $
-          evalState iniScoperState $ do
+      runInfoTableBuilder tab $
+        runReader iniScopeParameters $
+          runState iniScoperState $ do
            mergeTable (pr ^. Parser.resultTable)
            checkTopModules modules
  where
-    mkResult :: (Parser.InfoTable, (InfoTable, (NonEmpty (Module 'Scoped 'ModuleTop), HashSet NameId))) -> ScoperResult
-    mkResult (pt, (st, (ms, exp))) =
+    mkResult :: (Parser.InfoTable, (InfoTable, (ScoperState, (NonEmpty (Module 'Scoped 'ModuleTop), HashSet NameId)))) -> ScoperResult
+    mkResult (pt, (st, (scoperSt, (ms, exp)))) =
      ScoperResult
        { _resultParserResult = pr,
          _resultParserTable = pt,
          _resultScoperTable = st,
          _resultModules = ms,
-          _resultExports = exp
-        }
-    iniScoperState :: ScoperState
-    iniScoperState =
-      ScoperState
-        { _scoperModulesCache = ModulesCache mempty,
-          _scoperModules = mempty
-        }
-    scopeParameters :: ScopeParameters
-    scopeParameters =
-      ScopeParameters
-        { _scopeFileExtension = ".juvix",
-          _scopeTopParents = mempty
+          _resultExports = exp,
+          _resultScope = scoperSt ^. scoperScope
        }

+scopeCheckExpression ::
+  forall r.
+  Members '[Error JuvixError, NameIdGen] r =>
+  InfoTable ->
+  S.Scope ->
+  ExpressionAtoms 'Parsed ->
+  Sem r Expression
+scopeCheckExpression tab scope as = mapError (JuvixError @ScoperError) $ do
+  snd
+    <$> ( runInfoTableBuilder tab $
+            runReader iniScopeParameters $
+              evalState iniScoperState $
+                evalState scope $
+                  localScope $
+                    checkParseExpressionAtoms as
+        )
+
+checkParseExpressionAtoms' ::
+  Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
+  ExpressionAtoms 'Parsed ->
+  Sem r Expression
+checkParseExpressionAtoms' = checkExpressionAtoms >=> parseExpressionAtoms
+
 freshVariable :: Members '[NameIdGen, State Scope] r => Symbol -> Sem r S.Symbol
 freshVariable = freshSymbol S.KNameLocal

@ -283,7 +312,8 @@ lookupQualifiedSymbol (path, sym) = do
    here = lookupSymbolAux path sym
    -- Looks for a top level modules
    there :: Sem r [SymbolEntry]
-    there = concatMapM (fmap maybeToList . uncurry lookInTopModule) allTopPaths
+    there = do
+      concatMapM (fmap maybeToList . uncurry lookInTopModule) allTopPaths
      where
        allTopPaths :: [(TopModulePath, [Symbol])]
        allTopPaths = map (first nonEmptyToTopPath) raw
@ -540,7 +570,7 @@ checkTopModule m@(Module path params doc body) = do
    iniScope = emptyScope (getTopModulePath m)
    checkedModule :: Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
    checkedModule = do
-      evalState iniScope $ do
+      (s, (m', p)) <- runState iniScope $ do
        path' <- freshTopModulePath
        localScope $
          withParams params $ \params' -> do
@ -554,7 +584,9 @@ checkTopModule m@(Module path params doc body) = do
                      _moduleDoc = doc'
                    }
                _moduleRefName = set S.nameConcrete () path'
-            return ModuleRef'' {..}
+            return (ModuleRef'' {..}, path')
+      modify (set (scoperScope . at (p ^. S.nameConcrete)) (Just s))
+      return m'

 withScope :: Members '[State Scope] r => Sem r a -> Sem r a
 withScope ma = do
@ -829,7 +861,7 @@ lookupLocalEntry sym = do
    SymbolInfo {..} <- ms
    HashMap.lookup path _symbolInfo

-localScope :: Sem (Reader LocalVars : r) a -> Sem r a
+localScope :: forall r a. Sem (Reader LocalVars : r) a -> Sem r a
 localScope = runReader (LocalVars mempty)

 checkAxiomDef ::
@ -1213,6 +1245,7 @@ checkParens e@(ExpressionAtoms as _) = case as of
  _ -> checkParseExpressionAtoms e

 checkExpressionAtoms ::
+  forall r.
  Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
  ExpressionAtoms 'Parsed ->
  Sem r (ExpressionAtoms 'Scoped)
@ -1248,6 +1281,7 @@ checkJudocAtom = \case
  JudocExpression e -> JudocExpression <$> checkParseExpressionAtoms e

 checkParseExpressionAtoms ::
+  forall r.
  Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
  ExpressionAtoms 'Parsed ->
  Sem r Expression
@ -1358,6 +1392,7 @@ makeExpressionTable2 (ExpressionAtoms atoms _) = [appOpExplicit] : operators ++
                }

 parseExpressionAtoms ::
+  forall r.
  Members '[Error ScoperError, State Scope] r =>
  ExpressionAtoms 'Scoped ->
  Sem r Expression
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Data/Context.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Data/Context.hs
@ -2,6 +2,7 @@ module Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Cont

 import Juvix.Compiler.Concrete.Data.InfoTable
 import Juvix.Compiler.Concrete.Data.ParsedInfoTable qualified as Parsed
+import Juvix.Compiler.Concrete.Data.Scope
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as Parsed
 import Juvix.Prelude
@ -11,7 +12,8 @@ data ScoperResult = ScoperResult
    _resultParserTable :: Parsed.InfoTable,
    _resultScoperTable :: InfoTable,
    _resultModules :: NonEmpty (Module 'Scoped 'ModuleTop),
-    _resultExports :: HashSet NameId
+    _resultExports :: HashSet NameId,
+    _resultScope :: HashMap TopModulePath Scope
  }

 makeLenses ''ScoperResult
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@ -50,6 +50,19 @@ fromSource e = mapError (JuvixError @ParserError) $ do
              return txt
          | otherwise = readFile' fp

+-- | The fileName is only used for reporting errors. It is safe to pass
+-- an empty string.
+expressionFromTextSource ::
+  Members '[Error JuvixError, NameIdGen] r =>
+  FilePath ->
+  Text ->
+  Sem r (ExpressionAtoms 'Parsed)
+expressionFromTextSource fp txt = mapError (JuvixError @ParserError) $ do
+  exp <- runExpressionParser fp txt
+  case exp of
+    Left e -> throw e
+    Right exp' -> return exp'
+
 -- | The fileName is only used for reporting errors. It is safe to pass
 -- an empty string.
 runModuleParser :: Members '[NameIdGen] r => FilePath -> Text -> Sem r (Either ParserError (InfoTable, Module 'Parsed 'ModuleTop))
@ -62,6 +75,22 @@ runModuleParser fileName input = do
    (_, Left err) -> return (Left (ParserError err))
    (tbl, Right r) -> return (Right (tbl, r))

+-- | The fileName is only used for reporting errors. It is safe to pass
+-- an empty string.
+runExpressionParser ::
+  Members '[NameIdGen] r =>
+  FilePath ->
+  Text ->
+  Sem r (Either ParserError (ExpressionAtoms 'Parsed))
+runExpressionParser fileName input = do
+  m <-
+    runInfoTableBuilder $
+      evalState (Nothing @(Judoc 'Parsed)) $
+        P.runParserT parseExpressionAtoms fileName input
+  case m of
+    (_, Left err) -> return (Left (ParserError err))
+    (_, Right r) -> return (Right r)
+
 top ::
  Member InfoTableBuilder r =>
  ParsecS r a ->
--- a/src/Juvix/Compiler/Core.hs
+++ b/src/Juvix/Compiler/Core.hs
@ -0,0 +1,3 @@
+module Juvix.Compiler.Core (module Juvix.Compiler.Core.Translation) where
+
+import Juvix.Compiler.Core.Translation
--- a/src/Juvix/Compiler/Core/Data.hs
+++ b/src/Juvix/Compiler/Core/Data.hs
@ -0,0 +1,8 @@
+module Juvix.Compiler.Core.Data
+  ( module Juvix.Compiler.Core.Data.InfoTable,
+    module Juvix.Compiler.Core.Data.InfoTableBuilder,
+  )
+where
+
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Data.InfoTableBuilder
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@ -12,12 +12,15 @@ data InfoTableBuilder m a where
  RegisterConstructor :: ConstructorInfo -> InfoTableBuilder m ()
  RegisterInductive :: InductiveInfo -> InfoTableBuilder m ()
  RegisterIdentNode :: Symbol -> Node -> InfoTableBuilder m ()
+  RegisterMain :: Symbol -> InfoTableBuilder m ()
  SetIdentArgsInfo :: Symbol -> [ArgumentInfo] -> InfoTableBuilder m ()
  GetIdent :: Text -> InfoTableBuilder m (Maybe IdentKind)
  GetInfoTable :: InfoTableBuilder m InfoTable

 makeSem ''InfoTableBuilder

+type MkIdentIndex = Name -> Text
+
 getConstructorInfo :: Member InfoTableBuilder r => Tag -> Sem r ConstructorInfo
 getConstructorInfo tag = do
  tab <- getInfoTable
@ -28,8 +31,8 @@ checkSymbolDefined sym = do
  tab <- getInfoTable
  return $ HashMap.member sym (tab ^. identContext)

-runInfoTableBuilder :: InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
-runInfoTableBuilder tab =
+runInfoTableBuilder :: MkIdentIndex -> InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
+runInfoTableBuilder mkIdentIndex tab =
  runState tab
    . reinterpret interp
  where
@ -45,16 +48,18 @@ runInfoTableBuilder tab =
        return (UserTag (s ^. infoNextTag))
      RegisterIdent ii -> do
        modify' (over infoIdentifiers (HashMap.insert (ii ^. identifierSymbol) ii))
-        whenJust (ii ^? identifierName . _Just . nameText) $ \name ->
-          modify' (over identMap (HashMap.insert name (IdentFun (ii ^. identifierSymbol))))
+        whenJust (ii ^? identifierName . _Just) $ \n ->
+          modify' (over identMap (HashMap.insert (mkIdentIndex n) (IdentFun (ii ^. identifierSymbol))))
      RegisterConstructor ci -> do
        modify' (over infoConstructors (HashMap.insert (ci ^. constructorTag) ci))
-        modify' (over identMap (HashMap.insert (ci ^. (constructorName . nameText)) (IdentConstr (ci ^. constructorTag))))
+        modify' (over identMap (HashMap.insert (mkIdentIndex (ci ^. constructorName)) (IdentConstr (ci ^. constructorTag))))
      RegisterInductive ii -> do
        modify' (over infoInductives (HashMap.insert (ii ^. inductiveSymbol) ii))
-        modify' (over identMap (HashMap.insert (ii ^. (inductiveName . nameText)) (IdentInd (ii ^. inductiveSymbol))))
+        modify' (over identMap (HashMap.insert (mkIdentIndex (ii ^. inductiveName)) (IdentInd (ii ^. inductiveSymbol))))
      RegisterIdentNode sym node ->
        modify' (over identContext (HashMap.insert sym node))
+      RegisterMain sym -> do
+        modify' (set infoMain (Just sym))
      SetIdentArgsInfo sym argsInfo -> do
        modify' (set (infoIdentifiers . at sym . _Just . identifierArgsInfo) argsInfo)
        modify' (set (infoIdentifiers . at sym . _Just . identifierArgsNum) (length argsInfo))
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@ -370,8 +370,11 @@ instance PrettyCode Stripped.InfoTable where
            return (kwDef <+> sym' <+> kwAssign <+> body')

 instance PrettyCode a => PrettyCode (NonEmpty a) where
+  ppCode x = ppCode (toList x)
+
+instance PrettyCode a => PrettyCode [a] where
  ppCode x = do
-    cs <- mapM ppCode (toList x)
+    cs <- mapM ppCode x
    return $ encloseSep "(" ")" ", " cs

 {--------------------------------------------------------------------------------}
--- a/src/Juvix/Compiler/Core/Pretty/Options.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Options.hs
@ -28,3 +28,6 @@ traceOptions =

 fromGenericOptions :: GenericOptions -> Options
 fromGenericOptions GenericOptions {..} = set optShowNameIds _showNameIds defaultOptions
+
+instance CanonicalProjection GenericOptions Options where
+  project = fromGenericOptions
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@ -18,7 +18,7 @@ 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 $
+    runInfoTableBuilder (^. nameText) tab $
      mapM_
        (\(k, v) -> f v >>= registerIdentNode k)
        (HashMap.toList (tab ^. identContext))
--- a/src/Juvix/Compiler/Core/Translation.hs
+++ b/src/Juvix/Compiler/Core/Translation.hs
@ -0,0 +1,8 @@
+module Juvix.Compiler.Core.Translation
+  ( module Juvix.Compiler.Core.Translation.FromInternal,
+    module Juvix.Compiler.Core.Translation.FromInternal.Data,
+  )
+where
+
+import Juvix.Compiler.Core.Translation.FromInternal
+import Juvix.Compiler.Core.Translation.FromInternal.Data
--- a/src/Juvix/Compiler/Core/Translation/Base.hs
+++ b/src/Juvix/Compiler/Core/Translation/Base.hs
@ -0,0 +1,20 @@
+module Juvix.Compiler.Core.Translation.Base where
+
+import Juvix.Compiler.Core.Language
+
+freshName ::
+  Member NameIdGen r =>
+  NameKind ->
+  Text ->
+  Interval ->
+  Sem r Name
+freshName kind txt i = do
+  nid <- freshNameId
+  return $
+    Name
+      { _nameText = txt,
+        _nameId = nid,
+        _nameKind = kind,
+        _namePretty = txt,
+        _nameLoc = i
+      }
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@ -0,0 +1,498 @@
+module Juvix.Compiler.Core.Translation.FromInternal where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.List.NonEmpty (fromList)
+import Juvix.Compiler.Concrete.Data.Literal (LiteralLoc)
+import Juvix.Compiler.Core.Data
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.LocationInfo
+import Juvix.Compiler.Core.Info.NameInfo
+import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Transformation.Eta (etaExpandApps)
+import Juvix.Compiler.Core.Translation.FromInternal.Data
+import Juvix.Compiler.Internal.Extra qualified as Internal
+import Juvix.Compiler.Internal.Translation.Extra qualified as Internal
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped
+import Juvix.Data.Loc qualified as Loc
+import Juvix.Extra.Strings qualified as Str
+
+unsupported :: Text -> a
+unsupported thing = error ("Internal to Core: Not yet supported: " <> thing)
+
+isExplicit :: Internal.PatternArg -> Bool
+isExplicit = (== Internal.Explicit) . (^. Internal.patternArgIsImplicit)
+
+-- Translation of a Name into the identifier index used in the Core InfoTable
+mkIdentIndex :: Name -> Text
+mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)
+
+fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
+fromInternal i = do
+  (res, _) <- runInfoTableBuilder mkIdentIndex emptyInfoTable (runReader (i ^. InternalTyped.resultIdenTypes) f)
+  return $
+    CoreResult
+      { _coreResultTable = res,
+        _coreResultInternalTypedResult = i
+      }
+  where
+    f :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable] r => Sem r ()
+    f = do
+      let resultModules = toList (i ^. InternalTyped.resultModules)
+      runNameIdGen (runReader (Internal.buildTable resultModules) (mapM_ coreModule resultModules))
+      where
+        coreModule :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, NameIdGen] r => Internal.Module -> Sem r ()
+        coreModule m = do
+          registerInductiveDefs m
+          registerFunctionDefs m
+
+fromInternalExpression :: CoreResult -> Internal.Expression -> Sem r Node
+fromInternalExpression res exp = do
+  let modules = res ^. coreResultInternalTypedResult . InternalTyped.resultModules
+  snd
+    <$> runReader
+      (Internal.buildTable modules)
+      ( runInfoTableBuilder
+          mkIdentIndex
+          (res ^. coreResultTable)
+          ( runReader
+              (res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
+              (runReader initIndexTable (goExpression exp))
+          )
+      )
+
+registerInductiveDefs ::
+  forall r.
+  Members '[InfoTableBuilder, Reader Internal.InfoTable] r =>
+  Internal.Module ->
+  Sem r ()
+registerInductiveDefs m = registerInductiveDefsBody (m ^. Internal.moduleBody)
+
+registerInductiveDefsBody ::
+  forall r.
+  Members '[InfoTableBuilder, Reader Internal.InfoTable] r =>
+  Internal.ModuleBody ->
+  Sem r ()
+registerInductiveDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
+  where
+    go :: Internal.Statement -> Sem r ()
+    go = \case
+      Internal.StatementInductive d -> goInductiveDef d
+      Internal.StatementAxiom {} -> return ()
+      Internal.StatementForeign {} -> return ()
+      Internal.StatementFunction {} -> return ()
+      Internal.StatementInclude i ->
+        mapM_ go (i ^. Internal.includeModule . Internal.moduleBody . Internal.moduleStatements)
+
+registerFunctionDefs ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r =>
+  Internal.Module ->
+  Sem r ()
+registerFunctionDefs m = registerFunctionDefsBody (m ^. Internal.moduleBody)
+
+registerFunctionDefsBody ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r =>
+  Internal.ModuleBody ->
+  Sem r ()
+registerFunctionDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
+  where
+    go :: Internal.Statement -> Sem r ()
+    go = \case
+      Internal.StatementFunction f -> goMutualBlock f
+      Internal.StatementAxiom a -> goAxiomDef a
+      Internal.StatementInclude i -> mapM_ go (i ^. Internal.includeModule . Internal.moduleBody . Internal.moduleStatements)
+      _ -> return ()
+
+goInductiveDef ::
+  forall r.
+  Members '[InfoTableBuilder, Reader Internal.InfoTable] r =>
+  Internal.InductiveDef ->
+  Sem r ()
+goInductiveDef i = do
+  sym <- freshSymbol
+  ctorInfos <- mapM (goConstructor sym) (i ^. Internal.inductiveConstructors)
+  do
+    let info =
+          InductiveInfo
+            { _inductiveName = i ^. Internal.inductiveName,
+              _inductiveSymbol = sym,
+              _inductiveKind = mkDynamic',
+              _inductiveConstructors = ctorInfos,
+              _inductiveParams = [],
+              _inductivePositive = i ^. Internal.inductivePositive
+            }
+    registerInductive info
+
+goConstructor ::
+  forall r.
+  Members '[InfoTableBuilder, Reader Internal.InfoTable] r =>
+  Symbol ->
+  Internal.InductiveConstructorDef ->
+  Sem r ConstructorInfo
+goConstructor sym ctor = do
+  tag <- ctorTag
+  let info =
+        ConstructorInfo
+          { _constructorName = ctor ^. Internal.inductiveConstructorName,
+            _constructorTag = tag,
+            _constructorType = mkDynamic',
+            _constructorArgsNum = length (ctor ^. Internal.inductiveConstructorParameters),
+            _constructorInductive = sym
+          }
+  registerConstructor info
+  return info
+  where
+    ctorTag :: Sem r Tag
+    ctorTag = do
+      ctorInfo <- HashMap.lookupDefault impossible (ctor ^. Internal.inductiveConstructorName) <$> asks (^. Internal.infoConstructors)
+      case ctorInfo ^. Internal.constructorInfoBuiltin of
+        Just Internal.BuiltinBoolTrue -> return (BuiltinTag TagTrue)
+        Just Internal.BuiltinBoolFalse -> return (BuiltinTag TagFalse)
+        Just Internal.BuiltinNatZero -> freshTag
+        Just Internal.BuiltinNatSuc -> freshTag
+        Nothing -> freshTag
+
+goMutualBlock ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r =>
+  Internal.MutualBlock ->
+  Sem r ()
+goMutualBlock m = do
+  funcsWithSym <- mapM withSym (m ^. Internal.mutualFunctions)
+  mapM_ goFunctionDefIden funcsWithSym
+  mapM_ goFunctionDef funcsWithSym
+  where
+    withSym :: a -> Sem r (a, Symbol)
+    withSym x = do
+      sym <- freshSymbol
+      return (x, sym)
+
+goFunctionDefIden ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen] r =>
+  (Internal.FunctionDef, Symbol) ->
+  Sem r ()
+goFunctionDefIden (f, sym) = do
+  let info =
+        IdentifierInfo
+          { _identifierName = Just (f ^. Internal.funDefName),
+            _identifierSymbol = sym,
+            _identifierType = mkDynamic',
+            _identifierArgsNum = 0,
+            _identifierArgsInfo = [],
+            _identifierIsExported = False
+          }
+  registerIdent info
+  when (f ^. Internal.funDefName . Internal.nameText == Str.main) (registerMain sym)
+
+goFunctionDef ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r =>
+  (Internal.FunctionDef, Symbol) ->
+  Sem r ()
+goFunctionDef (f, sym) = do
+  mbody <- case f ^. Internal.funDefBuiltin of
+    Just Internal.BuiltinBoolIf -> return Nothing
+    Just Internal.BuiltinNatPlus -> Just <$> mkBody
+    Nothing -> Just <$> mkBody
+  forM_ mbody (registerIdentNode sym)
+  where
+    mkBody :: Sem r Node
+    mkBody =
+      if
+          | nExplicitPatterns == 0 -> runReader initIndexTable (goExpression (f ^. Internal.funDefClauses . _head1 . Internal.clauseBody))
+          | otherwise ->
+              ( do
+                  let values :: [Node]
+                      values = mkVar Info.empty <$> vs
+                      indexTable :: IndexTable
+                      indexTable = IndexTable {_indexTableVarsNum = nExplicitPatterns, _indexTableVars = mempty}
+                  ms <- mapM (runReader indexTable . goFunctionClause) (f ^. Internal.funDefClauses)
+                  let match = mkMatch' (fromList values) (toList ms)
+                  return $ foldr (\_ n -> mkLambda' n) match vs
+              )
+    -- Assumption: All clauses have the same number of patterns
+    nExplicitPatterns :: Int
+    nExplicitPatterns = length $ filter isExplicit (f ^. Internal.funDefClauses . _head1 . Internal.clausePatterns)
+
+    vs :: [Index]
+    vs = take nExplicitPatterns [0 ..]
+
+goLambda ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
+  Internal.Lambda ->
+  Sem r Node
+goLambda l = do
+  ms <-
+    local
+      (over indexTableVarsNum (+ nPatterns))
+      (mapM goLambdaClause (l ^. Internal.lambdaClauses))
+  values' <- values
+  let match = mkMatch' (fromList values') (toList ms)
+  return $ foldr (\_ n -> mkLambda' n) match values'
+  where
+    nPatterns :: Int
+    nPatterns = length (l ^. Internal.lambdaClauses . _head1 . Internal.lambdaPatterns)
+
+    values :: Sem r [Node]
+    values = do
+      varsNum <- asks (^. indexTableVarsNum)
+      let vs = take nPatterns [varsNum ..]
+      return (mkVar' <$> vs)
+
+goAxiomDef ::
+  forall r.
+  Members '[InfoTableBuilder, Reader Internal.InfoTable] r =>
+  Internal.AxiomDef ->
+  Sem r ()
+goAxiomDef a = case a ^. Internal.axiomBuiltin >>= builtinBody of
+  Just body -> do
+    sym <- freshSymbol
+    let info =
+          IdentifierInfo
+            { _identifierName = Just (a ^. Internal.axiomName),
+              _identifierSymbol = sym,
+              _identifierType = mkDynamic',
+              _identifierArgsNum = 0,
+              _identifierArgsInfo = [],
+              _identifierIsExported = False
+            }
+    registerIdent info
+    registerIdentNode sym body
+  Nothing -> return ()
+  where
+    builtinBody :: Internal.BuiltinAxiom -> Maybe Node
+    builtinBody = \case
+      Internal.BuiltinNatPrint -> Just writeLambda
+      Internal.BuiltinStringPrint -> Just writeLambda
+      Internal.BuiltinBoolPrint -> Just writeLambda
+      Internal.BuiltinIOSequence ->
+        Just
+          ( mkLambda'
+              ( mkLambda'
+                  ( mkConstr'
+                      (BuiltinTag TagBind)
+                      [mkVar' 1, mkLambda' (mkVar' 1)]
+                  )
+              )
+          )
+      Internal.BuiltinString -> Nothing
+      Internal.BuiltinIO -> Nothing
+
+    writeLambda :: Node
+    writeLambda = mkLambda' (mkConstr' (BuiltinTag TagWrite) [mkVar' 0])
+
+fromPattern ::
+  forall r.
+  Members '[InfoTableBuilder, Reader Internal.InfoTable] r =>
+  Internal.Pattern ->
+  Sem r Pattern
+fromPattern = \case
+  Internal.PatternWildcard {} -> return wildcard
+  Internal.PatternVariable n -> return $ PatBinder (PatternBinder (Binder (Just n) mkDynamic') wildcard)
+  Internal.PatternConstructorApp c -> do
+    let n = c ^. Internal.constrAppConstructor
+        explicitPatterns =
+          (^. Internal.patternArgPattern)
+            <$> filter
+              isExplicit
+              (c ^. Internal.constrAppParameters)
+
+    args <- mapM fromPattern explicitPatterns
+    m <- getIdent identIndex
+    case m of
+      Just (IdentConstr tag) -> return $ PatConstr (PatternConstr (setInfoName n Info.empty) tag args)
+      Just _ -> error ("internal to core: not a constructor " <> txt)
+      Nothing -> error ("internal to core: undeclared identifier: " <> txt)
+    where
+      identIndex :: Text
+      identIndex = mkIdentIndex (c ^. Internal.constrAppConstructor)
+
+      txt :: Text
+      txt = c ^. Internal.constrAppConstructor . Internal.nameText
+  where
+    wildcard :: Pattern
+    wildcard = PatWildcard (PatternWildcard Info.empty)
+
+goPatterns ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
+  Internal.Expression ->
+  [Internal.Pattern] ->
+  Sem r MatchBranch
+goPatterns body ps = do
+  vars <- asks (^. indexTableVars)
+  varsNum <- asks (^. indexTableVarsNum)
+  pats <- patterns
+  let bs :: [Binder]
+      bs = concatMap getPatternBinders pats
+      (vars', varsNum') =
+        foldl'
+          ( \(vs, k) name ->
+              (HashMap.insert (name ^. nameId) k vs, k + 1)
+          )
+          (vars, varsNum)
+          (map (fromJust . (^. binderName)) bs)
+      body' :: Sem r Node
+      body' =
+        local
+          (set indexTableVars vars' . set indexTableVarsNum varsNum')
+          (goExpression body)
+  MatchBranch Info.empty (fromList pats) <$> body'
+  where
+    patterns :: Sem r [Pattern]
+    patterns = reverse <$> mapM fromPattern ps
+
+goFunctionClause ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
+  Internal.FunctionClause ->
+  Sem r MatchBranch
+goFunctionClause clause =
+  local
+    (over indexTableVars (HashMap.union patternArgs))
+    (goPatterns (clause ^. Internal.clauseBody) ps)
+  where
+    explicitPatternArgs :: [Internal.PatternArg]
+    explicitPatternArgs = filter isExplicit (clause ^. Internal.clausePatterns)
+
+    ps :: [Internal.Pattern]
+    ps = (^. Internal.patternArgPattern) <$> explicitPatternArgs
+
+    patternArgs :: HashMap NameId Index
+    patternArgs = HashMap.fromList (first (^. nameId) <$> patternArgNames)
+      where
+        patternArgNames :: [(Name, Index)]
+        patternArgNames = catFstMaybes (first (^. Internal.patternArgName) <$> zip explicitPatternArgs [0 ..])
+
+        catFstMaybes :: [(Maybe a, b)] -> [(a, b)]
+        catFstMaybes = mapMaybe f
+          where
+            f :: (Maybe a, b) -> Maybe (a, b)
+            f (x, y) = fmap (\x' -> (x', y)) x
+
+goLambdaClause ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
+  Internal.LambdaClause ->
+  Sem r MatchBranch
+goLambdaClause clause = goPatterns (clause ^. Internal.lambdaBody) ps
+  where
+    ps :: [Internal.Pattern]
+    ps = (^. Internal.patternArgPattern) <$> toList (clause ^. Internal.lambdaPatterns)
+
+goExpression ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
+  Internal.Expression ->
+  Sem r Node
+goExpression e = do
+  node <- goExpression' e
+  tab <- getInfoTable
+  return $ etaExpandApps tab node
+
+goExpression' ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
+  Internal.Expression ->
+  Sem r Node
+goExpression' = \case
+  Internal.ExpressionLiteral l -> return (goLiteral l)
+  Internal.ExpressionIden i -> case i of
+    Internal.IdenVar n -> do
+      k <- HashMap.lookupDefault impossible id_ <$> asks (^. indexTableVars)
+      varsNum <- asks (^. indexTableVarsNum)
+      return (mkVar (Info.singleton (NameInfo n)) (varsNum - k - 1))
+    Internal.IdenFunction n -> do
+      m <- getIdent identIndex
+      return $ case m of
+        Just (IdentFun sym) -> mkIdent (Info.singleton (NameInfo n)) sym
+        Just _ -> error ("internal to core: not a function: " <> txt)
+        Nothing -> error ("internal to core: undeclared identifier: " <> txt)
+    Internal.IdenInductive {} -> unsupported "goExpression inductive"
+    Internal.IdenConstructor n -> do
+      m <- getIdent identIndex
+      case m of
+        Just (IdentConstr tag) -> return (mkConstr (Info.singleton (NameInfo n)) tag [])
+        Just _ -> error ("internal to core: not a constructor " <> txt)
+        Nothing -> error ("internal to core: undeclared identifier: " <> txt)
+    Internal.IdenAxiom n -> do
+      m <- getIdent identIndex
+      return $ case m of
+        Just (IdentFun sym) -> mkIdent (Info.singleton (NameInfo n)) sym
+        Just _ -> error ("internal to core: not a function: " <> txt)
+        Nothing -> error ("internal to core: undeclared identifier: " <> txt)
+    where
+      identIndex :: Text
+      identIndex = mkIdentIndex (Internal.getName i)
+
+      id_ :: NameId
+      id_ = Internal.getName i ^. nameId
+
+      txt :: Text
+      txt = Internal.getName i ^. Internal.nameText
+  Internal.ExpressionApplication a -> goApplication a
+  Internal.ExpressionSimpleLambda l -> goSimpleLambda l
+  Internal.ExpressionLambda l -> goLambda l
+  Internal.ExpressionFunction f -> unsupported ("goExpression function: " <> show (Loc.getLoc f))
+  Internal.ExpressionHole h -> error ("goExpression hole: " <> show (Loc.getLoc h))
+  Internal.ExpressionUniverse u -> error ("goExpression universe: " <> show (Loc.getLoc u))
+
+goSimpleLambda ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
+  Internal.SimpleLambda ->
+  Sem r Node
+goSimpleLambda l = do
+  updateFn <- update
+  local
+    updateFn
+    (mkLambda' <$> goExpression (l ^. Internal.slambdaBody))
+  where
+    update :: Sem r (IndexTable -> IndexTable)
+    update = do
+      idx <- asks (^. indexTableVarsNum)
+      return
+        ( over indexTableVars (HashMap.insert (l ^. Internal.slambdaVar . nameId) idx)
+            . over indexTableVarsNum (+ 1)
+        )
+
+goApplication ::
+  forall r.
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r =>
+  Internal.Application ->
+  Sem r Node
+goApplication a = do
+  (f, args) <- Internal.unfoldPolyApplication a
+  let exprArgs :: Sem r [Node]
+      exprArgs = mapM goExpression args
+
+      app :: Sem r Node
+      app = do
+        fExpr <- goExpression f
+        case a ^. Internal.appImplicit of
+          Internal.Implicit -> return fExpr
+          Internal.Explicit -> mkApps' fExpr <$> exprArgs
+
+  case f of
+    Internal.ExpressionIden (Internal.IdenFunction n) -> do
+      funInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoFunctions)
+      case funInfo ^. Internal.functionInfoDef . Internal.funDefBuiltin of
+        Just Internal.BuiltinBoolIf -> do
+          as <- exprArgs
+          case as of
+            (v : b1 : b2 : xs) -> return (mkApps' (mkIf' v b1 b2) xs)
+            _ -> error "if must be called with 3 arguments"
+        _ -> app
+    _ -> app
+
+goLiteral :: LiteralLoc -> Node
+goLiteral l = case l ^. withLocParam of
+  Internal.LitString s -> mkLitConst (ConstString s)
+  Internal.LitInteger i -> mkLitConst (ConstInteger i)
+  where
+    mkLitConst :: ConstantValue -> Node
+    mkLitConst = mkConstant (Info.singleton (LocationInfo (l ^. withLocInt)))
--- a/src/Juvix/Compiler/Core/Translation/FromInternal/Data.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal/Data.hs
@ -0,0 +1,8 @@
+module Juvix.Compiler.Core.Translation.FromInternal.Data
+  ( module Juvix.Compiler.Core.Translation.FromInternal.Data.Context,
+    module Juvix.Compiler.Core.Translation.FromInternal.Data.IndexTable,
+  )
+where
+
+import Juvix.Compiler.Core.Translation.FromInternal.Data.Context
+import Juvix.Compiler.Core.Translation.FromInternal.Data.IndexTable
--- a/src/Juvix/Compiler/Core/Translation/FromInternal/Data/Context.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal/Data/Context.hs
@ -0,0 +1,12 @@
+module Juvix.Compiler.Core.Translation.FromInternal.Data.Context where
+
+import Juvix.Compiler.Core.Data.InfoTable qualified as Core
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal
+import Juvix.Prelude
+
+data CoreResult = CoreResult
+  { _coreResultTable :: Core.InfoTable,
+    _coreResultInternalTypedResult :: Internal.InternalTypedResult
+  }
+
+makeLenses ''CoreResult
--- a/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs
@ -0,0 +1,13 @@
+module Juvix.Compiler.Core.Translation.FromInternal.Data.IndexTable where
+
+import Juvix.Compiler.Core.Language
+
+data IndexTable = IndexTable
+  { _indexTableVarsNum :: Index,
+    _indexTableVars :: HashMap NameId Index
+  }
+
+makeLenses ''IndexTable
+
+initIndexTable :: IndexTable
+initIndexTable = IndexTable 0 mempty
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@ -18,6 +18,7 @@ import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo as NameInfo
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Transformation.Eta
+import Juvix.Compiler.Core.Translation.Base
 import Juvix.Compiler.Core.Translation.FromSource.Lexer
 import Juvix.Parser.Error
 import Text.Megaparsec qualified as P
@ -31,29 +32,12 @@ parseText = runParser ""
 runParser :: FilePath -> InfoTable -> Text -> Either ParserError (InfoTable, Maybe Node)
 runParser fileName tab input =
  case run $
-    runInfoTableBuilder tab $
+    runInfoTableBuilder (^. nameText) tab $
      runNameIdGen $
        P.runParserT parseToplevel fileName input of
    (_, Left err) -> Left (ParserError err)
    (tbl, Right r) -> Right (tbl, r)

-freshName ::
-  Member NameIdGen r =>
-  NameKind ->
-  Text ->
-  Interval ->
-  Sem r Name
-freshName kind txt i = do
-  nid <- freshNameId
-  return $
-    Name
-      { _nameText = txt,
-        _nameId = nid,
-        _nameKind = kind,
-        _namePretty = txt,
-        _nameLoc = i
-      }
-
 guardSymbolNotDefined ::
  Member InfoTableBuilder r =>
  Symbol ->
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@ -190,6 +190,11 @@ instance HasExpressions Expression where
    ExpressionUniverse {} -> f e
    ExpressionHole {} -> f e

+instance HasExpressions TypedExpression where
+  leafExpressions f t@TypedExpression {..} = do
+    e' <- leafExpressions f _typedExpression
+    pure (t {_typedExpression = e'})
+
 instance HasExpressions SimpleLambda where
  leafExpressions f (SimpleLambda v ty b) = do
    b' <- leafExpressions f b
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@ -225,6 +225,7 @@ makeLenses ''TypedExpression
 makeLenses ''Function
 makeLenses ''SimpleLambda
 makeLenses ''Lambda
+makeLenses ''LambdaClause
 makeLenses ''FunctionParameter
 makeLenses ''InductiveParameter
 makeLenses ''InductiveConstructorDef
--- a/src/Juvix/Compiler/Internal/Pretty.hs
+++ b/src/Juvix/Compiler/Internal/Pretty.hs
@ -20,3 +20,6 @@ ppOut o = AnsiText . PPOutput . doc (project o)

 ppTrace :: PrettyCode c => c -> Text
 ppTrace = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc traceOptions
+
+ppPrint :: PrettyCode c => c -> Text
+ppPrint = show . ppOutDefault
--- a/src/Juvix/Compiler/Internal/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs
@ -304,10 +304,13 @@ ppCodeAtom c = do
  p' <- ppCode c
  return $ if isAtomic c then p' else parens p'

-instance PrettyCode a => PrettyCode (NonEmpty a) where
+instance PrettyCode a => PrettyCode [a] where
  ppCode x = do
    cs <- mapM ppCode (toList x)
    return $ encloseSep "(" ")" ", " cs

+instance PrettyCode a => PrettyCode (NonEmpty a) where
+  ppCode x = ppCode (toList x)
+
 instance PrettyCode ConcreteType where
  ppCode ConcreteType {..} = ppCode _unconcreteType
--- a/src/Juvix/Compiler/Internal/Pretty/Options.hs
+++ b/src/Juvix/Compiler/Internal/Pretty/Options.hs
@ -22,3 +22,6 @@ makeLenses ''Options

 fromGenericOptions :: GenericOptions -> Options
 fromGenericOptions GenericOptions {..} = Options {_optShowNameIds = _showNameIds}
+
+instance CanonicalProjection GenericOptions Options where
+  project = fromGenericOptions
--- a/src/Juvix/Compiler/Internal/Translation/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Translation/Extra.hs
@ -0,0 +1,39 @@
+module Juvix.Compiler.Internal.Translation.Extra
+  ( module Juvix.Compiler.Internal.Translation,
+    module Juvix.Compiler.Internal.Translation.Extra,
+  )
+where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Internal.Extra
+import Juvix.Compiler.Internal.Translation
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
+import Juvix.Prelude
+
+unfoldPolyApplication :: Member (Reader TypesTable) r => Application -> Sem r (Expression, [Expression])
+unfoldPolyApplication a =
+  let (f, args) = unfoldApplication a
+   in case f of
+        ExpressionLiteral {} -> return (f, toList args)
+        ExpressionIden iden -> do
+          args' <- filterCompileTimeArgsOrPatterns (getName iden) (toList args)
+          return (f, args')
+        ExpressionSimpleLambda {} -> return (f, toList args)
+        ExpressionLambda {} -> return (f, toList args)
+        _ -> impossible
+
+filterCompileTimeArgsOrPatterns :: Member (Reader TypesTable) r => Name -> [a] -> Sem r [a]
+filterCompileTimeArgsOrPatterns idenName lst = do
+  tab <- ask
+  let funParams = fst (unfoldFunType (ty tab))
+      typedArgs =
+        map fst $
+          filter (not . isUniverse . snd) $
+            zip lst (map (^. paramType) funParams)
+  return $ typedArgs ++ drop (length funParams) lst
+  where
+    ty = HashMap.lookupDefault impossible idenName
+    isUniverse :: Expression -> Bool
+    isUniverse = \case
+      (ExpressionUniverse {}) -> True
+      _ -> False
--- a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs
@ -4,6 +4,7 @@ module Juvix.Compiler.Internal.Translation.FromAbstract
    TranslationState,
    iniState,
    fromAbstract,
+    fromAbstractExpression,
  )
 where

@ -70,6 +71,11 @@ fromAbstract abstractResults = do
        . E.entryPointNoTermination
    depInfo = buildDependencyInfo (abstractResults ^. Abstract.resultModules) (abstractResults ^. Abstract.resultExports)

+fromAbstractExpression ::
+  Abstract.Expression ->
+  Sem r Expression
+fromAbstractExpression = goExpression
+
 goModule ::
  Members '[Reader ExportsTable, State TranslationState] r =>
  Abstract.TopModule ->
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
@ -2,6 +2,9 @@ module Juvix.Compiler.Internal.Translation.FromInternal
  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability,
    arityChecking,
    typeChecking,
+    typeCheckExpression,
+    arityCheckExpression,
+    inferExpressionType,
  )
 where

@ -32,17 +35,61 @@ arityChecking res@InternalResult {..} =
    table :: InfoTable
    table = buildTable _resultModules

+arityCheckExpression ::
+  Members '[Error JuvixError, NameIdGen] r =>
+  InternalResult ->
+  Expression ->
+  Sem r Expression
+arityCheckExpression InternalResult {..} exp =
+  mapError (JuvixError @ArityChecking.ArityCheckerError) $
+    runReader table (ArityChecking.withEmptyLocalVars (ArityChecking.checkExpression ArityChecking.ArityUnknown exp))
+  where
+    table :: InfoTable
+    table = buildTable _resultModules
+
+typeCheckExpressionType ::
+  Members '[Error JuvixError, NameIdGen, Builtins] r =>
+  InternalTypedResult ->
+  Expression ->
+  Sem r TypedExpression
+typeCheckExpressionType (InternalTypedResult {..}) exp =
+  mapError (JuvixError @TypeCheckerError)
+    $ do
+      runReader _resultFunctions
+      . evalState _resultIdenTypes
+      . runReader table
+      . withEmptyVars
+      . runInferenceDef
+    $ inferExpression' Nothing exp
+  where
+    table :: InfoTable
+    table = buildTable _resultModules
+
+typeCheckExpression ::
+  Members '[Error JuvixError, NameIdGen, Builtins] r =>
+  InternalTypedResult ->
+  Expression ->
+  Sem r Expression
+typeCheckExpression res exp = fmap (^. typedExpression) (typeCheckExpressionType res exp)
+
+inferExpressionType ::
+  Members '[Error JuvixError, NameIdGen, Builtins] r =>
+  InternalTypedResult ->
+  Expression ->
+  Sem r Expression
+inferExpressionType res exp = fmap (^. typedType) (typeCheckExpressionType res exp)
+
 typeChecking ::
  Members '[Error JuvixError, NameIdGen, Builtins] r =>
  ArityChecking.InternalArityResult ->
  Sem r InternalTypedResult
 typeChecking res@ArityChecking.InternalArityResult {..} =
  mapError (JuvixError @TypeCheckerError) $ do
-    (normalized, (idens, r)) <-
+    (normalized, (idens, (funs, r))) <-
      runOutputList
        . runState (mempty :: TypesTable)
        . runReader entryPoint
-        . evalState (mempty :: FunctionsTable)
+        . runState (mempty :: FunctionsTable)
        . runReader table
        $ mapM checkModule _resultModules
    return
@ -50,7 +97,8 @@ typeChecking res@ArityChecking.InternalArityResult {..} =
        { _resultInternalArityResult = res,
          _resultModules = r,
          _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],
-          _resultIdenTypes = idens
+          _resultIdenTypes = idens,
+          _resultFunctions = funs
        }
  where
    table :: InfoTable
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@ -252,7 +252,7 @@ checkConstructorReturnType indType ctor = do
    )

 inferExpression ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Builtins, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins] r =>
  Maybe Expression -> -- type hint
  Expression ->
  Sem r Expression
@ -265,7 +265,7 @@ lookupVar v = HashMap.lookupDefault err v <$> asks (^. localTypes)

 checkFunctionClause ::
  forall r.
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Builtins, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Builtins] r =>
  Expression ->
  FunctionClause ->
  Sem r FunctionClause
@ -280,7 +280,7 @@ checkFunctionClause clauseType FunctionClause {..} = do
 -- | helper function for function clauses and lambda functions
 checkClause ::
  forall r.
-  Members '[Reader InfoTable, Reader FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Builtins, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins] r =>
  -- | Type
  Expression ->
  -- | Arguments
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs
@ -8,6 +8,7 @@ import Juvix.Compiler.Internal.Data.InfoTable
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context (InternalArityResult)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as Arity
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable
 import Juvix.Compiler.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude

@ -19,7 +20,8 @@ data InternalTypedResult = InternalTypedResult
  { _resultInternalArityResult :: InternalArityResult,
    _resultModules :: NonEmpty Module,
    _resultNormalized :: NormalizedTable,
-    _resultIdenTypes :: TypesTable
+    _resultIdenTypes :: TypesTable,
+    _resultFunctions :: FunctionsTable
  }

 makeLenses ''InternalTypedResult
--- a/src/Juvix/Compiler/Pipeline.hs
+++ b/src/Juvix/Compiler/Pipeline.hs
@ -1,6 +1,7 @@
 module Juvix.Compiler.Pipeline
  ( module Juvix.Compiler.Pipeline,
    module Juvix.Compiler.Pipeline.EntryPoint,
+    module Juvix.Compiler.Pipeline.ExpressionContext,
  )
 where

@ -10,13 +11,76 @@ import Juvix.Compiler.Builtins
 import Juvix.Compiler.Concrete qualified as Concrete
 import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
+import Juvix.Compiler.Core.Language qualified as Core
+import Juvix.Compiler.Core.Translation qualified as Core
 import Juvix.Compiler.Internal qualified as Internal
 import Juvix.Compiler.Pipeline.EntryPoint
+import Juvix.Compiler.Pipeline.ExpressionContext
 import Juvix.Compiler.Pipeline.Setup
 import Juvix.Prelude

 type PipelineEff = '[Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, Embed IO]

+arityCheckExpression ::
+  Members '[Error JuvixError, NameIdGen, Builtins] r =>
+  FilePath ->
+  ExpressionContext ->
+  Text ->
+  Sem r Internal.Expression
+arityCheckExpression fp ctx txt =
+  Parser.expressionFromTextSource fp txt
+    >>= Scoper.scopeCheckExpression (ctx ^. contextScoperTable) (mainModuleScope ctx)
+    >>= Abstract.fromConcreteExpression
+    >>= Internal.fromAbstractExpression
+    >>= Internal.arityCheckExpression (ctx ^. contextInternalResult)
+
+inferExpression ::
+  Members '[Error JuvixError, NameIdGen, Builtins] r =>
+  FilePath ->
+  ExpressionContext ->
+  Text ->
+  Sem r Internal.Expression
+inferExpression fp ctx txt =
+  arityCheckExpression fp ctx txt
+    >>= Internal.inferExpressionType (ctx ^. contextInternalTypedResult)
+
+compileExpression ::
+  Members '[Error JuvixError, NameIdGen, Builtins] r =>
+  FilePath ->
+  ExpressionContext ->
+  Text ->
+  Sem r Core.Node
+compileExpression fp ctx txt =
+  arityCheckExpression fp ctx txt
+    >>= Internal.typeCheckExpression (ctx ^. contextInternalTypedResult)
+    >>= Core.fromInternalExpression (ctx ^. contextCoreResult)
+
+compileExpressionIO ::
+  FilePath ->
+  ExpressionContext ->
+  BuiltinsState ->
+  Text ->
+  IO (Either JuvixError Core.Node)
+compileExpressionIO fp ctx builtinsState txt =
+  runM
+    . runError
+    . runNameIdGen
+    . (fmap snd . runBuiltins builtinsState)
+    $ compileExpression fp ctx txt
+
+inferExpressionIO ::
+  FilePath ->
+  ExpressionContext ->
+  BuiltinsState ->
+  Text ->
+  IO (Either JuvixError Internal.Expression)
+inferExpressionIO fp ctx builtinsState txt =
+  runM
+    . runError
+    . runNameIdGen
+    . (fmap snd . runBuiltins builtinsState)
+    $ inferExpression fp ctx txt
+
 --------------------------------------------------------------------------------
 -- Workflows
 --------------------------------------------------------------------------------
@ -65,38 +129,44 @@ upToInternalArity ::
 upToInternalArity = upToInternal >>= Internal.arityChecking

 upToInternalTyped ::
-  Members '[Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError] r =>
+  Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins] r =>
  Sem r Internal.InternalTypedResult
 upToInternalTyped = upToInternalArity >>= Internal.typeChecking

 upToInternalReachability ::
-  Members '[Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError] r =>
+  Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins] r =>
  Sem r Internal.InternalTypedResult
 upToInternalReachability =
  Internal.filterUnreachable <$> upToInternalTyped

+upToCore ::
+  Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins] r =>
+  Sem r Core.CoreResult
+upToCore =
+  upToInternalReachability >>= Core.fromInternal
+
 upToMiniC ::
-  Members '[Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError] r =>
+  Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins] r =>
  Sem r C.MiniCResult
 upToMiniC = upToInternalReachability >>= C.fromInternal

-runIOEither :: EntryPoint -> Sem PipelineEff a -> IO (Either JuvixError a)
-runIOEither entry =
+runIOEither :: forall a. BuiltinsState -> EntryPoint -> Sem PipelineEff a -> IO (Either JuvixError (BuiltinsState, a))
+runIOEither builtinsState entry =
  runM
    . runError
-    . runBuiltins
+    . runBuiltins builtinsState
    . runNameIdGen
    . mapError (JuvixError @FilesError)
    . runFilesIO (entry ^. entryPointRoot)
    . runReader entry

-runIO :: GenericOptions -> EntryPoint -> Sem PipelineEff a -> IO a
-runIO opts entry = runIOEither entry >=> mayThrow
+runIO :: BuiltinsState -> GenericOptions -> EntryPoint -> Sem PipelineEff a -> IO (BuiltinsState, a)
+runIO builtinsState opts entry = runIOEither builtinsState entry >=> mayThrow
  where
    mayThrow :: Either JuvixError r -> IO r
    mayThrow = \case
      Left err -> runM $ runReader opts $ printErrorAnsiSafe err >> embed exitFailure
      Right r -> return r

-runIO' :: EntryPoint -> Sem PipelineEff a -> IO a
-runIO' = runIO defaultGenericOptions
+runIO' :: BuiltinsState -> EntryPoint -> Sem PipelineEff a -> IO (BuiltinsState, a)
+runIO' builtinsState = runIO builtinsState defaultGenericOptions
--- a/src/Juvix/Compiler/Pipeline/ExpressionContext.hs
+++ b/src/Juvix/Compiler/Pipeline/ExpressionContext.hs
@ -0,0 +1,55 @@
+module Juvix.Compiler.Pipeline.ExpressionContext where
+
+import Juvix.Compiler.Abstract.Translation qualified as Abstract
+import Juvix.Compiler.Concrete.Data.InfoTable qualified as Scoper
+import Juvix.Compiler.Concrete.Data.Scope qualified as S
+import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
+import Juvix.Compiler.Concrete.Language qualified as C
+import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Scoper
+import Juvix.Compiler.Core qualified as Core
+import Juvix.Compiler.Internal qualified as Internal
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as InternalTyped
+import Juvix.Prelude
+
+data ExpressionContext = ExpressionContext
+  { _contextInternalTypedResult :: InternalTyped.InternalTypedResult,
+    _contextInternalResult :: Internal.InternalResult,
+    _contextScoperResult :: Scoper.ScoperResult,
+    _contextScoperTable :: Scoper.InfoTable,
+    _contextCoreResult :: Core.CoreResult
+  }
+
+expressionContext :: Core.CoreResult -> ExpressionContext
+expressionContext _contextCoreResult = ExpressionContext {..}
+  where
+    _contextInternalTypedResult :: InternalTyped.InternalTypedResult
+    _contextInternalTypedResult = _contextCoreResult ^. Core.coreResultInternalTypedResult
+
+    _contextInternalResult :: Internal.InternalResult
+    _contextInternalResult =
+      _contextInternalTypedResult
+        ^. InternalTyped.resultInternalArityResult
+        . InternalArity.resultInternalResult
+
+    _contextScoperResult :: Scoper.ScoperResult
+    _contextScoperResult =
+      _contextInternalResult
+        ^. Internal.resultAbstract
+        . Abstract.resultScoper
+
+    _contextScoperTable :: Scoper.InfoTable
+    _contextScoperTable =
+      _contextScoperResult
+        ^. Scoper.resultScoperTable
+
+makeLenses ''ExpressionContext
+
+moduleScope :: ExpressionContext -> C.TopModulePath -> Maybe S.Scope
+moduleScope e p = e ^. contextScoperResult ^?! Scoper.resultScope . at p
+
+mainModuleScope :: ExpressionContext -> S.Scope
+mainModuleScope e = fromJust (moduleScope e mainModulePath)
+  where
+    mainModulePath :: C.TopModulePath
+    mainModulePath = e ^. contextScoperResult . Scoper.mainModule . C.modulePath . S.nameConcrete
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@ -92,9 +92,18 @@ string = "string"
 nat :: IsString s => s
 nat = "nat"

+stringPrint :: IsString s => s
+stringPrint = "string-print"
+
 bool_ :: IsString s => s
 bool_ = "bool"

+boolean_ :: IsString s => s
+boolean_ = "boolean"
+
+boolPrint :: IsString s => s
+boolPrint = "bool-print"
+
 io :: IsString s => s
 io = "IO"

--- a/test/Arity/Negative.hs
+++ b/test/Arity/Negative.hs
@ -1,6 +1,7 @@
 module Arity.Negative (allTests) where

 import Base
+import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error
 import Juvix.Compiler.Pipeline

@ -21,7 +22,7 @@ testDescr NegTest {..} =
          _testRoot = tRoot,
          _testAssertion = Single $ do
            let entryPoint = defaultEntryPoint _file
-            result <- runIOEither entryPoint upToInternalArity
+            result <- runIOEither iniState entryPoint upToInternalArity
            case mapLeft fromJuvixError result of
              Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure
              Left Nothing -> assertFailure "The arity checker did not find an error."
--- a/test/BackendC/Base.hs
+++ b/test/BackendC/Base.hs
@ -4,6 +4,7 @@ import Base
 import Data.FileEmbed
 import Data.Text.IO qualified as TIO
 import Juvix.Compiler.Backend.C.Translation.FromInternal as MiniC
+import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Pipeline
 import System.IO.Extra (withTempDir)
 import System.Process qualified as P
@ -32,7 +33,7 @@ wasmClangAssertionCGenOnly :: FilePath -> ((String -> IO ()) -> Assertion)
 wasmClangAssertionCGenOnly mainFile step = do
  step "C Generation"
  let entryPoint = defaultEntryPoint mainFile
-  (void . runIO' entryPoint) upToMiniC
+  (void . runIO' iniState entryPoint) upToMiniC

 wasmClangAssertion :: WASMInfo -> FilePath -> FilePath -> ((String -> IO ()) -> Assertion)
 wasmClangAssertion WASMInfo {..} mainFile expectedFile step = do
@ -42,7 +43,7 @@ wasmClangAssertion WASMInfo {..} mainFile expectedFile step = do

  step "C Generation"
  let entryPoint = defaultEntryPoint mainFile
-  p :: MiniC.MiniCResult <- runIO' entryPoint upToMiniC
+  p :: MiniC.MiniCResult <- snd <$> runIO' iniState entryPoint upToMiniC

  expected <- TIO.readFile expectedFile

@ -65,7 +66,7 @@ wasiClangAssertion stdlibMode mainFile expectedFile stdinText step = do

  step "C Generation"
  let entryPoint = (defaultEntryPoint mainFile) {_entryPointNoStdlib = stdlibMode == StdlibExclude}
-  p :: MiniC.MiniCResult <- runIO' entryPoint upToMiniC
+  p :: MiniC.MiniCResult <- snd <$> runIO' iniState entryPoint upToMiniC

  expected <- TIO.readFile expectedFile

--- a/test/Internal.hs
+++ b/test/Internal.hs
@ -0,0 +1,7 @@
+module Internal where
+
+import Base
+import Internal.Eval qualified as Eval
+
+allTests :: TestTree
+allTests = testGroup "Internal to Core tests" [Eval.allTests]
--- a/test/Internal/Eval.hs
+++ b/test/Internal/Eval.hs
@ -0,0 +1,7 @@
+module Internal.Eval where
+
+import Base
+import Internal.Eval.Positive qualified as EvalP
+
+allTests :: TestTree
+allTests = testGroup "Internal to Core eval" [EvalP.allTests]
--- a/test/Internal/Eval/Base.hs
+++ b/test/Internal/Eval/Base.hs
@ -0,0 +1,44 @@
+module Internal.Eval.Base where
+
+import Base
+import Core.Eval.Base
+import Data.HashMap.Strict qualified as HashMap
+import Data.Text.IO qualified as TIO
+import Juvix.Compiler.Builtins (iniState)
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NoDisplayInfo
+import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Translation.FromInternal.Data as Core
+import Juvix.Compiler.Pipeline
+import System.IO.Extra (withTempDir)
+
+internalCoreAssertion :: FilePath -> FilePath -> (String -> IO ()) -> Assertion
+internalCoreAssertion mainFile expectedFile step = do
+  step "Translate to Core"
+  let entryPoint = defaultEntryPoint mainFile
+  tab <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
+  case (tab ^. infoMain) >>= ((tab ^. identContext) HashMap.!?) of
+    Just node -> do
+      withTempDir
+        ( \dirPath -> do
+            let outputFile = dirPath </> "out.out"
+            hout <- openFile outputFile WriteMode
+            step "Evaluate"
+            r' <- doEval mainFile hout tab node
+            case r' of
+              Left err -> do
+                hClose hout
+                assertFailure (show (pretty err))
+              Right value -> do
+                unless
+                  (Info.member kNoDisplayInfo (getInfo value))
+                  (hPutStrLn hout (ppPrint value))
+                hClose hout
+                actualOutput <- TIO.readFile outputFile
+                step "Compare expected and actual program output"
+                expected <- TIO.readFile expectedFile
+                assertEqDiff ("Check: EVAL output = " <> expectedFile) actualOutput expected
+        )
+    Nothing -> assertFailure ("No main function registered in: " <> mainFile)
--- a/test/Internal/Eval/Positive.hs
+++ b/test/Internal/Eval/Positive.hs
@ -0,0 +1,145 @@
+module Internal.Eval.Positive where
+
+import Base
+import Internal.Eval.Base
+
+data PosTest = PosTest
+  { _name :: String,
+    _relDir :: FilePath,
+    _file :: FilePath,
+    _expectedFile :: FilePath
+  }
+
+root :: FilePath
+root = "tests/Internal/positive"
+
+coreRoot :: FilePath
+coreRoot = "tests/Internal/Core/positive"
+
+testDescr :: FilePath -> PosTest -> TestDescr
+testDescr r PosTest {..} =
+  let tRoot = r </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ internalCoreAssertion _file _expectedFile
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Internal to Core positive tests"
+    (map (mkTest . testDescr root) tests ++ map (mkTest . testDescr coreRoot) coreTests)
+
+coreTests :: [PosTest]
+coreTests =
+  [ PosTest
+      "If then else"
+      "."
+      "test006.juvix"
+      "out/test006.out",
+    PosTest
+      "Fibonacci"
+      "."
+      "test011.juvix"
+      "out/test011.out"
+  ]
+
+tests :: [PosTest]
+tests =
+  [ PosTest
+      "An integer literal"
+      "."
+      "IntegerLiteral.juvix"
+      "out/IntegerLiteral.out",
+    PosTest
+      "A zero argument function"
+      "."
+      "IdenFunctionIntegerLiteral.juvix"
+      "out/IdenFunctionIntegerLiteral.out",
+    PosTest
+      "A two argument function"
+      "."
+      "IdenFunctionArgs.juvix"
+      "out/IdenFunctionArgs.out",
+    PosTest
+      "A function with implicit arguments"
+      "."
+      "IdenFunctionArgsImplicit.juvix"
+      "out/IdenFunctionArgsImplicit.out",
+    PosTest
+      "A function with no explicit arguments"
+      "."
+      "IdenFunctionArgsNoExplicit.juvix"
+      "out/IdenFunctionArgsNoExplicit.out",
+    PosTest
+      "A module that imports another"
+      "Import"
+      "Importer.juvix"
+      "out/Importer.out",
+    PosTest
+      "A constructor valued function"
+      "."
+      "FunctionReturnConstructor.juvix"
+      "out/FunctionReturnConstructor.out",
+    PosTest
+      "Pattern matching on a constructor"
+      "."
+      "MatchConstructor.juvix"
+      "out/MatchConstructor.out",
+    PosTest
+      "Pattern matching Nat under suc"
+      "."
+      "NatMatch1.juvix"
+      "out/NatMatch1.out",
+    PosTest
+      "Pattern matching Nat as binder"
+      "."
+      "NatMatch2.juvix"
+      "out/NatMatch2.out",
+    PosTest
+      "Literal integer is Core integer"
+      "."
+      "LitInteger.juvix"
+      "out/LitInteger.out",
+    PosTest
+      "Literal integer is Core string"
+      "."
+      "LitString.juvix"
+      "out/LitString.out",
+    PosTest
+      "Mutually defined functions"
+      "."
+      "Mutual.juvix"
+      "out/Mutual.out",
+    PosTest
+      "Calling builtin addition"
+      "."
+      "BuiltinAdd.juvix"
+      "out/BuiltinAdd.out",
+    PosTest
+      "Builtin bool"
+      "."
+      "BuiltinBool.juvix"
+      "out/BuiltinBool.out",
+    PosTest
+      "Builtin if"
+      "."
+      "BuiltinIf.juvix"
+      "out/BuiltinIf.out",
+    PosTest
+      "Lambda"
+      "."
+      "Lambda.juvix"
+      "out/Lambda.out",
+    PosTest
+      "Pattern args"
+      "."
+      "PatternArgs.juvix"
+      "out/PatternArgs.out",
+    PosTest
+      "QuickSort"
+      "."
+      "QuickSort.juvix"
+      "out/QuickSort.out"
+  ]
--- a/test/Main.hs
+++ b/test/Main.hs
@ -5,6 +5,7 @@ import Asm qualified
 import BackendC qualified
 import Base
 import Core qualified
+import Internal qualified
 import Parsing qualified
 import Reachability qualified
 import Runtime qualified
@ -19,6 +20,7 @@ slowTests =
    [ BackendC.allTests,
      Core.allTests,
      Asm.allTests,
+      Internal.allTests,
      Runtime.allTests
    ]

--- a/test/Parsing/Negative.hs
+++ b/test/Parsing/Negative.hs
@ -1,6 +1,7 @@
 module Parsing.Negative where

 import Base
+import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Pipeline
 import Juvix.Parser.Error

@ -21,7 +22,7 @@ testDescr NegTest {..} =
          _testRoot = tRoot,
          _testAssertion = Single $ do
            let entryPoint = defaultEntryPoint _file
-            res <- runIOEither entryPoint upToParsing
+            res <- runIOEither iniState entryPoint upToParsing
            case mapLeft fromJuvixError res of
              Left (Just (_ :: ParserError)) -> return ()
              Left Nothing -> assertFailure "The parser did not find an error."
--- a/test/Reachability/Positive.hs
+++ b/test/Reachability/Positive.hs
@ -2,6 +2,7 @@ module Reachability.Positive where

 import Base
 import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Internal.Language qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal
 import Juvix.Compiler.Pipeline
@ -36,7 +37,7 @@ testDescr PosTest {..} =
                    }

            step "Pipeline up to reachability"
-            p :: Internal.InternalTypedResult <- runIO' entryPoint upToInternalReachability
+            p :: Internal.InternalTypedResult <- snd <$> runIO' iniState entryPoint upToInternalReachability

            step "Check reachability results"
            let names = concatMap getNames (p ^. Internal.resultModules)
--- a/test/Scope/Negative.hs
+++ b/test/Scope/Negative.hs
@ -1,6 +1,7 @@
 module Scope.Negative (allTests) where

 import Base
+import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
 import Juvix.Compiler.Pipeline

@ -24,7 +25,7 @@ testDescr NegTest {..} =
          _testRoot = tRoot,
          _testAssertion = Single $ do
            let entryPoint = defaultEntryPoint _file
-            res <- runIOEither entryPoint upToAbstract
+            res <- runIOEither iniState entryPoint upToAbstract
            case mapLeft fromJuvixError res of
              Left (Just err) -> whenJust (_checkErr err) assertFailure
              Left Nothing -> assertFailure "The scope checker did not find an error."
--- a/test/Scope/Positive.hs
+++ b/test/Scope/Positive.hs
@ -2,6 +2,7 @@ module Scope.Positive where

 import Base
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Concrete qualified as Concrete
 import Juvix.Compiler.Concrete.Extra
 import Juvix.Compiler.Concrete.Pretty qualified as M
@ -50,18 +51,20 @@ testDescr PosTest {..} =
                  | otherwise = HashMap.union fs stdlibMap

            step "Parsing"
-            p :: Parser.ParserResult <- runIO' entryPoint upToParsing
+            p :: Parser.ParserResult <- snd <$> runIO' iniState entryPoint upToParsing

            let p2 = head (p ^. Parser.resultModules)

            step "Scoping"
            s :: Scoper.ScoperResult <-
-              runIO'
-                entryPoint
-                ( do
-                    void entrySetup
-                    Concrete.fromParsed p
-                )
+              snd
+                <$> runIO'
+                  iniState
+                  entryPoint
+                  ( do
+                      void entrySetup
+                      Concrete.fromParsed p
+                  )

            let s2 = head (s ^. Scoper.resultModules)

--- a/test/Termination/Negative.hs
+++ b/test/Termination/Negative.hs
@ -1,6 +1,7 @@
 module Termination.Negative (module Termination.Negative) where

 import Base
+import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination
 import Juvix.Compiler.Pipeline

@ -21,7 +22,7 @@ testDescr NegTest {..} =
          _testRoot = tRoot,
          _testAssertion = Single $ do
            let entryPoint = (defaultEntryPoint _file) {_entryPointNoStdlib = True}
-            result <- runIOEither entryPoint upToInternal
+            result <- runIOEither iniState entryPoint upToInternal
            case mapLeft fromJuvixError result of
              Left (Just lexError) -> whenJust (_checkErr lexError) assertFailure
              Left Nothing -> assertFailure "The termination checker did not find an error."
--- a/test/Termination/Positive.hs
+++ b/test/Termination/Positive.hs
@ -1,6 +1,7 @@
 module Termination.Positive where

 import Base
+import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Pipeline
 import Termination.Negative qualified as N

@ -21,7 +22,7 @@ testDescr PosTest {..} =
          _testRoot = tRoot,
          _testAssertion = Single $ do
            let entryPoint = (defaultEntryPoint _file) {_entryPointNoStdlib = True}
-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' iniState entryPoint) upToInternal
        }

 --------------------------------------------------------------------------------
@ -45,7 +46,7 @@ testDescrFlag N.NegTest {..} =
                      _entryPointNoStdlib = True
                    }

-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' iniState entryPoint) upToInternal
        }

 --------------------------------------------------------------------------------
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@ -1,6 +1,7 @@
 module Typecheck.Negative where

 import Base
+import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 import Juvix.Compiler.Pipeline

@ -21,7 +22,7 @@ testDescr NegTest {..} =
          _testRoot = tRoot,
          _testAssertion = Single $ do
            let entryPoint = defaultEntryPoint _file
-            result <- runIOEither entryPoint upToInternalTyped
+            result <- runIOEither iniState entryPoint upToInternalTyped
            case mapLeft fromJuvixError result of
              Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure
              Left Nothing -> assertFailure "The type checker did not find an error."
--- a/test/Typecheck/Positive.hs
+++ b/test/Typecheck/Positive.hs
@ -1,6 +1,7 @@
 module Typecheck.Positive where

 import Base
+import Juvix.Compiler.Builtins (iniState)
 import Juvix.Compiler.Pipeline
 import Typecheck.Negative qualified as N

@ -21,7 +22,7 @@ testDescr PosTest {..} =
          _testRoot = tRoot,
          _testAssertion = Single $ do
            let entryPoint = defaultEntryPoint _file
-            (void . runIO' entryPoint) upToInternalTyped
+            (void . runIO' iniState entryPoint) upToInternalTyped
        }

 --------------------------------------------------------------------------------
@ -43,7 +44,7 @@ testNoPositivityFlag N.NegTest {..} =
                    { _entryPointNoPositivity = True
                    }

-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' iniState entryPoint) upToInternal
        }

 negPositivityTests :: [N.NegTest]
--- a/tests/Internal/Core/positive/juvix.yaml
+++ b/tests/Internal/Core/positive/juvix.yaml
--- a/tests/Internal/Core/positive/out/test006.out
+++ b/tests/Internal/Core/positive/out/test006.out
@ -0,0 +1 @@
+suc (suc zero)
--- a/tests/Internal/Core/positive/out/test011.out
+++ b/tests/Internal/Core/positive/out/test011.out
@ -0,0 +1 @@
+suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))))))))))))))))))))))))
--- a/tests/Internal/Core/positive/test006.juvix
+++ b/tests/Internal/Core/positive/test006.juvix
@ -0,0 +1,16 @@
+module test006;
+
+open import Stdlib.Prelude public;
+open import Stdlib.Data.Nat.Ord public;
+
+terminating
+loop : Nat;
+loop := loop;
+
+e : Nat;
+e := (if (three > zero) one loop) + (if (two < one) loop (if (seven >= eight) loop one));
+
+main : IO;
+main := printNatLn e;
+
+end;
--- a/tests/Internal/Core/positive/test011.juvix
+++ b/tests/Internal/Core/positive/test011.juvix
@ -0,0 +1,17 @@
+module test011;
+
+open import Stdlib.Prelude public;
+
+open import Stdlib.Data.Nat.Ord public;
+
+fib' : Nat -> Nat -> Nat -> Nat;
+fib' zero x _ := x;
+fib' (suc n) x y := fib' n y (x + y);
+
+fib : Nat -> Nat;
+fib n := fib' n zero one;
+
+main : IO;
+main := printNatLn (fib nine);
+
+end;
--- a/tests/Internal/positive/BuiltinAdd.juvix
+++ b/tests/Internal/positive/BuiltinAdd.juvix
@ -0,0 +1,14 @@
+module BuiltinAdd;
+
+open import Stdlib.Prelude;
+
+n : Nat;
+n := (suc (suc zero));
+
+m : Nat;
+m := (suc zero);
+
+main : Nat;
+main := m + n;
+
+end;
--- a/tests/Internal/positive/BuiltinBool.juvix
+++ b/tests/Internal/positive/BuiltinBool.juvix
@ -0,0 +1,8 @@
+module BuiltinBool;
+
+open import Stdlib.Prelude;
+
+main : Bool;
+main := true || false;
+
+end;
--- a/tests/Internal/positive/BuiltinIf.juvix
+++ b/tests/Internal/positive/BuiltinIf.juvix
@ -0,0 +1,8 @@
+module BuiltinIf;
+
+open import Stdlib.Prelude;
+
+main : Bool;
+main := if false ((&&) false) ((&&) true) true;
+
+end;
--- a/tests/Internal/positive/FunctionReturnConstructor.juvix
+++ b/tests/Internal/positive/FunctionReturnConstructor.juvix
@ -0,0 +1,10 @@
+module FunctionReturnConstructor;
+
+inductive Foo {
+  foo : Foo;
+};
+
+main : Foo;
+main := foo;
+
+end;
--- a/tests/Internal/positive/IdenFunctionArgs.juvix
+++ b/tests/Internal/positive/IdenFunctionArgs.juvix
@ -0,0 +1,11 @@
+module IdenFunctionArgs;
+
+open import Stdlib.Prelude;
+
+f : Nat → Nat → Nat;
+f x y := x;
+
+main : Nat;
+main := f 100 200;
+
+end;
--- a/tests/Internal/positive/IdenFunctionArgsImplicit.juvix
+++ b/tests/Internal/positive/IdenFunctionArgsImplicit.juvix
@ -0,0 +1,11 @@
+module IdenFunctionArgsImplicit;
+
+open import Stdlib.Prelude;
+
+f : {A : Type} → Nat → A → Nat;
+f x y := x;
+
+main : Nat;
+main := f 100 200;
+
+end;
--- a/tests/Internal/positive/IdenFunctionArgsNoExplicit.juvix
+++ b/tests/Internal/positive/IdenFunctionArgsNoExplicit.juvix
@ -0,0 +1,11 @@
+module IdenFunctionArgsNoExplicit;
+
+open import Stdlib.Prelude;
+
+f : {A : Type} → Nat;
+f := zero;
+
+main : Nat;
+main := f;
+
+end;
--- a/tests/Internal/positive/IdenFunctionIntegerLiteral.juvix
+++ b/tests/Internal/positive/IdenFunctionIntegerLiteral.juvix
@ -0,0 +1,11 @@
+module IdenFunctionIntegerLiteral;
+
+open import Stdlib.Prelude;
+
+f : Nat;
+f := 1;
+
+main : Nat;
+main := f;
+
+end;
--- a/tests/Internal/positive/Import/Importee.juvix
+++ b/tests/Internal/positive/Import/Importee.juvix
@ -0,0 +1,8 @@
+module Importee;
+
+open import Stdlib.Prelude;
+
+f : Nat;
+f := 1;
+
+end;
--- a/tests/Internal/positive/Import/Importer.juvix
+++ b/tests/Internal/positive/Import/Importer.juvix
@ -0,0 +1,9 @@
+module Importer;
+
+open import Stdlib.Prelude;
+open import Importee;
+
+main : Nat;
+main := f;
+
+end;
--- a/tests/Internal/positive/Import/juvix.yaml
+++ b/tests/Internal/positive/Import/juvix.yaml
--- a/tests/Internal/positive/Import/out/Importer.out
+++ b/tests/Internal/positive/Import/out/Importer.out
@ -0,0 +1 @@
+1
--- a/tests/Internal/positive/IntegerLiteral.juvix
+++ b/tests/Internal/positive/IntegerLiteral.juvix
@ -0,0 +1,8 @@
+module IntegerLiteral;
+
+open import Stdlib.Prelude;
+
+main : Nat;
+main := 1;
+
+end;
--- a/tests/Internal/positive/Lambda.juvix
+++ b/tests/Internal/positive/Lambda.juvix
@ -0,0 +1,28 @@
+module Lambda;
+
+open import Stdlib.Prelude public;
+
+id' : {A : Type} → A → A;
+id' := λ { a := a };
+
+uncurry' : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A × B → C;
+uncurry' := λ {f (a, b) := f a b};
+
+fst' : {A : Type} → {B : Type} → A × B → A;
+fst' {_} := λ {(a, _) := a};
+
+first' : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × B;
+first' := λ {f (a, b) := f a, b};
+
+foldr' : {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
+foldr' := λ {_ z nil := z;
+             f z (h ∷ hs) := f h (foldr' f z hs)};
+
+main : IO;
+main := printNatLn (id' zero)
+        >> printNatLn (uncurry' (+) (one, one))
+        >> printNatLn (fst' (zero, one))
+        >> printNatLn (fst (first' ((+) one) (one, zero)))
+        >> printNatLn (foldr' (+) zero (one ∷ two ∷ three ∷ nil));
+
+end;
--- a/tests/Internal/positive/LitInteger.juvix
+++ b/tests/Internal/positive/LitInteger.juvix
@ -0,0 +1,14 @@
+module LitInteger;
+
+open import Stdlib.Prelude public;
+
+main : Nat;
+main := 1;
+
+nilNat : List Nat;
+nilNat := nil;
+
+cons : Nat -> List Nat -> List Nat;
+cons a xs := a ∷ xs;
+
+end;
--- a/tests/Internal/positive/LitString.juvix
+++ b/tests/Internal/positive/LitString.juvix
@ -0,0 +1,8 @@
+module LitString;
+
+open import Stdlib.Prelude;
+
+main : String;
+main := "hello";
+
+end;
--- a/Show More
+++ b/Show More
				`@ -0,0 +1 @@`
				`suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))))))))))))))))))))))))`