M CHANGELOG.md => CHANGELOG.md +1 -0
@@ 10,6 10,7 @@
* New option `evaltiming` to time how long an evaluation takes at the REPL,
set with `:set evaltiming`.
* Renames `:lp/loadpackage` to `:package`.
+* Adds `:import`, with the same functionality as `:module`.
### Language changes
M src/Idris/Parser.idr => src/Idris/Parser.idr +6 -6
@@ 2007,7 2007,7 @@ mutual
export
data ParseCmd : Type where
ParseREPLCmd : List String -> ParseCmd
- ParseKeywordCmd : String -> ParseCmd
+ ParseKeywordCmd : List String -> ParseCmd
ParseIdentCmd : String -> ParseCmd
public export
@@ 2020,12 2020,12 @@ CommandTable = List CommandDefinition
extractNames : ParseCmd -> List String
extractNames (ParseREPLCmd names) = names
-extractNames (ParseKeywordCmd keyword) = [keyword]
+extractNames (ParseKeywordCmd keywords) = keywords
extractNames (ParseIdentCmd ident) = [ident]
runParseCmd : ParseCmd -> Rule ()
runParseCmd (ParseREPLCmd names) = replCmd names
-runParseCmd (ParseKeywordCmd keyword') = keyword keyword'
+runParseCmd (ParseKeywordCmd keywords) = choice $ map keyword keywords
runParseCmd (ParseIdentCmd ident) = exactIdent ident
@@ 2339,7 2339,7 @@ parserCommandsForHelp =
, exprArgCmd (ParseREPLCmd ["printdef"]) PrintDef "Show the definition of a function"
, exprArgCmd (ParseREPLCmd ["s", "search"]) TypeSearch "Search for values by type"
, nameArgCmd (ParseIdentCmd "di") DebugInfo "Show debugging information for a name"
- , moduleArgCmd (ParseKeywordCmd "module") ImportMod "Import an extra module"
+ , moduleArgCmd (ParseKeywordCmd ["module", "import"]) ImportMod "Import an extra module"
, stringArgCmd (ParseREPLCmd ["package"]) ImportPackage "Import every module of the package"
, noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit "Exit the Idris system"
, noArgCmd (ParseREPLCmd ["cwd"]) CWD "Displays the current working directory"
@@ 2355,7 2355,7 @@ parserCommandsForHelp =
, noArgCmd (ParseREPLCmd ["r", "reload"]) Reload "Reload current file"
, noArgCmd (ParseREPLCmd ["e", "edit"]) Edit "Edit current file using $EDITOR or $VISUAL"
, nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"
- , nameArgCmd (ParseKeywordCmd "total") Total "Check the totality of a name"
+ , nameArgCmd (ParseKeywordCmd ["total"]) Total "Check the totality of a name"
, docArgCmd (ParseIdentCmd "doc") Doc "Show documentation for a keyword, a name, or a primitive"
, moduleArgCmd (ParseIdentCmd "browse") (Browse . miAsNamespace) "Browse contents of a namespace"
, loggingArgCmd (ParseREPLCmd ["log", "logging"]) SetLog "Set logging level"
@@ 2376,7 2376,7 @@ parserCommandsForHelp =
, noArgCmd (ParseREPLCmd ["gdnext"]) (Editing GenerateDefNext) "Show next definition"
, noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
, noArgCmd (ParseREPLCmd ["?", "h", "help"]) Help "Display this help text"
- , declsArgCmd (ParseKeywordCmd "let") NewDefn "Define a new value"
+ , declsArgCmd (ParseKeywordCmd ["let"]) NewDefn "Define a new value"
, exprArgCmd (ParseREPLCmd ["fs", "fsearch"]) FuzzyTypeSearch "Search for global definitions by sketching the names distribution of the wanted type(s)."
]
M tests/Main.idr => tests/Main.idr +6 -0
@@ 184,6 184,11 @@ idrisTestsEvaluator = MkTestPool "Evaluation" [] Nothing
"interpreter001", "interpreter002", "interpreter003", "interpreter004",
"interpreter005", "interpreter006", "interpreter007", "interpreter008"]
+idrisTestsREPL : TestPool
+idrisTestsREPL = MkTestPool "REPL commands and help" [] Nothing
+ [ "repl001", "repl002"
+ ]
+
idrisTestsAllSchemes : Requirement -> TestPool
idrisTestsAllSchemes cg = MkTestPool
("Test across all scheme backends: " ++ show cg ++ " instance")
@@ 393,6 398,7 @@ main = runner $
, testPaths "idris2" idrisTestsData
, testPaths "idris2" idrisTestsBuiltin
, testPaths "idris2" idrisTestsEvaluator
+ , testPaths "idris2" idrisTestsREPL
, testPaths "idris2" idrisTestsTotality
, testPaths "idris2" idrisTestsSchemeEval
, testPaths "idris2" idrisTestsReflection
A tests/idris2/repl001/expected => tests/idris2/repl001/expected +47 -0
@@ 0,0 1,47 @@
+Main> <expr> Evaluate an expression
+ :t :type <expr> Check the type of an expression
+ :ti <expr> Check the type of an expression, showing implicit arguments
+ :printdef <expr> Show the definition of a function
+ :s :search <expr> Search for values by type
+ :di <name> Show debugging information for a name
+ :module :import <module> Import an extra module
+ :package <string> Import every module of the package
+ :q :quit :exit Exit the Idris system
+ :cwd Displays the current working directory
+ :cd <string> Change the current working directory
+ :sh <string> Run a shell command
+ :set <option> Set an option
+ :unset <option> Unset an option
+ :opts Show current options settings
+ :c :compile <file> <expr> Compile to an executable
+ :exec <expr> Compile to an executable and run
+ :directive <string> Set a codegen-specific directive
+ :l :load <string> Load a file
+ :r :reload Reload current file
+ :e :edit Edit current file using $EDITOR or $VISUAL
+ :miss :missing <name> Show missing clauses
+ :total <name> Check the totality of a name
+ :doc <keyword|expr> Show documentation for a keyword, a name, or a primitive
+ :browse <module> Browse contents of a namespace
+ :log :logging <string> <number> Set logging level
+ :consolewidth <number|auto> Set the width of the console output (0 for unbounded) (auto by default)
+ :color :colour (on|off) Whether to use color for the console output (enabled by default)
+ :m :metavars Show remaining proof obligations (metavariables or holes)
+ :typeat <l:number> <c:number> <n:string> Show type of term <n> defined on line <l> and column <c>
+ :cs :casesplit <l:number> <c:number> <n:string> Case split term <n> defined on line <l> and column <c>
+ :ac :addclause <l:number> <n:string> Add clause to term <n> defined on line <l>
+ :ml :makelemma <l:number> <n:string> Make lemma for term <n> defined on line <l>
+ :mc :makecase <l:number> <n:string> Make case on term <n> defined on line <l>
+ :mw :makewith <l:number> <n:string> Add with expression on term <n> defined on line <l>
+ :intro <l:number> <n:string> Introduce unambiguous constructor in hole <n> defined on line <l>
+ :refine <l:number> <c:number> <h:string> <e:expr>Refine hole <h> with identifier <n> on line <l> and column <c>
+ :ps :proofsearch <l:number> <n:string> <h:[name]> Search for a proof
+ :psnext Show next proof
+ :gd <l:number> <n:string> <r:number|0> Search for a proof
+ :gdnext Show next definition
+ :version Display the Idris version
+ :? :h :help Display this help text
+ :let <decls> Define a new value
+ :fs :fsearch <expr> Search for global definitions by sketching the names distribution of the wanted type(s).
+Main>
+Bye for now!
A tests/idris2/repl001/input => tests/idris2/repl001/input +1 -0
A tests/idris2/repl001/run => tests/idris2/repl001/run +1 -0
@@ 0,0 1,1 @@
+$1 --no-color --console-width 0 --no-banner < input
A tests/idris2/repl002/expected => tests/idris2/repl002/expected +4 -0
@@ 0,0 1,4 @@
+Main> Imported module Data.Nat
+Main> Imported module Data.List
+Main>
+Bye for now!
A tests/idris2/repl002/input => tests/idris2/repl002/input +2 -0
@@ 0,0 1,2 @@
+:module Data.Nat
+:import Data.List
A tests/idris2/repl002/run => tests/idris2/repl002/run +1 -0
@@ 0,0 1,1 @@
+$1 --no-color --console-width 0 --no-banner < input