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

feat(emacs): implement lean-show-type

Browse source
This commit is contained in:
Soonho Kong 2014-08-13 17:02:49 -07:00
parent d2ef577a14
commit 28d23390a6
11 changed files with 934 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/README.md
View file

@ -9,7 +9,7 @@ Requirement
-----------
``lean-mode`` requires [Emacs 24][emacs24] and following (optional)
packages which can be installed via ``M-x package-install``.
packages which can be installed via <kbd>M-x package-install</kbd>.
- [flycheck][flycheck]
- [fill-column-indicator][fci]

188
src/emacs/lean-cmd.el Normal file
View file

@ -0,0 +1,188 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(require 'lean-util)
;; Constructor
;; ===========
(defun lean-cmd-load (file-name)
"Load the Lean file named [file-name].
Lean will create a \"snapshot\" (aka backtracking point) after
each command. Lean uses the “snapshots” to process incremental
updates efficiently."
`(LOAD ,file-name))
(defun lean-cmd-visit (file-name)
"sets [file-name] as the \"current\" file.
Lean can keep information about multiple files. This command The
remaining commands are all with respect to the current file. If
[file-name] has not been loaded yet, then this command will load
it. Some of the remaining commands apply 'changes' to the current
file. The LOAD command can be used to discard all these changes,
and enforce the content of the file stored in file system."
`(VISIT ,file-name))
(defun lean-cmd-replace (line-number new-line)
"Replace the line [line-number] (in the current file) with [new-line].
Lean uses the snapshots to process the request efficiently. If
[line-number] is greater than the total number of lines in the
lean buffer, then empty lines are introduced. The lines are
indexed from 1."
`(REPLACE ,line-number ,new-line))
(defun lean-cmd-insert (line-number new-line)
"Insert [new-line] (in the current file) before line [line-number].
If [line-number] is greater than the total number of lines in the
lean buffer, then empty lines are introduced. The lines are
indexed from 1."
`(INSERT ,line-number ,new-line))
(defun lean-cmd-remove (line-number)
"Remove line [line-number] (in the current file).
The lines are indexed from 1. If [line-number] is greater than
the total number of lines in the lean buffer, then the command is
ignored."
`(REMOVE ,line-number))
(defun lean-cmd-info (line-number)
"Extracts typing information associated with line [line-number].
Lean produces a possible empty sequence of entries terminated with '--ENDINFO'"
`(INFO ,line-number))
(defun lean-cmd-check (line-number line)
"Check whether the text editor and Lean have the 'same view' of the current file + modifications"
`(CHECK ,line-number ,line))
;; Type
;; ====
(defun lean-cmd-type (cmd)
(cl-first cmd))
;; Get functions
;; =============
(defun lean-cmd-load-get-file-name (load-cmd)
(cl-second load-cmd))
(defun lean-cmd-visit-get-file-name (visit-cmd)
(cl-second visit-cmd))
(defun lean-cmd-replace-get-line-number (replace-cmd)
(cl-second replace-cmd))
(defun lean-cmd-replace-get-line (replace-cmd)
(cl-third replace-cmd))
(defun lean-cmd-insert-get-line-number (insert-cmd)
(cl-second insert-cmd))
(defun lean-cmd-insert-get-line (insert-cmd)
(cl-third insert-cmd))
(defun lean-cmd-remove-get-line-number (remove-cmd)
(cl-second remove-cmd))
(defun lean-cmd-info-get-line-number (info-cmd)
(cl-second info-cmd))
(defun lean-cmd-check-get-line-number (check-cmd)
(cl-second check-cmd))
(defun lean-cmd-check-get-line (check-cmd)
(cl-third check-cmd))
;; -- Test
(cl-assert (string= (lean-cmd-load-get-file-name (lean-cmd-load "nat.lean"))
"nat.lean"))
(cl-assert (string= (lean-cmd-visit-get-file-name (lean-cmd-visit "nat.lean"))
"nat.lean"))
(cl-assert (string=
(lean-cmd-load-get-file-name (lean-cmd-load "library/standard/bool.lean"))
"library/standard/bool.lean"))
(cl-assert (string=
(lean-cmd-load-get-file-name (lean-cmd-load "~/work/lean/basic.lean"))
"~/work/lean/basic.lean"))
(cl-assert (string=
(lean-cmd-visit-get-file-name (lean-cmd-visit "library/standard/bool.lean"))
"library/standard/bool.lean"))
(cl-assert (string=
(lean-cmd-visit-get-file-name (lean-cmd-visit "~/work/lean/basic.lean"))
"~/work/lean/basic.lean"))
(cl-assert (= (lean-cmd-replace-get-line-number
(lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
34))
(cl-assert (string= (lean-cmd-replace-get-line
(lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
"∀ (n : nat), ne (succ n) zero"))
(cl-assert (= (lean-cmd-insert-get-line-number
(lean-cmd-insert 34 "∀ (n : nat), ne (succ n) zero"))
34))
(cl-assert (string= (lean-cmd-insert-get-line
(lean-cmd-insert 34 "∀ (n : nat), ne (succ n) zero"))
"∀ (n : nat), ne (succ n) zero"))
(cl-assert (= (lean-cmd-insert-get-line-number (lean-cmd-remove 34))
34))
(cl-assert (= (lean-cmd-info-get-line-number (lean-cmd-info 34))
34))
(cl-assert (= (lean-cmd-check-get-line-number
(lean-cmd-check 34 "∀ (n : nat), ne (succ n) zero"))
34))
(cl-assert (string= (lean-cmd-check-get-line
(lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
"∀ (n : nat), ne (succ n) zero"))
;; to-string functions
;; ===================
(defun lean-cmd-load-to-string (cmd)
"Convert LOAD command to string"
(format "LOAD %s" (expand-file-name (lean-cmd-load-get-file-name cmd))))
(defun lean-cmd-visit-to-string (cmd)
"Convert VISIT command to string"
(format "VISIT %s" (expand-file-name (lean-cmd-load-get-file-name cmd))))
(defun lean-cmd-replace-to-string (cmd)
"Convert Replace command to string"
(format "REPLACE %d\n%s" (lean-cmd-replace-get-line-number cmd)
(lean-cmd-replace-get-line cmd)))
(defun lean-cmd-insert-to-string (cmd)
"Convert Insert command to string"
(format "INSERT %d\n%s" (lean-cmd-insert-get-line-number cmd)
(lean-cmd-insert-get-line cmd)))
(defun lean-cmd-remove-to-string (cmd)
"Convert Remove command to string"
(format "REMOVE %d" (lean-cmd-remove-get-line-number cmd)))
(defun lean-cmd-info-to-string (cmd)
"Convert Info command to string"
(format "INFO %d" (lean-cmd-info-get-line-number cmd)))
(defun lean-cmd-check-to-string (cmd)
"Convert Check command to string"
(format "CHECK %d\n%s" (lean-cmd-check-get-line-number cmd)
(lean-cmd-check-get-line cmd)))
(defun lean-cmd-to-string (cmd)
"Convert command to string"
(cl-case (lean-cmd-type cmd)
('LOAD (lean-cmd-load-to-string cmd))
('VISIT (lean-cmd-visit-to-string cmd))
('REPLACE (lean-cmd-replace-to-string cmd))
('INSERT (lean-cmd-insert-to-string cmd))
('REMOVE (lean-cmd-remove-to-string cmd))
('INFO (lean-cmd-info-to-string cmd))
('CHECK (lean-cmd-check-to-string cmd))))
;; -- Test
(cl-assert (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean"))
(concat "LOAD " (expand-file-name "~/work/lean/basic.lean"))))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-visit "~/work/lean/basic.lean"))
(concat "VISIT " (expand-file-name "~/work/lean/basic.lean"))))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-replace 42 "∀ (n : nat), ne (succ n) zero"))
(concat "REPLACE 42" "\n" "∀ (n : nat), ne (succ n) zero")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-insert 42 "∀ (n : nat), ne (succ n) zero"))
(concat "INSERT 42" "\n" "∀ (n : nat), ne (succ n) zero")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-remove 42))
(concat "REMOVE 42")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-info 42))
(concat "INFO 42")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-check 42 "∀ (n : nat), ne (succ n) zero"))
(concat "CHECK 42" "\n" "∀ (n : nat), ne (succ n) zero")))
;; ----------------
(provide 'lean-cmd)

13
src/emacs/lean-debug.el Normal file
View file

@ -0,0 +1,13 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(defun lean-debug-print (name obj)
"Display debugging output"
(message "[LEAN-DEBUG-PRINT] (%s):\n%s" name (prin1-to-string obj)))
(provide 'lean-debug)

2
src/emacs/lean-flycheck.el
View file

@ -4,6 +4,8 @@
;; Author: Soonho Kong
;;
(require 'lean-settings)
(defvar lean-flycheck-initialized nil
"Return true if lean-flycheck has been initialized")

217
src/emacs/lean-info.el Normal file
View file

@ -0,0 +1,217 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(require 'lean-util)
(require 'lean-debug)
;; Type Information
;; ----------------
(defun lean-typeinfo-str-p (str)
(string-prefix-p "-- TYPE|" str))
(defun lean-typeinfo-p (typeinfo)
(lean-typeinfo-str-p (cl-first typeinfo)))
(defun lean-typeinfo-pos (typeinfo)
(cl-second typeinfo))
(defun lean-typeinfo-parse-header (str)
(let ((items (split-string str "|")))
(list (string-to-number (cl-second items))
(string-to-number (cl-third items)))))
(defun lean-typeinfo-parse (seq)
(let ((header (lean-typeinfo-parse-header (car seq)))
(body (cdr seq)))
`(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)))
;; -- 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 (equal (lean-typeinfo-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
'(TYPE
(121 2)
("not (eq zero (succ m'))"
"→ decidable (eq zero (succ m'))"))))
(cl-assert (equal
(lean-typeinfo-pos
(lean-typeinfo-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
'(121 2)))
;; Overload Information
;; --------------------
(defun lean-overload-str-p (str)
(string-prefix-p "-- OVERLOAD|" str))
(defun lean-overload-p (overload)
(lean-overload-str-p (cl-first overload)))
(defun lean-overload-pos (overload)
(cl-second overload))
(defun lean-overload-parse-header (str)
(let ((items (split-string str "|")))
(list (string-to-number (cl-second items))
(string-to-number (cl-third items)))))
(defun lean-overload-parse (seq)
(let ((header (lean-overload-parse-header (car seq)))
(body (lean-split-seq (cdr seq) "--")))
`(OVERLOAD ,header ,body)))
;; -- Test
(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
(equal
(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'))"))
'(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'))")))))
(cl-assert (equal
(lean-overload-pos
(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'))")))
'(121 2)))
;; Basic
;; -----
(defun lean-info-type (info)
(cl-first info))
(defun lean-info-ack-str-p (str)
(string= "-- ACK" str))
(defun lean-info-endinfo-str-p (str)
(string= "-- ENDINFO" str))
(defun lean-info-pos (info)
(cl-case (lean-info-type info)
(TYPE (lean-typeinfo-pos info))
(OVERLOAD (lean-overload-pos info))))
;; -- test
(cl-assert (equal
(lean-info-pos
(lean-typeinfo-parse '("-- TYPE|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
'(121 2)))
(cl-assert (equal
(lean-info-pos
(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'))")))
'(121 2)))
;; Infolist Parsing
;; ================
(defun lean-infolist-split-lines (lines)
"Split lines into list of list of strings
Use \"-- ACK\" as a delim and stop processing when it encounters \"-- ENDINFO\""
(lean-split-seq-if
(split-string lines "\n")
'lean-info-ack-str-p
'(lambda (x) (not (lean-info-endinfo-str-p x)))))
(defun lean-infolist-filter-seq (seq)
"Filter warning and error messages"
(cl-loop for line in seq
when (and (not (search "warning:" line))
(not (search "error:" line)))
collect line))
(defun lean-infolist-parse (lines)
"TODO(soonhok): fill this"
(let ((string-seq-seq (lean-infolist-filter-seq (lean-infolist-split-lines lines))))
(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))))))
;; -- test
(cl-assert
(equal (lean-infolist-parse
(concat "-- TYPE|15|38" "\n"
"num" "\n"
"-- ACK" "\n"
"-- TYPE|15|40" "\n"
"num → num → Prop" "\n"
"-- ACK" "\n"
"-- OVERLOAD|15|42" "\n"
"f" "\n"
"--" "\n"
"foo.f" "\n"
"-- ACK" "\n"
"-- TYPE|15|42" "\n"
"num → num" "\n"
"-- ACK" "\n"
"-- TYPE|15|44" "\n"
"num" "\n"
"-- ACK" "\n"
"-- ENDINFO" "\n"))
'((TYPE (15 38) ("num"))
(TYPE (15 40) ("num → num → Prop"))
(OVERLOAD (15 42) (("f")
("foo.f")))
(TYPE (15 42) ("num → num"))
(TYPE (15 44) ("num")))))
(cl-assert
(equal
(lean-infolist-parse
(concat
"-- TYPE|121|2\nnot (eq zero (succ m')) → decidable (eq zero (succ m'))" "\n"
"-- ACK" "\n"
"-- TYPE|121|7\nne (succ m') zero → ne zero (succ m')" "\n"
"-- ACK" "\n"
"-- TYPE|121|16" "\n"
"∀ (n : nat), ne (succ n) zero" "\n"
"-- ACK" "\n"
"-- TYPE|121|29" "\n"
"nat" "\n"
"-- ACK" "\n"
"-- OVERLOAD|121|2" "\n"
"not (eq zero (succ m'))" "\n"
"→ decidable (eq zero (succ m'))" "\n"
"--" "\n"
"not (eq one (succ m'))" "\n"
"→ decidable (eq one (succ m'))" "\n"
"--" "\n"
"not (eq two (succ m'))" "\n"
"→ decidable (eq two (succ m'))" "\n"
"-- ENDINFO" "\n"))
'((TYPE (121 2) ("not (eq zero (succ m')) → decidable (eq zero (succ m'))"))
(TYPE (121 7) ("ne (succ m') zero → ne zero (succ m')"))
(TYPE (121 16) ("∀ (n : nat), ne (succ n) zero"))
(TYPE (121 29) ("nat"))
(OVERLOAD (121 2) (("not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")
("not (eq one (succ m'))" "→ decidable (eq one (succ m'))")
("not (eq two (succ m'))" "→ decidable (eq two (succ m'))"))))))
(provide 'lean-info)

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

@ -8,16 +8,18 @@
(require 'generic-x)
(require 'compile)
(require 'flymake)
(require 'lean-variable)
(require 'lean-util)
(require 'lean-settings)
(require 'lean-flycheck)
(require 'lean-input)
(require 'lean-type)
(defun lean-compile-string (exe-name args file-name)
"Concatenate exe-name, args, and file-name"
(format "%s %s %s" exe-name args file-name))
(defun lean-create-temp-in-system-tempdir (filename prefix)
(defun lean-create-temp-in-system-tempdir (file-name prefix)
"Create a temp lean file and return its name"
(make-temp-file (or prefix "flymake") nil ".lean"))
@ -25,8 +27,9 @@
"Execute Lean in the current buffer"
(interactive "sarg: ")
(let ((target-file-name
(or (buffer-file-name)
(flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir))))
(or
(buffer-file-name)
(flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir))))
(compile (lean-compile-string
(lean-get-executable lean-executable-name)
(or arg "")
@ -43,7 +46,8 @@
(defun lean-set-keys ()
(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-k" 'lean-hott-exe)
(local-set-key "\C-c\C-t" 'lean-show-type))
(define-abbrev-table 'lean-mode-abbrev-table '(
("var" "variable")
@ -77,17 +81,29 @@
(lean-set-keys)
(setq local-abbrev-table lean-mode-abbrev-table)
(abbrev-mode 1)
(add-hook 'before-change-functions '
lean-before-change-function nil t)
(add-hook 'after-change-functions '
lean-after-change-function nil t)
;; Draw a vertical line for rule-column
(when (and lean-rule-column
lean-show-rule-column-method)
(cl-case lean-show-rule-column-method
('vline (require 'fill-column-indicator)
(setq fci-rule-column lean-rule-column)
(setq fci-rule-color lean-rule-color)
(add-hook 'lean-mode-hook 'fci-mode))))
(add-hook 'lean-mode-hook 'fci-mode nil t))))
;; Delete Trailing Whitespace
(if lean-delete-trailing-whitespace
(progn (require 'whitespace-cleanup-mode)
(add-hook 'lean-mode-hook 'whitespace-cleanup-mode))
(add-hook 'lean-mode-hook 'whitespace-cleanup-mode nil t))
(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)
(eldoc-mode +1)
))
"A mode for Lean files" ;; doc string for this mode
)

174
src/emacs/lean-server.el Normal file
View file

@ -0,0 +1,174 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(require 'lean-variable)
(require 'lean-cmd)
(require 'lean-info)
(require 'lean-util)
;; Parameters
;; ==========
(defvar-local lean-server-process-name "lean-server")
(defvar-local lean-server-buffer-name "*lean-server*")
(defvar-local lean-server-option "--server")
;; How to read data from an async process
;; ======================================
(defun lean-server-has-error-p (buf-str)
"Return true if a buffer-string has --ERROR"
(lean-string-contains-line-p buf-str "-- ERROR"))
(defun lean-server-ready-to-process-p (buf-str)
"Return true if a buffer-string is ready to process"
(lean-string-contains-line-p buf-str "-- ENDINFO"))
(defun lean-server-cut-prefix (buf-str prefix)
"Cut prefix from the string"
(cond ((string-prefix-p prefix buf-str)
(substring-no-properties buf-str (length prefix)))
(t
(let* ((new-prefix (concat "\n" prefix))
(beg-pos (search new-prefix buf-str))
(len (length new-prefix)))
(when (not beg-pos)
error (concat prefix " is not found in buf-str " buf-str))
(substring-no-properties buf-str (+ beg-pos len))))))
;; -- Test
(cl-assert (string= (lean-server-cut-prefix "-- BEGININFO\nblablabla" "-- BEGININFO\n")
"blablabla"))
(cl-assert (string= (lean-server-cut-prefix "line1\nline2\n-- BEGININFO\nblablabla" "-- BEGININFO\n")
"blablabla"))
(defun lean-server-process-received-message (buf str)
"Process received message from lean-server"
(setq lean-global-info-buffer (concat lean-global-info-buffer str))
(with-current-buffer buf
(goto-char (point-max))
(insert "Received String:\n")
(insert str)
(insert "\n------------------\n")
(goto-char (point-max)))
(cond ((lean-server-ready-to-process-p lean-global-info-buffer)
(setq lean-global-info-buffer (lean-server-cut-prefix lean-global-info-buffer "-- BEGININFO\n"))
(setq lean-global-info-list (lean-infolist-parse lean-global-info-buffer))
(setq lean-global-info-processed t)
;; clear lean-global-info-buffer after processing
(setq lean-global-info-buffer "")
(with-current-buffer buf
(goto-char (point-max))
(prin1 lean-global-info-list buf)
(insert "\n=============================\n")))
((lean-server-has-error-p lean-global-info-buffer)
(setq lean-global-info-processed t)
;; clear lean-global-info-buffer after processing
(setq lean-global-info-buffer "")
(with-current-buffer buf
(goto-char (point-max))
(insert "Error Detected\n")
(insert "=============================\n")))))
(defun lean-server-output-filter (process string)
"Filter function attached to lean-server process"
(lean-server-process-received-message (process-buffer process) string))
;; How to create an async process
;; ==============================
(defun lean-server-create-process ()
"Create lean-server-process"
(let ((process-connection-type nil)
(lean-server-process
(start-process lean-server-process-name
lean-server-buffer-name
(lean-get-executable lean-executable-name)
lean-server-option)))
(set-process-coding-system lean-server-process 'utf-8 'utf-8)
(set-process-filter lean-server-process 'lean-server-output-filter)
(setq lean-global-info-buffer "")
(setq lean-global-server-current-file-name "")
(with-current-buffer (process-buffer lean-server-process)
(goto-char (point-max))
(insert "Server Created.\n")
(insert lean-global-server-current-file-name))
lean-server-process))
(defun lean-server-get-process ()
"Get the lean-server process.
If needed, create a one."
(let ((proc (get-process lean-server-process-name)))
(cond ((not proc) (lean-server-create-process))
((not (process-live-p proc)) (error "TODO(soonhok): need to kill and recreate one"))
(t proc))))
(defun lean-server-get-buffer ()
"Get the lean-server buffer"
(process-buffer (lean-server-get-process)))
;; How to send data to an async process
;; ====================================
(defun lean-flush-changed-lines ()
"Flush lean-changed-lines.
Send REPLACE commands to lean-server, reset lean-changed-lines to nil."
(cl-loop for n in lean-changed-lines
do (lean-server-send-cmd (lean-cmd-replace n (lean-grab-line n)))
finally (setq lean-changed-lines nil)))
(defun lean-server-check-current-file ()
"Check lean-global-server-current-file-name.
If it's not the same with (buffer-file-name), send VISIT cmd."
(let ((current-file-name (buffer-file-name)))
(unless (string= lean-global-server-current-file-name
current-file-name)
(lean-server-send-cmd (lean-cmd-visit current-file-name)))))
(defun lean-server-before-send-cmd (cmd)
"Operations to perform before sending a command"
(cl-case (lean-cmd-type cmd)
('LOAD ())
('VISIT ())
('REPLACE (lean-server-check-current-file))
('INSERT (lean-server-check-current-file))
('REMOVE (lean-server-check-current-file))
('INFO (lean-server-check-current-file)
(lean-flush-changed-lines)
(setq lean-global-info-processed nil)
(setq lean-global-info-buffer ""))
('CHECK (lean-server-check-current-file))))
(defun lean-server-after-send-cmd (cmd)
"Operations to perform after sending a commandn"
(cl-case (lean-cmd-type cmd)
('LOAD (setq lean-global-server-current-file-name
(lean-cmd-load-get-file-name cmd)))
('VISIT (setq lean-global-server-current-file-name
(lean-cmd-visit-get-file-name cmd)))
('REPLACE ())
('INSERT ())
('REMOVE ())
('INFO ())
('CHECK ())))
(defun lean-server-send-cmd (cmd)
"Send string to lean-server"
(let ((proc (lean-server-get-process))
(string-to-send (concat (lean-cmd-to-string cmd) "\n")))
(lean-server-before-send-cmd cmd)
;; Logging
(with-current-buffer (lean-server-get-buffer)
(goto-char (point-max))
(insert "Send\n===========\n")
(insert string-to-send)
(insert "==========\n"))
(process-send-string proc string-to-send))
(lean-server-after-send-cmd cmd))
;; TODO(soonhok): How to kill an async process
(provide 'lean-server)

2
src/emacs/lean-settings.el
View file

@ -8,7 +8,7 @@
(defgroup lean nil "Lean mode" :prefix 'lean :group 'languages)
(defvar lean-default-executable-name
(defvar-local lean-default-executable-name
(cl-case system-type
('gnu "lean")
('gnu/linux "lean")

194
src/emacs/lean-type.el Normal file
View file

@ -0,0 +1,194 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(require 'lean-variable)
(require 'lean-cmd)
(require 'lean-util)
(require 'lean-server)
(require 'lean-debug)
(defun lean-get-info-list (file-name line-number column)
"Get info list from lean server using file-name, line-number, and column.
TODO(soonhok): for now, it ignores file-name and column."
(lean-server-send-cmd (lean-cmd-info line-number))
(while (not lean-global-info-processed)
(accept-process-output (lean-server-get-process) 0 50 t))
lean-global-info-list)
(defun lean-filter-info-list (info-list when-pred)
"Filter info-list by given when-pred"
(cl-loop for info in info-list
when (funcall when-pred info)
collect info))
(defun lean-get-current-sym-info ()
"Return the information of current symbol at point.
The return valus has the form of '([symbol-string] [start-pos])"
(interactive)
(let ((bound (bounds-of-thing-at-point 'symbol))
start-pos end-pos sym)
(cond (bound
(setq start-pos (car bound))
(setq end-pos (cdr bound))
(setq sym (buffer-substring-no-properties start-pos end-pos)))
((= (point) (point-max))
(setq start-pos (point))
(setq sym ""))
(t
(setq start-pos (point))
(setq sym (buffer-substring-no-properties start-pos (1+ start-pos)))))
(list sym start-pos)))
(defun lean-eldoc-argument-list (string)
"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"
(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))))))
(defun lean-before-change-function (beg end)
"Function attached to before-change-functions hook.
It saves the following information to the global variable:
- lean-global-before-change-beg : beg
- lean-global-before-change-end : end
- lean-global-before-change-beg-line-number : line-number of beg
- lean-global-before-change-end-line-number : line-number of end
- lean-global-before-change-text : text between beg and end
These information will be used by lean-after-changed-function."
;; (message "lean-before-change %d %d" beg end)
(setq lean-global-before-change-beg beg)
(setq lean-global-before-change-end end)
(setq lean-global-before-change-beg-line-number (line-number-at-pos beg))
(setq lean-global-before-change-end-line-number (line-number-at-pos end))
(setq lean-global-before-change-text (buffer-substring-no-properties beg end)))
(defun lean-after-change-log (beg end after-beg-line-number after-end-line-number)
(message "before-change: beg=%d (%d) end=%d (%d)"
beg lean-global-before-change-beg-line-number
end lean-global-before-change-end-line-number)
(message "before-text:||%s||" lean-global-before-change-text)
(message "before-text # of lines = %d" (count-lines beg end))
(message "after-change: beg=%d (%d) end=%d (%d) leng-before=%d"
beg after-beg-line-number end after-end-line-number leng-before)
(message "after-text:||%s||" (buffer-substring-no-properties beg end))
(message "after-text # of lines = %d" (count-lines beg end))
(message "changed lines = %s" (prin1-to-string changed-lines))
(message "inserted lines = %s" (prin1-to-string inserted-lines))
(message "removed lines = %s" (prin1-to-string removed-lines))
(message "===================================="))
(defun lean-after-change-diff-lines (before-beg-line-number
before-end-line-number
after-beg-line-number
after-end-line-number)
"Given before and after (beg-line-number, end-line-number)
pairs, compute changed-lines, inserted-lines, and removed-lines."
(let* ((old-lines (cl-loop for n from before-beg-line-number to before-end-line-number
collect n))
(new-lines (cl-loop for n from after-beg-line-number to after-end-line-number
collect n))
(old-lines-len (length old-lines))
(new-lines-len (length new-lines))
changed-lines removed-lines inserted-lines)
;; (lean-debug-print "old-lines" old-lines)
;; (lean-debug-print "new-lines" new-lines)
(cond ((= old-lines-len new-lines-len)
(setq changed-lines old-lines)
;; (lean-debug-print "changed" changed-lines)
`(CHANGE-ONLY ,changed-lines))
;; Case "REMOVE"
((> old-lines-len new-lines-len)
(setq removed-lines (lean-take-first-n old-lines (- old-lines-len new-lines-len)))
;; Make sure that we return it in reverse order
(setq removed-lines (cl-sort removed-lines '>))
(setq changed-lines new-lines)
`(REMOVE ,removed-lines ,changed-lines))
;; Case "INSERT"
((< old-lines-len new-lines-len)
(setq inserted-lines (lean-take-last-n new-lines (- new-lines-len old-lines-len)))
;; Make sure that we return it in sorted order
(setq inserted-lines (cl-sort inserted-lines '<))
(setq changed-lines old-lines)
;; (lean-debug-print "inserted-lines" inserted-lines)
;; (lean-debug-print "changed-lines" changed-lines)
`(INSERT ,inserted-lines ,changed-lines)))))
(defun lean-after-changed-p (before-beg
before-end
after-beg
after-end
before-text
after-text)
"Return true if there is a really change"
(or (/= before-beg after-beg)
(/= before-end after-end)
(not (string= before-text after-text))))
(defun lean-after-change-handle-changes-only (changed-lines)
(cl-loop for n in changed-lines
do (add-to-list 'lean-changed-lines n))
;; (lean-debug-print "changes-only" lean-changed-lines)
)
(defun lean-after-change-handle-inserted (inserted-lines changed-lines)
;; (lean-debug-print "inserted lines" (cons inserted-lines changed-lines))
(lean-flush-changed-lines)
(cl-loop for n in inserted-lines
do (lean-server-send-cmd (lean-cmd-insert n (lean-grab-line n))))
(setq lean-changed-lines changed-lines)
(lean-flush-changed-lines))
(defun lean-after-change-handle-removed (removed-lines changed-lines)
;; (lean-debug-print "removed lines" (cons removed-lines changed-lines))
(lean-flush-changed-lines)
(cl-loop for n in removed-lines
do (lean-server-send-cmd (lean-cmd-remove n)))
(setq lean-changed-lines changed-lines)
(lean-flush-changed-lines))
(defun lean-after-change-function (beg end leng-before)
"Function attached to after-change-functions hook"
;; (message "lean-after-change-function: %d %d %d" beg end leng-before)
(let* ((before-beg lean-global-before-change-beg)
(before-end lean-global-before-change-end)
(before-beg-line-number lean-global-before-change-beg-line-number)
(before-end-line-number lean-global-before-change-end-line-number)
(after-beg-line-number (line-number-at-pos beg))
(after-end-line-number (line-number-at-pos end))
(before-text lean-global-before-change-text)
(after-text (buffer-substring-no-properties beg end)))
(when (lean-after-changed-p before-beg before-end beg end before-text after-text)
(pcase (lean-after-change-diff-lines before-beg-line-number before-end-line-number
after-beg-line-number after-end-line-number)
(`(CHANGE-ONLY ,changed-lines)
(lean-after-change-handle-changes-only changed-lines))
(`(INSERT ,inserted-lines ,changed-lines)
(lean-after-change-handle-inserted inserted-lines changed-lines))
(`(REMOVE ,removed-lines ,changed-lines)
(lean-after-change-handle-removed removed-lines changed-lines))))))
(provide 'lean-type)

96
src/emacs/lean-util.el
View file

@ -4,20 +4,94 @@
;; Author: Soonho Kong
;;
(require 'cl-lib)
(defun lean-concat-paths (&rest seq)
"Concatenate paths"
(cl-reduce (lambda (p1 p2) (concat (file-name-as-directory p1) p2))
seq))
(defun lean-string-contains-line-p (str line)
"return true if str contains line"
(or (string-prefix-p line str)
(search (concat "\n" line) str)))
(defun lean-grab-line (n)
"Return the contents of line n"
(let* ((cur-line-number (line-number-at-pos))
(rel-line-number (1+ (- n cur-line-number)))
(p1 (line-beginning-position rel-line-number))
(p2 (line-end-position rel-line-number)))
(buffer-substring-no-properties p1 p2)))
(defun lean-split-seq-if (seq delim-pred &optional while-pred)
(let ((result ())
(cell ()))
(cl-loop for item in seq
while (if while-pred (funcall while-pred item) t)
do (cond ((funcall delim-pred item)
(when cell
(setq result (cons (nreverse cell) result))
(setq cell nil)))
(t (setq cell (cons item cell))))
finally
(return (cond (cell (nreverse (cons (nreverse cell) result)))
(t (nreverse result)))))))
(defun lean-split-seq (seq delim)
(lean-split-seq-if seq (lambda (x) (equal delim x))))
(defun lean-take-first-n (seq n)
"Take first n elements from seq"
(cond ((< (length seq) n) seq)
(t (subseq seq 0 n))))
;; -- Test
(cl-assert (equal (lean-take-first-n '(1 2 3 4 5 6 7 8 9 10) 3)
'(1 2 3)))
(cl-assert (equal (lean-take-first-n '(1 2 3 4 5 6 7 8 9 10) 10)
'(1 2 3 4 5 6 7 8 9 10)))
(cl-assert (equal (lean-take-first-n '(1 2 3 4 5 6 7 8 9 10) 11)
'(1 2 3 4 5 6 7 8 9 10)))
(cl-assert (equal (lean-take-first-n '(1 2 3 4 5 6 7 8 9 10) 0)
nil))
(cl-assert (equal (lean-take-first-n '() 0)
nil))
(cl-assert (equal (lean-take-first-n '() 2)
nil))
(defun lean-take-last-n (seq n)
"Take first n elements from seq"
(let ((l (length seq)))
(cond ((< l n) seq)
(t (subseq seq (- l n) l)))))
;; -- Test
(cl-assert (equal (lean-take-last-n '(1 2 3 4 5 6 7 8 9 10) 3)
'(8 9 10)))
(cl-assert (equal (lean-take-last-n '(1 2 3 4 5 6 7 8 9 10) 10)
'(1 2 3 4 5 6 7 8 9 10)))
(cl-assert (equal (lean-take-last-n '(1 2 3 4 5 6 7 8 9 10) 11)
'(1 2 3 4 5 6 7 8 9 10)))
(cl-assert (equal (lean-take-last-n '(1 2 3 4 5 6 7 8 9 10) 0)
nil))
(cl-assert (equal (lean-take-last-n '() 0)
nil))
(cl-assert (equal (lean-take-last-n '() 2)
nil))
(defun lean-get-rootdir ()
(or lean-rootdir
(error "'lean-rootdir' is not defined. Please have\
(customize-set-variable 'lean-rootdir \"~/work/lean\")\
in your emacs configuration.\
Also make sure that your (custom-set-variable ...) comes before\
(require 'lean-mode).")))
(or
lean-rootdir
(error
(concat "'lean-rootdir' is not defined."
"Please have (customize-set-variable 'lean-rootdir \"~/work/lean\") "
"in your emacs configuration. "
"Also make sure that your (custom-set-variable ...) "
" comes before (require 'lean-mode)"))))
(defun lean-get-executable (exe-name)
"Return fullpath of lean executable"
(let ((lean-binary-dir-name "bin"))
(when lean-rootdir
(concat (file-name-as-directory (lean-get-rootdir))
(file-name-as-directory "bin")
exe-name))))
(let ((lean-bin-dir-name "bin"))
(lean-concat-paths (lean-get-rootdir) lean-bin-dir-name exe-name)))
(provide 'lean-util)

37
src/emacs/lean-variable.el Normal file
View file

@ -0,0 +1,37 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(defvar lean-global-info-list nil
"A placeholder we save the info-list that we get from lean server")
(defvar lean-global-info-processed nil
"A shared variable to indicate the finished processing of lean-info")
(defvar lean-global-info-buffer ""
"local buffer used to store messages sent by lean server")
(defvar lean-global-server-current-file-name ""
"Current filename that lean server is processing")
(defvar-local lean-changed-lines nil
"Changed lines")
(defvar-local lean-removed-lines nil
"Removed lines")
(defvar-local lean-inserted-lines nil
"Inserted lines")
(defvar lean-global-before-change-beg nil
"Before-change BEG")
(defvar lean-global-before-change-end nil
"Before-change END")
(defvar lean-global-before-change-beg-line-number nil
"Before-change BEG line-number")
(defvar lean-global-before-change-end-line-number nil
"Before-change END line-number")
(defvar lean-global-before-change-text ""
"Before-change text")
(provide 'lean-variable)