Commit | Line | Data |
---|---|---|
44710136 AB |
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 |