`george' seems to be a (the?) preferred stylizing of George
[~bandali/george-mode] / 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