1;;; hol-input.el --- The Hol input method (based/copied from Lean)
2;;;
3;;; DISCLAIMER: This file is based on lean-input.el provided with the Lean theorem prover.
4;;; We did minor modifications
5;;
6;;; Commentary:
7;;
8;;;; A highly customisable input method which can inherit from other
9;; Quail input methods. By default the input method is geared towards
10;; the input of mathematical and other symbols in Hol programs.
11;;
12;; Use M-x customize-group hol-input to customise this input method.
13;; Note that the functions defined under "Functions used to tweak
14;; translation pairs" below can be used to tweak both the key
15;; translations inherited from other input methods as well as the
16;; ones added specifically for this one.
17;;
18;; Use hol-input-show-translations to see all the characters which
19;; can be typed using this input method (except for those
20;; corresponding to ASCII characters).
21
22;;; Code:
23
24(require 'quail)
25
26(eval-when-compile
27  (require 'cl))
28;; Quail is quite stateful, so be careful when editing this code.  Note
29;; that with-temp-buffer is used below whenever buffer-local state is
30;; modified.
31
32;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
33;; Utility functions
34
35(defun hol-input-concat-map (f xs)
36  "Concat (map F XS)."
37  (apply 'append (mapcar f xs)))
38
39(defun hol-input-to-string-list (s)
40  "Convert a string S to a list of one-character strings, after
41removing all space and newline characters."
42  (hol-input-concat-map
43   (lambda (c) (if (member c (string-to-list " \n"))
44              nil
45            (list (string c))))
46   (string-to-list s)))
47
48(defun hol-input-character-range (from to)
49  "A string consisting of the characters from FROM to TO."
50  (let (seq)
51    (dotimes (i (1+ (- to from)))
52      (setq seq (cons (+ from i) seq)))
53    (concat (nreverse seq))))
54
55;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
56;; Functions used to tweak translation pairs
57
58;; lexical-let is used since Elisp lacks lexical scoping.
59
60(defun hol-input-compose (f g)
61  "\x -> concatMap F (G x)"
62  (lexical-let ((f1 f) (g1 g))
63    (lambda (x) (hol-input-concat-map f1 (funcall g1 x)))))
64
65(defun hol-input-or (f g)
66  "\x -> F x ++ G x"
67  (lexical-let ((f1 f) (g1 g))
68    (lambda (x) (append (funcall f1 x) (funcall g1 x)))))
69
70(defun hol-input-nonempty ()
71  "Only keep pairs with a non-empty first component."
72  (lambda (x) (if (> (length (car x)) 0) (list x))))
73
74(defun hol-input-prepend (prefix)
75  "Prepend PREFIX to all key sequences."
76  (lexical-let ((prefix1 prefix))
77    (lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x))))))
78
79(defun hol-input-prefix (prefix)
80  "Only keep pairs whose key sequence starts with PREFIX."
81  (lexical-let ((prefix1 prefix))
82    (lambda (x)
83      (if (equal (substring (car x) 0 (length prefix1)) prefix1)
84          (list x)))))
85
86(defun hol-input-suffix (suffix)
87  "Only keep pairs whose key sequence ends with SUFFIX."
88  (lexical-let ((suffix1 suffix))
89    (lambda (x)
90      (if (equal (substring (car x)
91                            (- (length (car x)) (length suffix1)))
92                 suffix1)
93          (list x)))))
94
95(defun hol-input-drop (ss)
96  "Drop pairs matching one of the given key sequences.
97SS should be a list of strings."
98  (lexical-let ((ss1 ss))
99    (lambda (x) (unless (member (car x) ss1) (list x)))))
100
101(defun hol-input-drop-beginning (n)
102  "Drop N characters from the beginning of each key sequence."
103  (lexical-let ((n1 n))
104    (lambda (x) `((,(substring (car x) n1) . ,(cdr x))))))
105
106(defun hol-input-drop-end (n)
107  "Drop N characters from the end of each key sequence."
108  (lexical-let ((n1 n))
109    (lambda (x)
110      `((,(substring (car x) 0 (- (length (car x)) n1)) .
111         ,(cdr x))))))
112
113(defun hol-input-drop-prefix (prefix)
114  "Only keep pairs whose key sequence starts with PREFIX.
115This prefix is dropped."
116  (hol-input-compose
117   (hol-input-drop-beginning (length prefix))
118   (hol-input-prefix prefix)))
119
120(defun hol-input-drop-suffix (suffix)
121  "Only keep pairs whose key sequence ends with SUFFIX.
122This suffix is dropped."
123  (lexical-let ((suffix1 suffix))
124    (hol-input-compose
125     (hol-input-drop-end (length suffix1))
126     (hol-input-suffix suffix1))))
127
128;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
129;; Customization
130
131;; The :set keyword is set to 'hol-input-incorporate-changed-setting
132;; so that the input method gets updated immediately when users
133;; customize it. However, the setup functions cannot be run before all
134;; variables have been defined. Hence the :initialize keyword is set to
135;; 'custom-initialize-default to ensure that the setup is not performed
136;; until hol-input-setup is called at the end of this file.
137
138(defgroup hol-input nil
139  "The Hol input method.
140After tweaking these settings you may want to inspect the resulting
141translations using `hol-input-show-translations'."
142  :group 'hol
143  :group 'leim)
144
145(defcustom hol-input-tweak-all
146  '(hol-input-compose
147    (hol-input-prepend "\\")
148    (hol-input-nonempty))
149  "An expression yielding a function which can be used to tweak
150all translations before they are included in the input method.
151The resulting function (if non-nil) is applied to every
152\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of such
153pairs. (Note that the translations can be anything accepted by
154`quail-defrule'.)
155
156If you change this setting manually (without using the
157customization buffer) you need to call `hol-input-setup' in
158order for the change to take effect."
159  :group 'hol-input
160  :set 'hol-input-incorporate-changed-setting
161  :initialize 'custom-initialize-default
162  :type 'sexp)
163
164(defcustom hol-input-inherit
165  `(("TeX" . (hol-input-compose
166              (hol-input-drop '("geq" "leq" "bullet" "qed" "par"))
167              (hol-input-or
168               (hol-input-drop-prefix "\\")
169               (hol-input-or
170                (hol-input-compose
171                 (hol-input-drop '("^o"))
172                 (hol-input-prefix "^"))
173                (hol-input-prefix "_")))))
174    )
175  "A list of Quail input methods whose translations should be
176inherited by the Hol input method (with the exception of
177translations corresponding to ASCII characters).
178
179The list consists of pairs (qp . tweak), where qp is the name of
180a Quail package, and tweak is an expression of the same kind as
181`hol-input-tweak-all' which is used to tweak the translation
182pairs of the input method.
183
184The inherited translation pairs are added last, after
185`hol-input-user-translations' and `hol-input-translations'.
186
187If you change this setting manually (without using the
188customization buffer) you need to call `hol-input-setup' in
189order for the change to take effect."
190  :group 'hol-input
191  :set 'hol-input-incorporate-changed-setting
192  :initialize 'custom-initialize-default
193  :type '(repeat (cons (string :tag "Quail package")
194                       (sexp :tag "Tweaking function"))))
195
196(defcustom hol-input-translations
197  (let ((max-lisp-eval-depth 2800)) `(
198
199  ;; Negation
200
201  ("not" . ("��"))
202
203  ;; Equality and similar symbols.
204
205  ("eq"  . ,(hol-input-to-string-list "=������������������������������������ ���������������������������������������������������������������������������"))
206  ("eqn" . ,(hol-input-to-string-list "������ ���     ���  ������  ���                 ���    "))
207  ("equiv" . ,(hol-input-to-string-list "������"))
208  ("iso" . ,(hol-input-to-string-list "������"))
209
210                    ("=n"  . ("���"))
211  ("~"    . ("���"))  ("~n"  . ("���")) ("homotopy"    . ("���"))
212  ("~~"   . ("���"))  ("~~n" . ("���"))
213  ("~~~"  . ("���"))
214  (":~"   . ("���"))
215  ("~-"   . ("���"))  ("~-n" . ("���"))
216  ("-~"   . ("���"))
217  ("~="   . ("���"))  ("~=n" . ("���"))
218  ("~~-"  . ("���"))
219  ("=="   . ("���"))  ("==n" . ("���"))
220  ("==="  . ("���"))
221  (".="   . ("���"))  (".=." . ("���"))
222  (":="   . ("���"))  ("=:"  . ("���"))
223  ("=o"   . ("���"))
224  ("(="   . ("���"))
225  ("and=" . ("���"))  ("or=" . ("���"))
226  ("*="   . ("���"))
227  ("t="   . ("���"))
228  ("def=" . ("���"))
229  ("m="   . ("���"))
230  ("?="   . ("���"))
231
232  ("pr" . ("���"))
233
234  ("1" . ("���"))
235  ("2" . ("���"))
236  ("3" . ("���"))
237  ("4" . ("���"))
238  ("5" . ("���"))
239  ("6" . ("���"))
240  ("7" . ("���"))
241  ("8" . ("���"))
242  ("9" . ("���"))
243  ("0" . ("���"))
244
245  ;; Inequality and similar symbols.
246
247  ("leq"  . ,(hol-input-to-string-list "���������<������ ������������������ ��������� ���������������������"))
248  ("leqn" . ,(hol-input-to-string-list "���������������   ������ ������������  ������ ������   ���"))
249  ("geq"  . ,(hol-input-to-string-list "���������>������ ������������������ ��������� ���������������������"))
250  ("geqn" . ,(hol-input-to-string-list "��������������� ���  ��� ������������  ������ ������   ���"))
251
252  ("<="   . ("���"))  (">="   . ("���"))
253  ("<=n"  . ("���"))  (">=n"  . ("���"))
254  ("len"  . ("���"))  ("gen"  . ("���"))
255  ("<n"   . ("���"))  (">n"   . ("���"))
256  ("<~"   . ("���"))  (">~"   . ("���"))
257  ("<~n"  . ("���"))  (">~n"  . ("���"))
258  ("<~nn" . ("���"))  (">~nn" . ("���"))
259
260  ("ssub"   . ("���"))  ("ssup"   . ("���"))
261  ("ssubn"  . ("���"))  ("ssupn"  . ("���"))
262  ("sub"  . ("���")) ("sup"  . ("���"))
263  ("subn" . ("���")) ("supn" . ("���"))
264  ("ssqub"   . ("���"))  ("ssqup"   . ("���"))
265  ("squb"  . ("���"))  ("squp"  . ("���"))
266  ("squbn" . ("���"))  ("squpn" . ("���"))
267
268  ;; Set membership etc.
269
270  ("member" . ,(hol-input-to-string-list "������������������������������������������������������������"))
271  ("mem" . ("���"))
272
273  ("inn" . ("���"))
274  ("nin" . ("���"))
275
276  ;; Types
277
278  ("T1" . ("Type���"))
279  ("T2" . ("Type���"))
280  ("T+" . ("Type���"))
281
282  ;; Intersections, unions etc.
283
284  ("intersection" . ,(hol-input-to-string-list "������������������������������ ���      ���"))
285  ("union"        . ,(hol-input-to-string-list "������������������������������������������������������������"))
286
287  ("and" . ("���"))  ("or"  . ("���"))
288  ("And" . ("���"))  ("Or"  . ("���"))
289  ("i"   . ("���"))  ("un"  . ("���"))  ("u+" . ("���"))  ("u." . ("���"))
290  ("I"   . ("���"))  ("Un"  . ("���"))  ("U+" . ("���"))  ("U." . ("���"))
291  ("glb" . ("���"))  ("lub" . ("���"))
292  ("Glb" . ("���"))  ("Lub" . ("���"))
293
294  ;; Entailment etc.
295
296  ("entails" . ,(hol-input-to-string-list "������������������������������������������"))
297
298  ("|-"   . ("���"))  ("|-n"  . ("���"))
299  ("-|"   . ("���"))
300  ("|="   . ("���"))  ("|=n"  . ("���"))
301  ("||-"  . ("���"))  ("||-n" . ("���"))
302  ("||="  . ("���"))  ("||=n" . ("���"))
303  ("|||-" . ("���"))
304
305  ;; Divisibility, parallelity.
306
307  ("|"  . ("���"))  ("|n"  . ("���"))
308  ("||" . ("���"))  ("||n" . ("���"))
309
310  ;; Some symbols from logic and set theory.
311
312  ("all" . ("���"))
313  ("ex"  . ("���"))
314  ("exn" . ("���"))
315  ("0"   . ("���"))
316  ("empty"   . ("���"))
317  ("C"   . ("���"))
318  ("powerset" . ("����"))
319
320  ;; Corners, ceilings and floors.
321
322  ("c"  . ,(hol-input-to-string-list "������������������������"))
323  ("cu" . ,(hol-input-to-string-list "������  ������  "))
324  ("cl" . ,(hol-input-to-string-list "  ������  ������"))
325
326  ("cul" . ("���"))  ("cuL" . ("���"))
327  ("cur" . ("���"))  ("cuR" . ("���"))
328  ("cll" . ("���"))  ("clL" . ("���"))
329  ("clr" . ("���"))  ("clR" . ("���"))
330
331  ;; Various operators/symbols.
332  ("tr"        . ,(hol-input-to-string-list "������"))
333  ("trans"     . ,(hol-input-to-string-list "������"))
334  ("transport" . ("���"))
335  ("con"       . ("���"))
336  ("cdot"      . ("���"))
337  ("dot"      . ("���"))
338  ("sy"        . ("�����"))
339  ("inv"       . ("�����"))
340  ("-1"        . ("�����" "������"))
341  ("-1e"       . ("��������"))
342  ("-1f"       . ("��������"))
343  ("-1g"       . ("��������"))
344  ("-1h"       . ("�������"))
345  ("-1i"       . ("��������"))
346  ("-1m"       . ("��������"))
347  ("-1o"       . ("��������"))
348  ("-1r"       . ("�������"))
349  ("-1p"       . ("��������"))
350  ("-1s"       . ("�������"))
351  ("-1v"       . ("��������"))
352  ("-1E"       . ("��������"))
353  ("-2"        . ("�����" "������"))
354  ("-2o"       . ("��������"))
355  ("-3"        . ("�����"))
356  ("qed"       . ("���"))
357  ("x"         . ("��"))
358  ("o"         . ("���"))
359  ("comp"      . ("���"))
360  ("."         . ("���"))
361  ("*"         . ("���"))
362  (".+"        . ("���"))
363  (".-"        . ("���"))
364  (":"         . ("���"))
365  ("::"        . ("���"))
366  ("::-"       . ("���"))
367  ("-:"        . ("���"))
368  ("+ "        . ("���"))
369  ("surd3"     . ("���"))
370  ("surd4"     . ("���"))
371  ("increment" . ("���"))
372  ("inf"       . ("���"))
373  ("&"         . ("���"))
374  ("op"        . ("������"))
375  ("opf"       . ("���������"))
376
377  ;; Circled operators.
378
379  ("o+"  . ("���"))
380  ("o--" . ("���"))
381  ("ox"  . ("���"))
382  ("o/"  . ("���"))
383  ("o."  . ("���"))
384  ("oo"  . ("���"))
385  ("o*"  . ("���*" "���"))
386  ("o="  . ("���"))
387  ("o-"  . ("���"))
388
389  ("O+"  . ("���"))
390  ("Ox"  . ("���"))
391  ("O."  . ("���"))
392  ("O*"  . ("���"))
393
394  ;; Boxed operators.
395
396  ("b+" . ("���"))
397  ("b-" . ("���"))
398  ("bx" . ("���"))
399  ("b." . ("���"))
400
401  ;; Various symbols.
402
403  ("integral" . ,(hol-input-to-string-list "���������������������������"))
404  ("angle"    . ,(hol-input-to-string-list "���������������"))
405  ("join"     . ,(hol-input-to-string-list "���������������������������"))
406
407  ;; Arrows.
408  ("iff" . ("���")) ("imp"  . ("���"))
409  ("l"  . ,(hol-input-to-string-list "��������������������������������������������������������� ���     ������������������������������������                                     "))
410  ("r"  . ,(hol-input-to-string-list "������������������������������������������������������������ ���    ������������������������������������������������ ������������������������������������������������������������������������������������������������"))
411  ("u"  . ,(hol-input-to-string-list "������������������������������������          ��������� ������������������                                           "))
412  ("d"  . ,(hol-input-to-string-list "������������������������������������         ������������ ���                                                "))
413  ("ud" . ,(hol-input-to-string-list "������   ������                                                                    "))
414  ("lr" . ,(hol-input-to-string-list "������         ������������������������                                                        "))
415  ("ul" . ,(hol-input-to-string-list "������                        ������                                               "))
416  ("ur" . ,(hol-input-to-string-list "������                                         ���������                             "))
417  ("dr" . ,(hol-input-to-string-list "������                        ���                ���������                             "))
418  ("dl" . ,(hol-input-to-string-list "������                                                                         "))
419  ("==>" . ("���")) ("nattrans" . ("���")) ("nat_trans" . ("���"))
420
421  ("l-"  . ("���"))  ("<-"  . ("���"))  ("l="  . ("���"))
422  ("r-"  . ("���"))  ("->"  . ("���"))  ("r="  . ("���"))  ("=>"  . ("���")) ("functor"  . ("���"))
423  ("u-"  . ("���"))                   ("u="  . ("���"))
424  ("d-"  . ("���"))                   ("d="  . ("���"))
425  ("ud-" . ("���"))                   ("ud=" . ("���"))
426  ("lr-" . ("���"))  ("<->" . ("���"))  ("lr=" . ("���"))  ("<=>" . ("���"))
427  ("ul-" . ("���"))                   ("ul=" . ("���"))
428  ("ur-" . ("���"))                   ("ur=" . ("���"))
429  ("dr-" . ("���"))                   ("dr=" . ("���"))
430  ("dl-" . ("���"))                   ("dl=" . ("���"))
431
432  ("l==" . ("���"))  ("l-2" . ("���"))                   ("l-r-" . ("���"))
433  ("r==" . ("���"))  ("r-2" . ("���"))  ("r-3" . ("���"))  ("r-l-" . ("���"))
434  ("u==" . ("���"))  ("u-2" . ("���"))                   ("u-d-" . ("���"))
435  ("d==" . ("���"))  ("d-2" . ("���"))                   ("d-u-" . ("���"))
436
437  ("l--"  . ("���"))  ("<--"  . ("���"))  ("l~"  . ("���" "���"))
438  ("r--"  . ("���"))  ("-->"  . ("���"))  ("r~"  . ("���" "���" "���")) ("hom"  . ("���"))
439  ("lr--" . ("���"))  ("<-->" . ("���"))  ("lr~" . ("���"))
440
441  ("l-n"  . ("���"))  ("<-n"  . ("���"))  ("l=n"  . ("���"))
442  ("r-n"  . ("���"))  ("->n"  . ("���"))  ("r=n"  . ("���"))  ("=>n"  . ("���"))
443  ("lr-n" . ("���"))  ("<->n" . ("���"))  ("lr=n" . ("���"))  ("<=>n" . ("���"))
444
445  ("l-|"  . ("���"))  ("ll-" . ("���"))
446  ("r-|"  . ("���"))  ("rr-" . ("���"))
447  ("u-|"  . ("���"))  ("uu-" . ("���"))
448  ("d-|"  . ("���"))  ("dd-" . ("���"))
449  ("ud-|" . ("���"))
450
451  ("l->" . ("���"))
452  ("r->" . ("���"))
453
454  ("r-o" . ("���"))  ("-o"  . ("���"))
455
456  ("dz" . ("���"))
457
458  ;; Ellipsis.
459
460  ("..." . ,(hol-input-to-string-list "������������"))
461
462  ;; Box-drawing characters.
463
464  ("---" . ,(hol-input-to-string-list "������������������������������������������������������������������"))
465  ("--=" . ,(hol-input-to-string-list "���������������������������������     ��������������������������� ���������������������������"))
466  ("--_" . ,(hol-input-to-string-list "���������������������������������������������
467                                        ������������������������������������������������������������������������������������������
468                                        ������������������������������������������������ ������������"))
469  ("--." . ,(hol-input-to-string-list "������������������
470                                        ������������������"))
471
472  ;; Triangles.
473
474  ;; Big/small, black/white.
475
476  ("t"     . ,(hol-input-to-string-list "������������������������������������������������������������"))
477  ("Tr"    . ,(hol-input-to-string-list "���������������������������������"))
478
479  ("tb" . ,(hol-input-to-string-list "������������������������������"))
480  ("tw" . ,(hol-input-to-string-list "������������������������������"))
481
482  ("Tb" . ,(hol-input-to-string-list "������������"))
483  ("Tw" . ,(hol-input-to-string-list "������������"))
484
485  ;; Squares.
486
487  ("sq"  . ,(hol-input-to-string-list "���������������������������������������������������������������������"))
488  ("sqb" . ,(hol-input-to-string-list "���������"))
489  ("sqw" . ,(hol-input-to-string-list "���������"))
490  ("sq." . ("���"))
491  ("sqo" . ("���"))
492
493  ;; Rectangles.
494
495  ("re"  . ,(hol-input-to-string-list "������������"))
496  ("reb" . ,(hol-input-to-string-list "������"))
497  ("rew" . ,(hol-input-to-string-list "������"))
498
499  ;; Parallelograms.
500
501  ("pa"  . ,(hol-input-to-string-list "������"))
502  ("pab" . ("���"))
503  ("paw" . ("���"))
504
505  ;; Diamonds.
506
507  ("di"  . ,(hol-input-to-string-list "���������"))
508  ("dib" . ("���"))
509  ("diw" . ("���"))
510  ("di." . ("���"))
511
512  ;; Circles.
513
514  ("ci"   . ,(hol-input-to-string-list "������������������������������������������������������������������������"))
515  ("cib"  . ("���"))
516  ("ciw"  . ("���"))
517  ("ci."  . ("���"))
518  ("ci.." . ("���"))
519  ("ciO"  . ("���"))
520
521  ;; Stars.
522
523  ("st"   . ,(hol-input-to-string-list "������������������ ���������������������������"))
524  ("st4"  . ,(hol-input-to-string-list "������"))
525  ("st6"  . ("���"))
526  ("st8"  . ("���"))
527  ("st12" . ("���"))
528
529  ;; Blackboard bold letters.
530
531  ("bn"   . ("���"))
532  ("bz"   . ("���"))
533  ("bq"   . ("���"))
534  ("br"   . ("���"))
535  ("bc"   . ("���"))
536  ("bp"   . ("���"))
537  ("bb"   . ("����"))
538  ("bsum" . ("���"))
539
540  ;; Blackboard bold numbers.
541
542  ("b0"   . ("����"))
543  ("b1"   . ("����"))
544  ("b2"   . ("����"))
545  ("b3"   . ("����"))
546  ("b4"   . ("����"))
547  ("b5"   . ("����"))
548  ("b6"   . ("����"))
549  ("b7"   . ("����"))
550  ("b8"   . ("����"))
551  ("b9"   . ("����"))
552
553  ;; Parentheses.
554
555  ("(" . ,(hol-input-to-string-list "([{�����������������������������������������������������������������������������������������������������������"))
556  (")" . ,(hol-input-to-string-list ")]}�����������������������������������������������������������������������������������������������������������"))
557
558  ("[[" . ("���"))
559  ("]]" . ("���"))
560  ("<"  . ("���"))
561  (">"  . ("���"))
562  ("<<" . ("���"))
563  (">>" . ("���"))
564  ("f<"  . ("���"))
565  ("f>"  . ("���"))
566  ("f<<" . ("��"))
567  ("f>>" . ("��"))
568  ("{{" . ("���"))
569  ("}}" . ("���"))
570
571  ("(b" . ("���"))
572  (")b" . ("���"))
573
574  ("lbag" . ("���"))
575  ("rbag" . ("���"))
576
577  ;; lambda
578
579  ("fun" . ("��"))
580  ("lam" . ("��"))
581
582  ("X" . ("���"))
583
584  ;; Primes.
585
586  ("'" . ,(hol-input-to-string-list "������������"))
587  ("`" . ,(hol-input-to-string-list "���������"))
588
589  ;; Fractions.
590
591  ("frac" . ,(hol-input-to-string-list "���������������������������������������������"))
592
593  ;; Bullets.
594
595  ("bu"  . ,(hol-input-to-string-list "���������������"))
596  ("bub" . ("���"))
597  ("buw" . ("���"))
598  ("but" . ("���"))
599
600  ;; Types
601  ("nat"  . ("���"))
602  ("Nat"  . ("���"))
603  ("N"    . ("���"))
604  ("N-2"  . ("���������"))
605  ("N-1"  . ("���������"))
606  ("int"  . ("���"))
607  ("Int"  . ("���"))
608  ("Z"    . ("���"))
609  ("rat"  . ("���"))
610  ("Rat"  . ("���"))
611  ("Q"    . ("���"))
612  ("real" . ("���"))
613  ("Real" . ("���"))
614  ("R"    . ("���"))
615  ("Com"  . ("���"))
616  ("com"  . ("���"))
617  ("C"    . ("���"))
618  ("A"    . ("����"))
619  ("F"    . ("����"))
620  ("H"    . ("���"))
621  ("K"    . ("����"))
622
623  ("a" . ("��"))
624  ("b" . ("��"))
625  ("g" . ("��"))
626
627  ;; Musical symbols.
628
629  ("note" . ,(hol-input-to-string-list "������������"))
630  ("flat" . ("���"))
631  ("#"    . ("���"))
632
633  ;; Other punctuation and symbols.
634
635  ("\\"         . ("\\\\"))
636  ("en"         . ("���"))
637  ("em"         . ("���"))
638  ("^i"         . ("���"))
639  ("^o"         . ("���"))
640  ("!!"         . ("���"))
641  ("??"         . ("���"))
642  ("?!"         . ("���" "���"))
643  ("!?"         . ("���"))
644  ("die"        . ,(hol-input-to-string-list "������������������"))
645  ("asterisk"   . ,(hol-input-to-string-list "������������������������������������������������������"))
646  ("8<"         . ("���" "���"))
647  ("tie"        . ("���"))
648  ("undertie"   . ("���"))
649  ("apl"        . ,(hol-input-to-string-list "���������������������������������������������������������
650                                               ���������������������������������������������������������
651                                               ���������������������������������������������������������
652                                               ���������������������������������������"))
653
654  ;; Some combining characters.
655  ;;
656  ;; The following combining characters also have (other)
657  ;; translations:
658  ;; �� �� �� �� �� �� �� �� �� �� �� �� ��
659
660  ("^--" . ,(hol-input-to-string-list"����"))
661  ("_--" . ,(hol-input-to-string-list"����"))
662  ("^~"  . ,(hol-input-to-string-list"����"))
663  ("_~"  .  (                         "��"))
664  ("^."  . ,(hol-input-to-string-list"����������"))
665  ("_."  . ,(hol-input-to-string-list"����"))
666  ("^l"  . ,(hol-input-to-string-list"���������"))
667  ("^l-" .  (                         "���"))
668  ("^r"  . ,(hol-input-to-string-list"���������"))
669  ("^r-" .  (                         "���"))
670  ("^lr" .  (                         "���"))
671  ("_lr" .  (                         "��"))
672  ("^^"  . ,(hol-input-to-string-list"������"))
673  ("_^"  . ,(hol-input-to-string-list"������"))
674  ("^v"  . ,(hol-input-to-string-list"����"))
675  ("_v"  . ,(hol-input-to-string-list"������"))
676
677  ;; Shorter forms of many greek letters plus ��.
678
679  ("Ga"  . ("��"))  ("GA"  . ("��"))
680  ("Gb"  . ("��"))  ("GB"  . ("��"))
681  ("Gg"  . ("��"))  ("GG"  . ("��"))
682  ("Gd"  . ("��"))  ("GD"  . ("��"))
683  ("Ge"  . ("��"))  ("GE"  . ("��"))  ("eps" . ("��"))
684  ("Gz"  . ("��"))  ("GZ"  . ("��"))
685  ;; \eta \Eta
686  ("Gth" . ("��"))  ("GTH" . ("��"))  ("th"  . ("��"))
687  ("Gi"  . ("��"))  ("GI"  . ("��"))
688  ("Gk"  . ("��"))  ("GK"  . ("��"))
689  ("Gl"  . ("��"))  ("GL"  . ("��"))  ("Gl-" . ("��"))
690  ("Gm"  . ("��"))  ("GM"  . ("��"))
691  ("Gn"  . ("��"))  ("GN"  . ("��"))
692  ("Gx"  . ("��"))  ("GX"  . ("��"))
693  ;; \omicron \Omicron
694  ;; \pi \Pi
695  ("Gr"  . ("��"))  ("GR"  . ("��"))
696  ("Gs"  . ("��"))  ("GS"  . ("��"))
697  ("Gt"  . ("��"))  ("GT"  . ("��"))
698  ("Gu"  . ("��"))  ("GU"  . ("��"))
699  ("Gf"  . ("��"))  ("GF"  . ("��"))
700  ("Gc"  . ("��"))  ("GC"  . ("��"))
701  ("Gp"  . ("��"))  ("GP"  . ("��"))
702  ("Go"  . ("��"))  ("GO"  . ("��"))
703  ;; even shorter versions for central type constructors
704  ("S"   . ("��"))  ("P"   . ("��"))
705
706  ;; Mathematical characters
707
708  ("MiA" . ("����"))
709  ("MiB" . ("����"))
710  ("MiC" . ("����"))
711  ("MiD" . ("����"))
712  ("MiE" . ("����"))
713  ("MiF" . ("����"))
714  ("MiG" . ("����"))
715  ("MiH" . ("����"))
716  ("MiI" . ("����"))
717  ("MiJ" . ("����"))
718  ("MiK" . ("����"))
719  ("MiL" . ("����"))
720  ("MiM" . ("����"))
721  ("MiN" . ("����"))
722  ("MiO" . ("����"))
723  ("MiP" . ("����"))
724  ("MiQ" . ("����"))
725  ("MiR" . ("����"))
726  ("MiS" . ("����"))
727  ("MiT" . ("����"))
728  ("MiU" . ("����"))
729  ("MiV" . ("����"))
730  ("MiW" . ("����"))
731  ("MiX" . ("����"))
732  ("MiY" . ("����"))
733  ("MiZ" . ("����"))
734  ("Mia" . ("����"))
735  ("Mib" . ("����"))
736  ("Mic" . ("����"))
737  ("Mid" . ("����"))
738  ("Mie" . ("����"))
739  ("Mif" . ("����"))
740  ("Mig" . ("����"))
741  ("Mii" . ("����"))
742  ("Mij" . ("����"))
743  ("Mik" . ("����"))
744  ("Mil" . ("����"))
745  ("Mim" . ("����"))
746  ("Min" . ("����"))
747  ("Mio" . ("����"))
748  ("Mip" . ("����"))
749  ("Miq" . ("����"))
750  ("Mir" . ("����"))
751  ("Mis" . ("����"))
752  ("Mit" . ("����"))
753  ("Miu" . ("����"))
754  ("Miv" . ("����"))
755  ("Miw" . ("����"))
756  ("Mix" . ("����"))
757  ("Miy" . ("����"))
758  ("Miz" . ("����"))
759  ("MIA" . ("����"))
760  ("MIB" . ("����"))
761  ("MIC" . ("����"))
762  ("MID" . ("����"))
763  ("MIE" . ("����"))
764  ("MIF" . ("����"))
765  ("MIG" . ("����"))
766  ("MIH" . ("����"))
767  ("MII" . ("����"))
768  ("MIJ" . ("����"))
769  ("MIK" . ("����"))
770  ("MIL" . ("����"))
771  ("MIM" . ("����"))
772  ("MIN" . ("����"))
773  ("MIO" . ("����"))
774  ("MIP" . ("����"))
775  ("MIQ" . ("����"))
776  ("MIR" . ("����"))
777  ("MIS" . ("����"))
778  ("MIT" . ("����"))
779  ("MIU" . ("����"))
780  ("MIV" . ("����"))
781  ("MIW" . ("����"))
782  ("MIX" . ("����"))
783  ("MIY" . ("����"))
784  ("MIZ" . ("����"))
785  ("MIa" . ("����"))
786  ("MIb" . ("����"))
787  ("MIc" . ("����"))
788  ("MId" . ("����"))
789  ("MIe" . ("����"))
790  ("MIf" . ("����"))
791  ("MIg" . ("����"))
792  ("MIh" . ("����"))
793  ("MIi" . ("����"))
794  ("MIj" . ("����"))
795  ("MIk" . ("����"))
796  ("MIl" . ("����"))
797  ("MIm" . ("����"))
798  ("MIn" . ("����"))
799  ("MIo" . ("����"))
800  ("MIp" . ("����"))
801  ("MIq" . ("����"))
802  ("MIr" . ("����"))
803  ("MIs" . ("����"))
804  ("MIt" . ("����"))
805  ("MIu" . ("����"))
806  ("MIv" . ("����"))
807  ("MIw" . ("����"))
808  ("MIx" . ("����"))
809  ("MIy" . ("����"))
810  ("MIz" . ("����"))
811  ("McA" . ("����"))
812  ("McC" . ("����"))
813  ("McD" . ("����"))
814  ("McG" . ("����"))
815  ("McJ" . ("����"))
816  ("McK" . ("����"))
817  ("McN" . ("����"))
818  ("McO" . ("����"))
819  ("McP" . ("����"))
820  ("McQ" . ("����"))
821  ("McS" . ("����"))
822  ("McT" . ("����"))
823  ("McU" . ("����"))
824  ("McV" . ("����"))
825  ("McW" . ("����"))
826  ("McX" . ("����"))
827  ("McY" . ("����"))
828  ("McZ" . ("����"))
829  ("Mca" . ("����"))
830  ("Mcb" . ("����"))
831  ("Mcc" . ("����"))
832  ("Mcd" . ("����"))
833  ("Mcf" . ("����"))
834  ("Mch" . ("����"))
835  ("Mci" . ("����"))
836  ("Mcj" . ("����"))
837  ("Mck" . ("����"))
838  ("Mcl" . ("����"))
839  ("Mcm" . ("����"))
840  ("Mcn" . ("����"))
841  ("Mcp" . ("����"))
842  ("Mcq" . ("����"))
843  ("Mcr" . ("����"))
844  ("Mcs" . ("����"))
845  ("Mct" . ("����"))
846  ("Mcu" . ("����"))
847  ("Mcv" . ("����"))
848  ("Mcw" . ("����"))
849  ("Mcx" . ("����"))
850  ("Mcy" . ("����"))
851  ("Mcz" . ("����"))
852  ("MCA" . ("����"))
853  ("MCB" . ("����"))
854  ("MCC" . ("����"))
855  ("MCD" . ("����"))
856  ("MCE" . ("����"))
857  ("MCF" . ("����"))
858  ("MCG" . ("����"))
859  ("MCH" . ("����"))
860  ("MCI" . ("����"))
861  ("MCJ" . ("����"))
862  ("MCK" . ("����"))
863  ("MCL" . ("����"))
864  ("MCM" . ("����"))
865  ("MCN" . ("����"))
866  ("MCO" . ("����"))
867  ("MCP" . ("����"))
868  ("MCQ" . ("����"))
869  ("MCR" . ("����"))
870  ("MCS" . ("����"))
871  ("MCT" . ("����"))
872  ("MCU" . ("����"))
873  ("MCV" . ("����"))
874  ("MCW" . ("����"))
875  ("MCX" . ("����"))
876  ("MCY" . ("����"))
877  ("MCZ" . ("����"))
878  ("MCa" . ("����"))
879  ("MCb" . ("����"))
880  ("MCc" . ("����"))
881  ("MCd" . ("����"))
882  ("MCe" . ("����"))
883  ("MCf" . ("����"))
884  ("MCg" . ("����"))
885  ("MCh" . ("����"))
886  ("MCi" . ("����"))
887  ("MCj" . ("����"))
888  ("MCk" . ("����"))
889  ("MCl" . ("����"))
890  ("MCm" . ("����"))
891  ("MCn" . ("����"))
892  ("MCo" . ("����"))
893  ("MCp" . ("����"))
894  ("MCq" . ("����"))
895  ("MCr" . ("����"))
896  ("MCs" . ("����"))
897  ("MCt" . ("����"))
898  ("MCu" . ("����"))
899  ("MCv" . ("����"))
900  ("MCw" . ("����"))
901  ("MCx" . ("����"))
902  ("MCy" . ("����"))
903  ("MCz" . ("����"))
904  ("MfA" . ("����"))
905  ("MfB" . ("����"))
906  ("MfD" . ("����"))
907  ("MfE" . ("����"))
908  ("MfF" . ("����"))
909  ("MfG" . ("����"))
910  ("MfJ" . ("����"))
911  ("MfK" . ("����"))
912  ("MfL" . ("����"))
913  ("MfM" . ("����"))
914  ("MfN" . ("����"))
915  ("MfO" . ("����"))
916  ("MfP" . ("����"))
917  ("MfQ" . ("����"))
918  ("MfS" . ("����"))
919  ("MfT" . ("����"))
920  ("MfU" . ("����"))
921  ("MfV" . ("����"))
922  ("MfW" . ("����"))
923  ("MfX" . ("����"))
924  ("MfY" . ("����"))
925  ("Mfa" . ("����"))
926  ("Mfb" . ("����"))
927  ("Mfc" . ("����"))
928  ("Mfd" . ("����"))
929  ("Mfe" . ("����"))
930  ("Mff" . ("����"))
931  ("Mfg" . ("����"))
932  ("Mfh" . ("����"))
933  ("Mfi" . ("����"))
934  ("Mfj" . ("����"))
935  ("Mfk" . ("����"))
936  ("Mfl" . ("����"))
937  ("Mfm" . ("����"))
938  ("Mfn" . ("����"))
939  ("Mfo" . ("����"))
940  ("Mfp" . ("����"))
941  ("Mfq" . ("����"))
942  ("Mfr" . ("����"))
943  ("Mfs" . ("����"))
944  ("Mft" . ("����"))
945  ("Mfu" . ("����"))
946  ("Mfv" . ("����"))
947  ("Mfw" . ("����"))
948  ("Mfx" . ("����"))
949  ("Mfy" . ("����"))
950  ("Mfz" . ("����"))
951
952  ;; Some ISO8859-1 characters.
953
954  (" "         . (" "))
955  ("!"         . ("��"))
956  ("cent"      . ("��"))
957  ("brokenbar" . ("��"))
958  ("degree"    . ("��"))
959  ("?"         . ("��"))
960  ("^a_"       . ("��"))
961  ("^o_"       . ("��"))
962
963  ;; Circled, parenthesised etc. numbers and letters.
964
965  ( "(0)" . ,(hol-input-to-string-list " ���"))
966  ( "(1)" . ,(hol-input-to-string-list "������������������"))
967  ( "(2)" . ,(hol-input-to-string-list "������������������"))
968  ( "(3)" . ,(hol-input-to-string-list "������������������"))
969  ( "(4)" . ,(hol-input-to-string-list "������������������"))
970  ( "(5)" . ,(hol-input-to-string-list "������������������"))
971  ( "(6)" . ,(hol-input-to-string-list "������������������"))
972  ( "(7)" . ,(hol-input-to-string-list "������������������"))
973  ( "(8)" . ,(hol-input-to-string-list "������������������"))
974  ( "(9)" . ,(hol-input-to-string-list "������������������"))
975  ("(10)" . ,(hol-input-to-string-list "������������������"))
976  ("(11)" . ,(hol-input-to-string-list "���������"))
977  ("(12)" . ,(hol-input-to-string-list "���������"))
978  ("(13)" . ,(hol-input-to-string-list "���������"))
979  ("(14)" . ,(hol-input-to-string-list "���������"))
980  ("(15)" . ,(hol-input-to-string-list "���������"))
981  ("(16)" . ,(hol-input-to-string-list "���������"))
982  ("(17)" . ,(hol-input-to-string-list "���������"))
983  ("(18)" . ,(hol-input-to-string-list "���������"))
984  ("(19)" . ,(hol-input-to-string-list "���������"))
985  ("(20)" . ,(hol-input-to-string-list "���������"))
986
987  ("(a)"  . ,(hol-input-to-string-list "���������"))
988  ("(b)"  . ,(hol-input-to-string-list "���������"))
989  ("(c)"  . ,(hol-input-to-string-list "���������"))
990  ("(d)"  . ,(hol-input-to-string-list "���������"))
991  ("(e)"  . ,(hol-input-to-string-list "���������"))
992  ("(f)"  . ,(hol-input-to-string-list "���������"))
993  ("(g)"  . ,(hol-input-to-string-list "���������"))
994  ("(h)"  . ,(hol-input-to-string-list "���������"))
995  ("(i)"  . ,(hol-input-to-string-list "���������"))
996  ("(j)"  . ,(hol-input-to-string-list "���������"))
997  ("(k)"  . ,(hol-input-to-string-list "���������"))
998  ("(l)"  . ,(hol-input-to-string-list "���������"))
999  ("(m)"  . ,(hol-input-to-string-list "���������"))
1000  ("(n)"  . ,(hol-input-to-string-list "���������"))
1001  ("(o)"  . ,(hol-input-to-string-list "���������"))
1002  ("(p)"  . ,(hol-input-to-string-list "���������"))
1003  ("(q)"  . ,(hol-input-to-string-list "���������"))
1004  ("(r)"  . ,(hol-input-to-string-list "���������"))
1005  ("(s)"  . ,(hol-input-to-string-list "���������"))
1006  ("(t)"  . ,(hol-input-to-string-list "���������"))
1007  ("(u)"  . ,(hol-input-to-string-list "���������"))
1008  ("(v)"  . ,(hol-input-to-string-list "���������"))
1009  ("(w)"  . ,(hol-input-to-string-list "���������"))
1010  ("(x)"  . ,(hol-input-to-string-list "���������"))
1011  ("(y)"  . ,(hol-input-to-string-list "���������"))
1012  ("(z)"  . ,(hol-input-to-string-list "���������"))
1013  ("y"    . ("��"))
1014
1015
1016  ))
1017  "A list of translations specific to the Hol input method.
1018Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS).
1019All the translation strings are possible translations
1020of the given key sequence; if there is more than one you can choose
1021between them using the arrow keys.
1022
1023Note that if you customize this setting you will not
1024automatically benefit (or suffer) from modifications to its
1025default value when the library is updated.  If you just want to
1026add some bindings it is probably a better idea to customize
1027`hol-input-user-translations'.
1028
1029These translation pairs are included after those in
1030`hol-input-user-translations', but before the ones inherited
1031from other input methods (see `hol-input-inherit').
1032
1033If you change this setting manually (without using the
1034customization buffer) you need to call `hol-input-setup' in
1035order for the change to take effect."
1036  :group 'hol-input
1037  :set 'hol-input-incorporate-changed-setting
1038  :initialize 'custom-initialize-default
1039  :type '(repeat (cons (string :tag "Key sequence")
1040                       (repeat :tag "Translations" string))))
1041
1042(defcustom hol-input-user-translations nil
1043  "Like `hol-input-translations', but more suitable for user
1044customizations since by default it is empty.
1045
1046These translation pairs are included first, before those in
1047`hol-input-translations' and the ones inherited from other input
1048methods."
1049  :group 'hol-input
1050  :set 'hol-input-incorporate-changed-setting
1051  :initialize 'custom-initialize-default
1052  :type '(repeat (cons (string :tag "Key sequence")
1053                       (repeat :tag "Translations" string))))
1054
1055;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1056;; Inspecting and modifying translation maps
1057
1058(defun hol-input-get-translations (qp)
1059  "Return a list containing all translations from the Quail
1060package QP (except for those corresponding to ASCII).
1061Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)."
1062  (with-temp-buffer
1063    (activate-input-method qp) ; To make sure that the package is loaded.
1064    (unless (quail-package qp)
1065      (error "%s is not a Quail package." qp))
1066    (let ((decode-map (list 'decode-map)))
1067      (quail-build-decode-map (list (quail-map)) "" decode-map 0)
1068      (cdr decode-map))))
1069
1070(defun hol-input-show-translations (qp)
1071  "Display all translations used by the Quail package QP (a string).
1072\(Except for those corresponding to ASCII)."
1073  (interactive (list (read-input-method-name
1074                      "Quail input method (default %s): " "Hol")))
1075  (let ((buf (concat "*" qp " input method translations*")))
1076    (with-output-to-temp-buffer buf
1077      (with-current-buffer buf
1078        (quail-insert-decode-map
1079         (cons 'decode-map (hol-input-get-translations qp)))))))
1080
1081(defun hol-input-add-translations (trans)
1082  "Add the given translations TRANS to the Hol input method.
1083TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The
1084translations are appended to the current translations."
1085  (with-temp-buffer
1086    (dolist (tr (hol-input-concat-map (eval hol-input-tweak-all) trans))
1087      (quail-defrule (car tr) (cdr tr) "Hol" t))))
1088
1089(defun hol-input-inherit-package (qp &optional fun)
1090  "Let the Hol input method inherit the translations from the
1091Quail package QP (except for those corresponding to ASCII).
1092
1093The optional function FUN can be used to modify the translations.
1094It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return
1095a list of such pairs."
1096  (let ((trans (hol-input-get-translations qp)))
1097    (hol-input-add-translations
1098     (if fun (hol-input-concat-map fun trans)
1099       trans))))
1100
1101;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1102;; Setting up the input method
1103
1104(defun hol-input-setup ()
1105  "Set up the Hol input method based on the customisable
1106variables and underlying input methods."
1107
1108  ;; Create (or reset) the input method.
1109  (with-temp-buffer
1110    (quail-define-package "Hol" "UTF-8" "���" t ; guidance
1111     "Hol input method.
1112The purpose of this input method is to edit Hol programs, but
1113since it is highly customisable it can be made useful for other
1114tasks as well."
1115     nil nil nil nil nil nil t ; maximum-shortest
1116     ))
1117
1118  (hol-input-add-translations
1119   (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr))))
1120           (append hol-input-user-translations
1121                   hol-input-translations)))
1122  (dolist (def hol-input-inherit)
1123    (hol-input-inherit-package (car def)
1124                                (eval (cdr def)))))
1125
1126(defun hol-input-incorporate-changed-setting (sym val)
1127  "Update the Hol input method based on the customisable
1128variables and underlying input methods.
1129Suitable for use in the :set field of `defcustom'."
1130  (set-default sym val)
1131  (hol-input-setup))
1132
1133;; Set up the input method.
1134
1135(hol-input-setup)
1136(quail-defrule "/\\" "���" "Hol")
1137(quail-defrule "\\/" "���" "Hol")
1138(quail-defrule "==>" "���" "Hol")
1139(quail-defrule "!" "���" "Hol")
1140(quail-defrule "?" "���" "Hol")
1141(quail-defrule "?!" ["���!"] "Hol")
1142(quail-defrule "!!" "!" "Hol")
1143(quail-defrule "??" "?" "Hol")
1144(quail-defrule "<=>" "���" "Hol")
1145(quail-defrule "<>" "���" "Hol")
1146(quail-defrule "<=" "���" "Hol")
1147
1148;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1149;; Administrative details
1150
1151(provide 'hol-input)
1152;;; hol-input.el ends here
1153