1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
;;; phox.el --- Major mode for the PhoX proof assistant
;; This file is part of Proof General.
;; Copyright © 2017 Christophe Raffalli
;;; Commentary:
;;
(require 'proof-site)
;;; Code:
(proof-ready-for-assistant 'phox)
(require 'proof)
(require 'proof-easy-config) ; easy configure mechanism
(defconst phox-goal-regexp
"\\(prop\\(osition\\)?\\)\\|\\(lem\\(ma\\)?\\)\\|\\(fact\\)\\|\\(cor\\(ollary\\)?\\)\\(theo\\(rem\\)?\\)")
(proof-easy-config
'phox "PhoX"
proof-prog-name "phox"
proof-terminal-string "."
proof-script-command-end-regexp"[.][ \n\t\r]"
proof-script-comment-start "(*"
proof-script-comment-end "*)"
proof-script-syntax-table-entries
'(?\( "()1"
?\) ")(4"
?* ". 23"
?$ "w"
?_ "w"
?. "w")
proof-shell-syntax-table-entries
'(?\( "()1"
?\) ")(4"
?* ". 23"
?$ "w"
?_ "w"
?. "w")
proof-goal-command-regexp (concat "^" phox-goal-regexp)
proof-save-command-regexp "^save"
proof-goal-with-hole-regexp (concat "^" phox-goal-regexp "\\(\\([a-zA-Z0-9_$]*\\)\\) ")
proof-save-with-hole-regexp "save \\(\\([a-zA-Z0-9_$]*\\)\\).[ \n\t\r]"
proof-non-undoables-regexp "\\(undo\\)\\|\\(abort\\)\\|\\(show\\)\\(.*\\)[ \n\t\r]"
proof-goal-command "fact \"%s\"."
proof-save-command "save \"%s\"."
proof-kill-goal-command "abort."
proof-showproof-command "show."
proof-undo-n-times-cmd "undo %s."
proof-auto-multiple-files t
proof-shell-cd-cmd "cd \"%s\"."
proof-shell-interrupt-regexp "Interrupt."
proof-shell-start-goals-regexp "goal [0-9]+/[0-9]+"
proof-shell-end-goals-regexp "%PhoX%"
proof-shell-quit-cmd "quit."
proof-assistant-home-page "http://www.lama.univ-savoie.fr/~raffalli/phox.html"
proof-shell-annotated-prompt-regexp "^\\(>PhoX>\\)\\|\\(%PhoX%\\) "
; proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
proof-shell-init-cmd ""
; proof-shell-proof-completed-regexp "^No subgoals!"
proof-script-font-lock-keywords
'("Cst" "Import" "Use" "Sort"
"new_intro" "new_elim" "new_rewrite"
"add_path" "author" "cd"
"claim" "close_def" "def" "del" "documents"
"depend" "elim_after_intro" "export"
"edel" "eshow" "flag" "goal" "include"
"institute" "path" "print_sort" "priority"
"quit" "save" "search" "tex" "tex_syntax" "title"
"proposition" "prop" "lemma" "lem" "fact" "corollary" "cor"
"theorem" "theo"
; proof command, FIXME: another color
"abort" "absurd" "apply" "axiom" "constraints"
"elim" "from" "goals" "intros" "intro" "instance"
"local" "lefts" "left" "next" "rewrite" "rewrite_hyp"
"rename" "rmh" "trivial" "slh" "use" "undo" "unfold"
"unfold_hyp")
)
;; code for displaying unicode borrowed from
;; Erik Parmann, Pål Drange latex-pretty-symbol
;; cf. https://bitbucket.org/mortiferus/latex-pretty-symbols.el
(require 'cl-lib)
(defun substitute-pattern-with-unicode-symbol (pattern symbol)
"Add a font lock hook to replace the matched part of PATTERN with the Unicode
symbol SYMBOL.
Symbol can be the symbol directly, no lookup needed."
(interactive)
(font-lock-add-keywords
nil
`((,pattern
(0 (progn
(compose-region (match-beginning 1) (match-end 1)
,symbol
'decompose-region)
nil))))))
(defun substitute-patterns-with-unicode-symbol (patterns)
"Mapping over PATTERNS, calling SUBSTITUTE-PATTERN-WITH-UNICODE for each of the patterns."
(mapcar #'(lambda (x)
(substitute-pattern-with-unicode-symbol (car x)
(cl-second x)))
patterns))
(defun phox-symbol-regex (str)
"Gets a string, e.g. Alpha, returns the regexp matching the escaped
version of it in Phox code, with no chars in [a-z0-9A-Z] after it."
(interactive "MString:")
(concat "[^!%&*+,-/:;≤=>@\\^`#|~]\\(" str "\\)[^!%&*+,-/:;≤=>@\\^`#|~]"))
(defun phox-word-regex (str)
"Gets a string, e.g. Alpha, returns the regexp matching the escaped
version of it in Phox code, with no chars in [a-z0-9A-Z] after it."
(interactive "MString:")
(concat "\\b\\(" str "\\)\\b"))
;;Goto http://www.fileformat.info/info/unicode/block/mathematical_operators/list.htm and copy the needed character
(defun phox-unicode-simplified ()
"Adds a bunch of font-lock rules to display phox commands as
their unicode counterpart"
(interactive)
(substitute-patterns-with-unicode-symbol
(list
;;These need to be on top, before the versions which are not subscriptet
(list (phox-symbol-regex "<=")"≤")
(list (phox-symbol-regex ">=")"≥")
(list (phox-symbol-regex "!=")"≠")
(list (phox-symbol-regex ":<")"∈")
(list (phox-symbol-regex ":") "∈")
(list (phox-symbol-regex "/\\\\")"∀")
(list (phox-symbol-regex "\\\\/")"∃")
(list (phox-symbol-regex "<->")"↔")
(list (phox-symbol-regex "-->")"⟶")
(list (phox-symbol-regex "->")"→")
(list (phox-symbol-regex "~")"¬")
(list (phox-symbol-regex "&")"∧")
(list (phox-word-regex "or")"∨")
)))
(add-hook 'phox-mode-hook 'phox-unicode-simplified)
(add-hook 'phox-goals-mode-hook 'phox-unicode-simplified)
(add-hook 'phox-response-mode-hook 'phox-unicode-simplified)
(provide 'phox)
;;; phox.el ends here
|
