;;; elpi-mode.el --- ELPI Major Mode		-*- lexical-binding: t; -*-

;; Copyright (C) 2023  Philip Kaludercic

;; Author: Philip Kaludercic <philipk@posteo.net>
;; Keywords: languages

;; This program is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or
;; (at your option) any later version.

;; This program is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.

;; You should have received a copy of the GNU General Public License
;; along with this program.  If not, see <https://www.gnu.org/licenses/>.

;;; Commentary:

;; Primitive Emacs support for the λProlog implementation ELPI
;; (https://github.com/LPCIC/elpi).

;;; Code:

(eval-when-compile (require 'rx))
(require 'comint)

(defgroup elpi-mode '()
  "Major mode for Lambda Prolog."
  :group 'languages)

(defvar elpi-interaction-font-lock-keywords
  '(("#\\(search\\|quit\\|query\\|help\\|load\\|compile\\)\\(\.\\| \\)" . font-lock-builtins-face)
    ("Teyjus>" . font-lock-header-face)
    (".+\\?\\-" . font-lock-definitions-face)
    ("\\?\\-" . (0 font-lock-header-face t))))

(defvar elpi-font-lock-keywords
  `(
    ;; Cut
    ("!" . font-lock-escape-face)
    ;; Headers
    (,(rx (group (or bol " ")) (group (or "module" "sig")) " ")
     . font-lock-preprocessor-face)
    ;; Builtin keywords
    (,(rx word-start
	  (group (or "abs" "sqrt" "sin" "cos" "arctan" "ln" "floor" "ceil" "truncate"
		     "rabs" "size" "chr" "string_to_int" "substring" "int_to_string"
		     "real_to_string" "std_in" "std_out" "std_err" "is" "open_in"
		     "open_out" "open_string" "open_append" "close_in" "close_out"
		     "term_to_string" "string_to_term" "input" "output" "input_line"
		     "lookahead" "eof" "flush" "print" "read" "printterm" "readterm"
		     "nil" "not" "true" "fail" "pi" "sigma" "i" "o" "if"))
	  word-end)
     2 font-lock-builtin-face keep t)
    ;; Preamble statements
    (,(rx (group (or bol " "))
	  (group (or "accumulate" "import" "accum_sig"))
	  (group " "))
     2 font-lock-preprocessor-face keep t)
    ;; Type/Kind declarations
    (,(rx (group (or bol " "))
	  (group (or "pred" "type" "kind" "infix" "infixl" "infixr" "prefix" "prefixr"
		     "postfix" "postfixl" "local" "exportdef" "useonly"))
	  (group " "))
     2 font-lock-builtin-face keep t)
    ;; Types
    (,(rx (group (or "int" "real" "string" "list" "out_stream" "in_stream" "any")))
     1 font-lock-type-face keep t)
    (,(rx "\"\\(" (not (any "A-Za-z" "_")) "\\)\\(o\\)\\("
	  (not (any "A-Za-z" "_")) "\\)\"")
     2 font-lock-type-face keep t)
    ;; Variables and constants
    (,(rx "_" (* word)) . 'shadow)
    (,(rx (group (+ word)) "." (+ word)) 1 font-lock-constant-face)
    (,(rx (group word-start (any "a-z") (* word) word-end))
     1 font-lock-function-name-face)
    (,(rx bow (any upper) (* word)) . font-lock-variable-name-face)
    (,(rx (: (any lower) (* word))) . font-lock-constant-face)
    ;; Connectives that do not need spaces around them
    (,(rx (any ",;|")) 0 font-lock-keyword-face t)
    ;; Logical and mathematical connectives
    (,(rx (group (or "->" ":-" "=>" "=" "::" "+" "*" "&" "\\"  "" "<" ">" ">=" "=<" "-")))
     1 font-lock-keyword-face keep t)

    ;; Comments
    (,(rx "%" (* nonl) eol) 0 font-lock-comment-face t)
    ))

(defvar elpi-mode-syntax-table
  (let ((st (make-syntax-table)))
    ;; (set-char-table-parent st prolog-mode-syntax-table)
    (modify-syntax-entry ?_ "w" st)
    (modify-syntax-entry ?\\ "\\" st)
    (modify-syntax-entry ?/ "w" st)
    (modify-syntax-entry ?* "w" st)
    (modify-syntax-entry ?+ "w" st)
    (modify-syntax-entry ?- "w" st)
    (modify-syntax-entry ?= "w" st)
    (modify-syntax-entry ?% "<" st)
    (modify-syntax-entry ?\n ">" st)
    (modify-syntax-entry ?< "w" st)
    (modify-syntax-entry ?> "w" st)
    (modify-syntax-entry ?\' "_" st)
    st))

;; Implementation-Specific Details
(defvar elpi-prompt-regexp (rx bol "goal> "))
(defvar elpi-executable "elpi")

(defvar elpi-executable-name "elpi")

(defcustom elpi-repl-display-action
  (cons
   (list #'display-buffer-reuse-window
	 #'display-buffer-pop-up-window)
   '())
  "Display action for the Elpi REPL used by `elpi-run-elpi'."
  :type display-buffer--action-custom-type)

(defun elpi-compile ()
  "Compile and type-check the current file."
  (interactive)
  (compile
   (mapconcat
    #'shell-quote-argument
    (list "elpi"			;REPLACEME
	  (or (buffer-file-name)
	      (user-error "Buffer has no file name")))
    " ")))

(defun elpi-run-elpi ()
  "Create or display an existing Comint buffer with an Elpi REPL."
  (interactive)
  (display-buffer
   (make-comint "*elpi*" elpi-executable)
   (car elpi-repl-display-action)
   (cdr elpi-repl-display-action)))

(defalias 'run-elpi #'elpi-run-elpi)

(defvar elpi-mode-map
  (let ((map (make-sparse-keymap)))
    (define-key map (kbd "C-c C-c") #'elpi-compile)
    (define-key map (kbd "C-c C-z") #'elpi-run-elpi)
    map))

;;;###autoload
(define-derived-mode elpi-mode prog-mode "λProlog"
  "Major mode for editing λProlog programmes."
  (setq-local comment-start "%")
  (setq-local comment-end "")
  (setq-local comment-start-skip "%+ *")
  (setq-local font-lock-defaults '(elpi-font-lock-keywords nil nil)))

;;;###autoload
(add-to-list 'auto-mode-alist '("\\.elpi\\'" . elpi-mode))

(provide 'elpi-mode)
;;; elpi-mode.el ends here