Agda mode for Yi

What is Yi

Yi is a text editor written in Haskell and extensible in Haskell. It provides a flexible, powerful and correct editor core scriptable in Haskell.

Yi already has a Haskell mode, emacs key bindings which can be used as a basis for this project.

What is Agda

Agda is a dependently typed programming language with good support for programming with inductively defined families of types.

Agda is also implemented in Haskell, so scripting should be natural. Agda currently has an emacs mode which also can be used as a basis for this project.

Goals of the project

Adding support for interactive programming / proving in Yi
Provide this as a Cabal package on Hackage

The long term goal is to provide a package that provides an Agda development environment.

Probable steps on the way:

learn about the framework (Yi and Agda)
set up a trivial cabal package (keep extending it below)
write a coarse-grained parser for Agda syntax using the Yi parsing library
add support for interaction points
add bindings for
- type-checking / loading
- show syntax highlighting
- show context, type, evaluate to normal form
- refining interaction points
- generate case skeleton
- ...

Prereq.: Functional programming, Programming (Languages or Paradigms), Software Architecture, (Types for Programs and Proofs is recommended)
Contact: Jean-Philippe Bernardy and Patrik Jansson
Number of people: 1-2

Learning outcomes:

good understanding of advanced software architecture
experience with software deployment (packaging etc.)
software engineering within functional programming
experience with software technology: combinator parsing, proof assistants