@@ -0,0 +1,125 @@
1+.. _sect-repl:
2+
3+**************
4+The Idris REPL
5+**************
6+
7+Idris comes with a ``REPL``.
8+
9+Evaluation
10+==========
11+
12+Being a fully dependently typed language, Idris has two phases where it
13+evaluates things, compile-time and run-time. At compile-time it will only
14+evaluate things which it knows to be total (i.e. terminating and covering all
15+possible inputs) in order to keep type checking decidable. The compile-time
16+evaluator is part of the Idris kernel, and is implemented in Haskell using a
17+HOAS (higher order abstract syntax) style representation of values. Since
18+everything is known to have a normal form here, the evaluation strategy doesn't
19+actually matter because either way it will get the same answer, and in practice
20+it will do whatever the Haskell run-time system chooses to do.
21+
22+The REPL, for convenience, uses the compile-time notion of evaluation. As well
23+as being easier to implement (because we have the evaluator available) this can
24+be very useful to show how terms evaluate in the type checker. So you can see
25+the difference between:
26+
27+.. code-block:: idris
28+
29+ Idris> \n, m => (S n) + m
30+ \n => \m => S (plus n m) : Nat -> Nat -> Nat
31+
32+ Idris> \n, m => n + (S m)
33+ \n => \m => plus n (S m) : Nat -> Nat -> Nat
34+
35+Customisation
36+=============
37+
38+Idris has an RC file. Documentation to be added.
39+
40+The ``REPL`` Commands
41+=====================
42+
43+The current set of supported commands are:
44+
45++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
46+|Command | Arguments | Purpose |
47++================+==============================+==========================================================================================================+
48+|<expr> | | Evaluate an expression |
49++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
50+|:t :type | <expr> | Check the type of an expression |
51++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
52+|:core | <expr> | View the core language representation of a term |
53++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
54+|:miss :missing | <name> | Show missing clauses |
55++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
56+|:doc | <name> | Show internal documentation |
57++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
58+|:mkdoc | <namespace> | Generate IdrisDoc for namespace(s) and dependencies |
59++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
60+|:apropos | [<package list>] <name> | Search names, types, and documentation |
61++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
62+|:s :search | [<package list>] <expr> | Search for values by type |
63++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
64+|:wc :whocalls | <name> | List the callers of some name |
65++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
66+|:cw :callswho | <name> | List the callees of some name |
67++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
68+|:browse | <namespace> | List the contents of some namespace |
69++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
70+|:total | <name> | Check the totality of a name |
71++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
72+|:r :reload | | Reload current file |
73++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
74+|:l :load | <filename> | Load a new file |
75++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
76+|:cd | <filename> | Change working directory |
77++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
78+|:module | <module> | Import an extra module |
79++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
80+|:e :edit | | Edit current file using $EDITOR or $VISUAL |
81++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
82+|:m :metavars | | Show remaining proof obligations (metavariables) |
83++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
84+|:p :prove | <metavar> | Prove a metavariable |
85++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
86+|:a :addproof | <name> | Add proof to source file |
87++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
88+|:rmproof | <name> | Remove proof from proof stack |
89++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
90+|:showproof | <name> | Show proof |
91++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
92+|:proofs | | Show available proofs |
93++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
94+|:x | <expr> | Execute IO actions resulting from an expression using the interpreter |
95++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
96+|:c :compile | <filename> | Compile to an executable [codegen] <filename> |
97++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
98+|:exec :execute | [<expr>] | Compile to an executable and run |
99++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
100+|:dynamic | <filename> | Dynamically load a C library (similar to %dynamic) |
101++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
102+|:dynamic | | List dynamically loaded C libraries |
103++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
104+|:? :h :help | | Display this help text |
105++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
106+|:set | <option> | Set an option (errorcontext, showimplicits) |
107++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
108+|:unset | <option> | Unset an option |
109++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
110+|:color :colour | <option> | Turn REPL colours on or off; set a specific colour |
111++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
112+|:consolewidth | auto|infinite|<number> | Set the width of the console |
113++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
114+|:q :quit | | Exit the Idris system |
115++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
116+|:w :warranty | | Displays warranty information |
117++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
118+|:let | (<top-level-declaration>)... | Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration |
119++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
120+|:unlet :undefine|(<name>)... | Remove the listed repl definitions, or all repl definitions if no names given |
121++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
122+|:printdef | <name> | Show the definition of a function |
123++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
124+|:pp :pprint | <option> <number> <name> | Pretty prints an Idris function in either LaTeX or HTML and for a specified width. |
125++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+