mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
Merge pull request #315 from ShinKage/repl-import-module
Module command to import module in REPL
This commit is contained in:
commit
0d2871db3c
@ -41,6 +41,10 @@ Compiler changes:
|
||||
exposes the function `mainWithCodegens` that takes a list of codegens. The
|
||||
feature in documented [here](https://idris2.readthedocs.io/en/latest/backends/custom.html).
|
||||
|
||||
REPL changes:
|
||||
|
||||
* Implemented `:module` command, to load a module during a REPL session.
|
||||
|
||||
Changes since Idris 2 v0.1.0
|
||||
----------------------------
|
||||
|
||||
|
@ -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"
|
||||
|
@ -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))
|
||||
|
@ -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"
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
11
tests/idris2/interpreter003/expected
Normal file
11
tests/idris2/interpreter003/expected
Normal file
@ -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!
|
8
tests/idris2/interpreter003/input
Normal file
8
tests/idris2/interpreter003/input
Normal file
@ -0,0 +1,8 @@
|
||||
fromMaybe "test" Nothing
|
||||
:module Data.Maybe
|
||||
fromMaybe "test" Nothing
|
||||
:module Data.Strings
|
||||
toLower "HELLO"
|
||||
isJust (Just 'x')
|
||||
:module DoesNotExists
|
||||
:q
|
1
tests/idris2/interpreter003/run
Executable file
1
tests/idris2/interpreter003/run
Executable file
@ -0,0 +1 @@
|
||||
$1 --no-banner < input
|
Loading…
Reference in New Issue
Block a user