;; 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)