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

feat(emacs): show synth information

Browse source
This commit is contained in:
Soonho Kong 2014-08-14 13:22:24 -07:00
parent 8afd433f34
commit 24220a5f9e
2 changed files with 56 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -122,6 +122,47 @@
"not (eq one (succ m'))\n→ decidable (eq zero (succ m'))"
"not (eq two (succ m'))\n→ decidable (eq zero (succ m'))")))
;; Synth Information
;; ----------------
(defun lean-synth-type (synth)
(cl-first synth))
(defun lean-synth-p (synth)
(equal (lean-synth-type synth) 'SYNTH))
(defun lean-synth-pos (synth)
(cl-second synth))
(defun lean-synth-str-p (str)
(string-prefix-p "-- SYNTH|" str))
(defun lean-synth-str-seq-p (seq)
(lean-synth-str-p (cl-first seq)))
(defun lean-synth-parse-header (str)
(let ((items (split-string str "|")))
(list (string-to-number (cl-second items))
(string-to-number (cl-third items)))))
(defun lean-synth-parse (seq)
(let ((header (lean-synth-parse-header (car seq)))
(body (cdr seq)))
`(SYNTH ,header ,body)))
(defun lean-synth-body (synth)
(cl-third synth))
(defun lean-synth-body-str (synth)
(lean-string-join (lean-synth-body synth) "\n"))
;; -- Test
(cl-assert (lean-synth-str-p "-- SYNTH|121|2"))
(cl-assert (equal (lean-synth-parse-header "-- SYNTH|121|2")
'(121 2)))
(cl-assert (lean-synth-str-seq-p '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
(cl-assert (equal (lean-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
'(SYNTH
(121 2)
("not (eq zero (succ m'))"
"→ decidable (eq zero (succ m'))"))))
(cl-assert (equal
(lean-synth-pos
(lean-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
'(121 2)))
;; Basic
;; -----
(defun lean-info-type (info)
@ -133,7 +174,8 @@
(defun lean-info-pos (info)
(cl-case (lean-info-type info)
(TYPE (lean-typeinfo-pos info))
(OVERLOAD (lean-overload-pos info))))
(OVERLOAD (lean-overload-pos info))
(SYNTH (lean-synth-pos info))))
(defun lean-info-line-number (info)
(cl-first (lean-info-pos info)))
(defun lean-info-column (info)
@ -182,7 +224,8 @@ Use \"-- ACK\" as a delim and stop processing when it encounters \"-- ENDINFO\""
when string-seq
collect (cond
((lean-typeinfo-str-seq-p string-seq) (lean-typeinfo-parse string-seq))
((lean-overload-str-seq-p string-seq) (lean-overload-parse string-seq))))))
((lean-overload-str-seq-p string-seq) (lean-overload-parse string-seq))
((lean-synth-str-seq-p string-seq) (lean-synth-parse string-seq))))))
;; -- test
(cl-assert

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

@ -60,15 +60,19 @@ The return valus has the form of '([symbol-string] [start-pos])"
'lean-typeinfo-p)))
(overload
(cl-first (lean-filter-info-list info-list-at-pos
'lean-overload-p))))
(list typeinfo overload)))
'lean-overload-p)))
(synth
(cl-first (lean-filter-info-list info-list-at-pos
'lean-synth-p))))
(list typeinfo overload synth)))
(defun lean-print-info (typeinfo overload sym-name)
(defun lean-print-info (typeinfo overload synth 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))
(synth-value (when synth (lean-synth-body-str synth)))
(name (or synth-value overload-name sym-name))
(type-str (lean-typeinfo-body-str typeinfo))
(type-output-str
(format "%s : %s"
@ -80,7 +84,7 @@ The return valus has the form of '([symbol-string] [start-pos])"
(propertize "overloaded" 'face 'font-lock-keyword-face)
(lean-string-join (cdr overload-names) ", "))))
(output-str (concat type-output-str overload-output-str)))
(message output-str))))
(message "%s" output-str))))
(defun lean-eldoc-documentation-function ()
"Show information of lean expression at point if any"
@ -93,9 +97,9 @@ The return valus has the form of '([symbol-string] [start-pos])"
(start-pos (cl-second sym-info))
(start-column (- column (- (point) start-pos)))
typeinfo overload)
(cl-multiple-value-setq (typeinfo overload)
(cl-multiple-value-setq (typeinfo overload synth)
(lean-extract-info-at-pos file-name line-number column start-pos))
(lean-print-info typeinfo overload sym-name)))
(lean-print-info typeinfo overload synth sym-name)))
(defun lean-before-change-function (beg end)
"Function attached to before-change-functions hook.