ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 14:38:20 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #2332 from jfdm/doc/lang-reference-update

Browse Source 
Reference Manual Improvements
This commit is contained in:
Jan de Muijnck-Hughes 2015-06-01 11:26:05 +01:00
commit 37119ebbd9
14 changed files with 1665 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
CHANGELOG
View File

@ -1,5 +1,7 @@
New in 0.9.19:
--------------
* The Idris Reference manual has been fleshed out with content originally found
on the GitHub wiki.
* The Show class has been moved into Prelude.Show and augmented with the method
showPrec, which allows correct parenthesization of showed terms. This comes
with the type Prec of precedences and a few helper functions.
@ -16,8 +18,8 @@ New in 0.9.18:
tested sufficiently, and lack a maintainer)
+ Float has been renamed 'Double' (Float is defined in the Prelude for
compatibility)
+ Externally defined primitives and operations now supported with
'%extern' directive, allowing back ends to define their own special
+ Externally defined primitives and operations now supported with
'%extern' directive, allowing back ends to define their own special
purpose primitives
+ Ptr and ManagedPtr have been removed and replaced with external primitives
* Add %hint function annotation, which allows functions to be used as

6
docs/faq/faq.rst
View File

@ -108,7 +108,7 @@ the undecidability of the `Halting Problem
to identify some programs which are definitely terminating. Idris does this
using "size change termination" which looks for recursive paths from a
function back to itself. On such a path, there must be at least one
argument which converges to a base case.
argument which converges to a base case.
- Mutually recursive functions are supported
- 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
IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,
Idris will use that path to find the C compiler.
Example:
.. code-block::
Example::
IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
What does the name ‘Idris’ mean?

1
docs/guides/index.rst
View File

@ -19,3 +19,4 @@ Tutorials submitted by community members.
:maxdepth: 1
type-providers-ffi
theorem-prover

217
docs/guides/theorem-prover.rst Normal file
View File

@ -0,0 +1,217 @@
*******************************
The Interactive Theorem Prover
*******************************
This short guide contributed by a community member illustrates how to prove associativity of addition on ``Nat`` using the interactive theorem prover.
First we define a module ``Foo.idr``
.. code-block:: idris
module Foo
plusAssoc : plus n (plus m o) = plus (plus n m) o
plusAssoc = ?rhs
We wish to perform induction on ``n``. First we load the file into the Idris ``REPL`` as follows::
$ idris Foo.idr
We will be given the following prompt, in future releases the version string will differ::
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.18.1
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Type checking ./Foo.idr
Metavariables: Foo.rhs
*Foo>
Explore the Context
====================
We start the interactive session by asking Idris to prove the
metavaraible ``rhs`` using the command ``:p rhs``. Idris by default
will show us the initial context. This looks as follows::
*Foo> :p rhs
---------- Goal: ----------
{ hole 0 }:
(n : Nat) ->
(m : Nat) ->
(o : Nat) ->
plus n (plus m o) = plus (plus n m) o
Application of Intros
=====================
We first apply the ``intros`` tactic::
-Foo.rhs> intros
---------- Other goals: ----------
{ hole 2 }
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
n : Nat
m : Nat
o : Nat
---------- Goal: ----------
{ hole 3 }:
plus n (plus m o) = plus (plus n m) o
Induction on ``n``
==================
Then apply ``induction`` on to ``n``::
-Foo.rhs> induction n
---------- Other goals: ----------
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
n : Nat
m : Nat
o : Nat
---------- Goal: ----------
elim_Z0:
plus Z (plus m o) = plus (plus Z m) o
Compute
=======
::
-Foo.rhs> compute
---------- Other goals: ----------
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
n : Nat
m : Nat
o : Nat
---------- Goal: ----------
elim_Z0:
plus m o = plus m o
Trivial
=======
::
-Foo.rhs> trivial
---------- Other goals: ----------
{ hole 2 }
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
n : Nat
m : Nat
o : Nat
---------- Goal: ----------
elim_S0:
(n__0 : Nat) ->
(plus n__0 (plus m o) = plus (plus n__0 m) o) ->
plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
Intros
======
::
-Foo.rhs> intros
---------- Other goals: ----------
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
n : Nat
m : Nat
o : Nat
n__0 : Nat
ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
---------- Goal: ----------
{ hole 5 }:
plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
Compute
=======
::
-Foo.rhs> compute
---------- Other goals: ----------
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
n : Nat
m : Nat
o : Nat
n__0 : Nat
ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
---------- Goal: ----------
{ hole 5 }:
S (plus n__0 (plus m o)) = S (plus (plus n__0 m) o)
Rewrite
=======
::
-Foo.rhs> rewrite ihn__0
---------- Other goals: ----------
{ hole 5 }
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
n : Nat
m : Nat
o : Nat
n__0 : Nat
ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
---------- Goal: ----------
{ hole 6 }:
S (plus n__0 (plus m o)) = S (plus n__0 (plus m o))
Trivial
=======
::
-Foo.rhs> trivial
rhs: No more goals.
-Foo.rhs> qed
Proof completed!
Foo.rhs = proof
intros
induction n
compute
trivial
intros
compute
rewrite ihn__0
trivial
Two goals were created: one for ``Z`` and one for ``S``.
Here we have proven associativity, and assembled a tactic based proof script.
This proof script can be added to ``Foo.idr``.

9
docs/index.rst
View File

@ -105,6 +105,13 @@ Language Reference
reference/ffi
reference/erasure
reference/ide-protocol
reference/semantic-highlighting
reference/repl
reference/tactics
reference/compilation
reference/language-features
reference/language-extensions
reference/misc
.. _guides:
@ -116,4 +123,4 @@ Short Guides
:maxdepth: 1
guides/type-providers-ffi
guides/theorem-prover

61
docs/reference/compilation.rst Normal file
View File

@ -0,0 +1,61 @@
***********************
Compilation and Logging
***********************
This section provides highlights of the Idris compilation process, and
provides details over how you can follow the process through logging.
Compilation Process
===================
Idris follows the following compilation process:
#. Parsing
#. Type Checking
#. Elaboration
#. Coverage
#. Unification
#. Totality Checking
#. Erasure
#. Code Generation
#. Defunctionalisation
#. Inlining
#. Resolving variables
#. Code Generation
Type Checking Only
==================
With Idris you can ask it to terminate the compilation process after type checking has completed. This is achieved through use of either:
+ The command line options
+ ``--check`` for files
+ ``--checkpkg`` for packages
+ The REPL command: ``:check``
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.
Logging Output
==============
Logging of the Idris output can be used to diagnose problems with the compilation of your program.
Idris supports the logging at various different levels of verbosity: 1 to 10.
+ Level 0: Show no logging output. Default level
+ Level 1: High level details of the compilation process.
+ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: Class, Clauses, Data, Term, and Types,
+ Level 3: Provides details of compilation of the IRTS, erasue, parsing, case splitting, and further details elaboration of: Instances, Providers, and Values.
+ Level 4: Provides further details on: Erasure, Coverage Checking, Case splitting, and elaboration of clauses.
+ Level 5: Provides details on the prover, and further details elaboration (adding declarations) and compilation of the IRTS.
+ Level 6: Further details elaboration and coverage checking.
+ Level 7:
+ Level 8:
+ Level 9:
+ Level 10: Further details elaboration.

8
docs/reference/index.rst
View File

@ -24,3 +24,11 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
uniqueness-types
ffi
erasure
semantic-highlighting
repl
syntax-guide
tactics
compilation
language-features
language-extensions
misc

36
docs/reference/language-extensions.rst Normal file
View File

@ -0,0 +1,36 @@
*******************
Language Extensions
*******************
Type Providers
===============
Idris type providers are a way to get the type system to reflect
observations about the world outside of Idris. Similarly to `F# type
providers <http://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
they cause effectful computations to run during type checking, returning
information that the type checker can use when checking the rest of the
program. While F# type providers are based on code generation, Idris
type providers use only the ordinary execution semantics of Idris to
generate the information.
A type provider is simply a term of type ``IO (Provider t)``, where
``Provider`` is a data type with constructors for a successful result
and an error. The type ``t`` can be either ``Type`` (the type of types)
or a concrete type. Then, a type provider ``p`` is invoked using the
syntax ``%provide (x : t) with p``. When the type checker encounters
this line, the IO action ``p`` is executed. Then, the resulting term is
extracted from the IO monad. If it is ``Provide y`` for some ``y : t``,
then ``x`` is bound to ``y`` for the remainder of typechecking and in
the compiled code. If execution fails, a generic error is reported and
type checking terminates. If the resulting term is ``Error e`` for some
string ``e``, then type checking fails and the error ``e`` is reported
to the user.
Example Idris type providers can be seen at `this
repository <https://github.com/david-christiansen/idris-type-providers>`__.
More detailed descriptions are available in David Christiansen's `WGP
'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.

54
docs/reference/language-features.rst Normal file
View File

@ -0,0 +1,54 @@
**********************
Core Language Features
**********************
- Full-spectrum dependent types
- Strict evaluation (plus ``Lazy : Type -> Type`` type constructor for
explicit laziness)
- Lambda, Pi (forall), Let bindings
- Pattern matching definitions
- Export modifiers ``public``, ``abstract``, ``private``
- Function options ``partial``, ``total``
- ``where`` clauses
- "magic with"
- Implicit arguments (in top level types)
- "Bound" implicit arguments ``{n : Nat} -> {a : Type} -> Vect n a``
- "Unbound" implicit arguments --- ``Vect n a`` is equivalent to the
above in a type, ``n`` and ``a`` are implicitly bound. This applies
to names beginning with a lower case letter in an argument position.
- 'Tactic' implicit arguments, which are solved by running a tactic
script or giving a default argument, rather than by unification.
- Unit type ``()``, empty type ``Void``
- Tuples (desugaring to nested pairs)
- Dependent pair syntax ``(x : T ** P x)`` (there exists an ``x`` of
type ``T`` such that ``P x``)
- Inline ``case`` expressions
- Heterogeneous equality
- ``do`` notation
- Idiom brackets
- Type classes, suppoting default methods and dependencies between
methods
- ``rewrite`` prf ``in`` expr
- Metavariables
- Inline proof/tactic scripts
- Implicit coercion
- ``codata``
- Also ``Inf : Type -> Type`` type constructor for mixed data/codata.
In fact ``codata`` is implemented by putting recusive arguments under
``Inf``.
- ``syntax`` rules for defining pattern and term syntactic sugar
- these are used in the standard library to define
``if ... then ... else`` expressions and an Agda-style preorder
reasoning syntax.
- `Uniqueness
typing <https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Types>`__
using the ``UniqueType`` universe.
- `Partial
evaluation <https://github.com/idris-lang/Idris-dev/wiki/Static-Arguments-and-Partial-Evaluation>`__
by ``[static]`` argument annotations.
- Error message reflection
- Eliminators
- Label types ``'name``
- ``%logging n``
- ``%unifyLog``

205
docs/reference/misc.rst Normal file
View File

@ -0,0 +1,205 @@
**************
Miscellaneous
**************
Things we have yet to classify, or are two small to justify their own page.
The Unifier Log
===============
If you're having a hard time debugging why the unifier won't accept
something (often while debugging the compiler itself), try applying the
special operator ``%unifyLog`` to the expression in question. This will
cause the type checker to spit out all sorts of informative messages.
Namespaces and type-directed disambiguation
===========================================
Names can be defined in separate namespaces, and disambiguated by type.
An expression ``with NAME EXPR`` will privilege the namespace ``NAME``
in the expression ``EXPR``. For example:
::
Idris> with List [[1,2],[3,4],[5,6]]
[[1, 2], [3, 4], [5, 6]] : List (List Integer)
Idris> with Vect [[1,2],[3,4],[5,6]]
[[1, 2], [3, 4], [5, 6]] : Vect 3 (Vect 2 Integer)
Idris> [[1,2],[3,4],[5,6]]
Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Prelude.Vect.::
Alternatives
============
The syntax ``(| option1, option2, option3, ... |)`` type checks each
of the options in turn until one of them works. This is used, for
example, when translating integer literals.
::
Idris> the Nat (| "foo", Z, (-3) |)
0 : Nat
This can also be used to give simple automated proofs, for example: trying
some constructors of proofs.
::
syntax Trivial = (| oh, refl |)
Totality checking assertions
============================
All definitions are checked for *coverage* (i.e. all well-typed
applications are handled) and either for *termination* (i.e. all
well-typed applications will eventually produce an answer) or, if
returning codata, for productivity (in practice, all recursive calls are
constructor guarded).
Obviously, termination checking is undecidable. In practice, the
termination checker looks for *size change* - every cycle of recursive
calls must have a decreasing argument, such as a recursive argument of a
strictly positive data type.
There are two built-in functions which can be used to give the totality
checker a hint:
- ``assert_total x`` asserts that the expression ``x`` is terminating
and covering, even if the totality checker cannot tell. This can be
used for example if ``x`` uses a function which does not cover all
inputs, but the caller knows that the specific input is covered.
- ``assert_smaller p x`` asserts that the expression ``x`` is
structurally smaller than the pattern ``p``.
For example, the following function is not checked as total:
::
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs) = qsort (filter (<= x) xs) ++ (x :: qsort (filter (>= x) xs)))
This is because the checker cannot tell that ``filter`` will always
produce a value smaller than the pattern ``x :: xs`` for the recursive
call to ``qsort``. We can assert that this will always be true as
follows:
::
total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++
(x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
Preorder reasoning
==================
This syntax is defined in the module ``Syntax.PreorderReasoning`` in the
``base`` package. It provides a syntax for composing proofs of
reflexive-transitive relations, using overloadable functions called
``step`` and ``qed``. This module also defines ``step`` and ``qed``
functions allowing the syntax to be used for demonstrating equality.
Here is an example:
.. code:: idris
import Syntax.PreorderReasoning
multThree : (a, b, c : Nat) -> a * b * c = c * a * b
multThree a b c =
(a * b * c) ={ sym (multAssociative a b c) }=
(a * (b * c)) ={ cong (multCommutative b c) }=
(a * (c * b)) ={ multAssociative a c b }=
(a * c * b) ={ cong {f = (*b)} (multCommutative a c) }=
(c * a * b) QED
Note that the parentheses are required -- only a simple expression can
be on the left of ``={ }=`` or ``QED``. Also, when using preorder
reasoning syntax to prove things about equality, remember that you can
only relate the entire expression, not subexpressions. This might
occasionally require the use of ``cong``.
Finally, although equality is the most obvious application of preorder
reasoning, it can be used for any reflexive-transitive relation.
Something like ``step1 ={ just1 }= step2 ={ just2 }= end QED`` is
translated to ``(step step1 just1 (step step2 just2 (qed end)))``,
selecting the appropriate definitions of ``step`` and ``qed`` through
the normal disambiguation process. The standard library, for example,
also contains an implementation of preorder reasoning on isomorphisms.
Pattern matching on Implicit Arguments
======================================
Pattern matching is only allowed on implicit arguments when they are
referred by name, e.g.
.. code:: idris
foo : {n : Nat} -> Nat
foo {n = Z} = Z
foo {n = S k} = k
or
.. code:: idris
foo : {n : Nat} -> Nat
foo {n = n} = n
The latter could be shortened to the following:
.. code:: idris
foo : {n : Nat} -> Nat
foo {n} = n
That is, ``{x}`` behaves like ``{x=x}``.
Existence of an instance
========================
In order to show that an instance of some typeclass is defined for some
type, one could use the ``%instance`` keyword:
.. code:: idris
foo : Num Nat
foo = %instance
'match' application
===================
``ty <== name`` applies the function ``name`` in such a way that it has
the type ``ty``, by matching ``ty`` against the function's type. This
can be used in proofs, for example:
::
plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)
-- Base case
(Z + m = m + Z) <== plus_comm =
rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
(Z + m = m) in refl
-- Step case
(S k + m = m + S k) <== plus_comm =
rewrite ((k + m = m + k) <== plus_comm) in
rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
refl
Reflection
==========
Including ``%reflection`` functions and ``quoteGoal x by fn in t``,
which applies ``fn`` to the expected type of the current expression, and
puts the result in ``x`` which is in scope when elaborating ``t``.

530
docs/reference/repl.rst Normal file
View File

@ -0,0 +1,530 @@
.. _sect-repl:
**************
The Idris REPL
**************
Idris comes with a ``REPL``.
Evaluation
==========
Being a fully dependently typed language, Idris has two phases where it
evaluates things, compile-time and run-time. At compile-time it will only
evaluate things which it knows to be total (i.e. terminating and covering all
possible inputs) in order to keep type checking decidable. The compile-time
evaluator is part of the Idris kernel, and is implemented in Haskell using a
HOAS (higher order abstract syntax) style representation of values. Since
everything is known to have a normal form here, the evaluation strategy doesn't
actually matter because either way it will get the same answer, and in practice
it will do whatever the Haskell run-time system chooses to do.
The REPL, for convenience, uses the compile-time notion of evaluation. As well
as being easier to implement (because we have the evaluator available) this can
be very useful to show how terms evaluate in the type checker. So you can see
the difference between:
.. code-block:: idris
Idris> \n, m => (S n) + m
\n => \m => S (plus n m) : Nat -> Nat -> Nat
Idris> \n, m => n + (S m)
\n => \m => plus n (S m) : Nat -> Nat -> Nat
Customisation
=============
Idris supports initialisation scripts.
Initialisation scripts
~~~~~~~~~~~~~~~~~~~~~~
When the Idris REPL starts up, it will attempt to open the file
repl/init in Idris's application data directory. The application data
directory is the result of the Haskell function call
``getAppUserDataDirectory "idris"``, which on most Unix-like systems
will return $HOME/.idris and on various versions of Windows will return
paths such as ``C:/Documents And Settings/user/Application Data/appName``.
The file repl/init is a newline-separate list of REPL commands. Not all
commands are supported in initialisation scripts — only the subset that
will not interfere with the normal operation of the REPL. In particular,
setting colours, display options such as showing implicits, and log
levels are supported.
Example initialisation script
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
::
:colour prompt white italic bold
:colour implicit magenta italic
The ``REPL`` Commands
=====================
The current set of supported commands are:
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|Command | Arguments | Purpose |
+================+==============================+==========================================================================================================+
|<expr> | | Evaluate an expression |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:t :type | <expr> | Check the type of an expression |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:core | <expr> | View the core language representation of a term |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:miss :missing | <name> | Show missing clauses |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:doc | <name> | Show internal documentation |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:mkdoc | <namespace> | Generate IdrisDoc for namespace(s) and dependencies |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:apropos | [<package list>] <name> | Search names, types, and documentation |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:s :search | [<package list>] <expr> | Search for values by type |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:wc :whocalls | <name> | List the callers of some name |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:cw :callswho | <name> | List the callees of some name |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:browse | <namespace> | List the contents of some namespace |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:total | <name> | Check the totality of a name |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:r :reload | | Reload current file |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:l :load | <filename> | Load a new file |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:cd | <filename> | Change working directory |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:module | <module> | Import an extra module |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:e :edit | | Edit current file using $EDITOR or $VISUAL |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:m :metavars | | Show remaining proof obligations (metavariables) |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:p :prove | <metavar> | Prove a metavariable |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:a :addproof | <name> | Add proof to source file |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:rmproof | <name> | Remove proof from proof stack |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:showproof | <name> | Show proof |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:proofs | | Show available proofs |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:x | <expr> | Execute IO actions resulting from an expression using the interpreter |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:c :compile | <filename> | Compile to an executable [codegen] <filename> |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:exec :execute | [<expr>] | Compile to an executable and run |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:dynamic | <filename> | Dynamically load a C library (similar to %dynamic) |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:dynamic | | List dynamically loaded C libraries |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:? :h :help | | Display this help text |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:set | <option> | Set an option (errorcontext, showimplicits) |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:unset | <option> | Unset an option |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:color :colour | <option> | Turn REPL colours on or off; set a specific colour |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:consolewidth | auto|infinite|<number> | Set the width of the console |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:q :quit | | Exit the Idris system |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:w :warranty | | Displays warranty information |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:let | (<top-level-declaration>)... | Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:unlet :undefine|(<name>)... | Remove the listed repl definitions, or all repl definitions if no names given |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:printdef | <name> | Show the definition of a function |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
|:pp :pprint | <option> <number> <name> | Pretty prints an Idris function in either LaTeX or HTML and for a specified width. |
+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+
Using the REPL
==============
Getting help
~~~~~~~~~~~~
The command ``:help`` (or ``:h`` or ``:?``) prints a short summary of
the available commands.
Quitting Idris
~~~~~~~~~~~~~~
If you would like to leave Idris, simply use ``:q`` or ``:quit``.
Evaluating expressions
~~~~~~~~~~~~~~~~~~~~~~
To evaluate an expression, simply type it. If Idris is unable to infer
the type, it can be helpful to use the operator ``the`` to manually
provide one, as Idris's syntax does not allow for direct type
annotations. Examples of ``the`` include:
::
Idris> the Nat 4
4 : Nat
Idris> the Int 4
4 : Int
Idris> the (List Nat) [1,2]
[1,2] : List Nat
Idris> the (Vect _ Nat) [1,2]
[1,2] : Vect 2 Nat
This may not work in cases where the expression still involves ambiguous
names. The name can be disambiguated by using the ``with`` keyword:
::
Idris> sum [1,2,3]
When elaborating an application of function Prelude.Foldable.sum:
Can't disambiguate name: Prelude.List.::,
Prelude.Stream.::,
Prelude.Vect.::
Idris> with List sum [1,2,3]
6 : Integer
Adding let bindings
~~~~~~~~~~~~~~~~~~~
To add a let binding to the REPL, use ``:let``. It's likely you'll also
need to provide a type annotation. ``:let`` also works for other
declarations as well, such as ``data``.
::
Idris> :let x : String; x = "hello"
Idris> x
"hello" : String
Idris> :let data Foo : Type where Bar : Foo
Idris> Bar
Bar : Foo
Getting type information
~~~~~~~~~~~~~~~~~~~~~~~~
To ask Idris for the type of some expression, use the ``:t`` command.
Additionally, if used with an overloaded name, Idris will provide all
overloadings and their types. To ask for the type of an infix operator,
surround it in parentheses.
::
Idris> :t "foo"
"foo" : String
Idris> :t plus
Prelude.Nat.plus : Nat -> Nat -> Nat
Idris> :t (++)
Builtins.++ : String -> String -> String
Prelude.List.++ : (List a) -> (List a) -> List a
Prelude.Vect.++ : (Vect m a) -> (Vect n a) -> Vect (m + n) a
Idris> :t plus 4
plus (Builtins.fromInteger 4) : Nat -> Nat
You can also ask for basic information about typeclasses with ``:doc``:
::
Idris> :doc Monad
Type class Monad
Parameters:
m
Methods:
(>>=) : Monad m => m a -> (a -> m b) -> m b
infixl 5
Instances:
Monad id
Monad PrimIO
Monad IO
Monad Maybe
...
Other documentation is also available from ``:doc``:
::
Idris> :doc (+)
Prelude.Classes.+ : (a : Type) -> (Num a) -> a -> a -> a
infixl 8
Arguments:
Class constraint Prelude.Classes.Num a
__pi_arg : a
__pi_arg1 : a
::
Idris> :doc Vect
Data type Prelude.Vect.Vect : Nat -> Type -> Type
Arguments:
Nat
Type
Constructors:
Prelude.Vect.Nil : (a : Type) -> Vect 0 a
Prelude.Vect.:: : (a : Type) -> (n : Nat) -> a -> (Vect n a) -> Vect (S n) a
infixr 7
Arguments:
a
Vect n a
::
Idris> :doc Monad
Type class Prelude.Monad.Monad
Methods:
Prelude.Monad.>>= : (m : Type -> Type) -> (a : Type) -> (b : Type) -> (Monad m) -> (m a) -> (a -> m b) -> m b
infixl 5
Arguments:
Class constraint Prelude.Monad.Monad m
__pi_arg : m a
__pi_arg1 : a -> m b
Finding things
~~~~~~~~~~~~~~
The command ``:apropos`` searches names, types, and documentation for
some string, and prints the results. For example:
::
Idris> :apropos eq
eqPtr : Ptr -> Ptr -> IO Bool
eqSucc : (left : Nat) -> (right : Nat) -> (left = right) -> S left = S right
S preserves equality
lemma_both_neq : ((x = x') -> _|_) -> ((y = y') -> _|_) -> ((x, y) = (x', y')) -> _|_
lemma_fst_neq_snd_eq : ((x = x') -> _|_) -> (y = y') -> ((x, y) = (x', y)) -> _|_
lemma_snd_neq : (x = x) -> ((y = y') -> _|_) -> ((x, y) = (x, y')) -> _|_
lemma_x_eq_xs_neq : (x = y) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_
lemma_x_neq_xs_eq : ((x = y) -> _|_) -> (xs = ys) -> (x :: xs = y :: ys) -> _|_
lemma_x_neq_xs_neq : ((x = y) -> _|_) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_
prim__eqB16 : Bits16 -> Bits16 -> Int
prim__eqB16x8 : Bits16x8 -> Bits16x8 -> Bits16x8
prim__eqB32 : Bits32 -> Bits32 -> Int
prim__eqB32x4 : Bits32x4 -> Bits32x4 -> Bits32x4
prim__eqB64 : Bits64 -> Bits64 -> Int
prim__eqB64x2 : Bits64x2 -> Bits64x2 -> Bits64x2
prim__eqB8 : Bits8 -> Bits8 -> Int
prim__eqB8x16 : Bits8x16 -> Bits8x16 -> Bits8x16
prim__eqBigInt : Integer -> Integer -> Int
prim__eqChar : Char -> Char -> Int
prim__eqFloat : Float -> Float -> Int
prim__eqInt : Int -> Int -> Int
prim__eqString : String -> String -> Int
prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)
sequence : Traversable t => Applicative f => (t (f a)) -> f (t a)
sequence_ : Foldable t => Applicative f => (t (f a)) -> f ()
Eq : Type -> Type
The Eq class defines inequality and equality.
GTE : Nat -> Nat -> Type
Greater than or equal to
LTE : Nat -> Nat -> Type
Proofs that n is less than or equal to m
gte : Nat -> Nat -> Bool
Boolean test than one Nat is greater than or equal to another
lte : Nat -> Nat -> Bool
Boolean test than one Nat is less than or equal to another
ord : Char -> Int
Convert the number to its ASCII equivalent.
replace : (x = y) -> (P x) -> P y
Perform substitution in a term according to some equality.
sym : (l = r) -> r = l
Symmetry of propositional equality
trans : (a = b) -> (b = c) -> a = c
Transitivity of propositional equality
``: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:
::
Idris> :search a -> b -> a
= Prelude.Basics.const : a -> b -> a
Constant function. Ignores its second argument.
= assert_smaller : a -> b -> b
Assert to the totality checker than y is always structurally
smaller than x (which is typically a pattern argument)
> malloc : Int -> a -> a
> Prelude.pow : Num a => a -> Nat -> a
> Prelude.Classes.(*) : Num a => a -> a -> a
> Prelude.Classes.(+) : Num a => a -> a -> a
... (More results)
``:search`` can also look for dependent types:
::
Idris> :search plus (S n) n = plus n (S n)
< Prelude.Nat.plusSuccRightSucc : (left : Nat) ->
(right : Nat) ->
S (left + right) = left + S right
Loading and reloading Idris code
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The command ``:l File.idr`` will load File.idr into the
currently-running REPL, and ``:r`` will reload the last file that was
loaded.
Totality
~~~~~~~~
All Idris definitions are checked for totality. The command
``:total <NAME>`` will display the result of that check. If a definition
is not total, this may be due to an incomplete pattern match. If that is
the case, ``:missing`` or ``:miss`` will display the missing cases.
Editing files
~~~~~~~~~~~~~
The command ``:e`` launches your default editor on the current module.
After control returns to Idris, the file is reloaded.
Invoking the compiler
~~~~~~~~~~~~~~~~~~~~~
The current module can be compiled to an executable using the command
``:c <FILENAME>`` or ``:compile <FILENAME>``. This command allows to
specify codegen, so for example JavaScript can be generated using
``:c javascript <FILENAME>``. The ``:exec`` command will compile the
program to a temporary file and run the resulting executable.
IO actions
~~~~~~~~~~
Unlike GHCI, the Idris REPL is not inside of an implicit IO monad. This
means that a special command must be used to execute IO actions.
``:x tm`` will execute the IO action ``tm`` in an Idris interpreter.
Dynamically loading C libraries
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Sometimes, an Idris program will depend on external libraries written in
C. In order to use these libraries from the Idris interpreter, they must
first be dynamically loaded. This is achieved through the
``%dynamic <LIB>`` directive in Idris source files or through the
``:dynamic <LIB>`` command at the REPL. The current set of dynamically
loaded libraries can be viewed by executing ``:dynamic`` with no
arguments. These libraries are available through the Idris FFI in `type
providers <#type-providers>`__ and ``:exec``.
Colours
=======
Idris terms are available in amazing colour! By default, the Idris REPL
uses colour to distinguish between data constructors, types or type
constructors, operators, bound variables, and implicit arguments. This
feature is available on all POSIX-like systems, and there are plans to
allow it to work on Windows as well.
If you do not like the default colours, they can be turned off using the
command
::
:colour off
and, when boredom strikes, they can be re-enabled using the command
::
:colour on
To modify a colour, use the command
::
:colour <CATEGORY> <OPTIONS>
where ``<CATEGORY`` is one of ``keyword``, ``boundvar``, ``implicit``,
``function``, ``type``, ``data``, or ``prompt``, and is a
space-separated list drawn from the colours and the font options. The
available colours are ``default``, ``black``, ``yellow``, ``cyan``,
``red``, ``blue``, ``white``, ``green``, and ``magenta``. If more than
one colour is specified, the last one takes precedence. The available
options are ``dull`` and ``vivid``, ``bold`` and ``nobold``, ``italic``
and ``noitalic``, ``underline`` and ``nounderline``, forming pairs of
opposites. The colour ``default`` refers to your terminal's default
colour.
The colours used at startup can be changed using REPL initialisation
scripts.
Colour can be disabled at startup by the ``--nocolour`` command-line
option.

50
docs/reference/semantic-highlighting.rst Normal file
View File

@ -0,0 +1,50 @@
****************************************
Semantic Highlighting & Pretty Printing
****************************************
Since ``v0.9.18`` Idris comes with support for semantic highlighting.
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.
The default styling scheme used was inspired by Connor McBride's own set of stylings, informally known as *Connor's Colours*.
Legend
======
The concepts and their default stylings are as follows:
+----------------+---------------+----------------+----------------+
| Idris Term | HTML | LaTeX | IDE/REPL |
+================+===============+================+================+
| Bound Variable | Purple | Magenta | |
+----------------+---------------+----------------+----------------+
| Keyword | Bold | Underlined | |
+----------------+---------------+----------------+----------------+
| Function | Green | Green | |
+----------------+---------------+----------------+----------------+
| Type | Blue | Blue | |
+----------------+---------------+----------------+----------------+
| Data | Red | Red | |
+----------------+---------------+----------------+----------------+
| Implicit | Italic Purple | Italic Magenta | |
+----------------+---------------+----------------+----------------+
Pretty Printing
===============
Idris also supports the pretty printing of code to HTML and LaTeX using the commands:
+ ``:pp <latex|html> <width> <function name>``
+ ``:pprint <latex|html> <width> <function name>``
Customisation
=============
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.
Further Information
===================
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.

275
docs/reference/syntax-guide.rst Normal file
View File

@ -0,0 +1,275 @@
**************
Syntax Guide
**************
Examples are mostly adapted from the Idris tutorial.
Variables
---------
A variable is always defined by defining its type on one line, and its
value on the next line, using the syntax
::
<id> : <type>
<id> = <value>
Examples
.. code:: idris
x : Int
x = 100
hello : String
hello = "hello"
Types
-----
In Idris, types are first class values. So a type declaration is the
same as just declaration of a variable whose type is ``Type``. In Idris,
variables that denote a type must being with a capital letter. Example:
.. code:: idris
MyIntType : Type
MyIntType = Int
a more interesting example:
.. code:: idris
MyListType : Type
MyListType = List Int
Data types
~~~~~~~~~~
Idris provides two kinds of syntax for defining data types. The first,
Haskell style syntax, defines a regular algebraic data type. For example
.. code:: idris
data Either a b = Left a | Right b
or
.. code:: idris
data List a = Nil | (::) a (List a)
The second, more general kind of data type, is defined using Agda or
GADT style syntax. This syntax defines a data type that is parameterized
by some values (in the ``Vect`` exampe, a value of type ``Nat`` and a
value of type ``Type``).
.. code:: idris
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
Operators
---------
Arithmetic
~~~~~~~~~~
::
x + y
x - y
x * y
x / y
(x * y) + (a / b)
Equality and Relational
~~~~~~~~~~~~~~~~~~~~~~~
::
x == y
x /= y
x >= y
x > y
x <= y
x < y
Conditional
~~~~~~~~~~~
::
x && y
x || y
not x
Conditionals
------------
If Then Else
~~~~~~~~~~~~
::
if <test> then <true> else <false>
Case Expressions
~~~~~~~~~~~~~~~~
::
case <test> of
<case 1> => <expr>
<case 2> => <expr>
...
otherwise => <expr>
Functions
---------
Named
~~~~~
Named functions are defined in the same way as variables, with the type
followed by the definition.
::
<id> : <argument type> -> <return type>
<id> arg = <expr>
Example
.. code:: idris
plusOne : Int -> Int
plusOne x = x + 1
Functions can also have multiple inputs, for example
.. code:: idris
makeHello : String -> String -> String
makeHello first last = "hello, my name is " ++ first ++ " " ++ last
Functions can also have named arguments. This is required if you want to
annotate parameters in a docstring. The following shows the same
``makeHello`` function as above, but with named parameters which are
also annotated in the docstring
.. code:: idris
||| Makes a string introducing a person
||| @first The person's first name
||| @last The person's last name
makeHello : (first : String) -> (last : String) -> String
makeHello first last = "hello, my name is " ++ first ++ " " ++ last
Like Haskell, Idris functions can be defined by pattern matching. For
example
.. code:: idris
sum : List Int -> Int
sum [] = 0
sum (x :: xs) = x + (sum xs)
Similarly case analysis looks like
.. code:: idris
answerString : Bool -> String
answerString False = "Wrong answer"
answerString True = "Correct answer"
Dependent Functions
~~~~~~~~~~~~~~~~~~~
Dependent functions are functions where the type of the return value
depends on the input value. In order to define a dependent function,
named parameters must be used, since the parameter will appear in the
return type. For example, consider
.. code:: idris
zeros : (n : Nat) -> Vect n Int
zeros Z = []
zeros (S k) = 0 :: (zeros k)
In this example, the return type is ``Vect n Int`` which is an
expression which depends on the input parameter ``n``. ### Anonymous
Arguments in anonymous functions are separated by comma.
::
(\x => <expr>)
(\x, y => <expr>)
Modifiers
~~~~~~~~~
Visibility
^^^^^^^^^^
::
public
abstract
private
Totality
^^^^^^^^
::
total
implicit
partial
covering
Options
^^^^^^^
::
%export
%hint
%no_implicit
%error_handler
%error_reverse
%assert_total
%reflection
%specialise [<name list>]
Misc
----
Comments
~~~~~~~~
::
-- Single Line
{- Multiline -}
||| Docstring (goes before definition)
Directives
----------
::
%lib <path>
%link <path>
%flag <path>
%include <path>
%hide <function>
%freeze <name>
%access <accessibility>
%default <totality>
%logging <level 0--11>
%dynamic <list of libs>
%name <list of names>
%error_handlers <list of names>
%language <extension>

213
docs/reference/tactics.rst Normal file
View File

@ -0,0 +1,213 @@
***************************
Tactics and Theorem Proving
***************************
Idris supports interactive theorem proving, and theh analyse of
context through metavariables. To list all unproven metavariables,
use the command ``:m``. This will display their qualified names and
the expected types. To interactively prove a metavariable, use the
command ``:p name`` where ``name`` is the metavariable. Once the proof
is complete, the command ``:a`` will append it to the current module.
Once in the interactive prover, the following commands are available:
Basic commands
==============
- ``:q`` - Quits the prover (gives up on proving current lemma).
- ``abandon`` - Same as :q
- ``state`` - Displays the current state of the proof.
- ``term`` - Displays the current proof term complete with its
yet-to-be-filled holes (is only really useful for debugging).
- ``undo`` - Undoes the last tactic.
- ``qed`` - Once the interactive theorem prover tells you "No more
goals," you get to type this in celebration! (Completes the proof and
exits the prover)
Commonly Used Tactics
=====================
Compute
-------
- ``compute`` - Normalizes all terms in the goal (note: does not
normalize assumptions)
::
---------- Goal: ----------
(Vect (S (S Z + (S Z) + (S n))) Nat) -> Vect (S (S (S (S n)))) Nat
-lemma> compute
---------- Goal: ----------
(Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
-lemma>
Exact
-----
- ``exact`` - Provide a term of the goal type directly.
::
---------- Goal: ----------
Nat
-lemma> exact Z
lemma: No more goals.
-lemma>
Refine
------
- ``refine`` - Use a name to refine the goal. If the name needs
arguments, introduce them as new goals.
Trivial
-------
- ``trivial`` - Satisfies the goal using an assumption that matches its
type.
::
---------- Assumptions: ----------
value : Nat
---------- Goal: ----------
Nat
-lemma> trivial
lemma: No more goals.
-lemma>
Intro
-----
- ``intro`` - If your goal is an arrow, turns the left term into an
assumption.
::
---------- Goal: ----------
Nat -> Nat -> Nat
-lemma> intro
---------- Assumptions: ----------
n : Nat
---------- Goal: ----------
Nat -> Nat
-lemma>
You can also supply your own name for the assumption:
::
---------- Goal: ----------
Nat -> Nat -> Nat
-lemma> intro number
---------- Assumptions: ----------
number : Nat
---------- Goal: ----------
Nat -> Nat
Intros
------
- ``intros`` - Exactly like intro, but it operates on all left terms at
once.
::
---------- Goal: ----------
Nat -> Nat -> Nat
-lemma> intros
---------- Assumptions: ----------
n : Nat
m : Nat
---------- Goal: ----------
Nat
-lemma>
let
---
- ``let`` - Introduces a new assumption; you may use current
assumptions to define the new one.
::
---------- Assumptions: ----------
n : Nat
---------- Goal: ----------
BigInt
-lemma> let x = toIntegerNat n
---------- Assumptions: ----------
n : Nat
x = toIntegerNat n: BigInt
---------- Goal: ----------
BigInt
-lemma>
rewrite
-------
- ``rewrite`` - Takes an expression with an equality type (x = y), and
replaces all instances of x in the goal with y. Is often useful in
combination with 'sym'.
::
---------- Assumptions: ----------
n : Nat
a : Type
value : Vect Z a
---------- Goal: ----------
Vect (mult n Z) a
-lemma> rewrite sym (multZeroRightZero n)
---------- Assumptions: ----------
n : Nat
a : Type
value : Vect Z a
---------- Goal: ----------
Vect Z a
-lemma>
induction
---------
- ``induction`` - (``Note that this is still experimental`` and you may
get strange results and error messages. We are aware of these and
will finish the implementation eventually!) Prove the goal by
induction. Each constructor of the datatype becomes a goal.
Constructors with recursive arguments become induction steps, while
simple constructors become base cases. Note that this only works for
datatypes that have eliminators: a datatype definition must have the
``%elim`` modifier.
sourceLocation
--------------
- ``sourceLocation`` - Solve the current goal with information about
the location in the source code where the tactic was invoked. This is
mostly for embedded DSLs and programmer tools like assertions that
need to know where they are called. See
``Language.Reflection.SourceLocation`` for more information.
Less commonly-used tactics
==========================
- ``applyTactic`` - Apply a user-defined tactic. This should be a
function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
the first argument represents the proof context and the second
represents the goal. If your tactic will produce a proof term
directly, use the ``Exact`` constructor from ``Tactic``.
- ``attack`` - ?
- ``equiv`` - Replaces the goal with a new one that is convertible with
the old one
- ``fill`` - ?
- ``focus`` - ?
- ``mrefine`` - Refining by matching against a type
- ``reflect`` - ?
- ``solve`` - Takes a guess with the correct type and fills a hole with
it, closing a proof obligation. This happens automatically in the
interactive prover, so ``solve`` is really only relevant in tactic
scripts used for helping implicit argument resolution.
- ``try`` - ?