From a574fe7ceacf5f6597890817d871d1b6d8a3ff76 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 31 Aug 2022 15:39:10 +0100 Subject: [PATCH 1/2] [ fix ] generate-def does work! --- idris2-commands.el | 57 ++++++++++++++++++++++++++++++++++++++++++++++ idris2-keys.el | 10 ++++---- idris2-mode.el | 2 ++ 3 files changed, 65 insertions(+), 4 deletions(-) diff --git a/idris2-commands.el b/idris2-commands.el index 97b70ff..244fd5c 100644 --- a/idris2-commands.el +++ b/idris2-commands.el @@ -800,6 +800,63 @@ prefix argument sets the recursion depth directly." (error "Nothing found") (idris2-replace-hole-with result))))) +(defvar-local def-region-start nil) +(defvar-local def-region-end nil) + +(defun idris2-generate-def () + "Generate defintion." + (interactive) + (let ((what (idris2-thing-at-point))) + (when (car what) + (save-excursion (idris2-load-file-sync)) + (let ((result (car (idris2-eval `(:generate-def ,(cadr what) ,(car what))))) + final-point + (prefix (save-excursion + (goto-char (point-min)) + (forward-line (1- (cadr what))) + (goto-char (line-beginning-position)) + (re-search-forward "\\(^>?\\s-*\\)" nil t) + (let ((prefix (match-string 1))) + (if prefix + prefix + ""))))) + (if (string= result "") + (error "Nothing found") + (goto-char (line-beginning-position)) + (forward-line) + (while (and (not (eobp)) + (progn (goto-char (line-beginning-position)) + (looking-at-p (concat prefix "\\s-+")))) + (forward-line)) + (insert prefix) + (setq final-point (point)) + (setq def-region-start (point)) + (insert result) + (setq def-region-end (point)) + (newline) + (goto-char final-point) +; (save-excursion +; (forward-line 1) +; (setq def-region-start (point)) +; (insert result) +; (setq def-region-end (point))) + ))))) + +(defun idris2-generate-def-next () + "Replace the previous generated definition with next definition, if it exists." + (interactive) + (if (not def-region-start) + (error "You must program search first before looking for subsequent program results.") + (let ((result (car (idris2-eval `:generate-def-next)))) + (if (string= result "No more results") + (message "No more results") + (save-excursion + (goto-char def-region-start) + (delete-region def-region-start def-region-end) + (setq def-region-start (point)) + (insert result) + (setq def-region-end (point))))))) + (defun idris2-intro () "Introduce the unambiguous constructor to use in this hole." (interactive) diff --git a/idris2-keys.el b/idris2-keys.el index 9ac9f8d..35a57dd 100644 --- a/idris2-keys.el +++ b/idris2-keys.el @@ -56,10 +56,12 @@ (define-key map (kbd "C-c C-c") 'idris2-case-dwim) ;; co: not in Idris2 yet ;; (define-key map (kbd "C-c C-m") 'idris2-add-missing) - (define-key map (kbd "C-c C-e") 'idris2-make-lemma) - (define-key map (kbd "C-c C-s") 'idris2-add-clause) - (define-key map (kbd "C-c C-w") 'idris2-make-with-block) - (define-key map (kbd "C-c C-a") 'idris2-proof-search) + (define-key map (kbd "C-c C-e") 'idris2-make-lemma) + (define-key map (kbd "C-c C-s") 'idris2-add-clause) + (define-key map (kbd "C-c C-w") 'idris2-make-with-block) + (define-key map (kbd "C-c C-a") 'idris2-proof-search) + (define-key map (kbd "C-c C-g") 'idris2-generate-def) + (define-key map (kbd "C-c C-S-g") 'idris2-generate-def-next) ;; co: not in Idris2 yet (define-key map (kbd "C-c C-r") 'idris2-refine) (define-key map (kbd "C-c C-i") 'idris2-intro) diff --git a/idris2-mode.el b/idris2-mode.el index 344508a..6322b39 100644 --- a/idris2-mode.el +++ b/idris2-mode.el @@ -81,6 +81,8 @@ ["Extract lemma from hole" idris2-make-lemma t] ["Solve hole with case expression" idris2-make-cases-from-hole t] ["Attempt to solve hole" idris2-proof-search t] + ["Generate definition" idris2-generate-def t] + ["Get next definition" idris2-generate-def-next t] ["Display type" idris2-type-at-point t] ["Goto definition" idris2-jump-to-def t] "-----------------" From 78496d4b0c5d24630b184dae3a2cb3edb926a91a Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 31 Aug 2022 15:43:04 +0100 Subject: [PATCH 2/2] [ cleanup ] other blocks are not aligned like this --- idris2-keys.el | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/idris2-keys.el b/idris2-keys.el index 35a57dd..ee84b90 100644 --- a/idris2-keys.el +++ b/idris2-keys.el @@ -56,11 +56,11 @@ (define-key map (kbd "C-c C-c") 'idris2-case-dwim) ;; co: not in Idris2 yet ;; (define-key map (kbd "C-c C-m") 'idris2-add-missing) - (define-key map (kbd "C-c C-e") 'idris2-make-lemma) - (define-key map (kbd "C-c C-s") 'idris2-add-clause) - (define-key map (kbd "C-c C-w") 'idris2-make-with-block) - (define-key map (kbd "C-c C-a") 'idris2-proof-search) - (define-key map (kbd "C-c C-g") 'idris2-generate-def) + (define-key map (kbd "C-c C-e") 'idris2-make-lemma) + (define-key map (kbd "C-c C-s") 'idris2-add-clause) + (define-key map (kbd "C-c C-w") 'idris2-make-with-block) + (define-key map (kbd "C-c C-a") 'idris2-proof-search) + (define-key map (kbd "C-c C-g") 'idris2-generate-def) (define-key map (kbd "C-c C-S-g") 'idris2-generate-def-next) ;; co: not in Idris2 yet (define-key map (kbd "C-c C-r") 'idris2-refine)