;;; -*- lexical-binding: t -*-

(require 'syd/base)
(require 'syd/handle)

(defun syd-agda-locate-and-load ()
  (interactive)
  (let ((agda-mode-path (executable-find "agda-mode")))
    (load-file
     (shell-command-to-string
      (format "%s locate" agda-mode-path))))
  (setq agda2-program-name (executable-find "agda")))

(defface syd-agda2-default
  `((t :font ,(font-spec :family "IBM Plex Sans" :size 17)
       :height unspecified))
  "Default face from which all agda2-* faces inherit.")

(defvar syd-agda2-symbol-font
  (font-spec :family "IBM Plex Math")
  "Math font for Agda symbols.")

(defvar syd-agda2-faces
  ;; (let (faces)
  ;;   (mapatoms (lambda (s)
  ;; 		(if (and (facep s) (s-prefix? "agda2-" (symbol-name s)))
  ;; 		    (push s faces))))
  ;;   faces)
  '(agda2-highlight-positivity-problem-face agda2-highlight-symbol-face
    agda2-highlight-coverage-problem-face agda2-highlight-record-face
    agda2-highlight-pragma-face agda2-highlight-inductive-constructor-face
    agda2-highlight-instance-problem-face agda2-highlight-dotted-face
    agda2-highlight-missing-definition-face agda2-highlight-deadcode-face
    agda2-highlight-error-face agda2-highlight-function-face
    agda2-highlight-string-face agda2-highlight-keyword-face
    agda2-highlight-datatype-face agda2-highlight-postulate-face
    agda2-highlight-primitive-type-face agda2-highlight-module-face
    agda2-highlight-operator-face agda2-highlight-primitive-face
    agda2-highlight-unsolved-constraint-face
    agda2-highlight-generalizable-variable-face
    agda2-highlight-catchall-clause-face agda2-highlight-field-face
    agda2-highlight-shadowing-in-telescope-face
    agda2-highlight-error-warning-face agda2-highlight-typechecks-face
    agda2-highlight-termination-problem-face
    agda2-highlight-confluence-problem-face agda2-highlight-macro-face
    agda2-highlight-coinductive-constructor-face
    agda2-highlight-bound-variable-face agda2-highlight-unsolved-meta-face
    agda2-highlight-cosmetic-problem-face agda2-highlight-number-face))

(with-eval-after-load 'project
  (add-to-list 'project-vc-extra-root-markers "*.agda-lib"))

(with-eval-after-load 'agda2
  (general-define-key
   :keymaps 'agda2-mode-map
   :states '(normal visual motion emacs insert)
   :major-modes t
   :prefix syd-localleader-key
   :non-normal-prefix syd-alt-localleader-key
   "?" #'agda2-show-goals
   "." #'agda2-goal-and-context-and-inferred
   "," #'agda2-goal-and-context
   "=" #'agda2-show-constraints
   "g" #'agda2-give
   "a" #'agda2-mimer-maybe-all
   "[" #'agda2-previous-goal
   "c" #'agda2-make-case
   "d" #'agda2-infer-type-maybe-toplevel
   "e" #'agda2-show-context
   "]" #'agda2-next-goal
   "h" #'agda2-helper-function-type
   "l" #'agda2-load
   "n" #'agda2-compute-normalised-maybe-toplevel
   "p" #'agda2-module-contents-maybe-toplevel
   "r" #'agda2-refine
   "s" #'agda2-solveAll
   "t" #'agda2-goal-type
   "w" #'agda2-why-in-scope-maybe-toplevel
   "x c" #'agda2-compile
   "x d" #'agda2-remove-annotations
   "x h" #'agda2-display-implicit-arguments
   "x q" #'agda2-quit
   "x r" #'agda2-restart)
  (general-def
    :keymaps 'agda2-mode-map
    :states '(motion normal)
    "[ n" #'agda2-previous-goal
    "] n" #'agda2-next-goal
    ;; FUCLK!!!!!!!!!
    "g d" #'agda2-goto-definition-keyboard
    "K" #'agda2-goal-and-context)
  ;; (setq agda2-fontset-name "JuliaMono")

  (add-to-list
   'auto-mode-alist
   '("\\.lagda\\.org\\'" . agda2-mode))

  (with-eval-after-load 'smartparens
    (sp-local-pair '(agda2-mode) "{!" "!}"))
  (with-eval-after-load 'evil-surround
    (syd-add-hook '(agda2-mode-hook)
      (defun syd-agda--configure-evil-surround-h ()
	(setq-local evil-surround-pairs-alist
		    (append '((?h . ("{!" . "!}")))
			    evil-surround-pairs-alist)))))
  ;; HACK: avoid org-mode bullshit occuring in literate agda projects
  ;; within my roam dir.
  (defun syd-agda--remove-org-roam-hooks-h ()
    (when (and (featurep 'org-roam)
	       (string-match-p (rx ".lagda.org" eol)
			       (buffer-file-name)))
      (remove-hook 'after-save-hook
		   #'org-roam-db-autosync--try-update-on-save-h t)))
  (add-hook 'agda2-mode-hook #'syd-agda--remove-org-roam-hooks-h
	    -10)

  (defun syd-agda-lookup-documentation ()
    (interactive "P")
    (call-interactively #'agda2-goal-and-context)
    agda2-info-buffer)

  (syd-handle 'agda2-mode
    :docs #'syd-agda-lookup-documentation)
  (setq agda-input-user-translations
	'(("inv" "⁻¹"))))

(with-eval-after-load 'agda2-highlight
  (set-face-attribute
   'agda2-highlight-symbol-face nil
   :family "IBM Plex Math")

  (defvar syd-agda-init-info-buffer-hook)

  (syd-defadvice syd-agda--run-agda-init-info-buffer-hook-a ()
    :after #'agda2-info-buffer
    (with-current-buffer agda2-info-buffer
      (run-hooks 'syd-agda-init-info-buffer-hook)))

  (syd-add-hook '(agda2-mode-hook syd-agda-init-info-buffer-hook)
    (defun syd-agda--configure-fonts-h ()
      (setq-local use-default-font-for-symbols nil)
      (buffer-face-set 'syd-agda2-default)
      (set-fontset-font
       t 'symbol syd-agda2-symbol-font))))

(provide 'syd/agda)
