@@ -0,0 +1,86 @@
1+;;;; Elisp for talking to idris --client
2+;;;; Stopgap until these features work with --ideslave - use with https://github.com/idris-hackers/idris-mode
3+(require 'idris-mode)
4+
5+(defvar *auto-idris-output-buf* "*auto-idris-output*")
6+
7+(defun string-no-properties (str)
8+ (substring-no-properties str 0 (length str)))
9+
10+(defun call-idris-client (cmd &optional return-output)
11+ (if return-output
12+ (with-temp-buffer
13+ (call-process "idris" nil t nil "--client" cmd)
14+ (buffer-string))
15+ (call-process "idris" nil *auto-idris-output-buf* nil "--client" cmd)
16+ nil))
17+
18+(defun idris-get-line-num ()
19+ "Get the current line number"
20+ (save-restriction
21+ (widen)
22+ (save-excursion
23+ (beginning-of-line)
24+ (1+ (count-lines 1 (point))))))
25+
26+
27+(defun idris-thing-at-point ()
28+ "Return the line number and name at point"
29+ (let ((name (string-no-properties (symbol-name (symbol-at-point))))
30+ (line (idris-get-line-num)))
31+ (cons name line)))
32+
33+(defun idris-load ()
34+ "Load the current buffer using Idris client mode"
35+ (interactive)
36+ (save-buffer)
37+ (let* ((file-name (buffer-file-name))
38+ (cmd (concat ":l " file-name)))
39+ (call-idris-client cmd)))
40+
41+(defun idris-type-at-point ()
42+ "Show the type of the name at point"
43+ (interactive)
44+ (message (call-idris-client (concat ":t " (string-no-properties (symbol-name (symbol-at-point)))) t)))
45+
46+(defun idris-add-clause ()
47+ "Add clauses to the declaration at point"
48+ (interactive)
49+ (idris-load)
50+ (let ((what (idris-thing-at-point)))
51+ (call-idris-client (concat ":ac! " (number-to-string (cdr what)) (car what))))
52+ (revert-buffer t t))
53+
54+(defun idris-case-split ()
55+ "Case split the pattern var at point"
56+ (interactive)
57+ (idris-load)
58+ (let ((what (idris-thing-at-point)))
59+ (call-idris-client (concat ":cs! " (number-to-string (cdr what)) " " (car what))))
60+ (revert-buffer t t))
61+
62+(defun idris-proof-search (&optional hints)
63+ "Invoke the proof search"
64+ (interactive "sHints: ")
65+ (let ((hints (if hints (split-string hints "[^a-zA-Z0-9']") " "))
66+ (what (idris-thing-at-point)))
67+ (call-idris-client (format ":ps! %s %s %s" (number-to-string (cdr what)) (car what) hints)))
68+ (revert-buffer t t))
69+
70+(defun idris-add-missing ()
71+ "Add missing cases"
72+ (interactive)
73+ (idris-load)
74+ (let ((what (idris-thing-at-point)))
75+ (call-idris-client (concat ":am! " (number-to-string (cdr what)) " " (car what))))
76+ (revert-buffer t t))
77+
78+;;;; Bindings to imitate Agda somewhat
79+(define-key idris-mode-map (kbd "C-c C-c") 'idris-case-split)
80+(define-key idris-mode-map (kbd "C-c C-a") 'idris-proof-search)
81+(define-key idris-mode-map (kbd "C-c C-m") 'idris-add-missing)
82+(define-key idris-mode-map (kbd "C-c C-t") 'idris-type-at-point)
83+(define-key idris-mode-map (kbd "C-c C-d") 'idris-add-clause)
84+
85+
86+(provide 'auto-idris)