diff --git a/src/emacs/README.md b/src/emacs/README.md index a9653a969..a15c73722 100644 --- a/src/emacs/README.md +++ b/src/emacs/README.md @@ -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 M-x package-install. - [flycheck][flycheck] - [fill-column-indicator][fci] diff --git a/src/emacs/lean-cmd.el b/src/emacs/lean-cmd.el new file mode 100644 index 000000000..9890c996b --- /dev/null +++ b/src/emacs/lean-cmd.el @@ -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) diff --git a/src/emacs/lean-debug.el b/src/emacs/lean-debug.el new file mode 100644 index 000000000..1ee98c1f8 --- /dev/null +++ b/src/emacs/lean-debug.el @@ -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) diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el index fb4768375..18e26ff39 100644 --- a/src/emacs/lean-flycheck.el +++ b/src/emacs/lean-flycheck.el @@ -4,6 +4,8 @@ ;; Author: Soonho Kong ;; +(require 'lean-settings) + (defvar lean-flycheck-initialized nil "Return true if lean-flycheck has been initialized") diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el new file mode 100644 index 000000000..4bbdc7e23 --- /dev/null +++ b/src/emacs/lean-info.el @@ -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) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 6b6d170ca..e0ba2b095 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -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 ) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el new file mode 100644 index 000000000..506290453 --- /dev/null +++ b/src/emacs/lean-server.el @@ -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) diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el index 9e2c16c6b..b60d6e836 100644 --- a/src/emacs/lean-settings.el +++ b/src/emacs/lean-settings.el @@ -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") diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el new file mode 100644 index 000000000..376d31ba4 --- /dev/null +++ b/src/emacs/lean-type.el @@ -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) diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el index cb187cf83..420f7f0b2 100644 --- a/src/emacs/lean-util.el +++ b/src/emacs/lean-util.el @@ -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) diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el new file mode 100644 index 000000000..78a35b626 --- /dev/null +++ b/src/emacs/lean-variable.el @@ -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)