;; Time-stamp: <2024-07-13 15h02 CEST (471b3659)>

;; -----------------------------------------------------------------------------
;; Coq

;; (defvar pg-inserted-newline nil)
;; (defconst pg-whitespace-match "[ \\t]")
;; (defconst pg-subgoal-match "[*+\\-]")

;; (defun pg-move-point-dwim ()
;;   (interactive)
;;   ;; Did we move to a blank new line?
;;   (when (= (point) (point-at-bol))
;;     ;; If there's nothing here, lets add another line below
;;     (when (looking-at-p (concat pg-whitespace-match "*$"))
;;       (save-excursion (newline))
;;       (setq pg-inserted-newline t))
;;     ;; Now let's work out where the point should go
;;     (previous-line)
;;     (beginning-of-line)
;;     ;; Is the previous line essentially a subgoal marker?
;;     (if (looking-at-p (concat pg-whitespace-match "*"
;;                               pg-subgoal-match "+"
;;                               pg-whitespace-match "*$"))
;;         ;; If so, trim the line and put the point in after the subgoal marker
;;         (progn
;;           (delete-trailing-whitespace (point-at-bol) (point-at-eol))
;;           (end-of-line)
;;           (insert-char ? ))
;;       ;; If not, go back to where we were and indent
;;       (next-line)
;;       (indent-for-tab-command))))

(defconst coq-env '(("UniMath"
                     :topdir "~/theorems/UniMath/"
                     :binary "/usr/bin/coqtop"
                     :args ("-emacs" "-noinit" "-indices-matter"
                            "-type-in-type" "-w" "-notation-overridden"
                            "-Q" "/home/tslil/theorems/UniMath/UniMath" "UniMath"
                            "-Q" "/home/tslil/typeset/proof_relevant_cats/formalisation" "PRCats"))
                    ("HoTT"
                     :topdir "~/theorems/Coq-HoTT/"
                     :binary "/usr/bin/coqtop"
                     :args ("-noinit" "-indices-matter"))))

(defvar use-coq-env "UniMath")

(defun mike-implicify (ntimes)
  (interactive "p")
  (save-excursion
    (re-search-backward "(\\|{")
    (dotimes (i ntimes)
      (if (looking-at "(")
          (progn (delete-char 1)
                 (insert "{")
                 (backward-char 1)
                 (forward-sexp 1)
                 (delete-char -1)
                 (insert "}"))
        (progn (delete-char 1)
               (insert "(")
               (backward-char 1)
               (forward-sexp 1)
               (delete-char -1)
               (insert ")")))
      (re-search-forward "(\\|{")
      (backward-char 1))))

(defun coq-local-environment ()
  (require 'corral)
  (bind-keys :map coq-mode-map
             ("M-i" . mike-implicify)
             ("M-a" . forward-sexp)
             ("M-e" . backward-sexp)
             ("M-/" . lh-matching-delim)
             ("M-(" . corral-parentheses-forward)
             ("M-)" . corral-parentheses-backward)
             ("M-{" . corral-braces-forward)
             ("M-}" . corral-braces-backward)
             ("M-[" . corral-brackets-forward)
             ("M-]" . corral-brackets-backward)
             ("C-(" . lh-slurp-forward)
             ("C-)" . lh-slurp-backward)
             ("C-s" . isearch-forward))
  (let* ((data (alist-get use-coq-env coq-env nil nil #'string-equal))
         (topdir (expand-file-name (plist-get data :topdir)))
         (binary (plist-get data :binary))
         (args (plist-get data :args)))
    (dolist (var '(coq-use-project-file coq-prog-args coq-prog-name))
      (make-local-variable var))
    (setq coq-use-project-file t
          coq-prog-args args
          coq-prog-name binary)
    ;; TAGS
    (visit-tags-table (concat topdir "TAGS")))
  ;; Formatting
  (setq fill-column 70)
  (visual-line-mode 1)
  (set-fringe-mode 0)
  (make-local-variable 'before-save-hook)
  (add-hook 'before-save-hook 'delete-trailing-whitespace)
  (setq proof-three-window-mode-policy 'hybrid
        proof-layout-windows-on-visit-file t
        proof-shrink-windows-tofit t
        proof-script-fly-past-comments t)
  ;; Tweak syntax table
  ;; (modify-syntax-entry ?' "w")
  ;; Use agda input method
  ;; (agda-input-setup)
  ;; (activate-input-method "Agda")
  )

(use-package proof-general
  :ensure
  :defer
  :functions coq-local-environment
  :init (setq proof-splash-enable nil
              proof-follow-mode 'followdown)
  ;; It's really annoying to have the code truncated due to equal
  ;; division ratios of the windows. The 5 is to accomodate line
  ;; numbers and the like
  (defadvice proof-layout-windows (after resize-window-properly activate)
    (let ((ww (window-width)))
      (when (< ww (+ 5 fill-column))
        (enlarge-window-horizontally (- (+ 5 fill-column) ww)))))
  :mode ("\\.v$" . coq-mode)
  :hook (coq-mode . (lambda ()
                      (programming-setup)
                      (coq-local-environment)
                      (auto-fill-mode))))

;; -----------------------------------------------------------------------------
;; Agda

;; (load-file (let ((coding-system-for-read 'utf-8))
;;              (shell-command-to-string "agda-mode locate")))

;; (add-hook 'agda2-mode
;;           (lambda ()
;;             (subword-mode 1)
;;             (auto-fill-mode)
;;             (aggressive-indent-mode -1)))

;; -----------------------------------------------------------------------------
;; Lean

;; (use-package lean-mode
;;   :ensure t
;;   :defer t
;;   :mode ("\\.lean$" . lean-mode))