;; -*- lexical-binding: t; -*-
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'company)
(require 'company-etags)
(require 'dash)
(require 'dash-functional)
(require 'lean-tags)
(require 'lean-server)

(defun company-lean-hook ()
  (set (make-local-variable 'company-backends) '(company-lean))
  (setq-local company-tooltip-limit 20)                      ; bigger popup window
  (setq-local company-idle-delay nil)                         ; decrease delay before autocompletion popup shows
  (setq-local company-echo-delay 0)                          ; remove annoying blinking
  (setq-local company-begin-commands '(self-insert-command)) ; start autocompletion only after typing
  (company-mode t))

(defun company-lean--need-autocomplete ()
  (not (looking-back
        (rx (or "theorem" "definition" "lemma" "axiom" "parameter"
                "abbreviation" "variable" "hypothesis" "conjecture"
                "corollary")
            (+ white)
            (* (not white))))))

(defun company-lean--prefix ()
  "Returns the symbol to complete. Also, if point is on a dot,
triggers a completion immediately."
  (let ((prefix (company-grab-symbol)))
    (cond ((looking-at (rx symbol-start "_")) "")
          ((and
            (company-lean--need-autocomplete)
            (or
             (>= (length prefix) 1)
             (string-match "[_.]" prefix)))
           prefix))))

(defun company-lean--make-candidate (arg)
  (propertize (car arg) 'type (cdr arg)))

(defun company-lean--candidates (prefix)
  (let ((line-number (line-number-at-pos))
        (column-number (current-column))
        pattern)
    (lean-server-send-cmd-sync (lean-cmd-wait) 'identity)
    (cond
     ((looking-at (rx symbol-start "_"))
      (setq pattern (if current-prefix-arg
                        (read-string "Filter for find declarations (e.g: +intro -and): " "" nil "")
                      ""))
      (lean-server-send-cmd-sync (lean-cmd-findg line-number column-number pattern)
                                 (lambda (candidates)
                                   (lean-server-debug "executing continuation for FINDG")
                                   (-map 'company-lean--make-candidate candidates))))
     (t
      (lean-server-send-cmd-sync (lean-cmd-findp line-number prefix)
                                 (lambda (candidates)
                                   (lean-server-debug "executing continuation for FINDP")
                                   (-map 'company-lean--make-candidate candidates)))))))

(defun company-lean--location (arg)
  (lean-generate-tags)
  (let ((tags-table-list (company-etags-buffer-table)))
    (when (fboundp 'find-tag-noselect)
      (save-excursion
        (let ((buffer (find-tag-noselect arg)))
          (cons buffer (with-current-buffer buffer (point))))))))

(defun company-lean--annotation (candidate)
  (let ((type (get-text-property 0 'type candidate)))
    (when type
      (let* ((annotation-str (format " : %s" type))
             (annotation-len (length annotation-str))
             (candidate-len  (length candidate))
             (entry-width    (+ candidate-len
                                annotation-len))
             (allowed-width  (truncate (* 0.90 (window-body-width)))))
        (when (> entry-width allowed-width)
          (setq annotation-str
                (concat
                 (substring-no-properties annotation-str
                                         0
                                         (- allowed-width candidate-len 3))
                 "...")))
        annotation-str))))

(defun company-lean--pre-completion (args)
  (when (looking-at (rx "_"))
    (delete-forward-char 1)))

;;;###autoload
(defun company-lean (command &optional arg &rest ignored)
  (case command
    (prefix (company-lean--prefix))
    (candidates (company-lean--candidates arg))
    (annotation (company-lean--annotation arg))
    (location (company-lean--location arg))
    (pre-completion (company-lean--pre-completion arg))
    (sorted t)))

(defadvice company--window-width
    (after lean-company--window-width activate)
  (when (eq major-mode 'lean-mode)
    (setq ad-return-value (truncate (* 0.95 (window-body-width))))))

(defun replace-regex-return-position (regex rep string &optional start)
  "Find regex and replace with rep on string.

Return replaced string and start and end positions of replacement."
  (let* ((start   (or start 0))
         (len     (length string))
         (m-start (string-match regex string start))
         (m-end   (match-end 0))
         pre-string post-string matched-string replaced-string result)
    (cond (m-start
           (setq pre-string     (substring string 0 m-start))
           (setq matched-string (substring string m-start m-end))
           (setq post-string    (substring string m-end))
           (string-match regex matched-string)
           (setq replaced-string
                 (replace-match rep nil nil matched-string))
           (setq result (concat pre-string
                                replaced-string
                                post-string))
           `(,result ,m-start ,(+ m-start (length replaced-string)))
           ))))

(defun replace-regex-add-properties-all (regex rep string properties)
  "Find all occurrences of regex in string, and replace them with
rep. Then, add text-properties on the replaced region."
  (let ((replace-result-items (replace-regex-return-position regex rep string))
        (result string))
    (while replace-result-items
      (pcase replace-result-items
        (`(,replaced-string ,m-start ,m-end)
         (setq result replaced-string)
         (add-text-properties m-start m-end properties result)
         (setq replace-result-items
               (replace-regex-return-position regex rep result m-end)))))
    result))

(defadvice company-fill-propertize
  (after lean-company-fill-propertize activate)
  (when (eq major-mode 'lean-mode)
    (let* ((selected (ad-get-arg 3))
           (properties `(face (:foreground ,(face-foreground 'font-lock-keyword-face)
                               :background ,(face-background (if selected 'company-tooltip-selection
                                                               'company-tooltip)))
                         mouse-face company-tooltip))
           (old-return ad-return-value)
           (old-len    (length old-return))
           new-return new-len)
      (setq new-return
            (replace-regex-add-properties-all
             (rx "?" word-start (group (+ (not white))) word-end)
             "\\1"
             ad-return-value
             properties))
      (setq new-len (length new-return))
      (while (< (length new-return) old-len)
        (setq new-return
              (concat new-return " ")))
      (add-text-properties new-len old-len properties new-return)
      (setq ad-return-value new-return))))

(provide 'lean-company)