Add module REPL command

CHANGELOG.md

@@ -27,6 +27,10 @@ Library changes:
      should be considered experimental with the API able to change at any time!
      Further experiments in `Data.Linear` are welcome :).
 
+REPL changes:
+
+* Implemented `:module` command, to load a module during a REPL session.
+
 Changes since Idris 2 v0.1.0
 ----------------------------
 

src/Idris/Parser.idr

@@ -1737,6 +1737,9 @@ data CmdArg : Type where
      ||| The command takes a file.
      FileArg : CmdArg
 
+     ||| The command takes a module.
+     ModuleArg : CmdArg
+
 export
 Show CmdArg where
   show NoArg = ""
@@ -1746,6 +1749,7 @@ Show CmdArg where
   show NumberArg = "<number>"
   show OptionArg = "<option>"
   show FileArg = "<filename>"
+  show ModuleArg = "<module>"
 
 export
 data ParseCmd : Type where
@@ -1794,6 +1798,19 @@ nameArgCmd parseCmd command doc = (names, NameArg, doc, parse)
       n <- name
       pure (command n)
 
+moduleArgCmd : ParseCmd -> (List String -> REPLCmd) -> String -> CommandDefinition
+moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse)
+  where
+    names : List String
+    names = extractNames parseCmd
+
+    parse : Rule REPLCmd
+    parse = do
+      symbol ":"
+      runParseCmd parseCmd
+      n <- moduleIdent
+      pure (command n)
+
 exprArgCmd : ParseCmd -> (PTerm -> REPLCmd) -> String -> CommandDefinition
 exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
   where
@@ -1865,6 +1882,7 @@ parserCommandsForHelp =
   , nameArgCmd (ParseREPLCmd ["printdef"]) PrintDef "Show the definition of a function"
   , nameArgCmd (ParseREPLCmd ["s", "search"]) ProofSearch "Search for values by type"
   , nameArgCmd (ParseIdentCmd "di") DebugInfo "Show debugging information for a name"
+  , moduleArgCmd (ParseKeywordCmd "module") ImportMod "Import an extra module"
   , noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit "Exit the Idris system"
   , noArgCmd (ParseREPLCmd ["cwd"]) CWD "Displays the current working directory"
   , optArgCmd (ParseIdentCmd "set") SetOpt True "Set an option"

src/Idris/ProcessIdr.idr

@@ -95,6 +95,17 @@ readImport full imp
     = do readModule full (loc imp) True (reexport imp) (path imp) (nameAs imp)
          addImported (path imp, reexport imp, nameAs imp)
 
+||| Adds new import to the namespace without changing the current top-level namespace
+export
+addImport : {auto c : Ref Ctxt Defs} ->
+            {auto u : Ref UST UState} ->
+            {auto s : Ref Syn SyntaxInfo} ->
+            Import -> Core ()
+addImport imp
+    = do topNS <- getNS
+         readImport True imp
+         setNS topNS
+
 readHash : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            Import -> Core (Bool, (List String, Int))

src/Idris/REPL.idr

@@ -29,6 +29,7 @@ import Idris.IDEMode.MakeClause
 import Idris.IDEMode.Holes
 import Idris.ModTree
 import Idris.Parser
+import Idris.ProcessIdr
 import Idris.Resugar
 import public Idris.REPLCommon
 import Idris.Syntax
@@ -417,6 +418,8 @@ data REPLResult : Type where
   Printed : List String -> REPLResult
   TermChecked : PTerm -> PTerm -> REPLResult
   FileLoaded : String -> REPLResult
+  ModuleLoaded : String -> REPLResult
+  ErrorLoadingModule : String -> Error -> REPLResult
   ErrorLoadingFile : String -> FileError -> REPLResult
   ErrorsBuildingFile : String -> List Error -> REPLResult
   NoFileLoaded : REPLResult
@@ -583,6 +586,10 @@ process (Load f)
          put ROpts (record { mainfile = Just f } opts)
          -- Clear the context and load again
          loadMainFile f
+process (ImportMod m)
+    = do catch (do addImport (MkImport emptyFC False m m)
+                   pure $ ModuleLoaded (showSep "." (reverse m)))
+               (\err => pure $ ErrorLoadingModule (showSep "." (reverse m)) err)
 process (CD dir)
     = do setWorkingDir dir
          workDir <- getWorkingDir
@@ -814,6 +821,8 @@ mutual
   displayResult  (Printed xs) = printResult (showSep "\n" xs)
   displayResult  (TermChecked x y) = printResult $ show x ++ " : " ++ show y
   displayResult  (FileLoaded x) = printResult $ "Loaded file " ++ x
+  displayResult  (ModuleLoaded x) = printResult $ "Imported module " ++ x
+  displayResult  (ErrorLoadingModule x err) = printError $ "Error loading module " ++ x ++ ": " ++ !(perror err)
   displayResult  (ErrorLoadingFile x err) = printError $ "Error loading file " ++ x ++ ": " ++ show err
   displayResult  (ErrorsBuildingFile x errs) = printError $ "Error(s) building file " ++ x -- messages already displayed while building
   displayResult  NoFileLoaded = printError "No file can be reloaded"

src/Idris/Syntax.idr

@@ -395,6 +395,7 @@ data REPLCmd : Type where
      PrintDef : Name -> REPLCmd
      Reload : REPLCmd
      Load : String -> REPLCmd
+     ImportMod : List String -> REPLCmd
      Edit : REPLCmd
      Compile : PTerm -> String -> REPLCmd
      Exec : PTerm -> REPLCmd

src/Parser/Rule/Source.idr

@@ -150,6 +150,15 @@ namespacedIdent
             Ident i => Just $ [i]
             _ => Nothing)
 
+export
+moduleIdent : Rule (List String)
+moduleIdent
+    = terminal "Expected module identifier"
+        (\x => case tok x of
+            DotSepIdent ns => Just ns
+            Ident i => Just $ [i]
+            _ => Nothing)
+
 export
 unqualifiedName : Rule String
 unqualifiedName = identPart

tests/Main.idr

@@ -65,7 +65,7 @@ idrisTests
        "interface009", "interface010", "interface011", "interface012",
        "interface013", "interface014", "interface015", "interface016",
        -- Miscellaneous REPL
-       "interpreter001", "interpreter002",
+       "interpreter001", "interpreter002", "interpreter003",
        -- Implicit laziness, lazy evaluation
        "lazy001",
        -- QTT and linearity related

tests/idris2/interpreter003/expected

@@ -0,0 +1,11 @@
+Main> (interactive):1:1--1:25:Undefined name fromMaybe at:
+1	fromMaybe "test" Nothing
+	^^^^^^^^^^^^^^^^^^^^^^^^
+
+Main> Imported module Data.Maybe
+Main> "test"
+Main> Imported module Data.Strings
+Main> "hello"
+Main> True
+Main> Error loading module DoesNotExists: DoesNotExists not found
+Main> Bye for now!

tests/idris2/interpreter003/input

@@ -0,0 +1,8 @@
+fromMaybe "test" Nothing
+:module Data.Maybe
+fromMaybe "test" Nothing
+:module Data.Strings
+toLower "HELLO"
+isJust (Just 'x')
+:module DoesNotExists
+:q

tests/idris2/interpreter003/run

@@ -0,0 +1 @@
+$1 --no-banner < input