git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2332 from jfdm/doc/lang-reference-update
37119ebJan de Muijnck-Hughes
CHANGELOG+4−2
compare with master
unifiedsplit
@@ -1,5 +1,7 @@
1New in 0.9.19:
1New in 0.9.19:
2--------------
2--------------
3+* The Idris Reference manual has been fleshed out with content originally found
4+ on the GitHub wiki.
3* The Show class has been moved into Prelude.Show and augmented with the method
5* The Show class has been moved into Prelude.Show and augmented with the method
4 showPrec, which allows correct parenthesization of showed terms. This comes
6 showPrec, which allows correct parenthesization of showed terms. This comes
5 with the type Prec of precedences and a few helper functions.
7 with the type Prec of precedences and a few helper functions.
@@ -16,8 +18,8 @@ New in 0.9.18:
16 tested sufficiently, and lack a maintainer)
18 tested sufficiently, and lack a maintainer)
17 + Float has been renamed 'Double' (Float is defined in the Prelude for
19 + Float has been renamed 'Double' (Float is defined in the Prelude for
18 compatibility)
20 compatibility)
19− + Externally defined primitives and operations now supported with
21+ + Externally defined primitives and operations now supported with
20− '%extern' directive, allowing back ends to define their own special
22+ '%extern' directive, allowing back ends to define their own special
21 purpose primitives
23 purpose primitives
22 + Ptr and ManagedPtr have been removed and replaced with external primitives
24 + Ptr and ManagedPtr have been removed and replaced with external primitives
23* Add %hint function annotation, which allows functions to be used as
25* Add %hint function annotation, which allows functions to be used as
docs/faq/faq.rst+3−3
@@ -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/guides/index.rst+1
@@ -19,3 +19,4 @@ Tutorials submitted by community members.
19 :maxdepth: 1
19 :maxdepth: 1
20
20
21 type-providers-ffi
21 type-providers-ffi
22+ theorem-prover
docs/guides/theorem-prover.rstnew file+217
@@ -0,0 +1,217 @@
1+*******************************
2+The Interactive Theorem Prover
3+*******************************
4+
5+This short guide contributed by a community member illustrates how to prove associativity of addition on ``Nat`` using the interactive theorem prover.
6+
7+First we define a module ``Foo.idr``
8+
9+.. code-block:: idris
10+
11+ module Foo
12+
13+ plusAssoc : plus n (plus m o) = plus (plus n m) o
14+ plusAssoc = ?rhs
15+
16+We wish to perform induction on ``n``. First we load the file into the Idris ``REPL`` as follows::
17+
18+ $ idris Foo.idr
19+
20+We will be given the following prompt, in future releases the version string will differ::
21+
22+ ____ __ _
23+ / _/___/ /____(_)____
24+ / // __ / ___/ / ___/ Version 0.9.18.1
25+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
26+ /___/\__,_/_/ /_/____/ Type :? for help
27+
28+ Idris is free software with ABSOLUTELY NO WARRANTY.
29+ For details type :warranty.
30+ Type checking ./Foo.idr
31+ Metavariables: Foo.rhs
32+ *Foo>
33+
34+
35+Explore the Context
36+====================
37+
38+We start the interactive session by asking Idris to prove the
39+metavaraible ``rhs`` using the command ``:p rhs``. Idris by default
40+will show us the initial context. This looks as follows::
41+
42+ *Foo> :p rhs
43+ ---------- Goal: ----------
44+ { hole 0 }:
45+ (n : Nat) ->
46+ (m : Nat) ->
47+ (o : Nat) ->
48+ plus n (plus m o) = plus (plus n m) o
49+
50+Application of Intros
51+=====================
52+
53+We first apply the ``intros`` tactic::
54+
55+ -Foo.rhs> intros
56+ ---------- Other goals: ----------
57+ { hole 2 }
58+ { hole 1 }
59+ { hole 0 }
60+ ---------- Assumptions: ----------
61+ n : Nat
62+ m : Nat
63+ o : Nat
64+ ---------- Goal: ----------
65+ { hole 3 }:
66+ plus n (plus m o) = plus (plus n m) o
67+
68+Induction on ``n``
69+==================
70+
71+Then apply ``induction`` on to ``n``::
72+
73+ -Foo.rhs> induction n
74+ ---------- Other goals: ----------
75+ elim_S0
76+ { hole 2 }
77+ { hole 1 }
78+ { hole 0 }
79+ ---------- Assumptions: ----------
80+ n : Nat
81+ m : Nat
82+ o : Nat
83+ ---------- Goal: ----------
84+ elim_Z0:
85+ plus Z (plus m o) = plus (plus Z m) o
86+
87+
88+Compute
89+=======
90+
91+::
92+
93+ -Foo.rhs> compute
94+ ---------- Other goals: ----------
95+ elim_S0
96+ { hole 2 }
97+ { hole 1 }
98+ { hole 0 }
99+ ---------- Assumptions: ----------
100+ n : Nat
101+ m : Nat
102+ o : Nat
103+ ---------- Goal: ----------
104+ elim_Z0:
105+ plus m o = plus m o
106+
107+Trivial
108+=======
109+
110+::
111+
112+ -Foo.rhs> trivial
113+ ---------- Other goals: ----------
114+ { hole 2 }
115+ { hole 1 }
116+ { hole 0 }
117+ ---------- Assumptions: ----------
118+ n : Nat
119+ m : Nat
120+ o : Nat
121+ ---------- Goal: ----------
122+ elim_S0:
123+ (n__0 : Nat) ->
124+ (plus n__0 (plus m o) = plus (plus n__0 m) o) ->
125+ plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
126+
127+Intros
128+======
129+
130+::
131+
132+ -Foo.rhs> intros
133+ ---------- Other goals: ----------
134+ { hole 4 }
135+ elim_S0
136+ { hole 2 }
137+ { hole 1 }
138+ { hole 0 }
139+ ---------- Assumptions: ----------
140+ n : Nat
141+ m : Nat
142+ o : Nat
143+ n__0 : Nat
144+ ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
145+ ---------- Goal: ----------
146+ { hole 5 }:
147+ plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
148+
149+
150+Compute
151+=======
152+
153+::
154+
155+ -Foo.rhs> compute
156+ ---------- Other goals: ----------
157+ { hole 4 }
158+ elim_S0
159+ { hole 2 }
160+ { hole 1 }
161+ { hole 0 }
162+ ---------- Assumptions: ----------
163+ n : Nat
164+ m : Nat
165+ o : Nat
166+ n__0 : Nat
167+ ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
168+ ---------- Goal: ----------
169+ { hole 5 }:
170+ S (plus n__0 (plus m o)) = S (plus (plus n__0 m) o)
171+
172+
173+Rewrite
174+=======
175+
176+::
177+
178+ -Foo.rhs> rewrite ihn__0
179+ ---------- Other goals: ----------
180+ { hole 5 }
181+ { hole 4 }
182+ elim_S0
183+ { hole 2 }
184+ { hole 1 }
185+ { hole 0 }
186+ ---------- Assumptions: ----------
187+ n : Nat
188+ m : Nat
189+ o : Nat
190+ n__0 : Nat
191+ ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
192+ ---------- Goal: ----------
193+ { hole 6 }:
194+ S (plus n__0 (plus m o)) = S (plus n__0 (plus m o))
195+
196+Trivial
197+=======
198+
199+::
200+
201+ -Foo.rhs> trivial
202+ rhs: No more goals.
203+ -Foo.rhs> qed
204+ Proof completed!
205+ Foo.rhs = proof
206+ intros
207+ induction n
208+ compute
209+ trivial
210+ intros
211+ compute
212+ rewrite ihn__0
213+ trivial
214+
215+Two goals were created: one for ``Z`` and one for ``S``.
216+Here we have proven associativity, and assembled a tactic based proof script.
217+This proof script can be added to ``Foo.idr``.
docs/index.rst+8−1
@@ -105,6 +105,13 @@ Language Reference
105 reference/ffi
105 reference/ffi
106 reference/erasure
106 reference/erasure
107 reference/ide-protocol
107 reference/ide-protocol
108+ reference/semantic-highlighting
109+ reference/repl
110+ reference/tactics
111+ reference/compilation
112+ reference/language-features
113+ reference/language-extensions
114+ reference/misc
108
115
109.. _guides:
116.. _guides:
110
117
@@ -116,4 +123,4 @@ Short Guides
116 :maxdepth: 1
123 :maxdepth: 1
117
124
118 guides/type-providers-ffi
125 guides/type-providers-ffi
119−
126+ guides/theorem-prover
docs/reference/compilation.rstnew file+61
@@ -0,0 +1,61 @@
1+***********************
2+Compilation and Logging
3+***********************
4+
5+
6+This section provides highlights of the Idris compilation process, and
7+provides details over how you can follow the process through logging.
8+
9+Compilation Process
10+===================
11+
12+Idris follows the following compilation process:
13+
14+#. Parsing
15+#. Type Checking
16+
17+ #. Elaboration
18+ #. Coverage
19+ #. Unification
20+ #. Totality Checking
21+ #. Erasure
22+
23+#. Code Generation
24+
25+ #. Defunctionalisation
26+ #. Inlining
27+ #. Resolving variables
28+ #. Code Generation
29+
30+
31+Type Checking Only
32+==================
33+
34+With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either:
35+
36++ The command line options
37+
38+ + ``--check`` for files
39+ + ``--checkpkg`` for packages
40+
41++ The REPL command: ``:check``
42+
43+Use of this option will still result in the generation of the Idris binary ``.ibc`` files, and is suitable if you do not wish to generate code from one of the supported backends.
44+
45+Logging Output
46+==============
47+
48+Logging of the Idris output can be used to diagnose problems with the compilation of your program.
49+Idris supports the logging at various different levels of verbosity: 1 to 10.
50+
51++ Level 0: Show no logging output. Default level
52++ Level 1: High level details of the compilation process.
53++ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: Class, Clauses, Data, Term, and Types,
54++ Level 3: Provides details of compilation of the IRTS, erasue, parsing, case splitting, and further details elaboration of: Instances, Providers, and Values.
55++ Level 4: Provides further details on: Erasure, Coverage Checking, Case splitting, and elaboration of clauses.
56++ Level 5: Provides details on the prover, and further details elaboration (adding declarations) and compilation of the IRTS.
57++ Level 6: Further details elaboration and coverage checking.
58++ Level 7:
59++ Level 8:
60++ Level 9:
61++ Level 10: Further details elaboration.
docs/reference/index.rst+8
@@ -24,3 +24,11 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
24 uniqueness-types
24 uniqueness-types
25 ffi
25 ffi
26 erasure
26 erasure
27+ semantic-highlighting
28+ repl
29+ syntax-guide
30+ tactics
31+ compilation
32+ language-features
33+ language-extensions
34+ 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+54
@@ -0,0 +1,54 @@
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+- Error message reflection
51+- Eliminators
52+- Label types ``'name``
53+- ``%logging n``
54+- ``%unifyLog``
docs/reference/misc.rstnew file+205
@@ -0,0 +1,205 @@
1+**************
2+Miscellaneous
3+**************
4+
5+Things we have yet to classify, or are two small to justify their own page.
6+
7+
8+The Unifier Log
9+===============
10+
11+If you're having a hard time debugging why the unifier won't accept
12+something (often while debugging the compiler itself), try applying the
13+special operator ``%unifyLog`` to the expression in question. This will
14+cause the type checker to spit out all sorts of informative messages.
15+
16+
17+Namespaces and type-directed disambiguation
18+===========================================
19+
20+Names can be defined in separate namespaces, and disambiguated by type.
21+An expression ``with NAME EXPR`` will privilege the namespace ``NAME``
22+in the expression ``EXPR``. For example:
23+
24+::
25+
26+ Idris> with List [[1,2],[3,4],[5,6]]
27+ [[1, 2], [3, 4], [5, 6]] : List (List Integer)
28+
29+ Idris> with Vect [[1,2],[3,4],[5,6]]
30+ [[1, 2], [3, 4], [5, 6]] : Vect 3 (Vect 2 Integer)
31+
32+ Idris> [[1,2],[3,4],[5,6]]
33+ Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Prelude.Vect.::
34+
35+
36+Alternatives
37+============
38+
39+The syntax ``(| option1, option2, option3, ... |)`` type checks each
40+of the options in turn until one of them works. This is used, for
41+example, when translating integer literals.
42+
43+::
44+
45+ Idris> the Nat (| "foo", Z, (-3) |)
46+ 0 : Nat
47+
48+
49+This can also be used to give simple automated proofs, for example: trying
50+some constructors of proofs.
51+
52+::
53+
54+ syntax Trivial = (| oh, refl |)
55+
56+
57+Totality checking assertions
58+============================
59+
60+All definitions are checked for *coverage* (i.e. all well-typed
61+applications are handled) and either for *termination* (i.e. all
62+well-typed applications will eventually produce an answer) or, if
63+returning codata, for productivity (in practice, all recursive calls are
64+constructor guarded).
65+
66+Obviously, termination checking is undecidable. In practice, the
67+termination checker looks for *size change* - every cycle of recursive
68+calls must have a decreasing argument, such as a recursive argument of a
69+strictly positive data type.
70+
71+There are two built-in functions which can be used to give the totality
72+checker a hint:
73+
74+- ``assert_total x`` asserts that the expression ``x`` is terminating
75+ and covering, even if the totality checker cannot tell. This can be
76+ used for example if ``x`` uses a function which does not cover all
77+ inputs, but the caller knows that the specific input is covered.
78+- ``assert_smaller p x`` asserts that the expression ``x`` is
79+ structurally smaller than the pattern ``p``.
80+
81+For example, the following function is not checked as total:
82+
83+::
84+
85+ qsort : Ord a => List a -> List a
86+ qsort [] = []
87+ qsort (x :: xs) = qsort (filter (<= x) xs) ++ (x :: qsort (filter (>= x) xs)))
88+
89+This is because the checker cannot tell that ``filter`` will always
90+produce a value smaller than the pattern ``x :: xs`` for the recursive
91+call to ``qsort``. We can assert that this will always be true as
92+follows:
93+
94+::
95+
96+ total
97+ qsort : Ord a => List a -> List a
98+ qsort [] = []
99+ qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++
100+ (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
101+
102+
103+Preorder reasoning
104+==================
105+
106+This syntax is defined in the module ``Syntax.PreorderReasoning`` in the
107+``base`` package. It provides a syntax for composing proofs of
108+reflexive-transitive relations, using overloadable functions called
109+``step`` and ``qed``. This module also defines ``step`` and ``qed``
110+functions allowing the syntax to be used for demonstrating equality.
111+Here is an example:
112+
113+.. code:: idris
114+
115+ import Syntax.PreorderReasoning
116+ multThree : (a, b, c : Nat) -> a * b * c = c * a * b
117+ multThree a b c =
118+ (a * b * c) ={ sym (multAssociative a b c) }=
119+ (a * (b * c)) ={ cong (multCommutative b c) }=
120+ (a * (c * b)) ={ multAssociative a c b }=
121+ (a * c * b) ={ cong {f = (*b)} (multCommutative a c) }=
122+ (c * a * b) QED
123+
124+Note that the parentheses are required -- only a simple expression can
125+be on the left of ``={ }=`` or ``QED``. Also, when using preorder
126+reasoning syntax to prove things about equality, remember that you can
127+only relate the entire expression, not subexpressions. This might
128+occasionally require the use of ``cong``.
129+
130+Finally, although equality is the most obvious application of preorder
131+reasoning, it can be used for any reflexive-transitive relation.
132+Something like ``step1 ={ just1 }= step2 ={ just2 }= end QED`` is
133+translated to ``(step step1 just1 (step step2 just2 (qed end)))``,
134+selecting the appropriate definitions of ``step`` and ``qed`` through
135+the normal disambiguation process. The standard library, for example,
136+also contains an implementation of preorder reasoning on isomorphisms.
137+
138+
139+Pattern matching on Implicit Arguments
140+======================================
141+
142+Pattern matching is only allowed on implicit arguments when they are
143+referred by name, e.g.
144+
145+.. code:: idris
146+
147+ foo : {n : Nat} -> Nat
148+ foo {n = Z} = Z
149+ foo {n = S k} = k
150+
151+or
152+
153+.. code:: idris
154+
155+ foo : {n : Nat} -> Nat
156+ foo {n = n} = n
157+
158+The latter could be shortened to the following:
159+
160+.. code:: idris
161+
162+ foo : {n : Nat} -> Nat
163+ foo {n} = n
164+
165+That is, ``{x}`` behaves like ``{x=x}``.
166+
167+
168+Existence of an instance
169+========================
170+
171+In order to show that an instance of some typeclass is defined for some
172+type, one could use the ``%instance`` keyword:
173+
174+.. code:: idris
175+
176+ foo : Num Nat
177+ foo = %instance
178+
179+'match' application
180+===================
181+
182+``ty <== name`` applies the function ``name`` in such a way that it has
183+the type ``ty``, by matching ``ty`` against the function's type. This
184+can be used in proofs, for example:
185+
186+::
187+
188+ plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)
189+ -- Base case
190+ (Z + m = m + Z) <== plus_comm =
191+ rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
192+ (Z + m = m) in refl
193+
194+ -- Step case
195+ (S k + m = m + S k) <== plus_comm =
196+ rewrite ((k + m = m + k) <== plus_comm) in
197+ rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
198+ refl
199+
200+Reflection
201+==========
202+
203+Including ``%reflection`` functions and ``quoteGoal x by fn in t``,
204+which applies ``fn`` to the expected type of the current expression, and
205+puts the result in ``x`` which is in scope when elaborating ``t``.
docs/reference/repl.rstnew file+530
@@ -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.
docs/reference/semantic-highlighting.rstnew file+50
@@ -0,0 +1,50 @@
1+****************************************
2+Semantic Highlighting & Pretty Printing
3+****************************************
4+
5+Since ``v0.9.18`` Idris comes with support for semantic highlighting.
6+When using the ``REPL`` or IDE support, Idris will highlight your code accordingly to its meaning within the Idris structure. A precursor to semantic highlighting support is the pretty printing of definitions to console, LaTeX, or HTML.
7+
8+The default styling scheme used was inspired by Connor McBride's own set of stylings, informally known as *Connor's Colours*.
9+
10+
11+Legend
12+======
13+
14+The concepts and their default stylings are as follows:
15+
16++----------------+---------------+----------------+----------------+
17+| Idris Term | HTML | LaTeX | IDE/REPL |
18++================+===============+================+================+
19+| Bound Variable | Purple | Magenta | |
20++----------------+---------------+----------------+----------------+
21+| Keyword | Bold | Underlined | |
22++----------------+---------------+----------------+----------------+
23+| Function | Green | Green | |
24++----------------+---------------+----------------+----------------+
25+| Type | Blue | Blue | |
26++----------------+---------------+----------------+----------------+
27+| Data | Red | Red | |
28++----------------+---------------+----------------+----------------+
29+| Implicit | Italic Purple | Italic Magenta | |
30++----------------+---------------+----------------+----------------+
31+
32+Pretty Printing
33+===============
34+
35+Idris also supports the pretty printing of code to HTML and LaTeX using the commands:
36+
37++ ``:pp <latex|html> <width> <function name>``
38++ ``:pprint <latex|html> <width> <function name>``
39+
40+
41+Customisation
42+=============
43+
44+If you are not happy with the colours used. The VIM and Emacs editor support allows for customisation of the colours used. When pretty printing Idris code as LaTeX and HTML, commands and a CSS style are provided. The colours used by the REPL can be customised through the initialisation script.
45+
46+
47+Further Information
48+===================
49+
50+Please also see the `Idris Extras <https://github.com/idris-hackers/idris-extras>`_ project for links to editor support, and pre-made style files for LaTeX and HTML.
docs/reference/syntax-guide.rstnew file+275
@@ -0,0 +1,275 @@
1+**************
2+Syntax Guide
3+**************
4+
5+Examples are mostly adapted from the Idris tutorial.
6+
7+Variables
8+---------
9+
10+A variable is always defined by defining its type on one line, and its
11+value on the next line, using the syntax
12+
13+::
14+
15+ <id> : <type>
16+ <id> = <value>
17+
18+Examples
19+
20+.. code:: idris
21+
22+ x : Int
23+ x = 100
24+ hello : String
25+ hello = "hello"
26+
27+Types
28+-----
29+
30+In Idris, types are first class values. So a type declaration is the
31+same as just declaration of a variable whose type is ``Type``. In Idris,
32+variables that denote a type must being with a capital letter. Example:
33+
34+.. code:: idris
35+
36+ MyIntType : Type
37+ MyIntType = Int
38+
39+a more interesting example:
40+
41+.. code:: idris
42+
43+ MyListType : Type
44+ MyListType = List Int
45+
46+Data types
47+~~~~~~~~~~
48+
49+Idris provides two kinds of syntax for defining data types. The first,
50+Haskell style syntax, defines a regular algebraic data type. For example
51+
52+.. code:: idris
53+
54+ data Either a b = Left a | Right b
55+
56+or
57+
58+.. code:: idris
59+
60+ data List a = Nil | (::) a (List a)
61+
62+The second, more general kind of data type, is defined using Agda or
63+GADT style syntax. This syntax defines a data type that is parameterized
64+by some values (in the ``Vect`` exampe, a value of type ``Nat`` and a
65+value of type ``Type``).
66+
67+.. code:: idris
68+
69+ data Vect : Nat -> Type -> Type where
70+ Nil : Vect Z a
71+ (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
72+
73+Operators
74+---------
75+
76+Arithmetic
77+~~~~~~~~~~
78+
79+::
80+
81+ x + y
82+ x - y
83+ x * y
84+ x / y
85+ (x * y) + (a / b)
86+
87+Equality and Relational
88+~~~~~~~~~~~~~~~~~~~~~~~
89+
90+::
91+
92+ x == y
93+ x /= y
94+ x >= y
95+ x > y
96+ x <= y
97+ x < y
98+
99+Conditional
100+~~~~~~~~~~~
101+
102+::
103+
104+ x && y
105+ x || y
106+ not x
107+
108+Conditionals
109+------------
110+
111+If Then Else
112+~~~~~~~~~~~~
113+
114+::
115+
116+ if <test> then <true> else <false>
117+
118+Case Expressions
119+~~~~~~~~~~~~~~~~
120+
121+::
122+
123+ case <test> of
124+ <case 1> => <expr>
125+ <case 2> => <expr>
126+ ...
127+ otherwise => <expr>
128+
129+Functions
130+---------
131+
132+Named
133+~~~~~
134+
135+Named functions are defined in the same way as variables, with the type
136+followed by the definition.
137+
138+::
139+
140+ <id> : <argument type> -> <return type>
141+ <id> arg = <expr>
142+
143+Example
144+
145+.. code:: idris
146+
147+ plusOne : Int -> Int
148+ plusOne x = x + 1
149+
150+Functions can also have multiple inputs, for example
151+
152+.. code:: idris
153+
154+ makeHello : String -> String -> String
155+ makeHello first last = "hello, my name is " ++ first ++ " " ++ last
156+
157+Functions can also have named arguments. This is required if you want to
158+annotate parameters in a docstring. The following shows the same
159+``makeHello`` function as above, but with named parameters which are
160+also annotated in the docstring
161+
162+.. code:: idris
163+
164+ ||| Makes a string introducing a person
165+ ||| @first The person's first name
166+ ||| @last The person's last name
167+ makeHello : (first : String) -> (last : String) -> String
168+ makeHello first last = "hello, my name is " ++ first ++ " " ++ last
169+
170+Like Haskell, Idris functions can be defined by pattern matching. For
171+example
172+
173+.. code:: idris
174+
175+ sum : List Int -> Int
176+ sum [] = 0
177+ sum (x :: xs) = x + (sum xs)
178+
179+Similarly case analysis looks like
180+
181+.. code:: idris
182+
183+ answerString : Bool -> String
184+ answerString False = "Wrong answer"
185+ answerString True = "Correct answer"
186+
187+Dependent Functions
188+~~~~~~~~~~~~~~~~~~~
189+
190+Dependent functions are functions where the type of the return value
191+depends on the input value. In order to define a dependent function,
192+named parameters must be used, since the parameter will appear in the
193+return type. For example, consider
194+
195+.. code:: idris
196+
197+ zeros : (n : Nat) -> Vect n Int
198+ zeros Z = []
199+ zeros (S k) = 0 :: (zeros k)
200+
201+In this example, the return type is ``Vect n Int`` which is an
202+expression which depends on the input parameter ``n``. ### Anonymous
203+Arguments in anonymous functions are separated by comma.
204+
205+::
206+
207+ (\x => <expr>)
208+ (\x, y => <expr>)
209+
210+Modifiers
211+~~~~~~~~~
212+
213+Visibility
214+^^^^^^^^^^
215+
216+::
217+
218+ public
219+ abstract
220+ private
221+
222+Totality
223+^^^^^^^^
224+
225+::
226+
227+ total
228+ implicit
229+ partial
230+ covering
231+
232+Options
233+^^^^^^^
234+
235+::
236+
237+ %export
238+ %hint
239+ %no_implicit
240+ %error_handler
241+ %error_reverse
242+ %assert_total
243+ %reflection
244+ %specialise [<name list>]
245+
246+Misc
247+----
248+
249+Comments
250+~~~~~~~~
251+
252+::
253+
254+ -- Single Line
255+ {- Multiline -}
256+ ||| Docstring (goes before definition)
257+
258+Directives
259+----------
260+
261+::
262+
263+ %lib <path>
264+ %link <path>
265+ %flag <path>
266+ %include <path>
267+ %hide <function>
268+ %freeze <name>
269+ %access <accessibility>
270+ %default <totality>
271+ %logging <level 0--11>
272+ %dynamic <list of libs>
273+ %name <list of names>
274+ %error_handlers <list of names>
275+ %language <extension>
docs/reference/tactics.rstnew file+213
@@ -0,0 +1,213 @@
1+***************************
2+Tactics and Theorem Proving
3+***************************
4+
5+Idris supports interactive theorem proving, and theh analyse of
6+context through metavariables. To list all unproven metavariables,
7+use the command ``:m``. This will display their qualified names and
8+the expected types. To interactively prove a metavariable, use the
9+command ``:p name`` where ``name`` is the metavariable. Once the proof
10+is complete, the command ``:a`` will append it to the current module.
11+
12+Once in the interactive prover, the following commands are available:
13+
14+Basic commands
15+==============
16+
17+- ``:q`` - Quits the prover (gives up on proving current lemma).
18+- ``abandon`` - Same as :q
19+- ``state`` - Displays the current state of the proof.
20+- ``term`` - Displays the current proof term complete with its
21+ yet-to-be-filled holes (is only really useful for debugging).
22+- ``undo`` - Undoes the last tactic.
23+- ``qed`` - Once the interactive theorem prover tells you "No more
24+ goals," you get to type this in celebration! (Completes the proof and
25+ exits the prover)
26+
27+Commonly Used Tactics
28+=====================
29+
30+Compute
31+-------
32+
33+- ``compute`` - Normalizes all terms in the goal (note: does not
34+ normalize assumptions)
35+
36+::
37+
38+ ---------- Goal: ----------
39+ (Vect (S (S Z + (S Z) + (S n))) Nat) -> Vect (S (S (S (S n)))) Nat
40+ -lemma> compute
41+ ---------- Goal: ----------
42+ (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
43+ -lemma>
44+
45+Exact
46+-----
47+
48+- ``exact`` - Provide a term of the goal type directly.
49+
50+::
51+
52+ ---------- Goal: ----------
53+ Nat
54+ -lemma> exact Z
55+ lemma: No more goals.
56+ -lemma>
57+
58+Refine
59+------
60+
61+- ``refine`` - Use a name to refine the goal. If the name needs
62+ arguments, introduce them as new goals.
63+
64+Trivial
65+-------
66+
67+- ``trivial`` - Satisfies the goal using an assumption that matches its
68+ type.
69+
70+::
71+
72+ ---------- Assumptions: ----------
73+ value : Nat
74+ ---------- Goal: ----------
75+ Nat
76+ -lemma> trivial
77+ lemma: No more goals.
78+ -lemma>
79+
80+Intro
81+-----
82+
83+- ``intro`` - If your goal is an arrow, turns the left term into an
84+ assumption.
85+
86+::
87+
88+ ---------- Goal: ----------
89+ Nat -> Nat -> Nat
90+ -lemma> intro
91+ ---------- Assumptions: ----------
92+ n : Nat
93+ ---------- Goal: ----------
94+ Nat -> Nat
95+ -lemma>
96+
97+You can also supply your own name for the assumption:
98+
99+::
100+
101+ ---------- Goal: ----------
102+ Nat -> Nat -> Nat
103+ -lemma> intro number
104+ ---------- Assumptions: ----------
105+ number : Nat
106+ ---------- Goal: ----------
107+ Nat -> Nat
108+
109+
110+Intros
111+------
112+
113+- ``intros`` - Exactly like intro, but it operates on all left terms at
114+ once.
115+
116+::
117+
118+ ---------- Goal: ----------
119+ Nat -> Nat -> Nat
120+ -lemma> intros
121+ ---------- Assumptions: ----------
122+ n : Nat
123+ m : Nat
124+ ---------- Goal: ----------
125+ Nat
126+ -lemma>
127+
128+let
129+---
130+
131+- ``let`` - Introduces a new assumption; you may use current
132+ assumptions to define the new one.
133+
134+::
135+
136+ ---------- Assumptions: ----------
137+ n : Nat
138+ ---------- Goal: ----------
139+ BigInt
140+ -lemma> let x = toIntegerNat n
141+ ---------- Assumptions: ----------
142+ n : Nat
143+ x = toIntegerNat n: BigInt
144+ ---------- Goal: ----------
145+ BigInt
146+ -lemma>
147+
148+rewrite
149+-------
150+
151+- ``rewrite`` - Takes an expression with an equality type (x = y), and
152+ replaces all instances of x in the goal with y. Is often useful in
153+ combination with 'sym'.
154+
155+::
156+
157+ ---------- Assumptions: ----------
158+ n : Nat
159+ a : Type
160+ value : Vect Z a
161+ ---------- Goal: ----------
162+ Vect (mult n Z) a
163+ -lemma> rewrite sym (multZeroRightZero n)
164+ ---------- Assumptions: ----------
165+ n : Nat
166+ a : Type
167+ value : Vect Z a
168+ ---------- Goal: ----------
169+ Vect Z a
170+ -lemma>
171+
172+induction
173+---------
174+
175+- ``induction`` - (``Note that this is still experimental`` and you may
176+ get strange results and error messages. We are aware of these and
177+ will finish the implementation eventually!) Prove the goal by
178+ induction. Each constructor of the datatype becomes a goal.
179+ Constructors with recursive arguments become induction steps, while
180+ simple constructors become base cases. Note that this only works for
181+ datatypes that have eliminators: a datatype definition must have the
182+ ``%elim`` modifier.
183+
184+
185+sourceLocation
186+--------------
187+
188+- ``sourceLocation`` - Solve the current goal with information about
189+ the location in the source code where the tactic was invoked. This is
190+ mostly for embedded DSLs and programmer tools like assertions that
191+ need to know where they are called. See
192+ ``Language.Reflection.SourceLocation`` for more information.
193+
194+Less commonly-used tactics
195+==========================
196+
197+- ``applyTactic`` - Apply a user-defined tactic. This should be a
198+ function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
199+ the first argument represents the proof context and the second
200+ represents the goal. If your tactic will produce a proof term
201+ directly, use the ``Exact`` constructor from ``Tactic``.
202+- ``attack`` - ?
203+- ``equiv`` - Replaces the goal with a new one that is convertible with
204+ the old one
205+- ``fill`` - ?
206+- ``focus`` - ?
207+- ``mrefine`` - Refining by matching against a type
208+- ``reflect`` - ?
209+- ``solve`` - Takes a guess with the correct type and fills a hole with
210+ it, closing a proof obligation. This happens automatically in the
211+ interactive prover, so ``solve`` is really only relevant in tactic
212+ scripts used for helping implicit argument resolution.
213+- ``try`` - ?