diff options
Diffstat (limited to '')
| -rw-r--r-- | george-mode.el | 173 |
1 files changed, 173 insertions, 0 deletions
diff --git a/george-mode.el b/george-mode.el new file mode 100644 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 |