#+TITLE: Idris contribution layer for Spacemacs

[[file:img/idris.png]]

* Table of Contents                                         :TOC_4_org:noexport:
 - [[Description][Description]]
 - [[Install][Install]]
   - [[Layer][Layer]]
   - [[Idris][Idris]]
 - [[Key bindings][Key bindings]]
   - [[Shorthands][Shorthands]]
   - [[Interactive editing][Interactive editing]]
   - [[Documentation][Documentation]]
   - [[REPL][REPL]]
   - [[Active term manipulations][Active term manipulations]]
   - [[Build system][Build system]]

* Description
This layer adds support for the [[http://www.idris-lang.org/][Idris]] language.

* Install

** Layer
To use this layer, add it to your =~/.spacemacs=

#+BEGIN_SRC elisp
(setq-default dotspacemacs-configuration-layers '(idris))
#+END_SRC

** Idris

Idris can be installed using =Haskell's cabal=:

#+BEGIN_SRC sh
cabal install idris
#+END_SRC

Binaries are also available for some platforms at
http://www.idris-lang.org/download/

* Key bindings

** Shorthands
Several (but not all) of the evil-leader shorthands that =idris-mode= provides
are reproduced under the local leader.

| Key Binding | Description                                                    |
|-------------+----------------------------------------------------------------|
| ~SPC m c~   | Case split the pattern variable under point.                   |
| ~SPC m d~   | Create an initial pattern match clause for a type declaration. |
| ~SPC m p~   | Attempt to solve a metavariable automatically.                 |
| ~SPC m r~   | Load current buffer into Idris.                                |
| ~SPC m t~   | Get the type for the identifier under point.                   |
| ~SPC m w~   | Add a with block for the pattern-match clause under point.     |

** Interactive editing

| Key Binding | Description                                                                                |
|-------------+--------------------------------------------------------------------------------------------|
| ~SPC m i a~ | Attempt to solve a metavariable automatically.                                             |
| ~SPC m i c~ | Case split the pattern variable under point.                                               |
| ~SPC m i e~ | Extract a metavariable or provisional definition name to an explicit top level definition. |
| ~SPC m i m~ | Add missing pattern-match cases to an existing definition.                                 |
| ~SPC m i r~ | Refine by name, without recursive proof search.                                            |
| ~SPC m i s~ | Create an initial pattern match clause for a type declaration.                             |
| ~SPC m i w~ | Add a with block for the pattern-match clause under point.                                 |

** Documentation

| Key Binding | Description                                           |
|-------------+-------------------------------------------------------|
| ~SPC m h a~ | Search the documentation for a string.                |
| ~SPC m h d~ | Search the documentation for the name under point.    |
| ~SPC m h s~ | Search the documentation regarding a particular type. |
| ~SPC m h t~ | Get the type for the identifier under point.          |

** REPL
| Key Binding | Description                                                                            |
|-------------+----------------------------------------------------------------------------------------|
| ~SPC m s b~ | Load the current buffer into Idris.                                                    |
| ~SPC m s B~ | Load the current buffer into Idris and switch to REPL in insert state                  |
| ~SPC m s i~ | Start Idris inferior process                                                           |
| ~SPC m s n~ | Extend the region to be loaded one line at a time.                                     |
| ~SPC m s N~ | Extend the region to be loaded one line at a time and switch to REPL in insert state   |
| ~SPC m s p~ | Contract the region to be loaded one line at a time                                    |
| ~SPC m s P~ | Contract the region to be loaded one line at a time and switch to REPL in insert state |
| ~SPC m s s~ | Switch to REPL buffer                                                                  |

** Active term manipulations

| Key Binding | Description                                   |
|-------------+-----------------------------------------------|
| ~SPC m m c~ | Show the core language for the term at point. |
| ~SPC m m i~ | Show implicits for the term at point.         |
| ~SPC m m h~ | Hide implicits for the term at point.         |
| ~SPC m m n~ | Normalize the term at point.                  |

** Build system

| Key Binding | Description                                                                |
|-------------+----------------------------------------------------------------------------|
| ~SPC m b c~ | Build the package.                                                         |
| ~SPC m b C~ | Clean the package, removing =.ibc= files                                   |
| ~SPC m b i~ | Install the package to the user's repository, building first if necessary. |
| ~SPC m b p~ | Open package file.                                                         |

When inside a package file, you can insert a field with ~SPC m f~.