;;; beluga-mode.el --- Major mode for Beluga source code  -*- coding: utf-8; lexical-binding:t -*-

;; Copyright (C) 2009-2018  Free Software Foundation, Inc.

;; Author: Stefan Monnier <monnier@iro.umontreal.ca>
;; Maintainer: beluga-dev@cs.mcgill.ca
;; Version: 0
;; Keywords:

;; 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 <http://www.gnu.org/licenses/>.

;;; Commentary:

;; BUGS

;; - Indentation thinks "." can only be the termination marker of
;;   an LF declaration.  This can mess things up badly.
;; - Indentation after curried terms like "fn x => fn y =>" is twice that
;;   after "fn x y =>".

;;; Code:

(eval-when-compile (require 'cl-lib))
(require 'smie)

(require 'ansi-color)
(add-hook 'compilation-filter-hook 'ansi-color-compilation-filter)

(provide 'beluga-unicode-input-method)
(require 'quail)

(defconst beluga-input-method-name
  "beluga-unicode"
  "The name of the Beluga unicode input method.")

(quail-define-package
 beluga-input-method-name ;; name
 "UTF-8"                  ;; language
 "B"                      ;; mode-line "title"
 t                        ;; guidance
 "Beluga unicode input method: actually replaces keyword strings with
a single unicode character instead of merely representing the keywords
in unicode using Font Lock mode."
  nil nil nil nil nil nil nil nil nil nil t)
;; This very final t is the SIMPLE flag of quail-define-package, and
;; causes Quail to not affect the meanings of C-{f,b,n,p} or TAB.

(quail-define-rules
 ;; Greek letters
 ("\\alpha" ["α"])
 ("\\Alpha" ["Α"])
 ("\\beta" ["β"])
 ("\\Beta" ["Β"])
 ("\\gamma" ["γ"])
 ("\\Gamma" ["Γ"])
 ("\\delta" ["δ"])
 ("\\Delta" ["Δ"])
 ("\\epsilon" ["ε"])
 ("\\Epsilon" ["Ε"])
 ("\\zeta" ["ζ"])
 ("\\Zeta" ["Ζ"])
 ("\\eta" ["η"])
 ("\\Eta" ["Η"])
 ("\\theta" ["θ"])
 ("\\Theta" ["Θ"])
 ("\\iota" ["ι"])
 ("\\Iota" ["Ι"])
 ("\\kappa" ["κ"])
 ("\\Kappa" ["Κ"])
 ("\\lambda" ["λ"])
 ("\\Lambda" ["Λ"])
 ("\\lamda" ["λ"])
 ("\\Lamda" ["Λ"])
 ("\\mu" ["μ"])
 ("\\Mu" ["Μ"])
 ("\\nu" ["ν"])
 ("\\Nu" ["Ν"])
 ("\\xi" ["ξ"])
 ("\\Xi" ["Ξ"])
 ("\\omicron" ["ο"])
 ("\\Omicron" ["Ο"])
 ("\\pi" ["π"])
 ("\\Pi" ["Π"])
 ("\\rho" ["ρ"])
 ("\\Rho" ["Ρ"])
 ("\\sigma" ["σ"])
 ("\\Sigma" ["Σ"])
 ("\\tau" ["τ"])
 ("\\Tau" ["Τ"])
 ("\\upsilon" ["υ"])
 ("\\Upsilon" ["Υ"])
 ("\\phi" ["φ"])
 ("\\Phi" ["Φ"])
 ("\\chi" ["χ"])
 ("\\Chi" ["Χ"])
 ("\\psi" ["ψ"])
 ("\\Psi" ["Ψ"])
 ("\\omega" ["ω"])
 ("\\Omega" ["Ω"])

 ;; Common logical symbol
 ("\\conj" ["∧"])
 ("\\disj" ["∨"])
 ("\\imp"  ["⊃"])
 ("\\top"  ["⊤"])
 ("\\bot"  ["⊥"])

 ("\\equiv"  ["≣"])
  
 ;; Arrows
 ("->" ["→"])
 ("<-" ["←"])
 ("=>" ["⇒"])

 ;;LF
 ("|-" ["⊢"])
 ("\\not" ["¬"])
 ("::" ["∷"])
 ("FN" ["Λ"])
)

(defgroup beluga-mode ()
  "Editing support for the Beluga language."
  :group 'languages)

(defvar beluga-mode-map
  (let ((map (make-sparse-keymap)))
    (define-key map "\C-c\C-c" 'compile)
    (define-key map "\C-c\C-l" 'beluga-highlight-holes)
    (define-key map "\C-c\C-e" 'beluga-erase-holes)
    (define-key map "\C-c\C-x" 'beluga-run-command)
    (define-key map "\C-c\C-t" 'beluga-get-type)
    (define-key map "\C-c\C-s" 'beluga-split-hole)
    (define-key map "\C-c\C-i" 'beluga-intro-hole)
    (define-key map "\C-c\C-j" 'beluga-hole-jump)
    (define-key map "\C-c\C-p" 'beluga-hole-info)
    map))

(defvar beluga-mode-syntax-table
  (let ((st (make-syntax-table)))
    (modify-syntax-entry ?% "< 14" st)
    (modify-syntax-entry ?\{ "(}2 b" st)
    (modify-syntax-entry ?\} "){3 b" st)
    (modify-syntax-entry ?\n ">" st)
    ;; the following line breaks using / in identifiers
    ;; (modify-syntax-entry ?/ "$/" st)
    ;; For application of dependent arguments "exp A < ctx . term >", we'd want
    ;; <..> to match, but that breaks ->, <-, and other things.
    ;; (modify-syntax-entry ?< "(>" st)
    ;; (modify-syntax-entry ?> ")<" st)
    ; see https://emacs.stackexchange.com/a/4149 for a possible solution
    (modify-syntax-entry ?#  "'" st)
    (modify-syntax-entry ?< "." st)
    (modify-syntax-entry ?> "." st)
    (modify-syntax-entry ?- "." st)
    (modify-syntax-entry ?| "." st)
    (modify-syntax-entry ?= "." st)
    (modify-syntax-entry ?\' "_" st)
    st))

(defun beluga--proc-live-p (process)
  "Return non-nil if PROCESS is alive.
A process is considered alive if its status is `run', `open',
    `listen', `connect' or `stop'."
  (and (not (eq process nil))
       (memq (process-status process)
             '(run open listen connect stop))))

(defun beluga-font-lock-compose-symbol (alist)
  "Compose a sequence of ascii chars into a symbol.
Regexp match data 0 points to the chars."
  ;; Check that the chars should really be composed into a symbol.
  (let* ((start (match-beginning 0))
         (end (match-end 0))
	 (syntaxes (cond
                    ((eq (char-syntax (char-after start)) ?w) '(?w))
                    ;; Special case for the . used for qualified names.
                    ((and (eq (char-after start) ?\.) (= end (1+ start)))
                     '(?_ ?\\ ?w))
                    (t '(?_ ?\\))))
         sym-data)
    (if (or (memq (char-syntax (or (char-before start) ?\ )) syntaxes)
	    (memq (char-syntax (or (char-after end) ?\ )) syntaxes)
	    (memq (get-text-property start 'face)
		  '(font-lock-doc-face font-lock-string-face
		    font-lock-comment-face))
            (and (consp (setq sym-data (cdr (assoc (match-string 0) alist))))
                 (let ((pred (cadr sym-data)))
                   (setq sym-data (car sym-data))
                   (funcall pred start))))
	;; No composition for you.  Let's actually remove any composition
	;; we may have added earlier and which is now incorrect.
	(remove-text-properties start end '(composition))
      ;; That's a symbol alright, so add the composition.
      (compose-region start end sym-data)))
  ;; Return nil because we're not adding any face property.
  nil)

(defun beluga-font-lock-symbols-keywords ()
  (when (and (fboundp 'compose-region) beluga-font-lock-symbols)
    (let ((alist nil))
      (dolist (x beluga-font-lock-symbols-alist)
	(when (and (if (fboundp 'char-displayable-p)
		       (char-displayable-p (if (consp (cdr x)) (cadr x) (cdr x)))
		     t)
		   (not (assoc (car x) alist)))	;Not yet in alist.
	  (push x alist)))
      (when alist
	`((,(regexp-opt (mapcar #'car alist) t)
	   (0 (beluga-font-lock-compose-symbol ',alist)
              ;; In Emacs-21, if the `override' field is nil, the face
              ;; expressions is only evaluated if the text has currently
              ;; no face.  So force evaluation by using `keep'.
              keep)))))))

(defconst beluga-syntax-id-re
  "[[:alpha:]_][[:alnum:]!'-@~$*/^&+=_]*"
  "A regexp for matching a Beluga identifier.")

(defconst beluga-syntax-fundec-re
  (regexp-opt '("rec" "proof") 'symbols)
  "A regexp for matching a function declaration.
Note that this will also match the 'and' keyword!")

(defvar beluga-imenu-generic-expression
  `(("Schemas"
     ,(concat "^[ \t]*schema[ \t\n]+\\(" beluga-syntax-id-re "\\)") 1)
    ("Constructors"
     ,(concat "^\\(" beluga-syntax-id-re "\\)[ \t\n]*:") 1)
    ("Type Constructors"
     ,(concat "^\\(?:inductive[ \t]+\\(" beluga-syntax-id-re
              "\\)\\|\\(?1:" beluga-syntax-id-re
              "\\)[ \t\n]*:[^.]*\\<type\\>[ \t\n]*.\\)")
     1)
    ("Functions"
     ,(concat beluga-syntax-fundec-re "[ \t\n]+\\(" beluga-syntax-id-re "\\)") 1)))

(define-obsolete-variable-alias 'beluga-interpreter-path
  ;; A "path" is a list of file names, as in $PATH, $MANPATH.
  'beluga-interpreter-name "Sep-2010")
(defcustom beluga-interpreter-name "beluga"
  "Name of the interpreter executable."
  :type 'string)

;;---------------------------- Interactive mode ----------------------------;;

(define-error 'beluga-interactive-error "Beluga interactive error")

(defun beluga-interactive-error (&rest data)
  (signal 'beluga-interactive-error data))

;; ------ process management ----- ;;

(defvar beluga--proc ()
  "Contain the process running beli.")
(make-variable-buffer-local 'beluga--proc)

(defvar beluga--output-wait-time
  0.025
  "How long to wait for output from Beluga on each iteration.")

(defvar beluga--output-timeout
  1.0
  "How long to wait in total for output before giving up.")

(defvar beluga--output-timer 0.0)

(defun beluga--proc ()
  (unless (beluga--proc-live-p beluga--proc) (beluga-start))
  beluga--proc)

(defun beluga-start ()
  "Start an inferior Beluga Interactive process with the -emacs option.
The process is put into a buffer called \"*beluga*\"."
  (interactive)
  (unless (beluga--proc-live-p beluga--proc)
    (setq beluga--proc
          (get-buffer-process
           (make-comint "beluga"
		                    beluga-interpreter-name
                        nil "-I" "-emacs" ))))
  beluga--proc)

(defun beluga-quit ()
  "Stop the Beluga interactive process by sending the quit command.
This is a graceful termination."
  (interactive)
  (beluga--rpc "quit"))

(defun beluga-stop ()
  "Stop the beli process."
  (interactive)
  (when (processp 'beluga--proc)
    (kill-process 'beluga--proc)))

;; ----- Stuff for hole overlays ----- ;;

(defvar beluga--holes-overlays ()
  "Will contain the list of hole overlays so that they can be resetted.")
(make-variable-buffer-local 'beluga--holes-overlays)

(defun beluga-sorted-holes ()
  (cl-labels
      ((hole-comp (a b)
                  (let* ((s1 (overlay-start a))
                         (s2 (overlay-start b)))
                    (< s1 s2))))
    (sort beluga--holes-overlays #'hole-comp)))

(defface beluga-holes
  '((t :background "cyan")) ;; :foreground "white"
  "Face used to highlight holes in Beluga mode.")

(defun beluga--pos (line bol offset)
  ;; According to http://caml.inria.fr/mantis/view.php?id=5159,
  ;; `line' can refer to line numbers in various source files,
  ;; whereas `bol' and `offset' refer to "character" (byte?) positions within
  ;; the actual parsed stream.
  ;; So if there might be #line directives, we need to do:
  ;; (save-excursion
  ;;   (goto-char (point-min))
  ;;   (forward-line (1- line)) ;Lines count from 1 :-(
  ;;   (+ (point) (- offset bol))))
  ;; But as long as we know there's no #line directive, we can ignore all that
  ;; and use the more efficient code below.  When #line directives can appear,
  ;; we will need to make further changes anyway, such as passing the file-name
  ;; to select the appropriate buffer.
  ;; Emacs considers the first character in the file to be at index 1,
  ;; but the Beluga lexer starts counting at zero, so we need to add
  ;; one here.
  (+ (point-min) offset))

(defun beluga--create-overlay (pos)
  "Create an overlay at the position described by POS (a Loc.to_tuple)."
  (let* (;; (file-name (nth 0 pos))
         (start-line (nth 1 pos))
         (start-bol (nth 2 pos))
         (start-off (nth 3 pos))
         (stop-line (nth 4 pos))
         (stop-bol (nth 5 pos))
         (stop-off (nth 6 pos))
         (ol
          (make-overlay (beluga--pos start-line start-bol start-off)
                        (beluga--pos stop-line  stop-bol  stop-off))))
    (overlay-put ol 'face 'beluga-holes)
    ol))

(defun beluga-erase-holes ()
  (interactive)
  (mapc #'delete-overlay beluga--holes-overlays)
  (setq beluga--holes-overlays nil))

;; ----- Interaction with the interactive mode ----- ;;

;; Sending and receiving strings from the inferior process.
;; Ultimately, all you really need to use is beluga--rpc to send a
;; command to the interactive mode and get back a string response.

(defun beluga--wait (proc)
  (assert (eq (current-buffer) (process-buffer proc)))
  (setq beluga--output-timer 0.0)
  (while (progn
           (goto-char comint-last-input-end)
           (not (re-search-forward ".*?;" nil t)))
    (accept-process-output proc beluga--output-wait-time)
    (setq beluga--output-timer (+ beluga--output-timer beluga--output-wait-time))
    (when (> beluga--output-timer beluga--output-timeout)
      (error "Beluga command didn't produce complete output"))))

(defun beluga--chomp (str)
  "Chomp leading and tailing whitespace from STR."
  (replace-regexp-in-string (rx (or (: bos (* (any " \t\n")))
                                    (: (* (any " \t\n")) eos)))
                            ""
                            str))
(defun beluga--trim (str)
  (let ((str2 (beluga--chomp str)))
    (substring str2 0 (1- (length str2)))))

(defun beluga--send (cmd)
  "Send CMD to beli."
  ; (interactive)
  (let ((proc (beluga--proc)))
    (with-current-buffer (process-buffer proc)
      ;; We could also just use `process-send-string', but then we wouldn't
      ;; have the input text in the buffer to separate the various prompts.
      (goto-char (point-max))
      (insert (concat "%:" cmd))
      (comint-send-input)
      (beluga--wait proc))))

(defun beluga--receive ()
  "Read the last output of beli."
  (let ((proc (beluga--proc)))
    (with-current-buffer (process-buffer proc)
      (beluga--wait proc)
      (beluga--trim (buffer-substring-no-properties comint-last-input-end (point-max))))))

(defun beluga--rpc (cmd)
  (beluga--send cmd)
  (beluga--receive))

(defun beluga--is-response-error (resp)
  "Determine whether a Beluga RPC response (RESP) is an error."
  (string= "-" (substring resp 0 1)))

(defun beluga--rpc! (cmd)
  "Variant of beluga--rpc that signals an error if CMD fails."
  (let ((resp (beluga--rpc cmd)))
    (when (beluga--is-response-error resp)
      (beluga-interactive-error (list (format "%s" (substring resp 2)))))
    resp))

(defvar beluga--last-load-time
  '(0 0 0 0)
  "The last time the file was loaded into the Beluga interpreter.
This variable is updated by `beluga--maybe-save-load-current-buffer'.")
(make-variable-buffer-local 'beluga--last-load-time)

(defun beluga--should-reload-p ()
  "Decide whether the current buffer should be reloaded into beli.
The `visited-file-modtime' is compared to `beluga--last-load-time'.
If the former is greater than the latter, then the former is
returned.  Else, nil is returned."
  (let ((mtime (visited-file-modtime)))
    (when (> (float-time mtime) (float-time beluga--last-load-time))
        mtime)))

;; ----- Beluga Interactive basic functions ----- ;;

;; Each of these functions directly corresponds to a command in src/core/command.ml

;; Since the construction of these functions is totally tedious and
;; straightforward, we define a macro to do the real work.
;; This macro takes:
;;   * the name of the function to define, e.g. beluga--printhole
;;   * the real name of the command to invoke, e.g. "printhole"
;;   * the arguments of the function, e.g. '((hole . "%s"))
;;
;; Note: the type of each argument is specified as a printf-style
;; format code. That's because the construction of the command will
;; construct a string formatting routine using these codes.
;;
;; What about constant portions of the string?
;; If you want to supply a constant portion in the format string,
;; simply provide a string as-is in the argument list.
;; e.g. ((hole . "%s") "with" (exp . "%s"))
;;
;; Two separate functions are generated by the macro invocation. The
;; first uses exactly the given function name, but the second appends
;; "!". This bang-variant will use beluga--rpc! under the hood, so you
;; get an exception-raising variant of every function for free.

(defun beluga--generate-format-string (args)
  "Construct the format string from the ARGS."
  (cons
   "%s"
   (mapcar
    (lambda (x)
      (if (stringp x)
          x
        (cdr x)))
    args)))

(defun beluga--generate-arg-list (args)
  "Construct a list of symbols representing the function arguments from ARGS."
  (mapcar 'car (cl-remove-if 'stringp args)))

(defun beluga--define-command (rpc name realname args)
  (let ((arglist (beluga--generate-arg-list args))
        (fmt (beluga--generate-format-string args)))
    `(defun ,name ,arglist
       (,rpc
        (format
         ;; construct the format string
         ,(mapconcat 'identity fmt " ")
         ;; construct the argument list
         ,realname ,@arglist)))))

(defmacro beluga-define-command (name realname args)
  `(progn
     ,(beluga--define-command 'beluga--rpc name realname args)
     ,(beluga--define-command 'beluga--rpc! (intern (concat (symbol-name name) "!")) realname args)))

(beluga-define-command beluga--basic-chatteron "chatteron" nil)
(beluga-define-command beluga--basic-chatteroff "chatteroff" nil)
(beluga-define-command beluga--basic-load "load" ((path . "%s")))
(beluga-define-command beluga--basic-clearholes "clearholes" nil)
(beluga-define-command beluga--basic-countholes "countholes" nil)
(beluga-define-command beluga--basic-lochole "lochole" ((hole . "%s")))
(beluga-define-command beluga--basic-lochole-n "lochole" ((hole . "%d")))
(beluga-define-command beluga--basic-printhole "printhole" ((hole . "%s")))
(beluga-define-command beluga--basic-printhole-n "printhole" ((hole . "%d")))
(beluga-define-command beluga--basic-types "types" nil)
(beluga-define-command beluga--basic-constructors-lf "constructors" ((type . "%s")))
(beluga-define-command beluga--basic-fill "fill" ((hole . "%s") "with" (exp . "%s")))
(beluga-define-command beluga--basic-split "split" ((hole . "%s") (var . "%s")))
(beluga-define-command beluga--basic-intro "intro" ((hole . "%s")))
(beluga-define-command beluga--basic-constructors "constructors-comp" ((type . "%s")))
(beluga-define-command beluga--basic-signature "fsig" ((fun . "%s")))
(beluga-define-command beluga--basic-printfun "fdef" ((fun . "%s")))
(beluga-define-command beluga--basic-query "query" ((expected . "%s") (tries . "%s") (type . "%s")))
(beluga-define-command beluga--basic-get-type "get-type" ((line . "%d") (col . "%d")))
(beluga-define-command beluga--basic-reset "reset" nil)
(beluga-define-command beluga--basic-quit "quit" nil)
(beluga-define-command beluga--basic-lookuphole "lookuphole" ((hole . "%s")))

;; ----- Higher-level commands ----- ;;

;; These build off the basic commands, and will typically do something
;; like parse the response or display it in a message.

(defun beli ()
  "Start beli mode."
  (interactive)
  (beluga-start))

(defun beluga-run-command (cmd)
  "Run CMD in beli."
  (interactive "MCommand: ")
  (message "%s" (beluga--rpc cmd)))

(defun beluga--maybe-save ()
  (if (buffer-modified-p)
    (if (y-or-n-p "Save current file? ")
      (save-buffer)
      ())))

(defun beluga-get-type ()
  "Get the type at the current cursor position (if it exists)."
  (interactive)
  (message "%s" (beluga--basic-get-type (count-lines 1 (point)) (current-column))))

(defun beluga--load-current-buffer (&optional mtime)
  "Load the current buffer in Beluga Interactive.
This command signals an error if loading fails.
The optional MTIME parameter, if given, will be written to `beluga--last-load-time'."
  (let ((resp (beluga--basic-load! (buffer-file-name))))
    (when mtime
      (setq beluga--last-load-time mtime))
    resp))

(defun beluga--maybe-save-load-current-buffer ()
  "Load the current buffer if it has either never been loaded, or
modified since the last time it was loaded.
This will update `beluga--last-load-time' if a load is performed."
  ;; prompt the user to save the buffer if it is modified
  (beluga--maybe-save)
  ;; retrieve the last time the file was written to disk, checking
  ;; whether a reload should occur
  (let ((mtime (beluga--should-reload-p)))
    (when mtime ;; mtime non-nil means we must reload
      (beluga--load-current-buffer mtime))))

(defun beluga--lochole-n! (hole-num)
  (read (beluga--basic-lochole-n! hole-num)))

(defun beluga--countholes! ()
  "Get the number of holes in the file."
  (string-to-number (beluga--basic-countholes!)))

(defun beluga--lookup-hole! (hole)
  "Look up a hole number by its name (HOLE)."
  (string-to-number (beluga--basic-lookuphole! hole)))

(defun beluga--highlight-holes ()
  "Create overlays for each of the holes and color them."
  (beluga-erase-holes)
  (let ((numholes (beluga--countholes!)))
    (dotimes (i numholes)
      (let* ((pos (beluga--lochole-n! i))
             (ol (beluga--create-overlay pos))
             (info (beluga--basic-printhole-n! i)))
        (overlay-put ol 'help-echo info)
        (push ol beluga--holes-overlays)
        ))))

(defun beluga--get-hole-overlay! (hole)
  "Get the overlay associated with HOLE."
  (nth (beluga--lookup-hole! hole) (beluga-sorted-holes)))

(defun beluga--apply-quail-completions (str)
  (if (string= current-input-method beluga-input-method-name)
     (replace-regexp-in-string "=>" "⇒"
      (replace-regexp-in-string "|-" "⊢" str))
     str))

(defun beluga--insert-formatted (str start)
  (goto-char start)
  (insert (beluga--apply-quail-completions str))
  (indent-region start (+ start (length str))))

(defun beluga--error-no-such-hole (n)
  (message "Couldn't find hole %s - make sure the file is loaded" n))

(defconst beluga-named-hole-re
  "\\_<?\\(\\sw+\\)\\_>")

(defun beluga-named-hole-at-point ()
  "Retrieve the name of the hole at point, if any.
If e.g. point is over \"?abracadabra\", then this function returns
\"abracadabra\". Else, if point is not over a valid hole, then this
function returns nil."
  (let ((thing (thing-at-point 'symbol)))
    (when (and thing (string-match beluga-named-hole-re thing))
      (match-string 1 thing))))

(defun beluga--prompt-with-hole-at-point (prompt)
  "Prompt the user to specify a hole, giving the named hole at point
as the default if any."
  (let ((name (beluga-named-hole-at-point)))
    (if name
        (read-string (format "%s (%s): " prompt name)
                     nil nil name)
      (read-string (format "%s: " prompt)))))

(defun beluga--begin-command ()
  "Perform necessary setup to begin a compound Beluga Interactive command.
Specifically, the following are performed, if necessary:
  - Starting the Beluga inferior process.
  - Saving the current buffer.
  - Loading the current buffer into Beluga.
  - Highlighting holes."
  (beluga-start)
  (beluga--maybe-save-load-current-buffer)
  (beluga--highlight-holes))

(defun beluga--prompt-string (prompt)
  "Prompts the user to input a string."
  (read-string (format "%s: " prompt)))

;; ----- Top-level commands ----- ;;

(defun beluga-load ()
  "Load the current file in Beluga Interactive.
This command will start the interactive mode if necessary and
prompt for saving."
  (interactive)
  (beluga-start)
  (let ((r (beluga--maybe-save-load-current-buffer)))
    (if r
        (message "%s" r)
      (message "Buffer does not require reload."))))

(defun beluga-highlight-holes ()
  "Create overlays for each of the holes and color them."
  (interactive)
  (beluga--begin-command))

(defun beluga-hole-info (hole)
  (interactive
   (list
    (beluga--prompt-with-hole-at-point "Hole to query")))
  (beluga--begin-command)
  (let ((resp (beluga--basic-printhole! hole)))
    (message resp)))

(defun beluga-split-hole (hole var)
  "Split on HOLE."
  (interactive
   (list
    (beluga--prompt-with-hole-at-point "Hole to split at")
    (beluga--prompt-string "Variable to split")))
  (beluga--begin-command)
  (let ((resp (beluga--basic-split! hole var))
        (ovr (beluga--get-hole-overlay! hole)))
    (if ovr
        (let ((start (overlay-start ovr))
              (end (overlay-end ovr)))
          (delete-overlay ovr)
          (delete-region start end)
          (beluga--insert-formatted (format "(%s)" resp) start)
          (save-buffer)
          (beluga--load-current-buffer)
          (beluga--highlight-holes))
      (beluga--error-no-such-hole hole))))

(defun beluga-intro-hole (hole)
  "Introduce variables into HOLE"
  (interactive
   (list
    (beluga--prompt-with-hole-at-point "Hole to introduce variables into")))
  (beluga--begin-command)
  (let ((resp (beluga--basic-intro! hole))
        (ovr (beluga--get-hole-overlay! hole)))
    (if ovr
        (let ((start (overlay-start ovr))
              (end (overlay-end ovr)))
          (delete-overlay ovr)
          (delete-region start end)
          (beluga--insert-formatted resp start)
          (save-buffer)
          (beluga--load-current-buffer)
          (beluga--highlight-holes))
      (beluga--error-no-such-hole hole))))

(defun beluga-hole-jump (hole)
  (interactive "sHole to jump to: ")
  (beluga--begin-command)
  (let ((ovr (beluga--get-hole-overlay! hole)))
    (if ovr
        (goto-char (+ 1 (overlay-start ovr)))
      (beluga--error-no-such-hole hole))))
(define-obsolete-function-alias 'hole-jump #'beluga-hole-jump "Jul-2018")

;; ----- Beluga indentation and navigation via SMIE ----- ;;

(defconst beluga-syntax-pragma-re
  "--\\(\\(name\\|query\\|infix\\|prefix\\|assoc\\).*?\\.\\|\\w+\\)"
  "A regexp for matching a Beluga pragma.
Long pragmas continue until a `.` is found, e.g. `--name oft D.`.
Short pragmas consist of only one word, e.g. `--nostrengthen`.
It's easy to use this regex to check which type of pragma (long or short)
was matched: simply check whether `match-string' 2 is non-nil.  In that case,
a long pragma was matched and the result is the name of the long pragma.
Otherwise, `match-string' 1 will contain the name of the matched short.")

(defconst beluga-slim-arrows
  '("->" "<-" "→" "←")
  "A list of the slim arrow strings.")

(defconst beluga-fat-arrows
  '("=>" "⇒")
  "A list of the fat arrow strings.")

(defconst beluga-punct-re
  (regexp-opt `(,@beluga-fat-arrows ,@beluga-slim-arrows "\\" "." "<" ">" "," ";" "..")))

(defconst beluga-syntax-keyword-re
  (regexp-opt
   '("FN" "and" "block" "case" "inductive" "LF" "coinductive"
     "stratified" "else" "ffalse" "fn" "if" "in" "impossible" "let"
     "mlam" "of" "rec" "proof" "schema" "some" "then" "type" "ctype" "ttrue"
     "typedef"
     "module" "struct" "end" "#stratified" "#positive" "fun")
   'symbols)
  "A regular expression to match any beluga keyword.")

(defface beluga-font-lock-annotation
  '((t :inherit italic))
  "Face used for Beluga's /.../ annotations.")

(defconst beluga-font-lock-keywords
  `((,beluga-syntax-pragma-re . ,font-lock-warning-face)

    ,beluga-syntax-keyword-re

    ("/\\s-*\\_<\\(total\\)\\_>.*?/"
     (0 'beluga-font-lock-annotation)
     (1 'font-lock-keyword-face prepend))

    (,(concat
       "^\\(" beluga-syntax-id-re "\\)"
       "\\s-*" ":"
       "\\([^.]*\\_<type\\_>\\s-*.\\)?")
     ;; This is a regexp that can span multiple lines, so it may not
     ;; always highlight properly.  `font-lock-multiline' tries to help.
     (0 (if (match-end 2) '(face nil font-lock-multiline t)))
     (1 (if (match-end 2)
            font-lock-type-face font-lock-variable-name-face)))

    (,(concat "^\\(?:schema\\|inductive\\|coinductive\\|LF\\|stratified\\)" "\\s-+"
              "\\(" beluga-syntax-id-re "\\)")
     (1 font-lock-type-face))

    (,(concat beluga-syntax-fundec-re "\\s-+\\(" beluga-syntax-id-re "\\)")
     (2 font-lock-function-name-face))
    ))

(defcustom beluga-indent-basic 4
  "Basic amount of indentation."
  :type 'integer)

(defun beluga-smie-forward-token ()
  ; skip all whitespace and comments
  (forward-comment (point-max))
  (cond
   ((looking-at "\\.[ \t]*$")
      ;; One of the LF-terminating dots.
    (progn (forward-char 1) ";."))
   ((looking-at beluga-syntax-pragma-re)
    ;; move point to the end of the long-pragma name if a long-pragma was matched.
    ;; otherwise, move it to the end of the short pragma name.
    (goto-char (or (match-end 2) (match-end 1)))
    ;; set to non-nil by beluga-syntax-pragma-re if the pragma is a long-form pragma
    (if (match-string 2)
        "--longpragma"
        "--shortpragma"))
   (t
    ; otherwise, we return a chunk of text that starts at point and
    ; ends according to the following `cond` check.
    (buffer-substring-no-properties
     (point)
     (progn
       (cond
        ((looking-at beluga-punct-re) (goto-char (match-end 0)))
        ((not (zerop (skip-syntax-forward "w_'"))))
        ;; In case of non-ASCII punctuation.
        ((not (zerop (skip-syntax-forward ".")))))
       (point))))))

(defun beluga-short-pragma-before-p ()
  "Decide whether there is a short pragma before point.
Return the starting position of the short pragma; else, nil."
  (save-excursion
    ;; idea: move backward across word-characters, and then check if
    ;; there are two dashes before point.
    (skip-syntax-backward "w")
    (save-match-data
      (when (looking-back "--" (- (point) 2))
        (match-beginning 0)))))

(defun beluga-smie-backward-token ()
  (forward-comment (- (point-max)))
  (cond
   ((and (eq ?\. (char-before))
         (looking-at "[ \t]*$") ;; "[ \t]*\\(?:$\\|[0-9]\\(\\)\\)"
         (not (looking-back "\\.\\." (- (point) 2))))
    ;; Either an LF-terminating dot, or a projection-dot.
    (progn (forward-char -1) ";."))
   ((setq pos (beluga-short-pragma-before-p))
    (goto-char pos)
    "--shortpragma")
   (t
    (buffer-substring-no-properties
     (point)
     (progn
       (cond
        ((looking-back beluga-punct-re (- (point) 2) 'greedy)
         (goto-char (match-beginning 0)))
        ((not (zerop (skip-syntax-backward "w_'"))))
        ;; In case of non-ASCII punctuation.
        ((not (zerop (skip-syntax-backward ".")))))
       (point))))))

(defun beluga-smie-grammar (bnf resolvers precs)
  (smie-prec2->grammar
   (smie-merge-prec2s
    (apply #'smie-bnf->prec2 bnf resolvers)
    (smie-precs->prec2 precs))))

(defconst beluga-smie-grammar
  ;; The "." used for terminating LF declarations is syntactically completely
  ;; different from the "." used in the binding forms.  Conflating the two
  ;; leads here to a lot of precedence conflicts, so we try and guess the two
  ;; based on a heuristic in the tokenizing code.
  (beluga-smie-grammar
   ;; FIXME: without this dummy, "=>" is marked as "open paren" because it
   ;; can only bind to `atom' on the left.
   '((atom ("--dummy--"))

     (def (exp "=" exp) (atom ":" exp))

     (decl
      (atom ":" type)
      (datatypes)
      ("schema" sdef)
      ("let" def)
      ("--shortpragma")
      ("--longpragma" atom)
      (recs))

     (datatypes
      ("inductive" datatype-def)
      ("coinductive" datatype-def)
      ("LF" datatype-def)
      ("stratified" datatype-def)
      (datatypes "and" datatypes))

     (simpletype
      (simpletype "->" simpletype)
      (simpletype "→" simpletype)
      (simpletype "←" simpletype)
      (simpletype "<-" simpletype))

     (recs
      ("rec" def)
      ("proof" def)
      (recs "and" recs))

     (decls
      (decl)
      (decls ";" decls)
      (decls ";." decls))

     ;; FIXME: only allow simple types here, otherwise we get nasty
     ;; precedence conflicts between "." and ",".  In practice, this seems to
     ;; be sufficient.
     (sdecl
      (atom ":" type))

     (sdecls
      (sdecl)
      (sdecls "," sdecls))

     (dotted-type
      (sdecls "|-" type)
      (sdecls "⊢" type))

     (type
      (simpletype)
      ("\\" atom "." type)         ;dotted-type
      ("block" sdecls "." type)    ;dotted-type
      ;; ("{" blabla "}" type)  ; FIXME!
      ;; FIXME: the projection via "." creates precedence conflicts.
      ;; (type "." atom)
      )

     (sdef
      (atom "=" schema))

     (schema
      (type)
      ;; Not sure if it's correct, and create precedence conflicts.
      ;; ("some" sdecls "block" sdecls "." schema)
      )

     (datatype-name
      (atom ":" type))

     (datatype-def
      (datatype-name "=" datatype-branches))

     (datatype-branches
      (datatype-branches "|" datatype-branches)
      (atom ":" type))

     (exp
      ("if" exp "then" exp "else" exp)
      (type)
      ("let" def "in" exp)
      ("fun" atom "=>" exp)
      ("fun" atom "⇒" exp)
      ("fn" atom "=>" exp)
      ("fn" atom "⇒" exp)
      ("FN" atom "=>" exp)
      ("FN" atom "⇒" exp)
      ("mlam" atom "=>" exp)
      ("mlam" atom "⇒" exp)
      ("<" dotted-type ">")
      ("case" exp "of" cases))

     (exps
      (exps ";" exps)
      (exp))

     ;; Separate cases/branch so that "|" is recognized as associative.
     (cases
      (branch)
      (cases "|" cases))

     (branch
      (atom "=>" exp)
      (atom "⇒" exp)))

   ; resolvers
   `(((assoc ";" ";."))
     ((assoc ,@beluga-slim-arrows))
     ((assoc ","))
     ((assoc "and"))
     ((nonassoc "of") (assoc "|"))      ; Trailing | ambiguity.
     ;; '((nonassoc "\\") (nonassoc ".")) ; Trailing . ambiguity.
     ;; '((nonassoc "block") (nonassoc ".")) ; Trailing . ambiguity.
     )

   ;; The above BNF grammar should cover this already, so this ends up only
   ;; useful to check that the BNF entails the expected precedences.
   ; precs
   `((assoc ";")
     (assoc ",")
     (left ":")
     (assoc ,@beluga-slim-arrows)
     (nonassoc " -dummy- "))))          ;Bogus anchor at the end.

(defconst beluga-pattern-fat-arrow
  `(or ,@beluga-fat-arrows)
  "A pattern for use in pcase that matches any fat arrow string.")

(defun beluga-rule-parent-p (parents)
  `(smie-rule-parent-p ,@parents))

(defun beluga-smie-indent-rules (method token)
  (pcase `(,method . ,token)
    (`(:elem . basic)
     beluga-indent-basic)

    ; describe the tokens that introduce lists (with no separators)
    (`(:list-intro . ,(or ":" "fn" "fun" "FN" "mlam"))
     't)

    ; if the token is a pipe preceded by an '=' or 'of', then we
    ; indent by adding the basic offset
    (`(:before . ,(and "|" (guard (smie-rule-prev-p "=" "of" "fun"))))
     2)

    ; if the token is a pipe, (and the preceding check didn't pass, so
    ; it isn't the first pipe in a sequence) then we consider it a
    ; separator
    (`(method . ,"|")
     (smie-rule-separator method))

    (`(:after . ,"of")
     beluga-indent-basic)

    (`(:after . ,"in")
     (when (smie-rule-hanging-p)
       (smie-rule-parent)))

    (`(:after . ,(and "=" (guard (smie-rule-parent-p "rec"))))
     (smie-rule-parent))

    (`(:after . ,(and "=" (guard (smie-rule-parent-p "proof"))))
     (smie-rule-parent))

    ; if the token is a form that will use => eventually but is
    ; preceded by a =>, then this is a chain, e.g.
    ; mlam G => mlam Q => fn x => fn y =>
    ; (code should be here, not indented 8 characters)
    (`(:before
       .
       ,(and
         (or "case" "fn" "FN" "mlam" "fun")
         (guard `(smie-rule-prev-p ,@beluga-fat-arrows))))
     (smie-rule-parent))

    (`(:after . ".")
     (smie-rule-parent))

    (`(:after . ,(and ":" (guard (smie-rule-parent-p "{"))))
     (smie-rule-parent 1))

    (`(:after . ,(or ":" "let" "if"))
     (smie-rule-parent beluga-indent-basic))

    (`(:before
       .
       ,(and "=" (guard `(smie-rule-parent-p ,@beluga-type-declaration-keywords))))
     (smie-rule-parent))
    ))

;;---------------------------- Loading of the mode ----------------------------;;

;;;###autoload
(add-to-list 'auto-mode-alist '("\\.s?bel\\'" . beluga-mode))

(defconst beluga-type-declaration-keywords
  '("inductive" "coinductive" "LF" "stratified")
  "The different keywords that introduce a type definition.")

(defconst beluga-type-declaration-keywords-re
  (regexp-opt beluga-type-declaration-keywords 'symbols)
  "A regular expression that matches any type definition keyword.")

;;;###autoload
(define-derived-mode beluga-mode prog-mode "Beluga"
  "Major mode to edit Beluga source code."
  (set (make-local-variable 'imenu-generic-expression)
       beluga-imenu-generic-expression)
  (set (make-local-variable 'outline-regexp)
       (concat beluga-syntax-fundec-re "\\|^(inductive\\|coinductive\\|LF\\|stratified)\\_>"))
  (set (make-local-variable 'require-final-newline) t)
  (when buffer-file-name
    (set (make-local-variable 'compile-command)
         ;; Quite dubious, but it's the intention that counts.
         (concat beluga-interpreter-name
                 " "
                 (shell-quote-argument buffer-file-name))))
  (set (make-local-variable 'comment-start) "%")
  (set (make-local-variable 'comment-start-skip) "%[%{]*[ \t]*")
  (set (make-local-variable 'comment-end-skip) "[ \t]*\\(?:\n\\|}%\\)")
  (comment-normalize-vars)
  (set (make-local-variable 'electric-indent-chars)
       (append '(?|) (if (boundp 'electric-indent-chars)
                         electric-indent-chars
                       '(?\n))))
  ;QUAIL
  (add-hook 'beluga-mode-hook
   (lambda () (set-input-method "beluga-unicode")))

  ;Turn off hilighting
  (setq input-method-highlight-flag nil)

  (smie-setup
   beluga-smie-grammar
   'beluga-smie-indent-rules
   :forward-token #'beluga-smie-forward-token
   :backward-token #'beluga-smie-backward-token)

  (set (make-local-variable 'parse-sexp-ignore-comments) t)

  (set
   (make-local-variable 'font-lock-defaults)
   '(beluga-font-lock-keywords
     nil
     nil
     ()
     nil
     (font-lock-syntactic-keywords . nil)))

  (message "beluga-mode loaded"))

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