git.shemshak.org - ~bandali/george-mode/blob - george-mode.el

   1 ;;; george-mode.el --- George mode  -*- lexical-binding: t; -*-
   2
   3 ;; Copyright (C) 2019 Amin Bandali
   4
   5 ;; Author: Amin Bandali <bandali@gnu.org>
   6 ;; Keywords: languages, george
   7 ;; URL: https://git.sr.ht/~bandali/george-mode
   8 ;; Version: 0.1.0
   9
  10 ;; This file is not part of GNU Emacs.
  11
  12 ;; GNU Emacs is free software: you can redistribute it and/or modify
  13 ;; it under the terms of the GNU General Public License as published by
  14 ;; the Free Software Foundation, either version 3 of the License, or
  15 ;; (at your option) any later version.
  16
  17 ;; GNU Emacs is distributed in the hope that it will be useful,
  18 ;; but WITHOUT ANY WARRANTY; without even the implied warranty of
  19 ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  20 ;; GNU General Public License for more details.
  21
  22 ;; You should have received a copy of the GNU General Public License
  23 ;; along with GNU Emacs.  If not, see <https://www.gnu.org/licenses/>.
  24
  25 ;;; Commentary:
  26
  27 ;; This is an Emacs major mode for editing George files.
  28
  29 ;;; Code:
  30
  31 (defvar george-mode-map
  32    (let ((map (make-sparse-keymap)))
  33      map)
  34    "Keymap for `george-mode'.")
  35
  36 (defvar george-mode-directives
  37   (let ((methods (regexp-opt
  38                   '("NONE" "PROP" "PRED" "TP" "ND" "ST" "Z" "PC")
  39                   'words)))
  40     (format "#\\(\\(u\\|a\\|q\\).*\\|check\\s-*%s\\)" methods))
  41   "Regexp matching George's directives.")
  42
  43 (defvar george-mode-symbols
  44   '(";" ":" "," "." "!" "="
  45     ":=" "==" "!="
  46     "+" "-" "*" "/"
  47     "^"
  48     ">" "<" ">=" "<="
  49     "{" "}" "[" "]"
  50     "&" "|"
  51     "=>" "<=>" "<==>"
  52     "|-"
  53     "||"
  54     "<|" "<-|" "|>" "|->"
  55     "(+)" "(|" "|)"
  56     "'" "~"
  57     "::="
  58     "<->" "-->" ">-->" "-->>" ">-->>"
  59     "-|->" ">-|->" "-|->>" ">-|->>"))
  60
  61 (defvar george-mode-keywords
  62   '(;; === PROP ===
  63     ;; "false" "true" ; will be constants
  64
  65     ;; === PRED ===
  66     "forall" "exists"
  67
  68     ;; === TP ===
  69     "by"
  70     ;; prop rules
  71     "comm"   "assoc"      "contr"  "lem"
  72     "impl"   "contrapos"  "simp1"  "simp2"
  73     "distr"  "dm"         "neg"    "equiv"
  74     "idemp"
  75     ;; pred rules
  76     "forall_over_and" "exists_over_or" "swap_vars" "move_exists"
  77     "move_forall" ;; "dm" ; (same name as for prop logic)
  78
  79     ;; === ND ===
  80     "premise"
  81     "and_i"        "and_e"
  82     "or_i"         "or_e"
  83     ;; "lem" ; same name as for TP
  84                    "imp_e"
  85                    "not_e"
  86     "not_not_i"    "not_not_e"
  87     "iff_i"        "iff_e"
  88     "trans"        "iff_mp"
  89     "exists_i"
  90                    "forall_e"
  91     ;; "true" ; will be a constant
  92     "eq_i"         "eq_e"
  93
  94     "disprove"     "raa"
  95     "case"         "cases"
  96     "assume"       "imp_i"
  97     "for" "every"  "forall_i"
  98           "some"   "exists_e"
  99     "magic"
 100
 101     ;; === ST ===
 102     "closed"
 103     "on"
 104     "and_nb"     "not_and_br"
 105     "or_br"      "not_or_nb"
 106     "imp_br"     "not_imp_br"
 107                  "not_not_nb"
 108     "iff_br"     "not_iff_br"
 109     "forall_nb"  "not_forall_nb"
 110     "exists_nb"  "not_exists_nb"
 111
 112     ;; === arith ===
 113     "arith"
 114     "induction"
 115
 116     ;; === sets ===
 117     "empty" "univ"
 118     "in" "sub" "sube"
 119     "pow"
 120     "union" "inter"
 121     "card"
 122     "gen_U" "gen_I"
 123     "dom" "ran"
 124     "id"
 125     "iter"
 126
 127     ;; === Z ===
 128     "schema" "begin"
 129     "pred" "end"
 130     "seq"
 131
 132     ;; === PC ===
 133     "proc" "fun"
 134     "if" "then" "else"
 135     "while" "for" "until" "do"
 136     "assert"))
 137
 138 (defvar george-mode-constants
 139   '("false"
 140     "true"))
 141
 142 (defconst george-mode-syntax-table
 143   (let ((st (make-syntax-table)))
 144     ;; % is a comment starter
 145     (modify-syntax-entry ?% "<" st)
 146     ;; \n is a comment ender
 147     (modify-syntax-entry ?\n ">" st)
 148
 149     ;; return our modified syntax table
 150     st))
 151
 152 (defvar george-mode-font-lock-defaults
 153   `((("\"\\.\\*\\?" . font-lock-string-face)
 154      (,george-mode-directives                    . font-lock-builtin-face)
 155      (,(regexp-opt george-mode-symbols 'symbols) . font-lock-keyword-face)
 156      (,(regexp-opt george-mode-keywords 'words)  . font-lock-keyword-face)
 157      (,(regexp-opt george-mode-constants 'words) . font-lock-constant-face))))
 158
 159 ;;;###autoload
 160 (define-derived-mode george-mode prog-mode "George"
 161   "Major mode for editing George files."
 162   :syntax-table george-mode-syntax-table
 163
 164   (setq-local font-lock-defaults george-mode-font-lock-defaults)
 165   (setq-local comment-start "%")
 166   (setq-local comment-end "")
 167   (font-lock-ensure))
 168
 169 ;;;###autoload
 170 (add-to-list 'auto-mode-alist '("\\.grg\\'" . george-mode))
 171
 172 (provide 'george-mode)
 173 ;;; george-mode.el ends here