Skip to content

Commit 2489268

Browse files
keramkeram
committed
Update idris-make-lemma to insert lemma above
doc string of current function. Why: Previously if function had a doc string the lemma was inserted before signature but after the doc string requiring user to further adjust the position. Before: ```idris ||| Useful doc for foo foo_rhs : String -> String foo : String -> String foo str = foo_rhs str ``` After: ```idris foo_rhs : String -> String ||| Useful doc for foo foo : String -> String foo str = foo_rhs str ```
1 parent 09de86a commit 2489268

File tree

2 files changed

+138
-3
lines changed

2 files changed

+138
-3
lines changed

‎idris-commands.el

+25-3
Original file line numberDiff line numberDiff line change
@@ -653,12 +653,33 @@ Otherwise, case split as a pattern variable."
653653
(re-search-backward (if (idris-lidr-p)
654654
"^\\(>\\s-*\\)\\(([^)]+)\\|[a-zA-Z_0-9]+\\)\\s-*:"
655655
"^\\(\\s-*\\)\\(([^)]+)\\|[a-zA-Z_0-9]+\\)\\s-*:"))
656-
(let ((indentation (match-string 1)) end-point)
656+
(let ((indentation (match-string 1))
657+
end-point)
657658
(beginning-of-line)
659+
660+
;; make sure we are above the documentation string
661+
(forward-line -1)
662+
(while (and (not (looking-at-p "^\\s-*$"))
663+
(not (equal (point) (point-min)))
664+
(or (looking-at-p "^|||") (looking-at-p "^--")))
665+
(forward-line -1))
666+
667+
;; if we reached beginning of file
668+
;; add new line between the type signature and the lemma
669+
(if (equal (point) (point-min))
670+
(progn
671+
(newline 1)
672+
(forward-line -1))
673+
;; otherwise find first non empty line
674+
(forward-line -1)
675+
(when (looking-at-p "^.*\\S-.*$")
676+
(forward-line 1)
677+
(newline 1)))
678+
658679
(insert indentation)
659680
(setq end-point (point))
660681
(insert type-decl)
661-
(newline 2)
682+
(newline 1)
662683
;; make sure point ends up ready to start a new pattern match
663684
(goto-char end-point))))
664685
((equal lemma-type :provisional-definition-lemma)
@@ -669,7 +690,8 @@ Otherwise, case split as a pattern variable."
669690
(let ((next-defn-point
670691
(re-search-forward (if (idris-lidr-p)
671692
"^\\(>\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:"
672-
"^\\(\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:") nil t)))
693+
"^\\(\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:")
694+
nil t)))
673695
(if next-defn-point ;; if we found a definition
674696
(let ((indentation (match-string 1)) end-point)
675697
(goto-char next-defn-point)

‎test/idris-commands-test.el

+113
Original file line numberDiff line numberDiff line change
@@ -313,6 +313,119 @@ myReverse xs = revAcc [] xs where
313313
(delete-directory mock-directory-name t)
314314
(idris-quit))))
315315

316+
(ert-deftest idris-test-idris-make-lemma ()
317+
"Test `idris-make-lemma' replacing a hole with a metavariable lemma."
318+
(cl-flet ((idris-load-file-sync-stub () nil)
319+
(idris-eval-stub (&optional &rest args)
320+
'((:metavariable-lemma
321+
(:replace-metavariable "closeDistance_rhs s1 s2")
322+
(:definition-type "closeDistance_rhs : String -> String -> IO Bool")))))
323+
(advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
324+
(advice-add 'idris-eval :override #'idris-eval-stub)
325+
(unwind-protect
326+
(progn
327+
(with-temp-buffer
328+
(insert "closeDistance : String -> String -> IO Bool
329+
closeDistance s1 s2 = ?closeDistance_rhs")
330+
(goto-char (point-min))
331+
(re-search-forward "closeDistance_rh")
332+
(funcall-interactively 'idris-make-lemma)
333+
(should (string= "closeDistance_rhs : String -> String -> IO Bool
334+
335+
closeDistance : String -> String -> IO Bool
336+
closeDistance s1 s2 = closeDistance_rhs s1 s2"
337+
(buffer-substring-no-properties (point-min) (point-max)))))
338+
339+
(with-temp-buffer
340+
(insert "something_else
341+
342+
closeDistance : String -> String -> IO Bool
343+
closeDistance s1 s2 = ?closeDistance_rhs")
344+
(goto-char (point-min))
345+
(re-search-forward "closeDistance_rh")
346+
(funcall-interactively 'idris-make-lemma)
347+
(should (string= "something_else
348+
349+
closeDistance_rhs : String -> String -> IO Bool
350+
351+
closeDistance : String -> String -> IO Bool
352+
closeDistance s1 s2 = closeDistance_rhs s1 s2"
353+
(buffer-substring-no-properties (point-min) (point-max)))))
354+
355+
(with-temp-buffer
356+
(insert "something_else
357+
358+
closeDistance : String -> String -> IO Bool
359+
closeDistance s1 s2 = ?closeDistance_rhs")
360+
(goto-char (point-min))
361+
(re-search-forward "closeDistance_rh")
362+
(funcall-interactively 'idris-make-lemma)
363+
(should (string= "something_else
364+
365+
closeDistance_rhs : String -> String -> IO Bool
366+
367+
closeDistance : String -> String -> IO Bool
368+
closeDistance s1 s2 = closeDistance_rhs s1 s2"
369+
(buffer-substring-no-properties (point-min) (point-max)))))
370+
371+
(with-temp-buffer
372+
(insert "||| Check if two strings are close enough to be similar,
373+
||| using the namespace distance criteria.
374+
closeDistance : String -> String -> IO Bool
375+
closeDistance s1 s2 = ?closeDistance_rhs")
376+
(goto-char (point-min))
377+
(re-search-forward "closeDistance_rh")
378+
(funcall-interactively 'idris-make-lemma)
379+
(should (string= "closeDistance_rhs : String -> String -> IO Bool
380+
381+
||| Check if two strings are close enough to be similar,
382+
||| using the namespace distance criteria.
383+
closeDistance : String -> String -> IO Bool
384+
closeDistance s1 s2 = closeDistance_rhs s1 s2"
385+
(buffer-substring-no-properties (point-min) (point-max)))))
386+
387+
(with-temp-buffer
388+
(insert "something_else
389+
390+
||| Check if two strings are close enough to be similar,
391+
||| using the namespace distance criteria.
392+
closeDistance : String -> String -> IO Bool
393+
closeDistance s1 s2 = ?closeDistance_rhs")
394+
(goto-char (point-min))
395+
(re-search-forward "closeDistance_rh")
396+
(funcall-interactively 'idris-make-lemma)
397+
;; (message "%s" (buffer-substring-no-properties (point-min) (point-max)))
398+
(should (string= "something_else
399+
400+
closeDistance_rhs : String -> String -> IO Bool
401+
402+
||| Check if two strings are close enough to be similar,
403+
||| using the namespace distance criteria.
404+
closeDistance : String -> String -> IO Bool
405+
closeDistance s1 s2 = closeDistance_rhs s1 s2"
406+
(buffer-substring-no-properties (point-min) (point-max)))))
407+
408+
(with-temp-buffer
409+
(insert "something else
410+
411+
-- some inline comment
412+
closeDistance : String -> String -> IO Bool
413+
closeDistance s1 s2 = ?closeDistance_rhs")
414+
(goto-char (point-min))
415+
(re-search-forward "closeDistance_rh")
416+
(funcall-interactively 'idris-make-lemma)
417+
(should (string= "something else
418+
419+
closeDistance_rhs : String -> String -> IO Bool
420+
421+
-- some inline comment
422+
closeDistance : String -> String -> IO Bool
423+
closeDistance s1 s2 = closeDistance_rhs s1 s2"
424+
(buffer-substring-no-properties (point-min) (point-max))))))
425+
426+
(advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
427+
(advice-remove 'idris-eval #'idris-eval-stub))))
428+
316429
;; Tests by Yasuhiko Watanabe
317430
;; https://github.com/idris-hackers/idris-mode/pull/537/files
318431
(idris-ert-command-action "test-data/CaseSplit.idr" idris-case-split idris-test-eq-buffer)

0 commit comments

Comments
 (0)