michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs): show overload information

Browse source
This commit is contained in:
Soonho Kong 2014-08-14 06:22:01 -07:00 committed by Leonardo de Moura
parent 6f062a005e
commit 243cf2abb0
3 changed files with 83 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
src/emacs/lean-info.el
View file

@ -10,12 +10,16 @@
;; Type Information
;; ----------------
(defun lean-typeinfo-str-p (str)
(string-prefix-p "-- TYPE|" str))
(defun lean-typeinfo-type (typeinfo)
(cl-first typeinfo))
(defun lean-typeinfo-p (typeinfo)
(lean-typeinfo-str-p (cl-first typeinfo)))
(equal (lean-typeinfo-type typeinfo) 'TYPE))
(defun lean-typeinfo-pos (typeinfo)
(cl-second typeinfo))
(defun lean-typeinfo-str-p (str)
(string-prefix-p "-- TYPE|" str))
(defun lean-typeinfo-str-seq-p (seq)
(lean-typeinfo-str-p (cl-first seq)))
(defun lean-typeinfo-parse-header (str)
(let ((items (split-string str "|")))
(list (string-to-number (cl-second items))
@ -26,16 +30,14 @@
`(TYPE ,header ,body)))
(defun lean-typeinfo-body (typeinfo)
(cl-third typeinfo))
(defun lean-typeinfo-body-text (typeinfo)
(cl-reduce
(lambda (l1 l2) (concat l1 "\n" l2))
(lean-typeinfo-body typeinfo)))
(defun lean-typeinfo-body-str (typeinfo)
(string-join (lean-typeinfo-body typeinfo) "\n"))
;; -- Test
(cl-assert (lean-typeinfo-str-p "-- TYPE|121|2"))
(cl-assert (equal (lean-typeinfo-parse-header "-- TYPE|121|2")
'(121 2)))
(cl-assert (lean-typeinfo-p '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
(cl-assert (lean-typeinfo-str-seq-p '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
(cl-assert (equal (lean-typeinfo-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
'(TYPE
(121 2)
@ -48,12 +50,20 @@
;; Overload Information
;; --------------------
(defun lean-overload-str-p (str)
(string-prefix-p "-- OVERLOAD|" str))
(defun lean-overload-type (overload)
(cl-first overload))
(defun lean-overload-p (overload)
(lean-overload-str-p (cl-first overload)))
(equal (lean-overload-type overload) 'OVERLOAD))
(defun lean-overload-pos (overload)
(cl-second overload))
(defun lean-overload-names (overload)
(cl-loop for seq in (cl-third overload)
collect (string-join seq "\n")))
(defun lean-overload-str-p (str)
(string-prefix-p "-- OVERLOAD|" str))
(defun lean-overload-str-seq-p (seq)
(lean-overload-str-p (cl-first seq)))
(defun lean-overload-parse-header (str)
(let ((items (split-string str "|")))
(list (string-to-number (cl-second items))
@ -67,7 +77,7 @@
(cl-assert (lean-overload-str-p "-- OVERLOAD|121|2"))
(cl-assert (equal (lean-overload-parse-header "-- OVERLOAD|121|2")
'(121 2)))
(cl-assert (lean-overload-p '("-- OVERLOAD|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
(cl-assert (lean-overload-str-seq-p '("-- OVERLOAD|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
(cl-assert
(equal
(lean-overload-parse
@ -98,6 +108,20 @@
"→ decidable (eq zero (succ m'))")))
'(121 2)))
(cl-assert (equal (lean-overload-names (lean-overload-parse
'("-- OVERLOAD|121|2"
"not (eq zero (succ m'))"
"→ decidable (eq zero (succ m'))"
"--"
"not (eq one (succ m'))"
"→ decidable (eq zero (succ m'))"
"--"
"not (eq two (succ m'))"
"→ decidable (eq zero (succ m'))")))
'("not (eq zero (succ m'))\n→ decidable (eq zero (succ m'))"
"not (eq one (succ m'))\n→ decidable (eq zero (succ m'))"
"not (eq two (succ m'))\n→ decidable (eq zero (succ m'))")))
;; Basic
;; -----
(defun lean-info-type (info)
@ -110,6 +134,10 @@
(cl-case (lean-info-type info)
(TYPE (lean-typeinfo-pos info))
(OVERLOAD (lean-overload-pos info))))
(defun lean-info-line-number (info)
(cl-first (lean-info-pos info)))
(defun lean-info-column (info)
(cl-second (lean-info-pos info)))
;; -- test
(cl-assert (equal
@ -153,8 +181,8 @@ Use \"-- ACK\" as a delim and stop processing when it encounters \"-- ENDINFO\""
(cl-loop for string-seq in string-seq-seq
when string-seq
collect (cond
((lean-typeinfo-p string-seq) (lean-typeinfo-parse string-seq))
((lean-overload-p string-seq) (lean-overload-parse string-seq))))))
((lean-typeinfo-str-seq-p string-seq) (lean-typeinfo-parse string-seq))
((lean-overload-str-seq-p string-seq) (lean-overload-parse string-seq))))))
;; -- test
(cl-assert

6
src/emacs/lean-mode.el
View file

@ -47,7 +47,7 @@
(local-set-key "\C-c\C-x" 'lean-std-exe)
(local-set-key "\C-c\C-l" 'lean-std-exe)
(local-set-key "\C-c\C-k" 'lean-hott-exe)
(local-set-key "\C-c\C-t" 'lean-show-type))
(local-set-key "\C-c\C-t" 'lean-eldoc-documentation-function))
(define-abbrev-table 'lean-mode-abbrev-table '(
("var" "variable")
@ -100,9 +100,7 @@
(remove-hook 'lean-mode-hook 'whitespace-cleanup-mode))
;; eldoc
(set (make-local-variable 'eldoc-documentation-function)
'lean-show-type)
;; (set (make-local-variable 'eldoc-argument-case)
;; 'lean-eldoc-argument-list)
'lean-eldoc-documentation-function)
(eldoc-mode +1)
))
"A mode for Lean files" ;; doc string for this mode

48
src/emacs/lean-type.el
View file

@ -49,23 +49,53 @@ The return valus has the form of '([symbol-string] [start-pos])"
"Upcase and fontify STRING for use with `eldoc-mode'."
(propertize string 'face 'font-lock-variable-name-face))
(defun lean-show-type ()
"Show the type of lean expression at point if any"
(defun lean-extract-info-at-pos (file-name line-number column start-pos)
(let* ((info-list (lean-get-info-list file-name line-number column))
(info-list-at-pos (lean-filter-info-list
info-list
'(lambda (info) (= start-column (lean-info-column info)))))
(typeinfo
(cl-first (lean-filter-info-list info-list-at-pos
'lean-typeinfo-p)))
(overload
(cl-first (lean-filter-info-list info-list-at-pos
'lean-overload-p))))
(list typeinfo overload)))
(defun lean-print-info (typeinfo overload sym-name)
"Given typeinfo, overload, and sym-name, print out information."
(when typeinfo
(let* ((overload-names (lean-overload-names overload))
(overload-name (cl-first overload-names))
(name (or overload-name sym-name))
(type-str (lean-typeinfo-body-str typeinfo))
(type-output-str
(format "%s : %s"
(propertize name 'face 'font-lock-variable-name-face)
type-str))
(overload-output-str
(when overload-names
(format "\n%s with %s"
(propertize "overloaded" 'face 'font-lock-keyword-face)
(string-join (cdr overload-names) ", "))))
(output-str (concat type-output-str overload-output-str)))
(message output-str))))
(defun lean-eldoc-documentation-function ()
"Show information of lean expression at point if any"
(interactive)
(let* ((file-name (buffer-file-name))
(line-number (line-number-at-pos))
(column (current-column))
(info-list (lean-get-info-list file-name line-number column))
(sym-info (lean-get-current-sym-info))
(sym-name (cl-first sym-info))
(start-pos (cl-second sym-info))
(start-column (- column (- (point) start-pos)))
(filtered-info-list (lean-filter-info-list
info-list
'(lambda (info) (= start-column (cl-second (lean-info-pos info)))))))
(when (and filtered-info-list (= (length filtered-info-list) 1))
(message "%s: %s" (lean-eldoc-argument-list sym-name)
(lean-typeinfo-body-text (cl-first filtered-info-list))))))
typeinfo overload)
(cl-multiple-value-setq (typeinfo overload)
(lean-extract-info-at-pos file-name line-number column start-pos))
(lean-print-info typeinfo overload sym-name)))
(defun lean-before-change-function (beg end)
"Function attached to before-change-functions hook.