Support module imports in Juvix REPL (#2029)

This PR adds support for importing modules from within a Juvix project
in the Juvix REPL.

The imported module is checked (parsed, arity-checked, type-checked etc)
as normal and added to the REPL session scope. Any errors during the
checking phase is reported to the user.

### Notes:

* You must load a file before using `import`. This is because the REPL
needs to know which Juvix project is active.
* You may only import modules from within the same Juvix project. 

### Examples

After launching `juvix repl`:

#### `open import`

```
Stdlib.Prelude> open import Stdlib.Data.Int.Ord
Stdlib.Prelude> 1 == 1
true
```

#### `import as`

```
Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int
Stdlib.Prelude> 1 Int.== 1
true
```

#### `import`then `open`

```
Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int
Stdlib.Prelude> open Int
Stdlib.Prelude> 1 == 1
true
```

#### Line-terminating semicolons are ignored:

```
Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int;;;;;
Stdlib.Prelude> 1 Int.== 1
true
```

* Closes #1951

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>

app/Commands/Repl.hs

@@ -22,6 +22,7 @@ import Juvix.Compiler.Core.Transformation qualified as Core
 import Juvix.Compiler.Core.Transformation.DisambiguateNames (disambiguateNames)
 import Juvix.Compiler.Internal.Language qualified as Internal
 import Juvix.Compiler.Internal.Pretty qualified as Internal
+import Juvix.Compiler.Pipeline.Repl
 import Juvix.Compiler.Pipeline.Setup (entrySetup)
 import Juvix.Data.Error.GenericError qualified as Error
 import Juvix.Extra.Paths
@@ -157,20 +158,26 @@ runCommand opts = do
             evalRes <- compileThenEval ctx' input
             case evalRes of
               Left err -> printError err
-              Right n
+              Right (Just n)
                 | Info.member Info.kNoDisplayInfo (Core.getInfo n) -> return ()
-              Right n
+              Right (Just n)
                 | opts ^. replPrintValues ->
                     renderOut (Core.ppOut opts (toValue tab n))
                 | otherwise ->
                     renderOut (Core.ppOut opts n)
+              Right Nothing -> return ()
           Nothing -> noFileLoadedMsg
         where
           defaultLoc :: Interval
           defaultLoc = singletonInterval (mkInitialLoc replPath)
 
-          compileThenEval :: ReplContext -> String -> Repl (Either JuvixError Core.Node)
-          compileThenEval ctx s = bindEither compileString eval
+          compileThenEval :: ReplContext -> String -> Repl (Either JuvixError (Maybe Core.Node))
+          compileThenEval ctx s = do
+            mn <- compileString
+            case mn of
+              Left err -> return (Left err)
+              Right Nothing -> return (Right Nothing)
+              Right (Just n) -> fmap Just <$> eval n
             where
               artif :: Artifacts
               artif = ctx ^. replContextArtifacts
@@ -195,21 +202,22 @@ runCommand opts = do
                 mapLeft (JuvixError @Core.CoreError)
                   <$> doEvalIO False defaultLoc (artif' ^. artifactCoreTable) n
 
-              compileString :: Repl (Either JuvixError Core.Node)
-              compileString = liftIO $ compileExpressionIO' ctx (strip (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)
+              compileString :: Repl (Either JuvixError (Maybe Core.Node))
+              compileString = do
+                (artifacts, res) <- liftIO $ compileReplInputIO' ctx (strip (pack s))
+                State.modify (over (replStateContext . _Just) (set replContextArtifacts artifacts))
+                return res
 
       core :: String -> Repl ()
       core input = Repline.dontCrash $ do
         ctx <- State.gets (^. replStateContext)
         case ctx of
           Just ctx' -> do
-            compileRes <- liftIO (compileExpressionIO' ctx' (strip (pack input)))
+            compileRes <- snd <$> liftIO (compileReplInputIO' ctx' (strip (pack input)))
             case compileRes of
               Left err -> printError err
-              Right n -> renderOut (Core.ppOut opts n)
+              Right (Just n) -> renderOut (Core.ppOut opts n)
+              Right Nothing -> return ()
           Nothing -> noFileLoadedMsg
 
       inferType :: String -> Repl ()
@@ -337,13 +345,23 @@ inferExpressionIO' :: ReplContext -> Text -> IO (Either JuvixError Internal.Expr
 inferExpressionIO' ctx txt =
   runM
     . evalState (ctx ^. replContextArtifacts)
+    . runReader (ctx ^. replContextEntryPoint)
     $ inferExpressionIO replPath txt
 
-compileExpressionIO' :: ReplContext -> Text -> IO (Either JuvixError Core.Node)
-compileExpressionIO' ctx txt =
+compileReplInputIO' :: ReplContext -> Text -> IO (Artifacts, (Either JuvixError (Maybe Core.Node)))
+compileReplInputIO' ctx txt =
   runM
-    . evalState (ctx ^. replContextArtifacts)
-    $ compileExpressionIO replPath txt
+    . runState (ctx ^. replContextArtifacts)
+    . runReader (ctx ^. replContextEntryPoint)
+    $ do
+      r <- compileReplInputIO replPath txt
+      return (extractNode <$> r)
+  where
+    extractNode :: ReplPipelineResult -> Maybe Core.Node
+    extractNode = \case
+      ReplPipelineResultNode n -> Just n
+      ReplPipelineResultImport {} -> Nothing
+      ReplPipelineResultOpenImport {} -> Nothing
 
 render' :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl ()
 render' t = do

src/Juvix/Compiler/Abstract/Data/InfoTableBuilder.hs

@@ -64,5 +64,8 @@ toState = reinterpret $ \case
 runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
 runInfoTableBuilder = runState emptyInfoTable . toState
 
+runInfoTableBuilder' :: InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
+runInfoTableBuilder' t = runState t . toState
+
 ignoreInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r a
 ignoreInfoTableBuilder = fmap snd . runInfoTableBuilder

src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs

@@ -17,21 +17,16 @@ import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
 import Juvix.Data.NameKind
 import Juvix.Prelude
 
-newtype ModulesCache = ModulesCache
-  {_cachedModules :: HashMap S.NameId Abstract.TopModule}
-
-makeLenses ''ModulesCache
-
 unsupported :: Text -> a
 unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported"
 
 fromConcrete :: (Members '[Error JuvixError, Builtins, NameIdGen] r) => Scoper.ScoperResult -> Sem r AbstractResult
 fromConcrete _resultScoper =
   mapError (JuvixError @ScoperError) $ do
-    (_resultTable, _resultModules) <-
+    (_resultTable, (_resultModulesCache, _resultModules)) <-
       runInfoTableBuilder $
         runReader @Pragmas mempty $
-          evalState (ModulesCache mempty) $
+          runState (ModulesCache mempty) $
             mapM goTopModule ms
     let _resultExports = _resultScoper ^. Scoper.resultExports
     return AbstractResult {..}
@@ -41,6 +36,18 @@ fromConcrete _resultScoper =
 fromConcreteExpression :: (Members '[Error JuvixError, NameIdGen] r) => Scoper.Expression -> Sem r Abstract.Expression
 fromConcreteExpression = mapError (JuvixError @ScoperError) . ignoreInfoTableBuilder . runReader @Pragmas mempty . goExpression
 
+fromConcreteImport ::
+  Members '[Error JuvixError, NameIdGen, Builtins, InfoTableBuilder, State ModulesCache] r =>
+  Scoper.Import 'Scoped ->
+  Sem r Abstract.TopModule
+fromConcreteImport = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goImport
+
+fromConcreteOpenImport ::
+  Members '[Error JuvixError, NameIdGen, Builtins, InfoTableBuilder, State ModulesCache] r =>
+  Scoper.OpenModule 'Scoped ->
+  Sem r (Maybe Abstract.TopModule)
+fromConcreteOpenImport = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goOpenModule'
+
 goTopModule ::
   (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
   Module 'Scoped 'ModuleTop ->
@@ -146,6 +153,13 @@ goModuleBody ss' = do
         sigs :: [Indexed (TypeSignature 'Scoped)]
         sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss]
 
+goImport ::
+  forall r.
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache, Reader Pragmas] r) =>
+  Import 'Scoped ->
+  Sem r Abstract.TopModule
+goImport t = goModule (t ^. importModule . moduleRefModule)
+
 goStatement ::
   forall r.
   (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
@@ -154,28 +168,33 @@ goStatement ::
 goStatement (Indexed idx s) =
   fmap (Indexed idx) <$> case s of
     StatementAxiom d -> Just . Abstract.StatementAxiom <$> goAxiom d
-    StatementImport t -> Just . Abstract.StatementImport <$> goModule (t ^. importModule . moduleRefModule)
+    StatementImport t -> Just . Abstract.StatementImport <$> goImport t
     StatementOperator {} -> return Nothing
     StatementOpenModule o -> goOpenModule o
     StatementInductive i -> Just . Abstract.StatementInductive <$> goInductive i
     StatementModule f -> Just . Abstract.StatementLocalModule <$> goLocalModule f
     StatementTypeSignature {} -> return Nothing
     StatementFunctionClause {} -> return Nothing
 
-goOpenModule ::
+goOpenModule' ::
   forall r.
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache, Reader Pragmas] r) =>
   OpenModule 'Scoped ->
-  Sem r (Maybe Abstract.Statement)
-goOpenModule o
+  Sem r (Maybe Abstract.TopModule)
+goOpenModule' o
   | isJust (o ^. openModuleImportKw) =
       case o ^. openModuleName of
-        ModuleRef' (SModuleTop :&: m) ->
-          Just . Abstract.StatementImport
-            <$> goModule (m ^. moduleRefModule)
+        ModuleRef' (SModuleTop :&: m) -> Just <$> goModule (m ^. moduleRefModule)
         _ -> impossible
   | otherwise = return Nothing
 
+goOpenModule ::
+  forall r.
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
+  OpenModule 'Scoped ->
+  Sem r (Maybe Abstract.Statement)
+goOpenModule o = fmap Abstract.StatementImport <$> goOpenModule' o
+
 goLetFunctionDef ::
   (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError] r) =>
   TypeSignature 'Scoped ->

src/Juvix/Compiler/Abstract/Translation/FromConcrete/Data/Context.hs

@@ -6,19 +6,26 @@ where
 
 import Juvix.Compiler.Abstract.Data.InfoTable
 import Juvix.Compiler.Abstract.Language
+import Juvix.Compiler.Abstract.Language qualified as Abstract
+import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Concrete
 import Juvix.Compiler.Concrete.Translation.FromSource qualified as Concrete
 import Juvix.Compiler.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude
 
+newtype ModulesCache = ModulesCache
+  {_cachedModules :: HashMap S.NameId Abstract.TopModule}
+
 data AbstractResult = AbstractResult
   { _resultScoper :: Concrete.ScoperResult,
     _resultTable :: InfoTable,
     _resultModules :: NonEmpty TopModule,
-    _resultExports :: HashSet NameId
+    _resultExports :: HashSet NameId,
+    _resultModulesCache :: ModulesCache
   }
 
 makeLenses ''AbstractResult
+makeLenses ''ModulesCache
 
 abstractResultEntryPoint :: Lens' AbstractResult E.EntryPoint
 abstractResultEntryPoint = resultScoper . Concrete.resultParserResult . Concrete.resultEntry

src/Juvix/Compiler/Concrete/Data/ParsedInfoTableBuilder.hs

@@ -1,18 +1,4 @@
-module Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder
-  ( InfoTableBuilder,
-    registerLiteral,
-    registerDelimiter,
-    registerKeyword,
-    registerJudocText,
-    registerPragmas,
-    registerSpaceSpan,
-    registerModule,
-    moduleVisited,
-    visitModule,
-    runParserInfoTableBuilder,
-    module Juvix.Compiler.Concrete.Data.ParsedInfoTable,
-  )
-where
+module Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
@@ -108,10 +94,9 @@ build st =
 registerItem' :: Members '[State BuilderState] r => ParsedItem -> Sem r ()
 registerItem' i = modify' (over stateItems (i :))
 
-runParserInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
-runParserInfoTableBuilder =
-  fmap (first build)
-    . runState iniState
+runParserInfoTableBuilder' :: BuilderState -> Sem (InfoTableBuilder ': r) a -> Sem r (BuilderState, a)
+runParserInfoTableBuilder' s =
+  runState s
     . reinterpret
       ( \case
           ModuleVisited i -> HashSet.member i <$> gets (^. stateVisited)
@@ -129,3 +114,8 @@ runParserInfoTableBuilder =
                     _parsedTag = ParsedTagComment
                   }
       )
+
+runParserInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (BuilderState, InfoTable, a)
+runParserInfoTableBuilder m = do
+  (builderState, x) <- runParserInfoTableBuilder' iniState m
+  return (builderState, build builderState, x)

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -14,7 +14,6 @@ import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Concrete.Data.InfoTableBuilder
 import Juvix.Compiler.Concrete.Data.Name qualified as N
 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
@@ -58,25 +57,24 @@ scopeCheck pr modules =
           _resultScoperTable = st,
           _resultModules = ms,
           _resultExports = exp,
-          _resultScope = scoperSt ^. scoperScope
+          _resultScope = scoperSt ^. scoperScope,
+          _resultScoperState = scoperSt
         }
 
 scopeCheckExpression ::
   forall r.
-  (Members '[Error JuvixError, NameIdGen] r) =>
+  (Members '[Error JuvixError, NameIdGen, State Scope] r) =>
   InfoTable ->
-  S.Scope ->
   ExpressionAtoms 'Parsed ->
   Sem r Expression
-scopeCheckExpression tab scope as = mapError (JuvixError @ScoperError) $ do
+scopeCheckExpression tab as = mapError (JuvixError @ScoperError) $ do
   snd
     <$> runInfoTableBuilder
       tab
       ( runReader iniScopeParameters $
           evalState iniScoperState $
-            evalState scope $
-              withLocalScope $
-                checkParseExpressionAtoms as
+            withLocalScope $
+              checkParseExpressionAtoms as
       )
   where
     iniScopeParameters :: ScopeParameters
@@ -92,6 +90,20 @@ checkParseExpressionAtoms' ::
   Sem r Expression
 checkParseExpressionAtoms' = checkExpressionAtoms >=> parseExpressionAtoms
 
+scopeCheckImport ::
+  forall r.
+  Members '[Error JuvixError, InfoTableBuilder, NameIdGen, State Scope, Reader ScopeParameters, State ScoperState] r =>
+  Import 'Parsed ->
+  Sem r (Import 'Scoped)
+scopeCheckImport i = mapError (JuvixError @ScoperError) $ checkImport i
+
+scopeCheckOpenModule ::
+  forall r.
+  Members '[Error JuvixError, InfoTableBuilder, NameIdGen, State Scope, Reader ScopeParameters, State ScoperState] r =>
+  OpenModule 'Parsed ->
+  Sem r (OpenModule 'Scoped)
+scopeCheckOpenModule i = mapError (JuvixError @ScoperError) $ checkOpenModule i
+
 freshVariable :: Members '[NameIdGen, State ScoperFixities, State Scope, State ScoperState] r => Symbol -> Sem r S.Symbol
 freshVariable = freshSymbol S.KNameLocal
 
@@ -316,7 +328,7 @@ lookInExport sym remaining e = case remaining of
 -- modules due to nesting.
 lookupQualifiedSymbol ::
   forall r.
-  Members '[State Scope, State ScoperState] r =>
+  Members '[State Scope] r =>
   ([Symbol], Symbol) ->
   Sem r [SymbolEntry]
 lookupQualifiedSymbol (path, sym) = do

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Data/Context.hs

@@ -17,7 +17,8 @@ data ScoperResult = ScoperResult
     _resultScoperTable :: InfoTable,
     _resultModules :: NonEmpty (Module 'Scoped 'ModuleTop),
     _resultExports :: HashSet NameId,
-    _resultScope :: HashMap TopModulePath Scope
+    _resultScope :: HashMap TopModulePath Scope,
+    _resultScoperState :: ScoperState
   }
 
 makeLenses ''ScoperResult