Edit-Time Tactics in Idris

<p>Metaprogramming allows users to write programs that write programs. In dependently-typed languages such as Idris, recent work on elaborator reflection paved theway for newapplications of metaprogramming by showing that a tactic-based proof language can be substituted with a monadic interface that exposes the internal elaborator. The goal of our work is to use elaborator reflection to write editor interaction actions in Idris.</p> <p>Currently in Idris modes of editors such as Emacs, users can perform actions like type-checking holes, case-splitting, and lemma extraction. Implementations of all of these Idris editor actions are hard-coded in the compiler, and they are written in Haskell. Ourwork will allowus to rewrite them in Idris as metaprograms and to move them into an Idris library, instead of having them embedded into the compiler.</p> <p>Furthermore, Idris users can write our own tactics through elaborator reflection and run them from the editor, i.e. in edit-time. This would extend the abilities of the editor interaction mode from the current built-in features to anything that can be done with tactics. In our work, we present the design and implementation of this feature in the Idris compiler.</p> <p>We also implement an intuitionistic theorem prover tactic, which is meant to be an better alternative to the built-in proof search editor action, and an add-clause tactic that exemplifies how we can move some of the hard-coded features from the compiler to a library.</p>