Initial check-in of George mode

[~bandali/george-mode] / george-mode.el

diff --git a/george-mode.el b/george-mode.el
new file mode 100644 (file)
index 0000000..4c929de
--- /dev/null
+++ b/george-mode.el
@@ -0,0 +1,173 @@
+;;; 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