Interactive Idris editing with vim

From Idris version 0.9.10 (and from now, if you’re tracking the git repository), the REPL provides various helpers for interactive editing. Agda users have known for a long time how useful this is, and I have become sufficiently jealous of it that I’ve decided it’s about time we had it too! I have implemented a short vim script to support interactive editing in vim, but since almost all of the work is done by the Idris REPL, it should be very easy to adapt to other editors. Here, I’ll briefly explain how to use it, then say a bit about how it works for anyone who might want to adapt it.

How to use it

Assuming you have an up-to-date Idris installed, install the vim Idris mode. This mode allows vim to communicate with a running Idris REPL instance. It provides the following basic commands:

  • \t displays the type of the name under the cursor (or a bit more information about its context if it happens to be a metavariable)
  • \e prompts for an expression to evaluate
  • \r reloads and typechecks the file in the current buffer

More interestingly, it provides support for interactive editing:

  • \c, if the cursor is over a variable in a pattern match clause, splits that variable into all the patterns which are well typed. This also works in case
    expressions.
  • \w, if the cursor is over a pattern clause of the form f x y z = ?rhs creates a new with clause, i.e. the clause becomes:
      f x y z with (_)
        f x y z | with_pat = ?rhs
  • \d, if the cursor is in a top level function type declaration (right of the :), creates a new clause for that function.

(With all of these, the \ (backslash) is your local leader key. I have this rebound to , (comma) but \ is the default.)

Example: Case splitting

For example, start up idris vadd.idr (this will create the file if it doesn’t already exist) edit it with :e and type the following:

  module vadd

  vadd : Num a => Vect n a -> Vect n a -> Vect n a

Press ESC, and before moving the cursor anywhere, hit \d. You should see:

  module vadd

  vadd : Num a => Vect n a -> Vect n a -> Vect n a
  vadd x1 x2 = ?vadd_rhs

Now move the cursor over x1 and hit \c to split x1 into patterns for [] and ::. You should see:

  module vadd

  vadd : Num a => Vect n a -> Vect n a -> Vect n a
  vadd [] x2 = ?vadd_rhs_1
  vadd (_ :: _) x2 = ?vadd_rhs_2

Note that it hasn’t attempted to invent any names for the patterns. This is because I have decided that making no choice is better than making a bad choice! We can type some in ourselves…

  module vadd

  vadd : Num a => Vect n a -> Vect n a -> Vect n a
  vadd [] x2 = ?vadd_rhs_1
  vadd (x :: xs) x2 = ?vadd_rhs_2

Now do the same over the first x2. Move the cursor over it and hit \c. You should see:

  module vadd

  vadd : Num a => Vect n a -> Vect n a -> Vect n a
  vadd [] [] = ?vadd_rhs_3
  vadd (x :: xs) x2 = ?vadd_rhs_2

Note that this has only produced one new pattern, because vadd [] (_ :: _) would not be well typed. Finally, over the remaining x2:

  module vadd

  vadd : Num a => Vect n a -> Vect n a -> Vect n a
  vadd [] [] = ?vadd_rhs_3
  vadd (x :: xs) (_ :: _) = ?vadd_rhs_1

If you move the cursor over the metavariable ?vadd_rhs_1 and hit \t, you will see the context and the required type of ?vadd_rhs_1:

  a : Type
  c : Num a
  n : Nat
  x : a
  xs : Vect n a
  _ : a
  _ : Vect n a
--------------------------------------
vadd_rhs_1 : Vect (S n) a

The interactive mode will work with any file in the working directory of your REPL instance, so you can edit multiple files at once.

Example: with rule

Let’s try completing the following definition, in a module elem.idr:

  module elem

  import Decidable.Equality

  using (xs : List a)
    data Elem  : a -> List a -> Type where
         Here  : Elem x (x :: xs)
         There : Elem x xs -> Elem x (y :: xs)

  isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)

As before, get a clause for isElem by hitting \d somewhere after the : on the line with isElem. You’ll see

  isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
  isElem x xs = ?isElem_rhs

Now expand xs using \c and give the pattern variables names:

  isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
  isElem x [] = ?isElem_rhs_1
  isElem x (y :: ys) = ?isElem_rhs_2

We’ll leave the [] case for now and concentrate on the y :: ys case. We’ll do this by attempting to build a proof that x = y using

  decEq : DecEq t => (x1 : t) -> (x2 : t) -> Dec (x1 = x2)

(This is why we imported Decidable.Equality.) Move to the line with the y :: ys case and hit \w. This gives:

  isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
  isElem x [] = ?isElem_rhs_1  
  isElem x (y :: ys) with (_)
    isElem x (y :: ys) | with_pat = ?isElem_rhs

The cursor is conveniently in the with argument. Change that to decEq x y, move the cursor over with_pat and hit \c again to split with_pat:

  isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
  isElem x [] = ?isElem_rhs_1
  isElem x (y :: ys) with (decEq x y)
    isElem x (y :: ys) | (Yes _) = ?isElem_rhs_2
    isElem x (y :: ys) | (No _) = ?isElem_rhs_3

The Yes case’s parameter is a proof that x = y. We’ll need to match on this to get a canonical proof. Change it to Yes p, and case split p. You’ll get:

  isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
  isElem x [] = ?isElem_rhs_1
  isElem x (y :: ys) with (decEq x y)
    isElem x (x :: ys) | (Yes refl) = ?isElem_rhs_4
    isElem x (y :: ys) | (No _) = ?isElem_rhs_3

Now that you have the canonical proof, the left hand side has been updated so that x and y are unified to x. I’ll leave the rest of this definition as an exercise — remember to use \t to check the types of isElem_rhs_3 and isElem_rhs_4.

How it works

When an Idris REPL starts, it also starts up a server running on port 4294 your local machine, responding to requests from a REPL client. This can be queried using the --client flag to Idris. For example, from the shell:

  $ idris --client '2+2'
  4 : Integer
  $ idris --client 'vadd [1,2,3] [4,5,6]'
  [5,7,9] : Vect 3 Integer
  $ idris --client ':t vadd'
  vadd.vadd : Num a => (Vect n a) -> (Vect n a) -> Vect n a

Therefore, if the REPL provides appropriate commands for editing a file in place, all an editor has to do is invoke it and reload the file. The REPL now provides:

  • :casesplit [line] [name], abbreviated :cs which displays the cases resulting when the variable [name] on line [line] is split, e.g.
      $ idris --client ':cs 4 x1'
      vadd [] x2 = ?vadd_rhs_1
      vadd (_ :: _) x2 = ?vadd_rhs_2
    
    

    There is also a destructive version :cs! which is the same, but updates the source file.

  • :addclause [line] [name], abbreviated :ac which displays a clause suitable for the function declaration for [name] on line [line]. Similarly, :ac! updates the source file.
  • :makewith [line] [name], abbreviated :mw which adds a with clause for the definition of [name] on line [line]. Again, :mw! updates the source file.

The vim script is simply a thin wrapper for these functions. It also uses the REPL to invoke the evaluator, and to call :r for quickly type checking a buffer.

Enjoy! If you prefer to use another editor, please consider contributing a similar script to support interactive development in your own editor. More features are planned, in particular automatically solving metavariables where possible.

Posted October 28, 2013 by edwinb in Dependent Types, Idris

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: