@@ -0,0 +1,530 @@
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 supports initialisation scripts.
39+
40+Initialisation scripts
41+~~~~~~~~~~~~~~~~~~~~~~
42+
43+When the Idris REPL starts up, it will attempt to open the file
44+repl/init in Idris's application data directory. The application data
45+directory is the result of the Haskell function call
46+``getAppUserDataDirectory "idris"``, which on most Unix-like systems
47+will return $HOME/.idris and on various versions of Windows will return
48+paths such as ``C:/Documents And Settings/user/Application Data/appName``.
49+
50+The file repl/init is a newline-separate list of REPL commands. Not all
51+commands are supported in initialisation scripts — only the subset that
52+will not interfere with the normal operation of the REPL. In particular,
53+setting colours, display options such as showing implicits, and log
54+levels are supported.
55+
56+Example initialisation script
57+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
58+::
59+
60+ :colour prompt white italic bold
61+ :colour implicit magenta italic
62+
63+
64+
65+The ``REPL`` Commands
66+=====================
67+
68+The current set of supported commands are:
69+
70++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
71+|Command | Arguments | Purpose |
72++================+==============================+==========================================================================================================+
73+|<expr> | | Evaluate an expression |
74++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
75+|:t :type | <expr> | Check the type of an expression |
76++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
77+|:core | <expr> | View the core language representation of a term |
78++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
79+|:miss :missing | <name> | Show missing clauses |
80++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
81+|:doc | <name> | Show internal documentation |
82++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
83+|:mkdoc | <namespace> | Generate IdrisDoc for namespace(s) and dependencies |
84++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
85+|:apropos | [<package list>] <name> | Search names, types, and documentation |
86++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
87+|:s :search | [<package list>] <expr> | Search for values by type |
88++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
89+|:wc :whocalls | <name> | List the callers of some name |
90++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
91+|:cw :callswho | <name> | List the callees of some name |
92++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
93+|:browse | <namespace> | List the contents of some namespace |
94++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
95+|:total | <name> | Check the totality of a name |
96++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
97+|:r :reload | | Reload current file |
98++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
99+|:l :load | <filename> | Load a new file |
100++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
101+|:cd | <filename> | Change working directory |
102++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
103+|:module | <module> | Import an extra module |
104++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
105+|:e :edit | | Edit current file using $EDITOR or $VISUAL |
106++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
107+|:m :metavars | | Show remaining proof obligations (metavariables) |
108++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
109+|:p :prove | <metavar> | Prove a metavariable |
110++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
111+|:a :addproof | <name> | Add proof to source file |
112++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
113+|:rmproof | <name> | Remove proof from proof stack |
114++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
115+|:showproof | <name> | Show proof |
116++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
117+|:proofs | | Show available proofs |
118++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
119+|:x | <expr> | Execute IO actions resulting from an expression using the interpreter |
120++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
121+|:c :compile | <filename> | Compile to an executable [codegen] <filename> |
122++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
123+|:exec :execute | [<expr>] | Compile to an executable and run |
124++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
125+|:dynamic | <filename> | Dynamically load a C library (similar to %dynamic) |
126++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
127+|:dynamic | | List dynamically loaded C libraries |
128++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
129+|:? :h :help | | Display this help text |
130++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
131+|:set | <option> | Set an option (errorcontext, showimplicits) |
132++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
133+|:unset | <option> | Unset an option |
134++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
135+|:color :colour | <option> | Turn REPL colours on or off; set a specific colour |
136++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
137+|:consolewidth | auto|infinite|<number> | Set the width of the console |
138++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
139+|:q :quit | | Exit the Idris system |
140++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
141+|:w :warranty | | Displays warranty information |
142++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
143+|:let | (<top-level-declaration>)... | Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration |
144++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
145+|:unlet :undefine|(<name>)... | Remove the listed repl definitions, or all repl definitions if no names given |
146++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
147+|:printdef | <name> | Show the definition of a function |
148++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
149+|:pp :pprint | <option> <number> <name> | Pretty prints an Idris function in either LaTeX or HTML and for a specified width. |
150++----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
151+
152+
153+Using the REPL
154+==============
155+
156+
157+Getting help
158+~~~~~~~~~~~~
159+
160+The command ``:help`` (or ``:h`` or ``:?``) prints a short summary of
161+the available commands.
162+
163+Quitting Idris
164+~~~~~~~~~~~~~~
165+
166+If you would like to leave Idris, simply use ``:q`` or ``:quit``.
167+
168+Evaluating expressions
169+~~~~~~~~~~~~~~~~~~~~~~
170+
171+To evaluate an expression, simply type it. If Idris is unable to infer
172+the type, it can be helpful to use the operator ``the`` to manually
173+provide one, as Idris's syntax does not allow for direct type
174+annotations. Examples of ``the`` include:
175+
176+::
177+
178+ Idris> the Nat 4
179+ 4 : Nat
180+ Idris> the Int 4
181+ 4 : Int
182+ Idris> the (List Nat) [1,2]
183+ [1,2] : List Nat
184+ Idris> the (Vect _ Nat) [1,2]
185+ [1,2] : Vect 2 Nat
186+
187+This may not work in cases where the expression still involves ambiguous
188+names. The name can be disambiguated by using the ``with`` keyword:
189+
190+::
191+
192+ Idris> sum [1,2,3]
193+ When elaborating an application of function Prelude.Foldable.sum:
194+ Can't disambiguate name: Prelude.List.::,
195+ Prelude.Stream.::,
196+ Prelude.Vect.::
197+ Idris> with List sum [1,2,3]
198+ 6 : Integer
199+
200+Adding let bindings
201+~~~~~~~~~~~~~~~~~~~
202+
203+To add a let binding to the REPL, use ``:let``. It's likely you'll also
204+need to provide a type annotation. ``:let`` also works for other
205+declarations as well, such as ``data``.
206+
207+::
208+
209+ Idris> :let x : String; x = "hello"
210+ Idris> x
211+ "hello" : String
212+ Idris> :let data Foo : Type where Bar : Foo
213+ Idris> Bar
214+ Bar : Foo
215+
216+Getting type information
217+~~~~~~~~~~~~~~~~~~~~~~~~
218+
219+To ask Idris for the type of some expression, use the ``:t`` command.
220+Additionally, if used with an overloaded name, Idris will provide all
221+overloadings and their types. To ask for the type of an infix operator,
222+surround it in parentheses.
223+
224+::
225+
226+ Idris> :t "foo"
227+ "foo" : String
228+ Idris> :t plus
229+ Prelude.Nat.plus : Nat -> Nat -> Nat
230+ Idris> :t (++)
231+ Builtins.++ : String -> String -> String
232+ Prelude.List.++ : (List a) -> (List a) -> List a
233+ Prelude.Vect.++ : (Vect m a) -> (Vect n a) -> Vect (m + n) a
234+ Idris> :t plus 4
235+ plus (Builtins.fromInteger 4) : Nat -> Nat
236+
237+You can also ask for basic information about typeclasses with ``:doc``:
238+
239+::
240+
241+ Idris> :doc Monad
242+ Type class Monad
243+
244+ Parameters:
245+ m
246+
247+ Methods:
248+ (>>=) : Monad m => m a -> (a -> m b) -> m b
249+
250+ infixl 5
251+
252+ Instances:
253+ Monad id
254+ Monad PrimIO
255+ Monad IO
256+ Monad Maybe
257+
258+ ...
259+
260+Other documentation is also available from ``:doc``:
261+
262+::
263+
264+ Idris> :doc (+)
265+ Prelude.Classes.+ : (a : Type) -> (Num a) -> a -> a -> a
266+
267+ infixl 8
268+
269+ Arguments:
270+ Class constraint Prelude.Classes.Num a
271+ __pi_arg : a
272+ __pi_arg1 : a
273+
274+::
275+
276+ Idris> :doc Vect
277+ Data type Prelude.Vect.Vect : Nat -> Type -> Type
278+
279+ Arguments:
280+ Nat
281+ Type
282+
283+ Constructors:
284+
285+ Prelude.Vect.Nil : (a : Type) -> Vect 0 a
286+
287+
288+ Prelude.Vect.:: : (a : Type) -> (n : Nat) -> a -> (Vect n a) -> Vect (S n) a
289+
290+ infixr 7
291+
292+ Arguments:
293+ a
294+ Vect n a
295+
296+::
297+
298+ Idris> :doc Monad
299+ Type class Prelude.Monad.Monad
300+ Methods:
301+
302+ Prelude.Monad.>>= : (m : Type -> Type) -> (a : Type) -> (b : Type) -> (Monad m) -> (m a) -> (a -> m b) -> m b
303+
304+ infixl 5
305+
306+ Arguments:
307+ Class constraint Prelude.Monad.Monad m
308+ __pi_arg : m a
309+ __pi_arg1 : a -> m b
310+
311+Finding things
312+~~~~~~~~~~~~~~
313+
314+The command ``:apropos`` searches names, types, and documentation for
315+some string, and prints the results. For example:
316+
317+::
318+
319+ Idris> :apropos eq
320+ eqPtr : Ptr -> Ptr -> IO Bool
321+
322+
323+ eqSucc : (left : Nat) -> (right : Nat) -> (left = right) -> S left = S right
324+ S preserves equality
325+
326+ lemma_both_neq : ((x = x') -> _|_) -> ((y = y') -> _|_) -> ((x, y) = (x', y')) -> _|_
327+
328+
329+ lemma_fst_neq_snd_eq : ((x = x') -> _|_) -> (y = y') -> ((x, y) = (x', y)) -> _|_
330+
331+
332+ lemma_snd_neq : (x = x) -> ((y = y') -> _|_) -> ((x, y) = (x, y')) -> _|_
333+
334+
335+ lemma_x_eq_xs_neq : (x = y) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_
336+
337+
338+ lemma_x_neq_xs_eq : ((x = y) -> _|_) -> (xs = ys) -> (x :: xs = y :: ys) -> _|_
339+
340+
341+ lemma_x_neq_xs_neq : ((x = y) -> _|_) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_
342+
343+
344+ prim__eqB16 : Bits16 -> Bits16 -> Int
345+
346+ prim__eqB16x8 : Bits16x8 -> Bits16x8 -> Bits16x8
347+
348+ prim__eqB32 : Bits32 -> Bits32 -> Int
349+
350+ prim__eqB32x4 : Bits32x4 -> Bits32x4 -> Bits32x4
351+
352+ prim__eqB64 : Bits64 -> Bits64 -> Int
353+
354+ prim__eqB64x2 : Bits64x2 -> Bits64x2 -> Bits64x2
355+
356+ prim__eqB8 : Bits8 -> Bits8 -> Int
357+
358+ prim__eqB8x16 : Bits8x16 -> Bits8x16 -> Bits8x16
359+
360+ prim__eqBigInt : Integer -> Integer -> Int
361+
362+ prim__eqChar : Char -> Char -> Int
363+
364+ prim__eqFloat : Float -> Float -> Int
365+
366+ prim__eqInt : Int -> Int -> Int
367+
368+ prim__eqString : String -> String -> Int
369+
370+ prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)
371+
372+ sequence : Traversable t => Applicative f => (t (f a)) -> f (t a)
373+
374+
375+ sequence_ : Foldable t => Applicative f => (t (f a)) -> f ()
376+
377+
378+ Eq : Type -> Type
379+ The Eq class defines inequality and equality.
380+
381+ GTE : Nat -> Nat -> Type
382+ Greater than or equal to
383+
384+ LTE : Nat -> Nat -> Type
385+ Proofs that n is less than or equal to m
386+
387+ gte : Nat -> Nat -> Bool
388+ Boolean test than one Nat is greater than or equal to another
389+
390+ lte : Nat -> Nat -> Bool
391+ Boolean test than one Nat is less than or equal to another
392+
393+ ord : Char -> Int
394+ Convert the number to its ASCII equivalent.
395+
396+ replace : (x = y) -> (P x) -> P y
397+ Perform substitution in a term according to some equality.
398+
399+ sym : (l = r) -> r = l
400+ Symmetry of propositional equality
401+
402+ trans : (a = b) -> (b = c) -> a = c
403+ Transitivity of propositional equality
404+
405+``:search`` does a type-based search, in the spirit of Hoogle. See `Type-directed search (:search) <https://github.com/idris-lang/Idris-dev/wiki/Type-directed-search-%28%3Asearch%29>`_ for more details. Here is an example:
406+
407+::
408+
409+ Idris> :search a -> b -> a
410+ = Prelude.Basics.const : a -> b -> a
411+ Constant function. Ignores its second argument.
412+
413+ = assert_smaller : a -> b -> b
414+ Assert to the totality checker than y is always structurally
415+ smaller than x (which is typically a pattern argument)
416+
417+ > malloc : Int -> a -> a
418+
419+
420+ > Prelude.pow : Num a => a -> Nat -> a
421+
422+
423+ > Prelude.Classes.(*) : Num a => a -> a -> a
424+
425+
426+ > Prelude.Classes.(+) : Num a => a -> a -> a
427+ ... (More results)
428+
429+``:search`` can also look for dependent types:
430+
431+::
432+
433+ Idris> :search plus (S n) n = plus n (S n)
434+ < Prelude.Nat.plusSuccRightSucc : (left : Nat) ->
435+ (right : Nat) ->
436+ S (left + right) = left + S right
437+
438+Loading and reloading Idris code
439+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
440+
441+The command ``:l File.idr`` will load File.idr into the
442+currently-running REPL, and ``:r`` will reload the last file that was
443+loaded.
444+
445+Totality
446+~~~~~~~~
447+
448+All Idris definitions are checked for totality. The command
449+``:total <NAME>`` will display the result of that check. If a definition
450+is not total, this may be due to an incomplete pattern match. If that is
451+the case, ``:missing`` or ``:miss`` will display the missing cases.
452+
453+Editing files
454+~~~~~~~~~~~~~
455+
456+The command ``:e`` launches your default editor on the current module.
457+After control returns to Idris, the file is reloaded.
458+
459+Invoking the compiler
460+~~~~~~~~~~~~~~~~~~~~~
461+
462+The current module can be compiled to an executable using the command
463+``:c <FILENAME>`` or ``:compile <FILENAME>``. This command allows to
464+specify codegen, so for example JavaScript can be generated using
465+``:c javascript <FILENAME>``. The ``:exec`` command will compile the
466+program to a temporary file and run the resulting executable.
467+
468+IO actions
469+~~~~~~~~~~
470+
471+Unlike GHCI, the Idris REPL is not inside of an implicit IO monad. This
472+means that a special command must be used to execute IO actions.
473+``:x tm`` will execute the IO action ``tm`` in an Idris interpreter.
474+
475+Dynamically loading C libraries
476+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
477+
478+Sometimes, an Idris program will depend on external libraries written in
479+C. In order to use these libraries from the Idris interpreter, they must
480+first be dynamically loaded. This is achieved through the
481+``%dynamic <LIB>`` directive in Idris source files or through the
482+``:dynamic <LIB>`` command at the REPL. The current set of dynamically
483+loaded libraries can be viewed by executing ``:dynamic`` with no
484+arguments. These libraries are available through the Idris FFI in `type
485+providers <#type-providers>`__ and ``:exec``.
486+
487+Colours
488+=======
489+
490+Idris terms are available in amazing colour! By default, the Idris REPL
491+uses colour to distinguish between data constructors, types or type
492+constructors, operators, bound variables, and implicit arguments. This
493+feature is available on all POSIX-like systems, and there are plans to
494+allow it to work on Windows as well.
495+
496+If you do not like the default colours, they can be turned off using the
497+command
498+
499+::
500+
501+ :colour off
502+
503+and, when boredom strikes, they can be re-enabled using the command
504+
505+::
506+
507+ :colour on
508+
509+To modify a colour, use the command
510+
511+::
512+
513+ :colour <CATEGORY> <OPTIONS>
514+
515+where ``<CATEGORY`` is one of ``keyword``, ``boundvar``, ``implicit``,
516+``function``, ``type``, ``data``, or ``prompt``, and is a
517+space-separated list drawn from the colours and the font options. The
518+available colours are ``default``, ``black``, ``yellow``, ``cyan``,
519+``red``, ``blue``, ``white``, ``green``, and ``magenta``. If more than
520+one colour is specified, the last one takes precedence. The available
521+options are ``dull`` and ``vivid``, ``bold`` and ``nobold``, ``italic``
522+and ``noitalic``, ``underline`` and ``nounderline``, forming pairs of
523+opposites. The colour ``default`` refers to your terminal's default
524+colour.
525+
526+The colours used at startup can be changed using REPL initialisation
527+scripts.
528+
529+Colour can be disabled at startup by the ``--nocolour`` command-line
530+option.