git.iko.soy/Idris-dev
on master help sign in
Updates
ab54660Jan de Muijnck-Hughes
docs/faq/faq.rst+3−3
compare with master
unifiedsplit
@@ -108,7 +108,7 @@ the undecidability of the `Halting Problem
108to identify some programs which are definitely terminating. Idris does this
108to identify some programs which are definitely terminating. Idris does this
109using "size change termination" which looks for recursive paths from a
109using "size change termination" which looks for recursive paths from a
110function back to itself. On such a path, there must be at least one
110function 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.
112
112
113- Mutually recursive functions are supported
113- Mutually recursive functions are supported
114- However, all functions on the path must be fully applied. In particular,
114- 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
166IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,
166IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,
167Idris will use that path to find the C compiler.
167Idris will use that path to find the C compiler.
168
168
169−Example:
169+Example::
170−.. code-block::
170+
171 IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
171 IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
172
172
173What does the name ‘Idris’ mean?
173What does the name ‘Idris’ mean?
docs/index.rst+4
@@ -107,6 +107,10 @@ Language Reference
107 reference/ide-protocol
107 reference/ide-protocol
108 reference/semantic-highlighting
108 reference/semantic-highlighting
109 reference/repl
109 reference/repl
110+ reference/theorem-prover
111+ reference/language-features
112+ reference/language-extensions
113+ reference/misc
110
114
111.. _guides:
115.. _guides:
112
116
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
26 erasure
26 erasure
27 semantic-highlighting
27 semantic-highlighting
28 repl
28 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:
35Customisation
35Customisation
36=============
36=============
37
37
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+
39
64
40The ``REPL`` Commands
65The ``REPL`` Commands
41=====================
66=====================
@@ -123,3 +148,383 @@ The current set of supported commands are:
123+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
148+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
124|:pp :pprint | <option> <number> <name> | Pretty prints an Idris function in either LaTeX or HTML and for a specified width. |
149|:pp :pprint | <option> <number> <name> | Pretty prints an Idris function in either LaTeX or HTML and for a specified width. |
125+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
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.
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** - ?