;;; george-mode.el --- George mode  -*- lexical-binding: t; -*-

;; Copyright (C) 2019 Amin Bandali

;; Author: Amin Bandali <bandali@gnu.org>
;; Keywords: languages, george
;; URL: https://git.sr.ht/~bandali/george-mode
;; Version: 0.1.0

;; This file is not part of GNU Emacs.

;; GNU Emacs 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.

;; GNU Emacs 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 GNU Emacs.  If not, see <https://www.gnu.org/licenses/>.

;;; Commentary:

;; This is an Emacs major mode for editing `george' files.

;;; Code:

(defvar george-mode-map
   (let ((map (make-sparse-keymap)))
     map)
   "Keymap for `george-mode'.")

(defvar george-mode-directives
  (let ((methods (regexp-opt
                  '("NONE" "PROP" "PRED" "TP" "ND" "ST" "Z" "PC")
                  'words)))
    (format "#\\(\\(u\\|a\\|q\\).*\\|check\\s-*%s\\)" methods))
  "Regexp matching `george''s directives.")

(defvar george-mode-symbols
  '(";" ":" "," "." "!" "="
    ":=" "==" "!="
    "+" "-" "*" "/"
    "^"
    ">" "<" ">=" "<="
    "{" "}" "[" "]"
    "&" "|"
    "=>" "<=>" "<==>"
    "|-"
    "||"
    "<|" "<-|" "|>" "|->"
    "(+)" "(|" "|)"
    "'" "~"
    "::="
    "<->" "-->" ">-->" "-->>" ">-->>"
    "-|->" ">-|->" "-|->>" ">-|->>"))

(defvar george-mode-keywords
  '(;; === PROP ===
    ;; "false" "true" ; will be constants

    ;; === PRED ===
    "forall" "exists"

    ;; === TP ===
    "by"
    ;; prop rules
    "comm"   "assoc"      "contr"  "lem"
    "impl"   "contrapos"  "simp1"  "simp2"
    "distr"  "dm"         "neg"    "equiv"
    "idemp"
    ;; pred rules
    "forall_over_and" "exists_over_or" "swap_vars" "move_exists"
    "move_forall" ;; "dm" ; (same name as for prop logic)

    ;; === ND ===
    "premise"
    "and_i"        "and_e"
    "or_i"         "or_e"
    ;; "lem" ; same name as for TP
                   "imp_e"
                   "not_e"
    "not_not_i"    "not_not_e"
    "iff_i"        "iff_e"
    "trans"        "iff_mp"
    "exists_i"
                   "forall_e"
    ;; "true" ; will be a constant
    "eq_i"         "eq_e"

    "disprove"     "raa"
    "case"         "cases"
    "assume"       "imp_i"
    "for" "every"  "forall_i"
          "some"   "exists_e"
    "magic"

    ;; === ST ===
    "closed"
    "on"
    "and_nb"     "not_and_br"
    "or_br"      "not_or_nb"
    "imp_br"     "not_imp_br"
                 "not_not_nb"
    "iff_br"     "not_iff_br"
    "forall_nb"  "not_forall_nb"
    "exists_nb"  "not_exists_nb"

    ;; === arith ===
    "arith"
    "induction"

    ;; === sets ===
    "empty" "univ"
    "in" "sub" "sube"
    "pow"
    "union" "inter"
    "card"
    "gen_U" "gen_I"
    "dom" "ran"
    "id"
    "iter"

    ;; === Z ===
    "schema" "begin"
    "pred" "end"
    "seq"

    ;; === PC ===
    "proc" "fun"
    "if" "then" "else"
    "while" "for" "until" "do"
    "assert"))

(defvar george-mode-constants
  '("false"
    "true"))

(defconst george-mode-syntax-table
  (let ((st (make-syntax-table)))
    ;; % is a comment starter
    (modify-syntax-entry ?% "<" st)
    ;; \n is a comment ender
    (modify-syntax-entry ?\n ">" st)

    ;; return our modified syntax table
    st))

(defvar george-mode-font-lock-defaults
  `((("\"\\.\\*\\?" . font-lock-string-face)
     (,george-mode-directives                    . font-lock-builtin-face)
     (,(regexp-opt george-mode-symbols 'symbols) . font-lock-keyword-face)
     (,(regexp-opt george-mode-keywords 'words)  . font-lock-keyword-face)
     (,(regexp-opt george-mode-constants 'words) . font-lock-constant-face))))

;;;###autoload
(define-derived-mode george-mode prog-mode "George"
  "Major mode for editing `george' files."
  :syntax-table george-mode-syntax-table

  (setq-local font-lock-defaults george-mode-font-lock-defaults)
  (setq-local comment-start "%")
  (setq-local comment-end "")
  (font-lock-ensure))

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

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