lang/agda-mode: New layer
This commit is contained in:
parent
5a1ee91f70
commit
ae8559648a
56
contrib/lang/agda/README.md
Normal file
56
contrib/lang/agda/README.md
Normal file
|
@ -0,0 +1,56 @@
|
|||
# Agda contribution layer for Spacemacs
|
||||
|
||||
## Description
|
||||
|
||||
This layer adds support for the [Agda][] programming language.
|
||||
|
||||
Some features:
|
||||
- Faces redefined to correctly play with themes.
|
||||
- Spacemacs bindings to Agda's interactive tools.
|
||||
|
||||
**This layer is in construction, it needs your contributions and bug reports.**
|
||||
|
||||
## Install
|
||||
|
||||
### Layer
|
||||
|
||||
To use this contribution add it to your `~/.spacemacs`
|
||||
|
||||
```elisp
|
||||
(setq-default dotspacemacs-configuration-layers '(agda))
|
||||
```
|
||||
|
||||
### Agda
|
||||
|
||||
This layer requires Agda to be installed, and available on the `PATH` as seen by Emacs.
|
||||
|
||||
## Key bindings
|
||||
|
||||
All Agda specific bindings are prefixed with the major-mode leader
|
||||
<kbd>SPC m</kbd>.
|
||||
|
||||
Top-level commands are prefixed by <kbd>SPC m</kbd>:
|
||||
|
||||
Key Binding | Description
|
||||
----------------------|------------------------------------------------------------
|
||||
<kbd>SPC m l</kbd> | Load current buffer.
|
||||
<kbd>SPC m a</kbd> | Simple proof search.
|
||||
<kbd>SPC m r</kbd> | Refine the goal at point.
|
||||
<kbd>SPC m s</kbd> | Solves all goals that are already instantiated internally.
|
||||
<kbd>SPC m t</kbd> | Show the type of the goal at point.
|
||||
<kbd>SPC m c</kbd> | Refine the pattern variables given in the goal.
|
||||
<kbd>SPC m f</kbd> | Go to the next goal, if any.
|
||||
<kbd>SPC m ?</kbd> | Show all goals.
|
||||
<kbd>SPC m e</kbd> | Show the context of the goal at point.
|
||||
<kbd>SPC m b</kbd> | Go to the previous goal, if any.
|
||||
<kbd>SPC m ,</kbd> | Shows the type of the goal at point and the currect context.
|
||||
<kbd>SPC m =</kbd> | Show constraints.
|
||||
<kbd>SPC m h</kbd> | Compute the type of a hypothetical helper function.
|
||||
<kbd>SPC m d</kbd> | Infers the type of the given expression.
|
||||
<kbd>SPC m w</kbd> | Explains why a given name is in scope.
|
||||
<kbd>SPC m .</kbd> | Shows the context, the goal and the given expression's inferred type.
|
||||
<kbd>SPC m o</kbd> | Shows all the top-level names in the given module.
|
||||
<kbd>SPC m n</kbd> | Computes the normal form of the given expression, using the scope of the current goal or, if point is not in a goal, the top-level scope.
|
||||
|
||||
|
||||
[Agda]: http://wiki.portal.chalmers.se/agda/pmwiki.php
|
48
contrib/lang/agda/extensions.el
Normal file
48
contrib/lang/agda/extensions.el
Normal file
|
@ -0,0 +1,48 @@
|
|||
;;; extensions.el --- Agda2 Layer extensions File for Spacemacs
|
||||
;;
|
||||
;; Copyright (c) 2012-2014 Sylvain Benner
|
||||
;; Copyright (c) 2015 Oliver Charles & Contributors
|
||||
;;
|
||||
;; Author: Oliver Charles <ollie@ocharles.org.uk>
|
||||
;; URL: https://github.com/syl20bnr/spacemacs
|
||||
;;
|
||||
;; This file is not part of GNU Emacs.
|
||||
;;
|
||||
;;; License: GPLv3
|
||||
|
||||
(defvar agda-pre-extensions '(agda))
|
||||
|
||||
(defun agda/init-agda ()
|
||||
(custom-set-faces
|
||||
'(agda2-highlight-datatype-face ((t (:inherit font-lock-type-face))))
|
||||
'(agda2-highlight-function-face ((t (:inherit font-lock-type-face))))
|
||||
'(agda2-highlight-inductive-constructor-face ((t (:inherit font-lock-function-name-face))))
|
||||
'(agda2-highlight-keyword-face ((t (:inherit font-lock-keyword-face))))
|
||||
'(agda2-highlight-module-face ((t (:inherit font-lock-constant-face))))
|
||||
'(agda2-highlight-number-face ((t nil)))
|
||||
'(agda2-highlight-postulate-face ((t (:inherit font-lock-type-face))))
|
||||
'(agda2-highlight-primitive-type-face ((t (:inherit font-lock-type-face))))
|
||||
'(agda2-highlight-record-face ((t (:inherit font-lock-type-face)))))
|
||||
|
||||
(load-file (let ((coding-system-for-read 'utf-8))
|
||||
(shell-command-to-string "agda-mode locate")))
|
||||
|
||||
(evil-leader/set-key-for-mode 'agda2-mode
|
||||
"ml" 'agda2-load
|
||||
"ma" 'agda2-auto
|
||||
"mr" 'agda2-refine
|
||||
"ms" 'agda2-solveAll
|
||||
"mt" 'agda2-goal-type
|
||||
"mc" 'agda2-make-case
|
||||
"mf" 'agda2-next-goal
|
||||
"m?" 'agda2-show-goals
|
||||
"me" 'agda2-show-context
|
||||
"mb" 'agda2-previous-goal
|
||||
"m," 'agda2-goal-and-context
|
||||
"m=" 'agda2-show-constraints
|
||||
"mh" 'agda2-helper-function-type
|
||||
"md" 'agda2-infer-type-maybe-toplevel
|
||||
"mw" 'agda2-why-in-scope-maybe-toplevel
|
||||
"m." 'agda2-goal-and-context-and-inferred
|
||||
"mo" 'agda2-module-contents-maybe-toplevel
|
||||
"mn" 'agda2-compute-normalised-maybe-toplevel))
|
Loading…
Reference in a new issue