git.iko.soy/Idris-dev
on master help sign in
Updates

+ Fix typo in FAQ + Added content from Idris WIKI, that should belong in the new sphinx docs. + Language Extensions + Language Features + Manual information + Syntac Guide + REPL usage. Of note the manual contents needs trimming and fixing up.

commitab546609e02e1e4892d7f38831c25686979d3013 authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateSat 30 May 2015, 12:26 (11 years ago) parent38c4fb2
9 files changed+1344−4
compare with master
unifiedsplit
docs/faq/faq.rst+3−3 docs/index.rst+4 docs/reference/index.rst+5 docs/reference/language-extensions.rst+36 docs/reference/language-features.rst+214 docs/reference/misc.rst+82 docs/reference/repl.rst+406−1 docs/reference/syntax-guide.rst+277 docs/reference/theorem-prover.rst+317
docs/faq/faq.rst+3−3
@@ -108,7 +108,7 @@ the undecidability of the `Halting Problem
108108to identify some programs which are definitely terminating. Idris does this
109109using "size change termination" which looks for recursive paths from a
110110function back to itself. On such a path, there must be at least one
111−argument which converges to a base case.
111+argument which converges to a base case.
112112
113113- Mutually recursive functions are supported
114114- However, all functions on the path must be fully applied. In particular,
@@ -166,8 +166,8 @@ where the Idris libs reside relative to the idris executable. The
166166IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,
167167Idris will use that path to find the C compiler.
168168
169−Example:
170−.. code-block::
169+Example::
170+
171171 IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
172172
173173What does the name ‘Idris’ mean?
docs/index.rst+4
@@ -107,6 +107,10 @@ Language Reference
107107 reference/ide-protocol
108108 reference/semantic-highlighting
109109 reference/repl
110+ reference/theorem-prover
111+ reference/language-features
112+ reference/language-extensions
113+ reference/misc
110114
111115.. _guides:
112116
docs/reference/index.rst+5
@@ -26,3 +26,8 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
2626 erasure
2727 semantic-highlighting
2828 repl
29+ syntax-guide
30+ theorem-prover
31+ language-features
32+ language-extensions
33+ misc
docs/reference/language-extensions.rstnew file+36
@@ -0,0 +1,36 @@
1+*******************
2+Language Extensions
3+*******************
4+
5+
6+
7+Type Providers
8+===============
9+
10+Idris type providers are a way to get the type system to reflect
11+observations about the world outside of Idris. Similarly to `F# type
12+providers <http://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
13+they cause effectful computations to run during type checking, returning
14+information that the type checker can use when checking the rest of the
15+program. While F# type providers are based on code generation, Idris
16+type providers use only the ordinary execution semantics of Idris to
17+generate the information.
18+
19+A type provider is simply a term of type ``IO (Provider t)``, where
20+``Provider`` is a data type with constructors for a successful result
21+and an error. The type ``t`` can be either ``Type`` (the type of types)
22+or a concrete type. Then, a type provider ``p`` is invoked using the
23+syntax ``%provide (x : t) with p``. When the type checker encounters
24+this line, the IO action ``p`` is executed. Then, the resulting term is
25+extracted from the IO monad. If it is ``Provide y`` for some ``y : t``,
26+then ``x`` is bound to ``y`` for the remainder of typechecking and in
27+the compiled code. If execution fails, a generic error is reported and
28+type checking terminates. If the resulting term is ``Error e`` for some
29+string ``e``, then type checking fails and the error ``e`` is reported
30+to the user.
31+
32+Example Idris type providers can be seen at `this
33+repository <https://github.com/david-christiansen/idris-type-providers>`__.
34+More detailed descriptions are available in David Christiansen's `WGP
35+'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
36+thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.
docs/reference/language-features.rstnew file+214
@@ -0,0 +1,214 @@
1+**********************
2+Core Language Features
3+**********************
4+
5+
6+- Full-spectrum dependent types
7+- Strict evaluation (plus ``Lazy : Type -> Type`` type constructor for
8+ explicit laziness)
9+- Lambda, Pi (forall), Let bindings
10+- Pattern matching definitions
11+- Export modifiers ``public``, ``abstract``, ``private``
12+- Function options ``partial``, ``total``
13+- ``where`` clauses
14+- "magic with"
15+- Implicit arguments (in top level types)
16+- "Bound" implicit arguments ``{n : Nat} -> {a : Type} -> Vect n a``
17+- "Unbound" implicit arguments --- ``Vect n a`` is equivalent to the
18+ above in a type, ``n`` and ``a`` are implicitly bound. This applies
19+ to names beginning with a lower case letter in an argument position.
20+- 'Tactic' implicit arguments, which are solved by running a tactic
21+ script or giving a default argument, rather than by unification.
22+- Unit type ``()``, empty type ``Void``
23+- Tuples (desugaring to nested pairs)
24+- Dependent pair syntax ``(x : T ** P x)`` (there exists an ``x`` of
25+ type ``T`` such that ``P x``)
26+- Inline ``case`` expressions
27+- Heterogeneous equality
28+- ``do`` notation
29+- Idiom brackets
30+- Type classes, suppoting default methods and dependencies between
31+ methods
32+- ``rewrite`` prf ``in`` expr
33+- Metavariables
34+- Inline proof/tactic scripts
35+- Implicit coercion
36+- ``codata``
37+- Also ``Inf : Type -> Type`` type constructor for mixed data/codata.
38+ In fact ``codata`` is implemented by putting recusive arguments under
39+ ``Inf``.
40+- ``syntax`` rules for defining pattern and term syntactic sugar
41+- these are used in the standard library to define
42+ ``if ... then ... else`` expressions and an Agda-style preorder
43+ reasoning syntax.
44+- `Uniqueness
45+ typing <https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Types>`__
46+ using the ``UniqueType`` universe.
47+- `Partial
48+ evaluation <https://github.com/idris-lang/Idris-dev/wiki/Static-Arguments-and-Partial-Evaluation>`__
49+ by ``[static]`` argument annotations.
50+
51+Namespaces and type-directed disambiguation
52+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
53+
54+Names can be defined in separate namespaces, and disambiguated by type.
55+An expression ``with Name expr`` will privilege the namespace ``Name``
56+in the expression ``expr``. For example:
57+
58+::
59+
60+ Idris> with List [[1,2],[3,4],[5,6]]
61+ [[1, 2], [3, 4], [5, 6]] : List (List Integer)
62+
63+ Idris> with Vect [[1,2],[3,4],[5,6]]
64+ [[1, 2], [3, 4], [5, 6]] : Vect 3 (Vect 2 Integer)
65+
66+ Idris> [[1,2],[3,4],[5,6]]
67+ Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Prelude.Vect.::
68+
69+Alternatives
70+~~~~~~~~~~~~
71+
72+``(| option1, option2, option3, ... |)`` type checks each of the options
73+in turn until one of them works. This can be used to give simple
74+automated proofs, e.g. for trying some constructors of proofs:
75+
76+::
77+
78+ syntax Trivial = (| oh, refl |)
79+
80+Totality checking assertions
81+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
82+
83+All definitions are checked for *coverage* (i.e. all well-typed
84+applications are handled) and either for *termination* (i.e. all
85+well-typed applications will eventually produce an answer) or, if
86+returning codata, for productivity (in practice, all recursive calls are
87+constructor guarded).
88+
89+Obviously, termination checking is undecidable. In practice, the
90+termination checker looks for *size change* - every cycle of recursive
91+calls must have a decreasing argument, such as a recursive argument of a
92+strictly positive data type.
93+
94+There are two built-in functions which can be used to give the totality
95+checker a hint:
96+
97+- ``assert_total x`` asserts that the expression ``x`` is terminating
98+ and covering, even if the totality checker cannot tell. This can be
99+ used for example if ``x`` uses a function which does not cover all
100+ inputs, but the caller knows that the specific input is covered.
101+- ``assert_smaller p x`` asserts that the expression ``x`` is
102+ structurally smaller than the pattern ``p``.
103+
104+For example, the following function is not checked as total:
105+
106+::
107+
108+ qsort : Ord a => List a -> List a
109+ qsort [] = []
110+ qsort (x :: xs) = qsort (filter (<= x) xs) ++ (x :: qsort (filter (>= x) xs)))
111+
112+This is because the checker cannot tell that ``filter`` will always
113+produce a value smaller than the pattern ``x :: xs`` for the recursive
114+call to ``qsort``. We can assert that this will always be true as
115+follows:
116+
117+::
118+
119+ total
120+ qsort : Ord a => List a -> List a
121+ qsort [] = []
122+ qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++
123+ (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
124+
125+Syntax in the standard library
126+------------------------------
127+
128+Preorder reasoning
129+~~~~~~~~~~~~~~~~~~
130+
131+This syntax is defined in the module ``Syntax.PreorderReasoning`` in the
132+``base`` package. It provides a syntax for composing proofs of
133+reflexive-transitive relations, using overloadable functions called
134+``step`` and ``qed``. This module also defines ``step`` and ``qed``
135+functions allowing the syntax to be used for demonstrating equality.
136+Here is an example:
137+
138+.. code:: idris
139+
140+ import Syntax.PreorderReasoning
141+ multThree : (a, b, c : Nat) -> a * b * c = c * a * b
142+ multThree a b c =
143+ (a * b * c) ={ sym (multAssociative a b c) }=
144+ (a * (b * c)) ={ cong (multCommutative b c) }=
145+ (a * (c * b)) ={ multAssociative a c b }=
146+ (a * c * b) ={ cong {f = (*b)} (multCommutative a c) }=
147+ (c * a * b) QED
148+
149+Note that the parentheses are required -- only a simple expression can
150+be on the left of ``={ }=`` or ``QED``. Also, when using preorder
151+reasoning syntax to prove things about equality, remember that you can
152+only relate the entire expression, not subexpressions. This might
153+occasionally require the use of ``cong``.
154+
155+Finally, although equality is the most obvious application of preorder
156+reasoning, it can be used for any reflexive-transitive relation.
157+Something like ``step1 ={ just1 }= step2 ={ just2 }= end QED`` is
158+translated to ``(step step1 just1 (step step2 just2 (qed end)))``,
159+selecting the appropriate definitions of ``step`` and ``qed`` through
160+the normal disambiguation process. The standard library, for example,
161+also contains an implementation of preorder reasoning on isomorphisms.
162+
163+Tactics
164+-------
165+
166+Advanced features
167+-----------------
168+
169+'match' application
170+~~~~~~~~~~~~~~~~~~~
171+
172+``ty <== name`` applies the function ``name`` in such a way that it has
173+the type ``ty``, by matching ``ty`` against the function's type. This
174+can be used in proofs, for example:
175+
176+::
177+
178+ plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)
179+ -- Base case
180+ (Z + m = m + Z) <== plus_comm =
181+ rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
182+ (Z + m = m) in refl
183+
184+ -- Step case
185+ (S k + m = m + S k) <== plus_comm =
186+ rewrite ((k + m = m + k) <== plus_comm) in
187+ rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
188+ refl
189+
190+DSL notation
191+~~~~~~~~~~~~
192+
193+Reflection
194+~~~~~~~~~~
195+
196+Including ``%reflection`` functions and ``quoteGoal x by fn in t``,
197+which applies ``fn`` to the expected type of the current expression, and
198+puts the result in ``x`` which is in scope when elaborating ``t``.
199+
200+Type providers
201+~~~~~~~~~~~~~~
202+
203+Experimental features
204+---------------------
205+
206+- Error message reflection
207+- Eliminators
208+- Label types ``'name``
209+
210+Debugging features
211+------------------
212+
213+- ``%logging n``
214+- ``%unifyLog``
docs/reference/misc.rstnew file+82
@@ -0,0 +1,82 @@
1+**************
2+Miscellaneous
3+**************
4+
5+Things we have yet to classify, or are two small to justify their own page.
6+
7+
8+Alternatives
9+============
10+
11+The syntax ``(| x, y, z |)`` means to try elaborating all three options
12+and keep the one that works. This is used, for example, when translating
13+integer literals.
14+
15+::
16+
17+ Idris> the Nat (| "foo", Z, (-3) |)
18+ 0 : Nat
19+
20+"with"-expressions
21+==================
22+
23+The syntax ``with NAME EXPR`` causes members of the namespace ``NAME``
24+to be privileged when resolving overloading. This is particularly useful
25+at the REPL:
26+
27+::
28+
29+ Idris> [1,2,3]
30+ Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Prelude.Vect.::
31+ Idris> with Vect [1,2,3]
32+ [1, 2, 3] : Vect 3 Integer
33+
34+The Unifier Log
35+===============
36+
37+If you're having a hard time debugging why the unifier won't accept
38+something (often while debugging the compiler itself), try applying the
39+special operator ``%unifyLog`` to the expression in question. This will
40+cause the type checker to spit out all sorts of informative messages.
41+
42+
43+
44+Pattern matching on Implicit Arguments
45+======================================
46+
47+Pattern matching is only allowed on implicit arguments when they are
48+referred by name, e.g.
49+
50+.. code:: idris
51+
52+ foo : {n : Nat} -> Nat
53+ foo {n = Z} = Z
54+ foo {n = S k} = k
55+
56+or
57+
58+.. code:: idris
59+
60+ foo : {n : Nat} -> Nat
61+ foo {n = n} = n
62+
63+The latter could be shortened to the following:
64+
65+.. code:: idris
66+
67+ foo : {n : Nat} -> Nat
68+ foo {n} = n
69+
70+That is, ``{x}`` behaves like ``{x=x}``.
71+
72+
73+Existence of an instance
74+========================
75+
76+In order to show that an instance of some typeclass is defined for some
77+type, one could use the ``%instance`` keyword:
78+
79+.. code:: idris
80+
81+ foo : Num Nat
82+ foo = %instance
docs/reference/repl.rst+406−1
@@ -35,7 +35,32 @@ the difference between:
3535Customisation
3636=============
3737
38−Idris has an RC file. Documentation to be added.
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+
3964
4065The ``REPL`` Commands
4166=====================
@@ -123,3 +148,383 @@ The current set of supported commands are:
123148+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
124149|:pp :pprint | <option> <number> <name> | Pretty prints an Idris function in either LaTeX or HTML and for a specified width. |
125150+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
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.
docs/reference/syntax-guide.rstnew file+277
@@ -0,0 +1,277 @@
1+.. _sect-repl:
2+
3+**************
4+Syntax Guide
5+**************
6+
7+Examples are mostly adapted from the Idris tutorial.
8+
9+Variables
10+---------
11+
12+A variable is always defined by defining its type on one line, and its
13+value on the next line, using the syntax
14+
15+::
16+
17+ <id> : <type>
18+ <id> = <value>
19+
20+Examples
21+
22+.. code:: idris
23+
24+ x : Int
25+ x = 100
26+ hello : String
27+ hello = "hello"
28+
29+Types
30+-----
31+
32+In Idris, types are first class values. So a type declaration is the
33+same as just declaration of a variable whose type is ``Type``. In Idris,
34+variables that denote a type must being with a capital letter. Example:
35+
36+.. code:: idris
37+
38+ MyIntType : Type
39+ MyIntType = Int
40+
41+a more interesting example:
42+
43+.. code:: idris
44+
45+ MyListType : Type
46+ MyListType = List Int
47+
48+Data types
49+~~~~~~~~~~
50+
51+Idris provides two kinds of syntax for defining data types. The first,
52+Haskell style syntax, defines a regular algebraic data type. For example
53+
54+.. code:: idris
55+
56+ data Either a b = Left a | Right b
57+
58+or
59+
60+.. code:: idris
61+
62+ data List a = Nil | (::) a (List a)
63+
64+The second, more general kind of data type, is defined using Agda or
65+GADT style syntax. This syntax defines a data type that is parameterized
66+by some values (in the ``Vect`` exampe, a value of type ``Nat`` and a
67+value of type ``Type``).
68+
69+.. code:: idris
70+
71+ data Vect : Nat -> Type -> Type where
72+ Nil : Vect Z a
73+ (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
74+
75+Operators
76+---------
77+
78+Arithmetic
79+~~~~~~~~~~
80+
81+::
82+
83+ x + y
84+ x - y
85+ x * y
86+ x / y
87+ (x * y) + (a / b)
88+
89+Equality and Relational
90+~~~~~~~~~~~~~~~~~~~~~~~
91+
92+::
93+
94+ x == y
95+ x /= y
96+ x >= y
97+ x > y
98+ x <= y
99+ x < y
100+
101+Conditional
102+~~~~~~~~~~~
103+
104+::
105+
106+ x && y
107+ x || y
108+ not x
109+
110+Conditionals
111+------------
112+
113+If Then Else
114+~~~~~~~~~~~~
115+
116+::
117+
118+ if <test> then <true> else <false>
119+
120+Case Expressions
121+~~~~~~~~~~~~~~~~
122+
123+::
124+
125+ case <test> of
126+ <case 1> => <expr>
127+ <case 2> => <expr>
128+ ...
129+ otherwise => <expr>
130+
131+Functions
132+---------
133+
134+Named
135+~~~~~
136+
137+Named functions are defined in the same way as variables, with the type
138+followed by the definition.
139+
140+::
141+
142+ <id> : <argument type> -> <return type>
143+ <id> arg = <expr>
144+
145+Example
146+
147+.. code:: idris
148+
149+ plusOne : Int -> Int
150+ plusOne x = x + 1
151+
152+Functions can also have multiple inputs, for example
153+
154+.. code:: idris
155+
156+ makeHello : String -> String -> String
157+ makeHello first last = "hello, my name is " ++ first ++ " " ++ last
158+
159+Functions can also have named arguments. This is required if you want to
160+annotate parameters in a docstring. The following shows the same
161+``makeHello`` function as above, but with named parameters which are
162+also annotated in the docstring
163+
164+.. code:: idris
165+
166+ ||| Makes a string introducing a person
167+ ||| @first The person's first name
168+ ||| @last The person's last name
169+ makeHello : (first : String) -> (last : String) -> String
170+ makeHello first last = "hello, my name is " ++ first ++ " " ++ last
171+
172+Like Haskell, Idris functions can be defined by pattern matching. For
173+example
174+
175+.. code:: idris
176+
177+ sum : List Int -> Int
178+ sum [] = 0
179+ sum (x :: xs) = x + (sum xs)
180+
181+Similarly case analysis looks like
182+
183+.. code:: idris
184+
185+ answerString : Bool -> String
186+ answerString False = "Wrong answer"
187+ answerString True = "Correct answer"
188+
189+Dependent Functions
190+~~~~~~~~~~~~~~~~~~~
191+
192+Dependent functions are functions where the type of the return value
193+depends on the input value. In order to define a dependent function,
194+named parameters must be used, since the parameter will appear in the
195+return type. For example, consider
196+
197+.. code:: idris
198+
199+ zeros : (n : Nat) -> Vect n Int
200+ zeros Z = []
201+ zeros (S k) = 0 :: (zeros k)
202+
203+In this example, the return type is ``Vect n Int`` which is an
204+expression which depends on the input parameter ``n``. ### Anonymous
205+Arguments in anonymous functions are separated by comma.
206+
207+::
208+
209+ (\x => <expr>)
210+ (\x, y => <expr>)
211+
212+Modifiers
213+~~~~~~~~~
214+
215+Visibility
216+^^^^^^^^^^
217+
218+::
219+
220+ public
221+ abstract
222+ private
223+
224+Totality
225+^^^^^^^^
226+
227+::
228+
229+ total
230+ implicit
231+ partial
232+ covering
233+
234+Options
235+^^^^^^^
236+
237+::
238+
239+ %export
240+ %hint
241+ %no_implicit
242+ %error_handler
243+ %error_reverse
244+ %assert_total
245+ %reflection
246+ %specialise [<name list>]
247+
248+Misc
249+----
250+
251+Comments
252+~~~~~~~~
253+
254+::
255+
256+ -- Single Line
257+ {- Multiline -}
258+ ||| Docstring (goes before definition)
259+
260+Directives
261+----------
262+
263+::
264+
265+ %lib <path>
266+ %link <path>
267+ %flag <path>
268+ %include <path>
269+ %hide <function>
270+ %freeze <name>
271+ %access <accessibility>
272+ %default <totality>
273+ %logging <level 0--11>
274+ %dynamic <list of libs>
275+ %name <list of names>
276+ %error_handlers <list of names>
277+ %language <extension>
docs/reference/theorem-prover.rstnew file+317
@@ -0,0 +1,317 @@
1+*****************************
2+Metavariables and the prover
3+*****************************
4+
5+To list all unproven metavariables, use the command ``:m``. This will
6+display their qualified names and the expected types. To interactively
7+prove a metavariable, use the command ``:p name`` where ``name`` is the
8+metavariable. Once the proof is complete, the command ``:a`` will append
9+it to the current module.
10+
11+Once in the interactive prover, the following commands are available:
12+
13+Basic commands
14+==============
15+
16+- **:q** - Quits the prover (gives up on proving current lemma).
17+- **abandon** - Same as :q
18+- **state** - Displays the current state of the proof.
19+- **term** - Displays the current proof term complete with its
20+ yet-to-be-filled holes (is only really useful for debugging).
21+- **undo** - Undoes the last tactic.
22+- **qed** - Once the interactive theorem prover tells you "No more
23+ goals," you get to type this in celebration! (Completes the proof and
24+ exits the prover)
25+
26+Most common tactics
27+===================
28+
29+- **compute** - Normalizes all terms in the goal (note: does not
30+ normalize assumptions)
31+
32+::
33+
34+ ---------- Goal: ----------
35+ (Vect (S (S Z + (S Z) + (S n))) Nat) -> Vect (S (S (S (S n)))) Nat
36+ -lemma> compute
37+ ---------- Goal: ----------
38+ (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
39+ -lemma>
40+
41+- **exact** - Provide a term of the goal type directly.
42+
43+::
44+
45+ ---------- Goal: ----------
46+ Nat
47+ -lemma> exact Z
48+ lemma: No more goals.
49+ -lemma>
50+
51+- **refine** - Use a name to refine the goal. If the name needs
52+ arguments, introduce them as new goals.
53+
54+- **trivial** - Satisfies the goal using an assumption that matches its
55+ type.
56+
57+::
58+
59+ ---------- Assumptions: ----------
60+ value : Nat
61+ ---------- Goal: ----------
62+ Nat
63+ -lemma> trivial
64+ lemma: No more goals.
65+ -lemma>
66+
67+- **intro** - If your goal is an arrow, turns the left term into an
68+ assumption.
69+
70+::
71+
72+ ---------- Goal: ----------
73+ Nat -> Nat -> Nat
74+ -lemma> intro
75+ ---------- Assumptions: ----------
76+ n : Nat
77+ ---------- Goal: ----------
78+ Nat -> Nat
79+ -lemma>
80+
81+You can also supply your own name for the assumption:
82+
83+::
84+
85+ ---------- Goal: ----------
86+ Nat -> Nat -> Nat
87+ -lemma> intro number
88+ ---------- Assumptions: ----------
89+ number : Nat
90+ ---------- Goal: ----------
91+ Nat -> Nat
92+
93+- **intros** - Exactly like intro, but it operates on all left terms at
94+ once.
95+
96+::
97+
98+ ---------- Goal: ----------
99+ Nat -> Nat -> Nat
100+ -lemma> intros
101+ ---------- Assumptions: ----------
102+ n : Nat
103+ m : Nat
104+ ---------- Goal: ----------
105+ Nat
106+ -lemma>
107+
108+- **let** - Introduces a new assumption; you may use current
109+ assumptions to define the new one.
110+
111+::
112+
113+ ---------- Assumptions: ----------
114+ n : Nat
115+ ---------- Goal: ----------
116+ BigInt
117+ -lemma> let x = toIntegerNat n
118+ ---------- Assumptions: ----------
119+ n : Nat
120+ x = toIntegerNat n: BigInt
121+ ---------- Goal: ----------
122+ BigInt
123+ -lemma>
124+
125+- **rewrite** - Takes an expression with an equality type (x = y), and
126+ replaces all instances of x in the goal with y. Is often useful in
127+ combination with 'sym'.
128+
129+::
130+
131+ ---------- Assumptions: ----------
132+ n : Nat
133+ a : Type
134+ value : Vect Z a
135+ ---------- Goal: ----------
136+ Vect (mult n Z) a
137+ -lemma> rewrite sym (multZeroRightZero n)
138+ ---------- Assumptions: ----------
139+ n : Nat
140+ a : Type
141+ value : Vect Z a
142+ ---------- Goal: ----------
143+ Vect Z a
144+ -lemma>
145+
146+- **induction** - (**Note that this is still experimental** and you may
147+ get strange results and error messages. We are aware of these and
148+ will finish the implementation eventually!) Prove the goal by
149+ induction. Each constructor of the datatype becomes a goal.
150+ Constructors with recursive arguments become induction steps, while
151+ simple constructors become base cases. Note that this only works for
152+ datatypes that have eliminators: a datatype definition must have the
153+ ``%elim`` modifier.
154+
155+Example: To prove associativity of addition on ``Nat``:
156+
157+::
158+
159+ module Foo
160+
161+ plusAssoc : plus n (plus m o) = plus (plus n m) o
162+ plusAssoc = ?rhs
163+
164+we can perform induction on ``n``:
165+
166+::
167+
168+ *Foo> :p rhs
169+ ---------- Goal: ----------
170+ { hole 0 }:
171+ (n : Nat) ->
172+ (m : Nat) ->
173+ (o : Nat) ->
174+ plus n (plus m o) = plus (plus n m) o
175+ -Foo.rhs> intros
176+ ---------- Other goals: ----------
177+ { hole 2 }
178+ { hole 1 }
179+ { hole 0 }
180+ ---------- Assumptions: ----------
181+ n : Nat
182+ m : Nat
183+ o : Nat
184+ ---------- Goal: ----------
185+ { hole 3 }:
186+ plus n (plus m o) = plus (plus n m) o
187+ -Foo.rhs> induction n
188+ ---------- Other goals: ----------
189+ elim_S0
190+ { hole 2 }
191+ { hole 1 }
192+ { hole 0 }
193+ ---------- Assumptions: ----------
194+ n : Nat
195+ m : Nat
196+ o : Nat
197+ ---------- Goal: ----------
198+ elim_Z0:
199+ plus Z (plus m o) = plus (plus Z m) o
200+ -Foo.rhs> compute
201+ ---------- Other goals: ----------
202+ elim_S0
203+ { hole 2 }
204+ { hole 1 }
205+ { hole 0 }
206+ ---------- Assumptions: ----------
207+ n : Nat
208+ m : Nat
209+ o : Nat
210+ ---------- Goal: ----------
211+ elim_Z0:
212+ plus m o = plus m o
213+ -Foo.rhs> trivial
214+ ---------- Other goals: ----------
215+ { hole 2 }
216+ { hole 1 }
217+ { hole 0 }
218+ ---------- Assumptions: ----------
219+ n : Nat
220+ m : Nat
221+ o : Nat
222+ ---------- Goal: ----------
223+ elim_S0:
224+ (n__0 : Nat) ->
225+ (plus n__0 (plus m o) = plus (plus n__0 m) o) ->
226+ plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
227+ -Foo.rhs> intros
228+ ---------- Other goals: ----------
229+ { hole 4 }
230+ elim_S0
231+ { hole 2 }
232+ { hole 1 }
233+ { hole 0 }
234+ ---------- Assumptions: ----------
235+ n : Nat
236+ m : Nat
237+ o : Nat
238+ n__0 : Nat
239+ ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
240+ ---------- Goal: ----------
241+ { hole 5 }:
242+ plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
243+ -Foo.rhs> compute
244+ ---------- Other goals: ----------
245+ { hole 4 }
246+ elim_S0
247+ { hole 2 }
248+ { hole 1 }
249+ { hole 0 }
250+ ---------- Assumptions: ----------
251+ n : Nat
252+ m : Nat
253+ o : Nat
254+ n__0 : Nat
255+ ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
256+ ---------- Goal: ----------
257+ { hole 5 }:
258+ S (plus n__0 (plus m o)) = S (plus (plus n__0 m) o)
259+ -Foo.rhs> rewrite ihn__0
260+ ---------- Other goals: ----------
261+ { hole 5 }
262+ { hole 4 }
263+ elim_S0
264+ { hole 2 }
265+ { hole 1 }
266+ { hole 0 }
267+ ---------- Assumptions: ----------
268+ n : Nat
269+ m : Nat
270+ o : Nat
271+ n__0 : Nat
272+ ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
273+ ---------- Goal: ----------
274+ { hole 6 }:
275+ S (plus n__0 (plus m o)) = S (plus n__0 (plus m o))
276+ -Foo.rhs> trivial
277+ rhs: No more goals.
278+ -Foo.rhs> qed
279+ Proof completed!
280+ Foo.rhs = proof
281+ intros
282+ induction n
283+ compute
284+ trivial
285+ intros
286+ compute
287+ rewrite ihn__0
288+ trivial
289+
290+Two goals were created: one for ``Z`` and one for ``S``.
291+
292+- **sourceLocation** - Solve the current goal with information about
293+ the location in the source code where the tactic was invoked. This is
294+ mostly for embedded DSLs and programmer tools like assertions that
295+ need to know where they are called. See
296+ ``Language.Reflection.SourceLocation`` for more information.
297+
298+Less commonly-used tactics
299+==========================
300+
301+- **applyTactic** - Apply a user-defined tactic. This should be a
302+ function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
303+ the first argument represents the proof context and the second
304+ represents the goal. If your tactic will produce a proof term
305+ directly, use the ``Exact`` constructor from ``Tactic``.
306+- **attack** - ?
307+- **equiv** - Replaces the goal with a new one that is convertible with
308+ the old one
309+- **fill** - ?
310+- **focus** - ?
311+- **mrefine** - Refining by matching against a type
312+- **reflect** - ?
313+- **solve** - Takes a guess with the correct type and fills a hole with
314+ it, closing a proof obligation. This happens automatically in the
315+ interactive prover, so ``solve`` is really only relevant in tactic
316+ scripts used for helping implicit argument resolution.
317+- **try** - ?