1;;; -*- emacs-lisp -*- 2;;; to use this mode, you will need to do something along the lines of 3;;; the following and have it in your .emacs file: 4;;; (setq hol-executable "<fullpath to HOL executable>") 5;;; (load "<fullpath to this file>") 6 7;;; The fullpath to this file can be just the name of the file, if 8;;; your elisp variable load-path includes the directory where it 9;;; lives. 10 11(require 'thingatpt) 12(require 'cl) 13(require 'subr-x) 14 15(defgroup hol nil 16 "Customising the Emacs interface to the HOL4 proof assistant." 17 :group 'external) 18 19(define-prefix-command 'hol-map) 20(define-prefix-command 'hol-d-map) 21(make-variable-buffer-local 'hol-buffer-name) 22(make-variable-buffer-local 'hol-buffer-ready) 23(set-default 'hol-buffer-ready nil) 24(set-default 'hol-buffer-name "*HOL*") 25 26(set-default 'hol-default-buffer nil) 27 28(defcustom hol-executable HOL-EXECUTABLE 29 "Path-name for the HOL executable." 30 :group 'hol 31 :type '(file :must-match t)) 32 33(defcustom holmake-executable HOLMAKE-EXECUTABLE 34 "Path-name for the Holmake executable." 35 :group 'hol 36 :type '(file :must-match t)) 37 38(defcustom hol-new-buffer-style-default 'new-frame 39 "Default style for creating new HOL buffers. Possible values are 40new-frame (create in a new-frame); horizontal (create in a new buffer 41that is horizontally adjacent and to the right); and vertical (create in 42a new buffer that is vertically adjacent and below)." 43 :group 'hol 44 :type '(choice (const new-frame :tag "new-frame") 45 (const horizontal :tag "horizontal") 46 (const vertical :tag "vertical"))) 47 48(defun hol-set-executable (filename) 49 "*Set hol executable variable to be NAME." 50 (interactive "fHOL executable: ") 51 (setq hol-executable filename) 52 (setq hol-bare-p nil)) 53 54(defun holmake-set-executable (filename) 55 "*Set holmake executable variable to be NAME." 56 (interactive "fHOL executable: ") 57 (setq holmake-executable filename)) 58 59(defvar hol-mode-sml-init-command 60 "use (Globals.HOLDIR ^ \"/tools/hol-mode.sml\")" 61 "*The command to send to HOL to load the ML-part of hol-mode.") 62 63 64(defcustom hol-echo-commands-p nil 65 "Whether or not to echo the text of commands originating elsewhere." 66 :group 'hol 67 :type 'boolean) 68 69(defcustom hol-raise-on-recentre nil 70 "Controls if hol-recentre (\\[hol-recentre]) also raises the HOL frame." 71 :group 'hol 72 :type 'boolean) 73 74(defcustom hol-unicode-print-font-filename 75 "/usr/share/fonts/truetype/ttf-dejavu/DejaVuSans.ttf" 76 "File name of font to use when printing HOL output to a PDF file." 77 :group 'hol 78 :type '(file :must-match t)) 79 80 81 82(defvar hol-generate-locpragma-p t 83 "*Whether or not to generate (*#loc row col *) pragmas for HOL.") 84 85(defvar hol-emit-time-elapsed-p nil 86 "*Whether or not to print time elapsed messages after causing HOL 87evaluations.") 88 89(defvar hol-auto-load-p t 90 "*Do automatic loading?") 91 92(defvar hol-bare-p nil 93 "*use hol.bare?") 94 95;;; For compatability between both Emacs and XEmacs, please use the following 96;;; two functions to determine if the mark is active, or to set it active. 97 98(defun is-region-active () 99 (or 100 (and (fboundp 'region-active-p) (region-active-p) 101 (fboundp 'region-exists-p) (region-exists-p)) 102 (and transient-mark-mode (boundp 'mark-active) mark-active))) 103 104(defun set-region-active () 105 (or 106 (and (fboundp 'zmacs-activate-region) (zmacs-activate-region)) 107 (and (boundp 'mark-active) (setq mark-active t)))) 108 109(put 'hol-term 'end-op 110 (function (lambda () (skip-chars-forward "^`������")))) 111(defvar hol-beg-pos nil) ; ugh, global, but easiest this way 112(put 'hol-term 'beginning-op 113 (function (lambda () (skip-chars-backward "^`������") (setq hol-beg-pos (point))))) 114(defun hol-term-at-point () 115 (let ((s (thing-at-point 'hol-term))) 116 (with-hol-locpragma hol-beg-pos s))) 117 118;;; makes buffer hol aware. Currently this consists of no more than 119;;; altering the syntax table if its major is sml-mode. 120(defun make-buffer-hol-ready () 121 (if (eq major-mode 'sml-mode) 122 (progn 123 (modify-syntax-entry ?` "$") 124 (modify-syntax-entry ?\\ "\\")))) 125 126(defun hol-buffer-ok (string) 127 "Checks a string to see if it is the name of a good HOL buffer. 128In reality this comes down to checking that a buffer-name has a live 129process in it." 130 (and string (get-buffer-process string) 131 (eq 'run 132 (process-status 133 (get-buffer-process string))))) 134 135(defun ensure-hol-buffer-ok () 136 "Ensures by prompting that a HOL buffer name is OK, and returns it." 137 (if (not hol-buffer-ready) 138 (progn (make-buffer-hol-ready) (setq hol-buffer-ready t))) 139 (if (hol-buffer-ok hol-buffer-name) hol-buffer-name 140 (message 141 (cond (hol-buffer-name (concat hol-buffer-name " not valid anymore.")) 142 (t "Please choose a HOL to attach this buffer to."))) 143 (sleep-for 1) 144 (setq hol-buffer-name (read-buffer "HOL buffer: " hol-default-buffer t)) 145 (while (not (hol-buffer-ok hol-buffer-name)) 146 (ding) 147 (message "Not a valid HOL process") 148 (sleep-for 1) 149 (setq hol-buffer-name 150 (read-buffer "HOL buffer: " hol-default-buffer t))) 151 (setq hol-default-buffer hol-buffer-name) 152 hol-buffer-name)) 153 154 155(defun forward-smlsymbol (n) 156 (interactive "p") 157 (cond ((> n 0) 158 (while (> n 0) 159 (skip-syntax-forward "^.") 160 (skip-syntax-forward ".") 161 (setq n (- n 1)))) 162 ((< n 0) 163 (setq n (- n)) 164 (setq n (- n (if (equal (skip-syntax-backward ".") 0) 0 1)))) 165 (while (> n 0) 166 (skip-syntax-backward "^.") 167 (skip-syntax-backward ".") 168 (setq n (- n 1))))) 169 170(defun is-a-then (s) 171 (and s (or (string-equal s "THEN") 172 (string-equal s "THENL") 173 (string-equal s "val") 174 (string-equal s ">-") 175 (string-equal s ">>") 176 (string-equal s ">|") 177 (string-equal s "\\\\")))) 178 179(defun next-hol-lexeme-terminates-tactic () 180 (skip-syntax-forward " ") 181 (or (eobp) 182 (char-equal (following-char) ?,) 183 (char-equal (following-char) ?\)) 184 ;; (char-equal (following-char) ?=) 185 (char-equal (following-char) ?\;) 186 (is-a-then (word-at-point)) 187 (is-a-then (thing-at-point 'smlsymbol t)) 188 (string= (word-at-point) "val"))) 189 190(defun previous-hol-lexeme-terminates-tactic () 191 (save-excursion 192 (skip-chars-backward " \n\t\r") 193 (or (bobp) 194 (char-equal (preceding-char) ?,) 195 (char-equal (preceding-char) ?=) 196 (char-equal (preceding-char) ?\;) 197 (char-equal (preceding-char) ?\)) 198 (and (condition-case nil 199 (progn (backward-char 1) t) 200 (error nil)) 201 (or (is-a-then (word-at-point)) 202 (is-a-then (thing-at-point 'smlsymbol t)) 203 (string= (word-at-point) "val")))))) 204 205(defun looking-at-tactic-terminator () 206 "Returns a cons-pair (x . y), with x the distance to end, and y the 207 size of the terminator, or nil if there isn't one there. The x value may 208 be zero, if point is immediately after the terminator." 209 (interactive) 210 (let ((c (following-char)) 211 (pc (preceding-char))) 212 (cond ((char-equal c ?,) '(1 . 1)) 213 ((char-equal pc ?,) '(0 . 1)) 214 ((char-equal c ?\)) '(1 . 1)) 215 ((char-equal pc ?\)) '(0 . 1)) 216 ((char-equal c ?\]) '(1 . 1)) 217 ((char-equal pc ?\]) '(0 . 1)) 218 ((char-equal c ?\;) '(1 . 1)) 219 ((char-equal pc ?\;) '(0 . 1)) 220 ((let ((w (word-at-point))) 221 (if (is-a-then w) 222 (cons 223 (- (cdr (bounds-of-thing-at-point 'word)) (point)) 224 (length w)) 225 (let ((w (thing-at-point 'smlsymbol t))) 226 (if (is-a-then w) 227 (cons 228 (- (cdr (bounds-of-thing-at-point 'smlsymbol)) (point)) 229 (length w)) 230 nil)))))))) 231 232(defun looking-at-tactic-starter () 233 "Returns a cons-pair (x . y), with x the distance to end, and y the 234 size of the terminator, or nil if there isn't one there. The x value may 235 be zero, if point is immediately after the terminator." 236 (interactive) 237 (let ((c (following-char)) 238 (pc (preceding-char))) 239 (cond ((char-equal c ?,) '(1 . 1)) 240 ((char-equal pc ?,) '(0 . 1)) 241 ((char-equal c ?\() '(1 . 1)) 242 ((char-equal pc ?\() '(0 . 1)) 243 ((char-equal c ?\[) '(1 . 1)) 244 ((char-equal pc ?\[) '(0 . 1)) 245 ((char-equal c ?\;) '(1 . 1)) 246 ((char-equal pc ?\;) '(0 . 1)) 247 ((let ((w (word-at-point))) 248 (if (is-a-then w) 249 (cons 250 (- (cdr (bounds-of-thing-at-point 'word)) (point)) 251 (length w)) 252 (let ((w (thing-at-point 'smlsymbol t))) 253 (if (is-a-then w) 254 (cons 255 (- (cdr (bounds-of-thing-at-point 'smlsymbol)) (point)) 256 (length w)) 257 nil)))))))) 258 259 260(defun forward-tactic-terminator (n) 261 (interactive "^p") 262 (cond ((> n 0) 263 (let (c) 264 (while (> n 0) 265 (skip-syntax-forward " ") 266 (setq c (looking-at-tactic-terminator)) 267 (while (or (not c) (equal (car c) 0)) 268 (forward-sexp) 269 (skip-syntax-forward " ") 270 (setq c (looking-at-tactic-terminator))) 271 (forward-char (car c)) 272 (setq n (- n 1))))) 273 ((< n 0) 274 (setq n (- n)) 275 (let (c) 276 (while (> n 0) 277 (skip-syntax-backward " ") 278 (setq c (looking-at-tactic-terminator)) 279 (while (or (not c) (equal (car c) (cdr c))) 280 (condition-case nil 281 (backward-sexp) 282 (error (backward-char))) 283 (skip-syntax-backward " ") 284 (setq c (looking-at-tactic-terminator))) 285 (backward-char (- (cdr c) (car c))) 286 (setq n (- n 1))))))) 287 288(defun forward-tactic-starter (n) 289 (interactive "^p") 290 (cond ((> n 0) 291 (let (c) 292 (while (> n 0) 293 (skip-syntax-forward " ") 294 (setq c (looking-at-tactic-starter)) 295 (while (or (not c) (equal (car c) 0)) 296 (forward-sexp) 297 (skip-syntax-forward " ") 298 (setq c (looking-at-tactic-starter))) 299 (forward-char (car c)) 300 (setq n (- n 1))))) 301 ((< n 0) 302 (setq n (- n)) 303 (let (c) 304 (while (> n 0) 305 (skip-syntax-backward " ") 306 (setq c (looking-at-tactic-starter)) 307 (while (or (not c) (equal (car c) (cdr c))) 308 (condition-case nil 309 (backward-sexp) 310 (error (backward-char))) 311 (skip-syntax-backward " ") 312 (setq c (looking-at-tactic-starter))) 313 (backward-char (- (cdr c) (car c))) 314 (setq n (- n 1))))))) 315 316(defun preceded-by-starter () 317 (save-excursion 318 (backward-char) 319 (thing-at-point 'tactic-starter))) 320(defun forward-hol-tactic (n) 321 (interactive "^p") 322 (cond ((> n 0) 323 (while (> n 0) 324 (skip-syntax-forward " ") 325 (while (thing-at-point 'tactic-terminator) 326 (forward-tactic-terminator 1) 327 (skip-syntax-forward " ")) 328 (while (not (thing-at-point 'tactic-terminator)) 329 (forward-sexp 1) 330 (skip-syntax-forward " ")) 331 (skip-syntax-backward " ") 332 (setq n (- n 1)))) 333 ((< n 0) 334 (setq n (- n)) 335 (while (> n 0) 336 (skip-syntax-backward " ") 337 (while (preceded-by-starter) 338 (forward-tactic-starter -1) 339 (skip-syntax-backward " ")) 340 (while (not (preceded-by-starter)) 341 (forward-sexp -1) 342 (skip-syntax-backward " ")) 343 (skip-syntax-forward " ") 344 (setq n (- n 1)))))) 345 346;;; returns true and moves forward a sexp if this is possible, returns nil 347;;; and stays where it is otherwise 348(defun my-forward-sexp () 349 (condition-case nil 350 (progn (forward-sexp 1) t) 351 (error nil))) 352(defun my-backward-sexp() 353 (condition-case nil 354 (progn (backward-sexp 1) t) 355 (error nil))) 356 357(defun word-before-point () 358 (save-excursion 359 (condition-case nil 360 (progn (backward-char 1) (word-at-point)) 361 (error nil)))) 362 363(defun backward-hol-tactic (n) 364 (interactive "p") 365 (forward-hol-tactic (if n (- n) -1))) 366 367(defun prim-mark-hol-tactic () 368 (let ((bounds (bounds-of-thing-at-point 'hol-tactic))) 369 (if bounds 370 (progn 371 (goto-char (cdr bounds)) 372 (push-mark (car bounds) t t) 373 (set-region-active)) 374 (error "No tactic at point")))) 375 376(defun mark-hol-tactic () 377 (interactive) 378 (let ((initial-point (point))) 379 (condition-case nil 380 (prim-mark-hol-tactic) 381 (error 382 ;; otherwise, skip white-space forward to see if this would move us 383 ;; onto a tactic. If so, great, otherwise, go backwards and look for 384 ;; one there. Only if all this fails signal an error. 385 (condition-case nil 386 (progn 387 (skip-chars-forward " \n\t\r") 388 (prim-mark-hol-tactic)) 389 (error 390 (condition-case e 391 (progn 392 (if (skip-chars-backward " \n\t\r") 393 (progn 394 (backward-char 1) 395 (prim-mark-hol-tactic)) 396 (prim-mark-hol-tactic))) 397 (error 398 (goto-char initial-point) 399 (signal (car e) (cdr e)))))))))) 400 401 402(defun with-hol-locpragma (pos s) 403 (if hol-generate-locpragma-p 404 (concat (hol-locpragma-of-position pos) s) 405 s)) 406 407(defun hol-locpragma-of-position (pos) 408 "Convert Elisp position into HOL location pragma. Not for interactive use." 409 (let ((initial-point (point))) 410 (goto-char pos) 411 (let* ((rowstart (point-at-bol)) ;; (line-beginning-position) 412 (row (+ (count-lines 1 pos) 413 (if (= rowstart pos) 1 0))) 414 (col (+ (current-column) 1))) 415 (goto-char initial-point) 416 (format " (*#loc %d %d *)" row col)))) 417 418(defun send-timed-string-to-hol (string echo-p) 419 "Send STRING to HOL (with send-string-to-hol), and emit information about 420how long this took." 421 (interactive) 422 (send-raw-string-to-hol 423 "val hol_mode_time0 = #usr (Timer.checkCPUTimer Globals.hol_clock);" nil nil) 424 (send-string-to-hol string echo-p) 425 (send-raw-string-to-hol 426 "val _ = let val t = #usr (Timer.checkCPUTimer Globals.hol_clock) 427 val elapsed = Time.-(t, hol_mode_time0) 428 in 429 print (\"\\n*** Time taken: \"^ 430 Time.toString elapsed^\"s\\n\") 431 end" nil nil)) 432 433(defvar tactic-connective-regexp 434 "[[:space:]]*\\(THEN1\\|THENL\\|THEN\\|>>\\|>|\\|>-\\|\\\\\\\\\\)[[:space:]]*[[(]?" 435 "Regular expression for strings used to put tactics together.") 436 437(defun tactic-cleanup-leading (string) 438 "Remove leading instances of tactic connectives from a string. 439A tactic connective is any one of \"THEN\", \"THENL\", \"THEN1\", \">>\", \">|\" 440or \">-\"." 441 (let* ((case-fold-search nil) 442 (pattern (concat "\\`" tactic-connective-regexp))) 443 (replace-regexp-in-string pattern "" string))) 444 445(defun tactic-cleanup-trailing (string) 446 "Remove trailing instances of tactic connectives from a string. 447A tactic connective is any one of \"THEN\", \"THENL\", \"THEN1\", \">>\", \">|\" 448or \">-\"." 449 (let* ((case-fold-search nil) 450 (pattern (concat tactic-connective-regexp "\\'"))) 451 (replace-regexp-in-string pattern "" string))) 452 453(defun hol-find-eval-next-tactic (arg) 454 "Highlights the next tactic in the source and evaluates in the HOL buffer. 455With a prefix ARG, uses `expandf' rather than `e'." 456 (interactive "P") 457 (deactivate-mark) 458 (skip-syntax-forward " ") 459 (let 460 ((term (thing-at-point 'tactic-terminator)) 461 (sqb (char-equal (following-char) ?\[))) 462 (while (or term sqb) 463 (cond (term (forward-tactic-terminator 1)) 464 (sqb (forward-char))) 465 (skip-syntax-forward " ") 466 (setq term (thing-at-point 'tactic-terminator)) 467 (setq sqb (char-equal (following-char) ?\[)))) 468 (mark-hol-tactic) 469 (copy-region-as-hol-tactic (region-beginning) (region-end) arg) 470 (goto-char (region-end))) 471 472(defun copy-region-as-hol-tactic (start end arg) 473 "Send selected region to HOL process as tactic." 474 (interactive "r\nP") 475 (let* 476 ((region-string0 (buffer-substring start end)) 477 (region-string1 (tactic-cleanup-leading region-string0)) 478 (region-string2 (tactic-cleanup-trailing region-string1)) 479 (start-offset (- (length region-string0) (length region-string1))) 480 (region-string3 (with-hol-locpragma (+ start start-offset) region-string2)) 481 (ste "\"show_typecheck_errors\"") 482 (region-string (concat "let val old = Feedback.current_trace " 483 ste 484 " val _ = Feedback.set_trace " 485 ste 486 " 0 in (" 487 region-string3 488 ") before " 489 "Feedback.set_trace " ste " old end")) 490 (e-string (concat "proofManagerLib." (if arg "expandf" "e"))) 491 (tactic-string (format "%s (%s)" e-string region-string)) 492 (sender (if hol-emit-time-elapsed-p 493 'send-timed-string-to-hol 494 'send-string-to-hol))) 495 (funcall sender tactic-string hol-echo-commands-p))) 496 497;;; For goaltrees 498(defun copy-region-as-goaltree-tactic (start end) 499 "Send selected region to HOL process as goaltree tactic." 500 (interactive "r\nP") 501 (let* ((region-string (with-hol-locpragma start 502 (buffer-substring-no-properties start end))) 503 (tactic-string 504 (format "proofManagerLib.expandv (%S,%s) handle e => Raise e" 505 region-string region-string)) 506 (sender (if hol-emit-time-elapsed-p 507 'send-timed-string-to-hol 508 'send-string-to-hol))) 509 (funcall sender tactic-string hol-echo-commands-p))) 510 511(defun send-string-as-hol-goal (s) 512 (let ((goal-string (format "proofManagerLib.g `%s`" s))) 513 (send-raw-string-to-hol goal-string hol-echo-commands-p t) 514 (send-raw-string-to-hol "proofManagerLib.set_backup 100;" nil nil))) 515 516(defun hol-do-goal (arg) 517 "Send term around point to HOL process as goal. 518If prefix ARG is true, or if in transient mark mode, region is active and 519the region contains no backquotes, then send region instead." 520 (interactive "P") 521 (let ((txt (condition-case nil 522 (with-hol-locpragma (region-beginning) 523 (buffer-substring (region-beginning) (region-end))) 524 (error nil)))) 525 (if (or (and (is-region-active) (= (count ?\` txt) 0)) 526 arg) 527 (send-string-as-hol-goal txt) 528 (send-string-as-hol-goal (hol-term-at-point))))) 529 530 531(defun send-string-as-hol-goaltree (s) 532 (let ((goal-string 533 (format "proofManagerLib.gt `%s` handle e => Raise e" s))) 534 (send-raw-string-to-hol goal-string hol-echo-commands-p t) 535 (send-raw-string-to-hol "proofManagerLib.set_backup 100;" nil nil))) 536 537 538(defun hol-do-goaltree (arg) 539 "Send term around point to HOL process as goaltree. 540If prefix ARG is true, or if in transient mark mode, region is active and 541the region contains no backquotes, then send region instead." 542 (interactive "P") 543 (let ((txt (condition-case nil 544 (with-hol-locpragma (region-beginning) 545 (buffer-substring (region-beginning) (region-end))) 546 (error nil)))) 547 (if (or (and (is-region-active) (= (count ?\` txt) 0)) 548 arg) 549 (send-string-as-hol-goaltree txt) 550 (send-string-as-hol-goaltree (hol-term-at-point))))) 551 552(defun copy-region-as-hol-definition (start end arg) 553 "Send selected region to HOL process as definition/expression. With a 554prefix arg of 4 (hit control-u once), wrap what is sent so that it becomes 555( .. ) handle e => Raise e, allowing HOL_ERRs to be displayed cleanly. 556With a prefix arg of 16 (hit control-u twice), toggle Moscow ML's quiet-dec 557variable before and after the region is sent." 558 (interactive "r\np") 559 (let* ((buffer-string 560 (with-hol-locpragma start (buffer-substring start end))) 561 (send-string 562 (if (= arg 4) 563 (concat "(" buffer-string ") handle e => Raise e") 564 buffer-string)) 565 (sender (if hol-emit-time-elapsed-p 566 'send-timed-string-to-hol 567 'send-string-to-hol))) 568 (if (= arg 16) (hol-toggle-quietdec)) 569 (funcall sender send-string hol-echo-commands-p) 570 (if (> (length send-string) 300) 571 (send-string-to-hol 572 "val _ = print \"\\n*** Emacs/HOL command completed ***\\n\\n\"")) 573 (if (= (prefix-numeric-value arg) 16) (hol-toggle-quietdec)))) 574 575 576 577(defun copy-region-as-hol-definition-quietly (start end) 578 (interactive "r") 579 (hol-toggle-quiet-quietdec) 580 (copy-region-as-hol-definition start end 0) 581 (hol-toggle-quiet-quietdec)) 582 583 584(defun hol-name-top-theorem (string arg) 585 "Name the top theorem of the proofManagerLib. 586With prefix argument, drop the goal afterwards." 587 (interactive "sName for top theorem: \nP") 588 (if (not (string= string "")) 589 (send-raw-string-to-hol 590 (format "val %s = top_thm()" string) 591 hol-echo-commands-p t)) 592 (if arg (send-raw-string-to-hol "proofManagerLib.drop()" hol-echo-commands-p nil))) 593 594(defun hol-start-termination-proof (arg) 595 "Send definition around point to HOL process as Defn.tgoal. 596If prefix ARG is true, or if in transient mark mode, region is active and 597the region contains no backquotes, then send region instead." 598 (interactive "P") 599 (let ((txt (condition-case nil 600 (with-hol-locpragma (region-beginning) 601 (buffer-substring (region-beginning) (region-end))) 602 (error nil)))) 603 (if (or (and (is-region-active) (= (count ?\` txt) 0)) 604 arg) 605 (hol-send-string-as-termination-proof txt) 606 (hol-send-string-as-termination-proof (hol-term-at-point))))) 607 608(defun hol-send-string-as-termination-proof (str) 609 (send-raw-string-to-hol 610 (concat 611 "Defn.tgoal (Defn.Hol_defn \"HOLmode_defn\" `" str "`) handle e => Raise e") nil t)) 612 613(defun remove-sml-comments (end) 614 (let (done (start (point))) 615 (while (and (not done) (re-search-forward "(\\*\\|\\*)" end t)) 616 (if (string= (match-string 0) "*)") 617 (progn 618 (delete-region (- start 2) (point)) 619 (setq done t)) 620 ;; found a comment beginning 621 (if (not (remove-sml-comments end)) (setq done t)))) 622 (if (not done) (message "Incomplete comment in region given")) 623 done)) 624 625(defun remove-quoted-hol-term (bq eq end-marker) 626 (let ((start (point)) 627 (bqsize (length bq))) 628 (if (re-search-forward eq end-marker t) 629 (delete-region (- start bqsize) (point)) 630 (error 631 (format "Incomplete (%s...%s-quoted) HOL term in region given; \ 632starts >%s%s<" 633 bq eq 634 bq 635 (buffer-substring (point) (+ (point) 10))))))) 636 637(defun remove-hol-string (end-marker) 638 (let ((start (point))) 639 (if (re-search-forward "\n\\|[^\\]?\"" end-marker t) 640 (if (string= (match-string 0) "\n") 641 (message "String literal terminated by newline - not allowed!") 642 (delete-region (- start 1) (point)))))) 643 644 645(defun remove-sml-junk (start end) 646 "Removes all sml comments, HOL terms and strings in the given region." 647 (interactive "r") 648 (let ((m (make-marker))) 649 (set-marker m end) 650 (save-excursion 651 (goto-char start) 652 (while (re-search-forward "(\\*\\|`\\|\"\\|���\\|���" m t) 653 (let ((ms (match-string 0))) 654 (cond ((string= ms "(*") (remove-sml-comments m)) 655 ((string= ms "\"") (remove-hol-string m)) 656 ((string= ms "���") (remove-quoted-hol-term "���" "���" m)) 657 ((string= ms "���") (remove-quoted-hol-term "���" "���" m)) 658 (t ; must be a back-tick 659 (if (not (looking-at "`")) 660 (remove-quoted-hol-term "`" "`" m) 661 (forward-char 1) 662 (remove-quoted-hol-term "``" "``" m)))))) 663 (set-marker m nil)))) 664 665(defun remove-sml-lets-locals 666 (start end &optional looking-for-end &optional recursing) 667 "Removes all local-in-ends and let-in-ends from a region. We assume 668that the buffer has already had HOL terms, comments and strings removed." 669 (interactive "r") 670 (let ((m (if (not recursing) (set-marker (make-marker) end) end)) 671 retval) 672 (if (not recursing) (goto-char start)) 673 (if (re-search-forward "\\blet\\b\\|\\blocal\\b\\|\\bend\\b" m t) 674 (let ((declstring (match-string 0))) 675 (if (or (string= declstring "let") (string= declstring "local")) 676 (and 677 (remove-sml-lets-locals (- (point) (length declstring)) m t t) 678 (remove-sml-lets-locals start m looking-for-end t) 679 (setq retval t)) 680 ;; found an "end" 681 (if (not looking-for-end) 682 (message "End without corresponding let/local") 683 (delete-region start (point)) 684 (setq retval t)))) 685 ;; didn't find anything 686 (if looking-for-end 687 (message "Let/local without corresponding end") 688 (setq retval t))) 689 (if (not recursing) (set-marker m nil)) 690 retval)) 691 692(defun word-list-to-regexp (words) 693 (mapconcat (lambda (s) (concat "\\b" s "\\b")) words "\\|")) 694 695(setq hol-open-terminator-regexp 696 (concat ";\\|" 697 (word-list-to-regexp 698 '("val" "fun" "in" "infix[lr]?" "open" "local" "type" 699 "datatype" "nonfix" "exception" "end" "structure")))) 700 701(setq sml-struct-id-regexp "[A-Za-z][A-Za-z0-9_]*") 702 703(defun send-string-to-hol (string &optional echoit) 704 "Send a string to HOL process." 705 (let ((buf (ensure-hol-buffer-ok)) 706 (hol-ok hol-buffer-ready) 707 (tmpbuf (generate-new-buffer "*HOL temporary*")) 708 (old-mark-active (is-region-active))) 709 (unwind-protect 710 (save-excursion 711 (set-buffer tmpbuf) 712 (modify-syntax-entry ?_ "w") 713 (setq hol-buffer-name buf) ; version of this variable in tmpbuf 714 (setq hol-buffer-ready hol-ok) ; version of this variable in tmpbuf 715 (setq case-fold-search nil) ; buffer-local version 716 (insert string) 717 (goto-char (point-min)) 718 (remove-sml-junk (point-min) (point-max)) 719 (goto-char (point-min)) 720 ;; first thing to do is to search through buffer looking for 721 ;; identifiers of form id.id. When spotted such identifiers need 722 ;; to have the first component of the name loaded. 723 (if hol-auto-load-p 724 (while (re-search-forward (concat "\\(" sml-struct-id-regexp 725 "\\)\\.\\w+") 726 (point-max) t) 727 (hol-load-string (match-string 1))) 728 t) 729 ;; next thing to do is to look for open declarations 730 (goto-char (point-min)) 731 ;; search through buffer for open declarations 732 (while (re-search-forward "\\s-open\\s-" (point-max) t) 733 ;; point now after an open, now search forward to end of 734 ;; buffer or a semi-colon, or an infix declaration or a 735 ;; val or a fun or another open (as per the regexp defined just 736 ;; before this function definition 737 (let ((start (point)) 738 (end 739 (save-excursion 740 (if (re-search-forward hol-open-terminator-regexp 741 (point-max) t) 742 (- (point) (length (match-string 0))) 743 (point-max))))) 744 (hol-load-modules-in-region start end))) 745 ;; send the string 746 (delete-region (point-min) (point-max)) 747 (insert string) 748 (send-buffer-to-hol-maybe-via-file echoit)) 749 (kill-buffer tmpbuf)) ; kill buffer always 750 ;; deactivate-mark will have likely been set by all the editting actions 751 ;; in the temporary buffer. We fix this here, thereby keeping the mark 752 ;; active, if it is active. 753 ;; if in XEmacs, use (zmacs-activate-region) instead. 754 (if (boundp 'deactivate-mark) 755 (if deactivate-mark (setq deactivate-mark nil)) 756 (if (and old-mark-active (fboundp 'zmacs-activate-region)) 757 (zmacs-activate-region))))) 758 759(defun interactive-send-string-to-hol (string &optional echoit) 760 "Send a string to HOL process." 761 (interactive "sString to send to HOL process: \nP") 762 (if hol-emit-time-elapsed-p 763 (send-timed-string-to-hol string echoit) 764 (send-string-to-hol string echoit))) 765 766(if (null temporary-file-directory) 767 (if (equal system-type 'windows-nt) 768 (if (not (null (getenv "TEMP"))) 769 (setq temporary-file-directory (getenv "TEMP"))) 770 (setq temporary-file-directory "/tmp"))) 771 772(defun make-temp-file-xemacs (prefix &optional dir-flag) 773 "Create a temporary file. 774The returned file name (created by appending some random characters at the end 775of PREFIX, and expanding against `temporary-file-directory' if necessary, 776is guaranteed to point to a newly created empty file. 777You can then use `write-region' to write new data into the file. 778 779If DIR-FLAG is non-nil, create a new empty directory instead of a file." 780 (let (file) 781 (while (condition-case () 782 (progn 783 (setq file 784 (make-temp-name 785 (expand-file-name prefix temporary-file-directory))) 786 (if dir-flag 787 (make-directory file) 788 (write-region "" nil file nil 'silent nil)) ;; 'excl 789 nil) 790 (file-already-exists t)) 791 ;; the file was somehow created by someone else between 792 ;; `make-temp-name' and `write-region', let's try again. 793 nil) 794 file)) 795 796(defvar hol-mode-to-delete nil 797 "String optionally containing name of last temporary file used to transmit 798HOL sources to a running session (using \"use\")") 799 800(defun send-buffer-to-hol-maybe-via-file (&optional echoit) 801 "Send the contents of current buffer to HOL, possibly putting it into a 802file to \"use\" first." 803 (if (< 500 (buffer-size)) 804 (let ((fname (if (fboundp 'make-temp-file) 805 ;; then 806 (make-temp-file "hol") 807 ;; else 808 (make-temp-file-xemacs "hol") 809 ))) 810 (if (stringp hol-mode-to-delete) 811 (progn (condition-case nil 812 (delete-file hol-mode-to-delete) 813 (error nil)) 814 (setq hol-mode-to-delete nil))) 815 ; below, use visit parameter = 1 to stop message in mini-buffer 816 (write-region (point-min) (point-max) fname nil 1) 817 (send-raw-string-to-hol (format "use \"%s\"" fname) nil t) 818 (setq hol-mode-to-delete fname)) 819 (send-raw-string-to-hol (buffer-string) echoit t))) 820 821 822(defun send-raw-string-to-hol (string echoit newstart) 823 "Sends a string in the raw to HOL. Not for interactive use." 824 (let ((buf (ensure-hol-buffer-ok))) 825 (if echoit 826 (save-excursion 827 (set-buffer buf) 828 (goto-char (point-max)) 829 (princ (concat string ";") (get-buffer buf)) 830 (goto-char (point-max)) 831 (comint-send-input) 832 (hol-recentre)) 833 (comint-send-string buf (concat string ";\n"))))) 834 835 836(defun hol-backup () 837 "Perform a HOL backup." 838 (interactive) 839 (send-raw-string-to-hol "proofManagerLib.b()" hol-echo-commands-p t)) 840 841(defun hol-user-backup () 842 "Perform a HOL backup to a user-defined save-point." 843 (interactive) 844 (send-raw-string-to-hol "proofManagerLib.restore()" hol-echo-commands-p t)) 845 846(defun hol-print-info () 847 "Show some information about the currently running HOL and the settings of hol-mode." 848 (interactive) 849 (send-raw-string-to-hol 850 (concat "print_current_hol_status" "\"" 851 hol-executable "\" \"" holmake-executable "\" ();") hol-echo-commands-p t)) 852 853(defun hol-user-save-backup () 854 "Saves the current status of the proof for later backups to this point." 855 (interactive) 856 (send-raw-string-to-hol "proofManagerLib.save()" hol-echo-commands-p t)) 857 858(defun hol-print-goal () 859 "Print the current HOL goal." 860 (interactive) 861 (send-raw-string-to-hol "proofManagerLib.p()" hol-echo-commands-p t)) 862 863(defun hol-print-all-goals () 864 "Print all the current HOL goals." 865 (interactive) 866 (send-raw-string-to-hol "proofManagerLib.status()" hol-echo-commands-p t)) 867 868(defun hol-interrupt () 869 "Perform a HOL interrupt." 870 (interactive) 871 (let ((buf (ensure-hol-buffer-ok))) 872 (interrupt-process (get-buffer-process buf)))) 873 874 875(defun hol-kill () 876 "Kill HOL process." 877 (interactive) 878 (let ((buf (ensure-hol-buffer-ok))) 879 (kill-process (get-buffer-process buf)))) 880 881(defun hol-recentre () 882 "Display the HOL window in such a way that it displays most text." 883 (interactive) 884 (if (get-buffer-window hol-buffer-name t) 885 (save-selected-window 886 (select-window (get-buffer-window hol-buffer-name t)) 887 (and hol-raise-on-recentre (raise-frame)) 888 (goto-char (point-max)) 889 (recenter -1)))) 890 891(defun hol-rotate (arg) 892 "Rotate the goal stack N times. Once by default." 893 (interactive "p") 894 (send-raw-string-to-hol (format "proofManagerLib.r %d" arg) 895 hol-echo-commands-p t)) 896 897(defun hol-scroll-up (arg) 898 "Scrolls the HOL window." 899 (interactive "P") 900 (ensure-hol-buffer-ok) 901 (save-excursion 902 (select-window (get-buffer-window hol-buffer-name t)) 903 (scroll-up arg))) 904 905(defun hol-scroll-down (arg) 906 "Scrolls the HOL window." 907 (interactive "P") 908 (ensure-hol-buffer-ok) 909 (save-excursion 910 (select-window (get-buffer-window hol-buffer-name t)) 911 (scroll-down arg))) 912 913(defun hol-use-file (filename) 914 "Gets HOL session to \"use\" a file." 915 (interactive "fFile to use: ") 916 (send-raw-string-to-hol (concat "use \"" filename "\";") 917 hol-echo-commands-p nil)) 918 919(defun hol-load-string (s) 920 "Loads the ML object file NAME.uo; checking that it isn't already loaded." 921 (let* ((buf (ensure-hol-buffer-ok)) 922 (mys (format "%s" s)) ;; gets rid of text properties 923 (commandstring 924 (concat "val _ = if List.exists (fn s => s = \"" 925 mys 926 "\") (emacs_hol_mode_loaded()) then () else " 927 "(print \"Loading " mys 928 "\\n\"; " "Meta.load \"" mys "\");\n"))) 929 (comint-send-string buf commandstring))) 930 931(defun hol-load-modules-in-region (start end) 932 "Attempts to load all of the words in the region as modules." 933 (interactive "rP") 934 (save-excursion 935 (goto-char start) 936 (while (re-search-forward (concat "\\b" sml-struct-id-regexp "\\b") end t) 937 (hol-load-string (match-string 0))))) 938 939(defun hol-load-file (arg) 940 "Gets HOL session to \"load\" the file at point. 941If there is no filename at point, then prompt for file. If the region 942is active (in transient mark mode) and it looks like it might be a 943module name or a white-space delimited list of module names, then send 944region instead. With prefix ARG prompt for a file-name to load." 945 (interactive "P") 946 (let* ((wap (word-at-point)) 947 (txt (condition-case nil 948 (buffer-substring (region-beginning) (region-end)) 949 (error nil)))) 950 (cond (arg (hol-load-string (read-string "Library to load: "))) 951 ((and (is-region-active) 952 (string-match (concat "^\\(\\s-*" sml-struct-id-regexp 953 "\\)+\\s-*$") txt)) 954 (hol-load-modules-in-region (region-beginning) (region-end))) 955 ((and wap (string-match "^\\w+$" wap)) (hol-load-string wap)) 956 (t (hol-load-string (read-string "Library to load: ")))))) 957 958 959(defun hol-mode-init-sml () 960 (hol-toggle-quiet-quietdec) 961 (send-raw-string-to-hol hol-mode-sml-init-command nil nil) 962 (hol-toggle-quiet-quietdec)) 963 964(defun turn-off-hol-font-lock (oldvar) 965 (interactive) 966 (if (not oldvar) 967 (progn 968 (message "Turning on font-lock mode does nothing in HOL mode") 969 (setq font-lock-defaults nil))) 970 (setq font-lock-mode nil)) 971 972(defun holmake (&optional dir) 973 (interactive "DRun Holmake in dir: ") 974 (if (not (null dir)) 975 (save-excursion 976 (set-buffer (get-buffer-create "*Holmake*")) 977 (delete-region (point-min) (point-max)) 978 (cd (expand-file-name dir))) 979 ) 980 (let* ((buf (make-comint "Holmake" 981 holmake-executable nil "--qof" "-k"))) 982 (save-excursion 983 (set-buffer buf) 984 (font-lock-mode 0) 985 (make-local-variable 'font-lock-function) 986 (setq font-lock-function 'turn-off-hol-font-lock) 987 (setq comint-preoutput-filter-functions '(holmakepp-output-filter))) 988 (setq comint-scroll-show-maximum-output t) 989 (setq comint-scroll-to-bottom-on-output t) 990 (display-buffer buf) 991 )) 992 993;** hol map keys and function definitions 994(defun hol-executable-with-bare () 995 (if hol-bare-p (concat hol-executable ".bare") 996 hol-executable)) 997 998(defun hol () 999 "Runs a HOL session in a comint window." 1000 (interactive) 1001 (let* ((hol-was-ok (hol-buffer-ok hol-buffer-name)) 1002 (buf (make-comint "HOL" (hol-executable-with-bare)))) 1003 (setq hol-buffer-name (buffer-name buf)) 1004 (switch-to-buffer buf) 1005 (setq comint-prompt-regexp "^- ") 1006 (setq hol-buffer-name (buffer-name buf)) 1007 ;; must go to ridiculous lengths to ensure that font-lock-mode is 1008 ;; turned off and stays off 1009 (font-lock-mode 0) 1010 (make-local-variable 'font-lock-function) 1011 (setq font-lock-function 'turn-off-hol-font-lock) 1012 (make-local-variable 'comint-preoutput-filter-functions) 1013 (holpp-quiet-reset) 1014 (setq comint-preoutput-filter-functions '(holpp-output-filter)) 1015 (setq comint-scroll-show-maximum-output t) 1016 (setq comint-scroll-to-bottom-on-output t) 1017 (if hol-was-ok t (hol-mode-init-sml)) 1018 (send-raw-string-to-hol 1019 "val _ = Parse.current_backend := PPBackEnd.emacs_terminal;" nil nil))) 1020 1021(defun hol-toggle-bare () 1022 "Toggles the elisp variable 'hol-bare-p." 1023 (interactive) 1024 (setq hol-bare-p (not hol-bare-p)) 1025 (concat "using " (hol-executable-with-bare))) 1026 1027(defun hol-display () 1028 (interactive) 1029 (display-buffer hol-buffer-name)); 1030 1031 1032(defun hol-vertical () 1033 "Runs a HOL session after splitting the window" 1034 (interactive) 1035 (split-window-vertically) 1036 (other-window 1) 1037 (hol) 1038 (other-window -1)) 1039 1040(defun hol-horizontal () 1041 "Runs a HOL session after splitting the window" 1042 (interactive) 1043 (split-window-horizontally) 1044 (other-window 1) 1045 (hol) 1046 (other-window -1)) 1047 1048(defun hol-new-frame () 1049 "Runs a HOL session in a new frame" 1050 (interactive) 1051 (let* ((curframe (selected-frame)) 1052 (oldtop (cdr (assoc 'top (frame-parameters)))) 1053 (oldleft (cdr (assoc 'left (frame-parameters)))) 1054 (newframe (make-frame))) 1055 (set-frame-position newframe (+ oldleft 500) oldtop) ; disgusting 1056 (select-frame newframe) 1057 (hol) 1058 (select-frame-set-input-focus curframe))) 1059 1060(defvar hol-new-buffer-style hol-new-buffer-style-default) 1061 1062(setq hol-new-buffer-style-alist 1063 '((horizontal . hol-horizontal) 1064 (vertical . hol-vertical) 1065 (new-frame . hol-new-frame))) 1066 1067(defun hol-with-region () 1068 "Starts a HOL session and pastes selected region into it. If there is no active region, pastes whole buffer." 1069 (interactive) 1070 (let* ((style-str (completing-read 1071 (concat "HOL buffer position (" 1072 (symbol-name hol-new-buffer-style) 1073 "): ") 1074 '("horizontal" "vertical" "new-frame") 1075 nil 1076 t 1077 nil 1078 nil 1079 (symbol-name hol-new-buffer-style) 1080 t)) 1081 (style (intern style-str)) 1082 (starter (cdr (assoc style hol-new-buffer-style-alist)))) 1083 (setq hol-new-buffer-style style) 1084 (funcall starter) 1085 (if (region-active-p) 1086 (copy-region-as-hol-definition-quietly (region-beginning) (region-end)) 1087 (copy-region-as-hol-definition-quietly (point-min) (point-max))))) 1088 1089(defun run-program (filename niceness) 1090 "Runs a PROGRAM in a comint window, with a given (optional) NICENESS." 1091 (interactive "fProgram to run: \nP") 1092 (let* ((niceval (cond ((null niceness) 0) 1093 ((listp niceness) 10) 1094 (t (prefix-numeric-value niceness)))) 1095 (progname (format "%s(n:%d)" 1096 (file-name-nondirectory filename) 1097 niceval)) 1098 (buf (cond ((> niceval 0) 1099 (make-comint progname "nice" nil 1100 (format "-%d" niceval) 1101 (expand-file-name filename))) 1102 (t (make-comint progname 1103 (expand-file-name filename) 1104 nil))))) 1105 (switch-to-buffer buf))) 1106 1107(defun hol-toggle-var (s) 1108 "Toggles the boolean variable STRING." 1109 (message (concat "Toggling " s)) 1110 (send-raw-string-to-hol 1111 (format (concat "val _ = (%s := not (!%s);" 1112 "print (\"*** %s now \" ^" 1113 "Bool.toString (!%s)^\" ***\\n\"))") 1114 s s s s) nil nil)) 1115 1116(defun hol-toggle-var-quiet (s) 1117 "Toggles the boolean variable STRING." 1118 (send-raw-string-to-hol 1119 (format "val _ = (%s := not (!%s));" 1120 s s) nil nil)) 1121 1122(defun hol-toggle-trace (s &optional arg) 1123 "Toggles the trace variable STRING between zero and non-zero. With prefix 1124argument N, sets the trace to that value in particular." 1125 (interactive "sTrace name: \nP") 1126 (if (null arg) 1127 (progn 1128 (message (concat "Toggling " s)) 1129 (send-raw-string-to-hol 1130 (format "val _ = let val nm = \"%s\" 1131 fun findfn r = #name r = nm 1132 val old = 1133 #trace_level (valOf (List.find findfn (traces()))) 1134 in 1135 print (\"** \"^nm^\" trace now \"); 1136 if 0 < old then (set_trace nm 0; print \"off\\n\") 1137 else (set_trace nm 1; print \"on\\n\") 1138 end handle Option => 1139 print \"** No such trace var: \\\"%s\\\"\\n\"" 1140 s s) nil nil)) 1141 (let ((n (prefix-numeric-value arg))) 1142 (message (format "Setting %s to %d" s n)) 1143 (send-raw-string-to-hol 1144 (format "val _ = (set_trace \"%s\" %d; print \"** %s trace now %d\\n\") 1145 handle HOL_ERR _ => 1146 print \"** No such trace var: \\\"%s\\\"\\n\"" 1147 s n s n s) nil nil)))) 1148 1149(defun hol-toggle-unicode () 1150 "Toggles the \"Unicode\" trace." 1151 (interactive) 1152 (hol-toggle-trace "Unicode")) 1153 1154 1155(defun hol-toggle-emacs-tooltips () 1156 "Toggles whether HOL produces tooltip information while pretty-printing." 1157 (interactive) 1158 (hol-toggle-trace "PPBackEnd show types")) 1159 1160(defun hol-toggle-pp-styles () 1161 "Toggles whether HOL produces style informations while pretty-printing." 1162 (interactive) 1163 (hol-toggle-trace "PPBackEnd use styles")) 1164 1165(defun hol-toggle-pp-cases () 1166 "Toggles the \"pp_cases\" trace." 1167 (interactive) 1168 (hol-toggle-trace "pp_cases") 1169 (hol-toggle-trace "use pmatch_pp")) 1170 1171(defun hol-toggle-pp-annotations () 1172 "Toggles whether HOL produces annotations while pretty-printing." 1173 (interactive) 1174 (hol-toggle-trace "PPBackEnd use annotations")) 1175 1176(defun hol-toggle-goalstack-fvs () 1177 "Toggles the trace \"Goalstack.print_goal_fvs\"." 1178 (interactive) 1179 (hol-toggle-trace "Goalstack.print_goal_fvs")) 1180 1181(defun hol-toggle-goalstack-print-goal-at-top () 1182 "Toggles the trace \"Goalstack.print_goal_at_top\"." 1183 (interactive) 1184 (hol-toggle-trace "Goalstack.print_goal_at_top")) 1185 1186(defun hol-toggle-goalstack-num-assums (arg) 1187 "Toggles the number of assumptions shown in a goal." 1188 (interactive "nMax. number of visible assumptions: ") 1189 (hol-toggle-trace "Goalstack.howmany_printed_assums" arg)) 1190 1191(defun hol-toggle-goalstack-num-subgoals (arg) 1192 "Toggles the number of shown subgoals." 1193 (interactive "nMax. number of shown subgoals: ") 1194 (hol-toggle-trace "Goalstack.howmany_printed_subgoals" arg)) 1195 1196(defun hol-toggle-simplifier-trace (arg) 1197 "Toggles the trace \"simplifier\". With ARG sets trace to this value." 1198 (interactive "P") 1199 (hol-toggle-trace "simplifier" arg)) 1200 1201(defun hol-toggle-show-types (arg) 1202 "Toggles the global show_types variable. With prefix ARG sets trace to this value (setting trace to 2, is the same as setting the show_types_verbosely variable)." 1203 (interactive "P") 1204 (hol-toggle-trace "types" arg)) 1205 1206(defun hol-toggle-show-types-verbosely () 1207 "Toggles the global show_types_verbosely variable." 1208 (interactive) 1209 (hol-toggle-var "Globals.show_types_verbosely")) 1210 1211(defun hol-toggle-show-numeral-types() 1212 "Toggles the global show_numeral_types variable." 1213 (interactive) 1214 (hol-toggle-var "Globals.show_numeral_types")) 1215 1216(defun hol-toggle-show-assums() 1217 "Toggles the global show_assums variable." 1218 (interactive) 1219 (hol-toggle-var "Globals.show_assums")) 1220 1221(defun hol-toggle-show-tags() 1222 "Toggles the global show_tags variable." 1223 (interactive) 1224 (hol-toggle-var "Globals.show_tags")) 1225 1226(defun hol-toggle-show-axioms() 1227 "Toggles the global show_axioms variable." 1228 (interactive) 1229 (hol-toggle-var "Globals.show_axioms")) 1230 1231(defun hol-toggle-quietdec () 1232 "Toggles quiet declarations in the interactive system." 1233 (interactive) 1234 (message "Toggling 'Quiet declaration'") 1235 (send-raw-string-to-hol 1236 (concat 1237 "val _ = print (\"*** 'Quiet declaration' now \" ^" 1238 "Bool.toString (HOL_Interactive.toggle_quietdec()) ^ \" ***\\n\")") nil nil) 1239 (hol-toggle-var "Globals.interactive")) 1240 1241(defun hol-toggle-quiet-quietdec () 1242 "Toggles quiet declarations in the interactive system." 1243 (interactive) 1244 (send-raw-string-to-hol 1245 "val _ = HOL_Interactive.toggle_quietdec()" nil nil) 1246 (hol-toggle-var-quiet "Globals.interactive")) 1247 1248(defun hol-toggle-show-times() 1249 "Toggles the elisp variable 'hol-emit-time-elapsed-p." 1250 (interactive) 1251 (setq hol-emit-time-elapsed-p (not hol-emit-time-elapsed-p)) 1252 (message (if hol-emit-time-elapsed-p "Elapsed times WILL be displayed" 1253 "Elapsed times WON'T be displayed"))) 1254 1255(defun hol-toggle-echo-commands () 1256 "Toggles the elisp variable 'hol-echo-commands-p." 1257 (interactive) 1258 (setq hol-echo-commands-p (not hol-echo-commands-p)) 1259 (message (if hol-echo-commands-p "Commands WILL be echoed" 1260 "Commands WON'T be echoed"))) 1261 1262(defun hol-toggle-auto-load () 1263 "Toggles the elisp variable 'hol-auto-load-p." 1264 (interactive) 1265 (setq hol-auto-load-p (not hol-auto-load-p)) 1266 (message (if hol-auto-load-p "automatic loading ON" 1267 "automatic loading OFF"))) 1268 1269(defun hol-toggle-ppbackend () 1270 "Toggles between using the Emacs and \"raw\" terminal pretty-printing." 1271 (interactive) 1272 (send-raw-string-to-hol 1273 (concat 1274 "val _ = if #name (!Parse.current_backend) = \"emacs_terminal\" then" 1275 "(Parse.current_backend := PPBackEnd.raw_terminal;" 1276 "print \"*** PP Backend now \\\"raw\\\" ***\\n\")" 1277 "else (Parse.current_backend := PPBackEnd.emacs_terminal;" 1278 "print \"*** PP Backend now \\\"emacs\\\" ***\\n\")") nil nil)) 1279 1280(defun hol-restart-goal () 1281 "Restarts the current goal." 1282 (interactive) 1283 (send-raw-string-to-hol "proofManagerLib.restart()" hol-echo-commands-p t)) 1284 1285(defun hol-drop-goal () 1286 "Drops the current goal." 1287 (interactive) 1288 (send-raw-string-to-hol "proofManagerLib.drop()" hol-echo-commands-p t)) 1289 1290(defun hol-open-string (prefixp) 1291 "Opens HOL modules, prompting for the name of the module to load. 1292With prefix ARG, toggles quietdec variable before and after opening, 1293potentially saving a great deal of time as tediously large modules are 1294printed out. (That's assuming that quietdec is false to start with.)" 1295 (interactive "P") 1296 (let* ((prompt0 "Name of module to (load and) open") 1297 (prompt (concat prompt0 (if prefixp " (toggling quietness)") ": ")) 1298 (module-name (read-string prompt))) 1299 (hol-load-string module-name) 1300 (if prefixp (hol-toggle-quietdec)) 1301 (send-raw-string-to-hol (concat "open " module-name) hol-echo-commands-p t) 1302 (if prefixp (hol-toggle-quietdec)))) 1303 1304(defun hol-db-match (tm) 1305 "Does a DB.match [] on the given TERM (given as a string, without quotes) and formats the result nicely." 1306 (interactive "sTerm to match on: ") 1307 (send-raw-string-to-hol (format "Hol_pp.print_match [] (Term`%s`)" tm) 1308 hol-echo-commands-p t)) 1309 1310(defun hol-db-find (tm) 1311 "Does a DB.find on the given string and formats the result nicely." 1312 (interactive "sTheorem name part: ") 1313 (send-raw-string-to-hol (format "Hol_pp.print_find \"%s\"" tm) 1314 hol-echo-commands-p t)) 1315 1316(defun hol-db-check (ty) 1317 "Does a sanity check on the current theory." 1318 (interactive "sTheory name: ") 1319 (send-raw-string-to-hol (format "Sanity.sanity_check_theory \"%s\"" ty) 1320 hol-echo-commands-p t)) 1321 1322(defun hol-db-check-current () 1323 "Does a sanity check on the current theory." 1324 (interactive) 1325 (send-raw-string-to-hol "Sanity.sanity_check()" 1326 hol-echo-commands-p t)) 1327 1328(defun hol-drop-all-goals () 1329 "Drops all HOL goals from the current proofs object." 1330 (interactive) 1331 (send-raw-string-to-hol 1332 (concat "proofManagerLib.dropn (case proofManagerLib.status() of " 1333 "Manager.PRFS l => List.length l)") nil t)) 1334 1335(defun hol-subgoal-tactic (p) 1336 "Without a prefix argument, sends term at point (delimited by backquote 1337characters) as a subgoal to prove. Will usually create at least two sub- 1338goals; one will be the term just sent, and the others will be the term sent 1339STRIP_ASSUME'd onto the assumption list of the old goal. This mimicks what 1340happens with the \"by\" command. 1341 1342With a prefix argument, sends the delimited term as if the 1343argument of a \"suffices_by\" command, making two new goals: the 1344first is to show that the new term implies the old goal, and the 1345second is to show the new term. 1346 1347(Loads the BasicProvers module if not already loaded.)" 1348 (interactive "P") 1349 (let ((tactic (if p "Tactical.Q_TAC Tactic.SUFF_TAC" 1350 "(fn q => BasicProvers.byA(q,ALL_TAC))"))) 1351 (send-string-to-hol 1352 (format "proofManagerLib.e (%s `%s`)" 1353 tactic 1354 (hol-term-at-point))))) 1355 1356 1357;; (defun hol-return-key () 1358;; "Run comint-send-input, but only if both: the user is editting the 1359;; last command in the buffer, and that command ends with a semicolon. 1360;; Otherwise, insert a newline at point." 1361;; (interactive) 1362;; (let ((comand-finished 1363;; (let ((process (get-buffer-process (current-buffer)))) 1364;; (and (not (null process)) 1365;; (let ((pmarkpos (marker-position 1366;; (process-mark process)))) 1367;; (and (< (point) pmarkpos) 1368;; (string-match ";[ \t\n\r]*$" 1369;; (buffer-substring pmarkpos 1370;; (point-max))))))))) 1371;; (if command-finished 1372;; (progn 1373;; (goto-char (point-max)) 1374;; (comint-send-input)) 1375;; (insert "\n")))) 1376 1377;; (define-key comint-mode-map "\r" 'hol-return-key) 1378 1379 1380 1381;;templates 1382(defun hol-extract-script-name (arg) 1383 "Return the name of the theory associated with the given filename" 1384(let* ( 1385 (pos (string-match "[^/]*Script\.sml" arg))) 1386 (cond (pos (substring arg pos -10)) 1387 (t "<insert theory name here>")))) 1388 1389(defun hol-template-new-script-file () 1390 "Inserts standard template for a HOL theory" 1391 (interactive) 1392 (insert "open HolKernel Parse boolLib bossLib;\n\nval _ = new_theory \"") 1393 (insert (hol-extract-script-name buffer-file-name)) 1394 (insert "\";\n\n\n\n\nval _ = export_theory();\n\n")) 1395 1396(defun hol-template-comment-star () 1397 (interactive) 1398 (insert "\n\n") 1399 (insert "(******************************************************************************)\n") 1400 (insert "(* *)\n") 1401 (insert "(* *)\n") 1402 (insert "(* *)\n") 1403 (insert "(******************************************************************************)\n")) 1404 1405(defun hol-template-comment-minus () 1406 (interactive) 1407 (insert "\n\n") 1408 (insert "(* -------------------------------------------------------------------------- *)\n") 1409 (insert "(* *)\n") 1410 (insert "(* *)\n") 1411 (insert "(* *)\n") 1412 (insert "(* -------------------------------------------------------------------------- *)\n")) 1413 1414(defun hol-template-comment-equal () 1415 (interactive) 1416 (insert "\n\n") 1417 (insert "(* ========================================================================== *)\n") 1418 (insert "(* *)\n") 1419 (insert "(* *)\n") 1420 (insert "(* *)\n") 1421 (insert "(* ========================================================================== *)\n")) 1422 1423(defun hol-template-define (name) 1424 (interactive "sNew name: ") 1425 (insert "val ") 1426 (insert name) 1427 (insert "_def = Define `") 1428 (insert name) 1429 (insert " = `;\n")) 1430 1431(defun hol-template-store-thm (name) 1432 (interactive "sTheorem name: ") 1433 (insert "val ") 1434 (insert name) 1435 (insert " = store_thm(") 1436 (cond ((> (length name) 30) (insert "\n ")) 1437 (t t)) 1438 (insert "\"") 1439 (insert name) 1440 (insert "\",\n `` ``,\n")) 1441 1442(defun hol-template-new-datatype () 1443 (interactive) 1444 (insert "val _ = Datatype `TREE = LEAF ('a -> num) | BRANCH TREE TREE`;\n")) 1445 1446;;checking for trouble with names in store_thm, save_thm, Define 1447(setq store-thm-regexp 1448 "val[ \t\n]*\\([^ \t\n]*\\)[ \t\n]*=[ \t\n]*store_thm[ \t\n]*([ \t\n]*\"\\([^\"]*\\)\"") 1449(setq save-thm-regexp 1450 "val[ \t\n]*\\([^ \t\n]*\\)[ \t\n]*=[ \t\n]*save_thm[ \t\n]*([ \t\n]*\"\\([^\"]*\\)\"") 1451(setq define-thm-regexp 1452 "val[ \t\n]*\\([^ \t\n]*\\)_def[ \t\n]*=[ \t\n]*Define[ \t\n]*`[ \t\n(]*\$?\\([^ \t\n([!?:]*\\)") 1453 1454(setq statement-eq-regexp-list (list store-thm-regexp save-thm-regexp define-thm-regexp)) 1455 1456(defun hol-correct-eqstring (s1 p1 s2 p2) 1457 (interactive) 1458 (let (choice) 1459 (setq choice 0) 1460 (while (eq choice 0) 1461 (message 1462 (concat 1463 "Different names used. Please choose one:\n(0) " 1464 s1 "\n(1) " s2 "\n(i) ignore")) 1465 (setq choice (if (fboundp 'read-char-exclusive) 1466 (read-char-exclusive) 1467 (read-char))) 1468 (cond ((= choice ?0) t) 1469 ((= choice ?1) t) 1470 ((= choice ?i) t) 1471 (t (progn (setq choice 0) (ding)))) 1472 ) 1473 (if (= choice ?i) t 1474 (let (so sr pr) 1475 (cond ((= choice ?0) (setq so s1 sr s2 pr p2)) 1476 (t (setq so s2 sr s1 pr p1))) 1477 (delete-region pr (+ pr (length sr))) 1478 (goto-char pr) 1479 (insert so) 1480 )))) 1481 1482 1483(defun hol-check-statement-eq-string () 1484 (interactive) 1485 (save-excursion 1486 (dolist (current-regexp statement-eq-regexp-list t) 1487 (goto-char 0) 1488 (let (no-error-found s1 p1 s2 p2) 1489 (while (re-search-forward current-regexp nil t) 1490 (progn (setq s1 (match-string-no-properties 1)) 1491 (setq s2 (match-string-no-properties 2)) 1492 (setq p1 (match-beginning 1)) 1493 (setq p2 (match-beginning 2)) 1494 (setq no-error-found (string= s1 s2)) 1495 (if no-error-found t (hol-correct-eqstring s1 p1 s2 p2))))) 1496 (message "checking for problematic names done")))) 1497 1498 1499;;indentation and other cleanups 1500(defun hol-replace-tabs-with-spaces () 1501 (save-excursion 1502 (goto-char (point-min)) 1503 (while (search-forward "\t" nil t) 1504 (delete-region (- (point) 1) (point)) 1505 (let* ((count (- tab-width (mod (current-column) tab-width)))) 1506 (dotimes (i count) (insert " ")))))) 1507 1508(defun hol-remove-tailing-whitespaces () 1509 (save-excursion 1510 (goto-char (point-min)) 1511 (while (re-search-forward " +$" nil t) 1512 (delete-region (match-beginning 0) (match-end 0))))) 1513 1514 1515(defun hol-remove-tailing-empty-lines () 1516 (save-excursion 1517 (goto-char (point-max)) 1518 (while (bolp) (delete-char -1)) 1519 (insert "\n"))) 1520 1521(defun hol-cleanup-buffer () 1522 (interactive) 1523 (hol-replace-tabs-with-spaces) 1524 (hol-remove-tailing-whitespaces) 1525 (hol-remove-tailing-empty-lines) 1526 (message "Buffer cleaned up!")) 1527 1528;;replace common unicode chars with ascii version 1529(setq hol-unicode-replacements '( 1530 (nil "��" "~") 1531 (nil "���" "/\\\\") 1532 (nil "���" "\\\\/") 1533 (nil "���" "==>") 1534 (nil "���" "<=>") 1535 (nil "���" "<=/=>") 1536 (nil "���" "<>") 1537 (nil "���" "?") 1538 (nil "���" "!") 1539 (nil "��" "\\\\") 1540 (nil "���" "``") 1541 (nil "���" "``") 1542 (nil "���" "`") 1543 (nil "���" "`") 1544 (t "���" "IN") 1545 (t "���" "NOTIN") 1546 (nil "��" "'a") 1547 (nil "��" "'b") 1548 (nil "��" "'c") 1549 (nil "��" "'d") 1550 (nil "��" "'e") 1551 (nil "��" "'f") 1552 (nil "��" "'g") 1553 (nil "��" "'h") 1554 (nil "��" "'i") 1555 (nil "��" "'j") 1556 (nil "��" "'l") 1557 (nil "��" "'m") 1558 (nil "��" "'n") 1559 (nil "��" "'o") 1560 (nil "��" "'p") 1561 (nil "��" "'q") 1562 (nil "��" "'r") 1563 (nil "��" "'s") 1564 (nil "��" "'t") 1565 (nil "��" "'u") 1566 (nil "��" "'v") 1567 (nil "��" "'w") 1568 (nil "��" "'x") 1569 (nil "��" "'y") 1570 (t "������" "<=+") 1571 (t ">���" ">+") 1572 (t "<���" "<+") 1573 (t "������" ">=+") 1574 (t "���" "<=") 1575 (t "���" ">=") 1576 (nil "���" "^+") 1577 (t "������" "EMPTY_REL") 1578 (t "�������" "RUNIV") 1579 (t "������" "RSUBSET") 1580 (t "������" "RUNION") 1581 (t "������" "RINTER") 1582 (t "���" "EMPTY") 1583 (t "����" "UNIV") 1584 (t "���" "SUBSET") 1585 (t "���" "UNION") 1586 (t "���" "INTER") 1587 (t "���" "??") 1588 (t "���" "||") 1589 (t "���" "<<") 1590 (t "���" ">>") 1591 (t "���" ">>>") 1592 (t "���" "#>>") 1593 (t "���" "#<<") 1594)) 1595 1596 1597(defun replace-string-in-buffer (s_old s_new) 1598 (save-excursion 1599 (goto-char (point-min)) 1600 (while (search-forward s_old nil t) 1601 (replace-match s_new)))) 1602 1603(defun replace-string-in-buffer_ensure_ws (s_old s_new) 1604 (replace-string-in-buffer (concat " " s_old " ") (concat " " s_new " ")) 1605 (replace-string-in-buffer (concat s_old " ") (concat " " s_new " ")) 1606 (replace-string-in-buffer (concat " " s_old) (concat " " s_new " ")) 1607 (replace-string-in-buffer s_old (concat " " s_new " ")) 1608) 1609 1610(defun hol-remove-unicode () 1611 (interactive) 1612 (save-excursion 1613 (save-restriction 1614 (if (use-region-p) (narrow-to-region (region-beginning) (region-end))) 1615 (dolist (elt hol-unicode-replacements) 1616 (if (nth 0 elt) 1617 (replace-string-in-buffer_ensure_ws (nth 1 elt) (nth 2 elt)) 1618 (replace-string-in-buffer (nth 1 elt) (nth 2 elt)) 1619 ))))) 1620 1621 1622;;load-path 1623(defun ml-quote (s) 1624 (let* ( 1625 (s1 (replace-regexp-in-string "\\\\" "\\\\\\\\" s)) 1626 (s2 (replace-regexp-in-string "\n" "\\\\n" s1)) 1627 (s3 (replace-regexp-in-string "\t" "\\\\t" s2)) 1628 (s4 (replace-regexp-in-string "\"" "\\\\\"" s3)) 1629 ) s4)) 1630 1631(defun hol-add-load-path (path) 1632 (interactive "DAdd new load-path: ") 1633 (let ((epath (expand-file-name path))) 1634 (if (file-accessible-directory-p epath) 1635 (progn 1636 (send-raw-string-to-hol 1637 (concat "loadPath := \"" (ml-quote epath) "\" :: !loadPath;") 1638 nil nil) 1639 (message (concat "Load-path \"" epath "\" added."))) 1640 (progn (ding) (message "Not a directory!"))) 1641)) 1642 1643 1644(defun hol-show-current-load-paths () 1645 (interactive) 1646 (send-raw-string-to-hol "print_current_load_paths ()" 1647 nil nil)) 1648 1649(defun hol-type-info () 1650 "Gives informations about the type of a term" 1651 (interactive) 1652 (let* ((txt (buffer-substring-no-properties (region-beginning) (region-end))) 1653 (use-marked (and (is-region-active) (= (count ?\` txt) 0))) 1654 (at-point-term (thing-at-point 'hol-term)) 1655 1656 (main-term (ml-quote (if use-marked txt at-point-term))) 1657 (context-term (ml-quote (if use-marked at-point-term ""))) 1658 (command-s (concat "print_type_of_in_context true " 1659 (if use-marked (concat "(SOME \"" context-term "\")") "NONE") 1660 " \"" main-term "\""))) 1661 (send-raw-string-to-hol command-s nil nil))) 1662 1663 1664(defun holpp-decode-color (code) 1665 (cond ((equal code "0") "#000000") 1666 ((equal code "1") "#840000") 1667 ((equal code "2") "#008400") 1668 ((equal code "3") "#848400") 1669 ((equal code "4") "#000084") 1670 ((equal code "5") "#840084") 1671 ((equal code "6") "#008484") 1672 ((equal code "7") "#555555") 1673 ((equal code "8") "#949494") 1674 ((equal code "9") "#FF0000") 1675 ((equal code "A") "#00C600") 1676 ((equal code "B") "#FFFF00") 1677 ((equal code "C") "#0000FF") 1678 ((equal code "D") "#FF00FF") 1679 ((equal code "E") "#00FFFF") 1680 ((equal code "F") "#FFFFFF") 1681)) 1682 1683(defun holpp-decode-full-style (style) 1684 (let* ( 1685 (fg (substring style 0 1)) 1686 (bg (substring style 1 2)) 1687 (b (substring style 2 3)) 1688 (u (substring style 3 4)) 1689 (fg-face (if (equal fg "-") nil 1690 (cons :foreground (cons (holpp-decode-color fg) ())))) 1691 (bg-face (if (equal bg "-") nil 1692 (cons :background (cons (holpp-decode-color bg) ())))) 1693 (b-face (if (equal b "-") nil 1694 (cons :weight (cons 'bold ())))) 1695 (u-face (if (equal u "-") nil 1696 (cons :underline (cons t ()))))) 1697 (cons 'face (cons (append fg-face bg-face b-face u-face) ())))) 1698 1699 1700(defun holpp-find-comment-end (n) 1701 (if (not (re-search-forward "\\((\\*(\\*(\\*\\)\\|\\(\\*)\\*)\\*)\\)" nil t 1)) 1702 nil 1703 (if (save-excursion (goto-char (- (point) 6)) 1704 (looking-at "(\\*(\\*(\\*")) 1705 (progn 1706 (holpp-find-comment-end (+ n 1))) 1707 (if (= n 1) t (holpp-find-comment-end (- n 1)))))) 1708 1709(defun holpp-execute-code-face-tooltip (start end toolprop codeface) 1710 (let ((tooltipprop 1711 (if (equal toolprop nil) nil (list 'help-echo toolprop)))) 1712 (add-text-properties start end (append codeface tooltipprop)))) 1713 1714(defun holpp-execute-code (code arg1 start end) 1715 (cond ((equal code "FV") 1716 (holpp-execute-code-face-tooltip start end arg1 1717 '(face hol-free-variable))) 1718 ((equal code "BV") 1719 (holpp-execute-code-face-tooltip start end arg1 1720 '(face hol-bound-variable))) 1721 ((equal code "TV") 1722 (holpp-execute-code-face-tooltip start end arg1 1723 '(face hol-type-variable))) 1724 ((equal code "TY") 1725 (holpp-execute-code-face-tooltip start end arg1 1726 '(face hol-type))) 1727 ((equal code "CO") 1728 (holpp-execute-code-face-tooltip start end arg1 nil)) 1729 ((equal code "ST") 1730 (add-text-properties start end 1731 (holpp-decode-full-style arg1))))) 1732 1733(setq temp-hol-output-buf nil) 1734 1735(defun holpp-quiet-reset () 1736 (let ((tmpbuf (or temp-hol-output-buf 1737 (generate-new-buffer " *HOL output filter*)")))) 1738 (setq temp-hol-output-buf tmpbuf) 1739 (save-excursion 1740 (set-buffer tmpbuf) 1741 (delete-region (point-min) (point-max))))) 1742 1743(defun holpp-reset () 1744 (interactive) 1745 (holpp-quiet-reset) 1746 (send-raw-string-to-hol "print \"\\n\\n*** hol-mode reset ***\\n\";" nil nil)) 1747 1748; this filter function is complicated by the fact that comint chunks 1749; output (in 1024 character chunks in my tests) and so doesn't 1750; necessarily give complete (in the sense of containing matching 1751; comment-blocks) strings to the filter. This means that a solution 1752; with with-temp-buffer won't work. Instead, there is a persistent 1753; working space buffer, and if the code finds a non-matching comment 1754; start (a "(*(*(*" substring), it just leaves that in the working 1755; space so that the next piece of output can be appended and processed 1756; properly. 1757(defun holpp-output-filter (s) 1758 "Converts a munged emacs_terminal string into a pretty one with text properties." 1759 (interactive "sinput: ") 1760 (let* ((tmpbuf (or temp-hol-output-buf 1761 (generate-new-buffer " *HOL output filter*)"))) 1762 end) 1763 (setq temp-hol-output-buf tmpbuf) 1764 (save-excursion 1765 (set-buffer tmpbuf) 1766 (unwind-protect 1767 (progn 1768 (goto-char (point-max)) 1769 (insert s) 1770 (goto-char (point-min)) 1771 (while (and (not end) (search-forward "(*(*(*" nil t)) 1772 (let ((uptoann (- (point) 6)) 1773 (start (point))) 1774 (if (not (holpp-find-comment-end 1)) 1775 (progn 1776 (goto-char uptoann) 1777 (setq end t)) 1778 (delete-region uptoann start) 1779 (let* 1780 ((start (- start 6)) 1781 (code (buffer-substring start (+ start 2))) 1782 (argument 1783 (save-excursion 1784 (goto-char (+ start 2)) 1785 (if (equal (following-char) 0) 1786 (progn 1787 (goto-char (+ (point) 1)) 1788 (skip-chars-forward "^\^@") 1789 (prog1 1790 (if (equal (+ start 3) (point)) nil 1791 (buffer-substring (+ start 3) 1792 (point))) 1793 (delete-region (+ start 2) (1+ (point))))) 1794 nil)))) 1795 (holpp-execute-code code argument 1796 (+ start 2) 1797 (- (point) 6)) 1798 (delete-region start (+ start 2)) 1799 (delete-region (- (point) 6) (point)) 1800 (goto-char start))))) 1801 (if (not end) 1802 (progn 1803 (goto-char (point-max)) 1804 (skip-chars-backward "(*"))) 1805 (prog1 1806 (buffer-substring (point-min) (point)) 1807 (delete-region (point-min) (point)))))))) 1808 1809(defun holmakepp-mark-error (start end) 1810 (add-text-properties start end '(face holmake-error))) 1811 1812 1813(defun holmakepp-mark-mosml-error () 1814 (interactive) 1815 (goto-char (point-min)) 1816 (while (re-search-forward "^!" nil t) 1817 (let* ((start (match-beginning 0))) 1818 (forward-line) 1819 (while (or (looking-at "!") (looking-at " ")) (forward-line)) 1820 (holmakepp-mark-error start (- (point) 1)))) 1821) 1822 1823(setq temp-holmake-output-buf nil) 1824(defun holmakepp-output-filter (s) 1825 "Converts a munged emacs_terminal string into a pretty one with text properties." 1826 (interactive "sinput: ") 1827 (let* ((tmpbuf (or temp-holmake-output-buf 1828 (generate-new-buffer " *HOLMAKE output filter*)"))) 1829 end) 1830 (setq temp-holmake-output-buf tmpbuf) 1831 (save-excursion 1832 (set-buffer tmpbuf) 1833 (unwind-protect 1834 (progn 1835 (goto-char (point-max)) 1836 (insert s) 1837 (holmakepp-mark-mosml-error) 1838 (prog1 1839 (buffer-substring (point-min) (point-max)) 1840 (delete-region (point-min) (point-max)))))))) 1841 1842(defgroup hol-faces nil "Faces used in pretty-printing HOL values" 1843 :group 'faces 1844 :group 'hol) 1845 1846(defface holmake-error 1847 '((((class color)) 1848 :foreground "red" 1849 :weight bold)) 1850 "The face for errors shown by HOLMAKE." 1851 :group 'hol-faces) 1852 1853(defface hol-free-variable 1854 '((((class color)) 1855 :foreground "blue" 1856 :weight bold)) 1857 "The face for presenting free variables in HOL terms." 1858 :group 'hol-faces) 1859 1860(defface hol-bound-variable 1861 '((((class color)) 1862 :foreground "#009900")) 1863 "The face for presenting bound variables in HOL terms." 1864 :group 'hol-faces) 1865 1866(defface hol-type-variable 1867 '((((class color)) 1868 :foreground "purple" 1869 :slant italic)) 1870 "The face for presenting free type variables in HOL terms." 1871 :group 'hol-faces) 1872 1873(defface hol-type 1874 '((((class color)) 1875 :foreground "cyan3" 1876 :slant italic)) 1877 "The face for presenting HOL types." 1878 :group 'hol-faces) 1879 1880(defun hol-region-to-unicode-pdf (filename beg end) 1881 "Print region to FILE as a PDF, handling Unicode characters." 1882 (interactive "FFile to write to: \nr") 1883 (if (and transient-mark-mode (not mark-active)) 1884 (error "No active region")) 1885 (let* ((temp-ps-file (make-temp-file "holprint" nil ".ps")) 1886 (lpr-switches 1887 (list "-font" hol-unicode-print-font-filename 1888 "-out" temp-ps-file)) 1889 (lpr-add-switches nil) 1890 (lpr-command "uniprint")) 1891 (lpr-region beg end) 1892 (shell-command (concat "ps2pdf " temp-ps-file " " filename)) 1893 (delete-file temp-ps-file))) 1894 1895;;The key combinations 1896(define-key global-map "\M-h" 'hol-map) 1897(define-prefix-command 'holpp-map) 1898(define-key hol-map "\M-p" 'holpp-map) 1899 1900 1901(define-key hol-map "\C-c" 'hol-interrupt) 1902(define-key hol-map "\C-l" 'hol-recentre) 1903(define-key hol-map "\C-q" 'hol-toggle-quietdec) 1904(define-key hol-map "\C-s" 'hol-toggle-simplifier-trace) 1905(define-key hol-map "\C-v" 'hol-scroll-up) 1906(define-key hol-map "\M-f" 'forward-hol-tactic) 1907(define-key hol-map "\M-b" 'backward-hol-tactic) 1908(define-key hol-map "\M-r" 'copy-region-as-hol-definition) 1909(define-key hol-map "\C-r" 'copy-region-as-hol-definition-quietly) 1910(define-key hol-map "\M-q" 'copy-region-as-hol-definition-real-quietly) 1911(define-key hol-map "\M-t" 'hol-toggle-show-times) 1912(define-key hol-map "\M-s" 'hol-subgoal-tactic) 1913(define-key hol-map "\M-v" 'hol-scroll-down) 1914(define-key hol-map "b" 'hol-backup) 1915(define-key hol-map "B" 'hol-user-backup) 1916(define-key hol-map "S" 'hol-user-save-backup) 1917(define-key hol-map "d" 'hol-drop-goal) 1918(define-key hol-map "D" 'hol-drop-all-goals) 1919(define-key hol-map "e" 'copy-region-as-hol-tactic) 1920(define-key hol-map "\M-e" 'hol-find-eval-next-tactic) 1921(define-key hol-map "E" 'copy-region-as-goaltree-tactic) 1922(define-key hol-map "g" 'hol-do-goal) 1923(define-key hol-map "G" 'hol-do-goaltree) 1924(define-key hol-map "h" 'hol) 1925(define-key hol-map "H" 'hol-with-region) 1926(define-key hol-map "\M-m" 'holmake) 1927(define-key hol-map "4" 'hol-display) 1928(define-key hol-map "3" 'hol-horizontal) 1929(define-key hol-map "2" 'hol-vertical) 1930(define-key hol-map "l" 'hol-load-file) 1931(define-key hol-map "m" 'hol-db-match) 1932(define-key hol-map "f" 'hol-db-find) 1933(define-key hol-map "n" 'hol-name-top-theorem) 1934(define-key hol-map "o" 'hol-open-string) 1935(define-key hol-map "p" 'hol-print-goal) 1936(define-key hol-map "P" 'hol-print-all-goals) 1937(define-key hol-map "r" 'hol-rotate) 1938(define-key hol-map "R" 'hol-restart-goal) 1939(define-key hol-map "t" 'mark-hol-tactic) 1940(define-key hol-map "T" 'hol-start-termination-proof) 1941(define-key hol-map "i" 'hol-type-info) 1942(define-key hol-map "s" 'interactive-send-string-to-hol) 1943(define-key hol-map "u" 'hol-use-file) 1944(define-key hol-map "c" 'hol-db-check-current) 1945(define-key hol-map "a" 'hol-remove-unicode) 1946(define-key hol-map "*" 'hol-template-comment-star) 1947(define-key hol-map "-" 'hol-template-comment-minus) 1948(define-key hol-map "=" 'hol-template-comment-equal) 1949(define-key hol-map "\M-d" 'hol-template-define) 1950(define-key hol-map "\M-x" 'hol-template-store-thm) 1951 1952 1953(define-key hol-map "\C-a" 'hol-toggle-show-assums) 1954(define-key holpp-map "a" 'hol-toggle-show-assums) 1955(define-key hol-map "\C-t" 'hol-toggle-show-types) 1956(define-key holpp-map "\C-t" 'hol-toggle-show-types) 1957(define-key hol-map "\C-n" 'hol-toggle-show-numeral-types) 1958(define-key holpp-map "n" 'hol-toggle-show-numeral-types) 1959(define-key hol-map "\C-f" 'hol-toggle-goalstack-fvs) 1960(define-key holpp-map "f" 'hol-toggle-goalstack-fvs) 1961(define-key hol-map "\C-o" 'hol-toggle-goalstack-print-goal-at-top) 1962(define-key holpp-map "o" 'hol-toggle-goalstack-print-goal-at-top) 1963(define-key hol-map "\M-a" 'hol-toggle-goalstack-num-assums) 1964(define-key holpp-map "\M-a" 'hol-toggle-goalstack-num-assums) 1965(define-key hol-map "\C-u" 'hol-toggle-unicode) 1966(define-key holpp-map "u" 'hol-toggle-unicode) 1967(define-key hol-map "\C-p" 'hol-toggle-ppbackend) 1968(define-key holpp-map "p" 'hol-toggle-ppbackend) 1969(define-key holpp-map "b" 'hol-toggle-emacs-tooltips) 1970(define-key holpp-map "t" 'hol-toggle-pp-annotations) 1971(define-key holpp-map "s" 'hol-toggle-pp-styles) 1972(define-key holpp-map "c" 'hol-toggle-pp-cases) 1973 1974 1975;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 1976;; The definition of the HOL menu 1977;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 1978 1979(define-key-after (lookup-key global-map [menu-bar]) 1980 [hol-menu] 1981 (cons "HOL" (make-sparse-keymap "HOL")) 1982 'tools) 1983 1984 1985;; HOL misc 1986(define-key 1987 global-map 1988 [menu-bar hol-menu hol-misc] 1989 (cons "Misc" (make-sparse-keymap "Misc"))) 1990 1991(define-key global-map [menu-bar hol-menu hol-misc clean-up] 1992 '("Clean up (remove tab, white spaces at end of line, etc...)" . 1993 hol-cleanup-buffer)) 1994 1995(define-key global-map [menu-bar hol-menu hol-misc remove-unicode] 1996 '("Replace common HOL unicode symbols" . 1997 hol-remove-unicode)) 1998 1999(define-key global-map [menu-bar hol-menu hol-misc check-names] 2000 '("Check names in store_thm, ..." . hol-check-statement-eq-string)) 2001 2002(define-key global-map [menu-bar hol-menu hol-misc sep4] 2003 '(menu-item "--")) 2004 2005(define-key global-map [menu-bar hol-menu hol-misc check-theory-current] 2006 '("Sanity check current theory" . hol-db-check-current)) 2007 2008(define-key global-map [menu-bar hol-menu hol-misc check-theory] 2009 '("Sanity check theory" . hol-db-check)) 2010 2011(define-key global-map [menu-bar hol-menu hol-misc sep3] 2012 '(menu-item "--")) 2013 2014(define-key global-map [menu-bar hol-menu hol-misc mark-tactic] 2015 '("Mark tactic" . mark-hol-tactic)) 2016 2017(define-key global-map [menu-bar hol-menu hol-misc backward-tactic] 2018 '("Move to previous tactic" . backward-hol-tactic)) 2019 2020(define-key global-map [menu-bar hol-menu hol-misc forward-tactic] 2021 '("Move to next tactic" . forward-hol-tactic)) 2022 2023(define-key global-map [menu-bar hol-menu hol-misc sep2] 2024 '(menu-item "--")) 2025 2026(define-key global-map [menu-bar hol-menu hol-misc open-string] 2027 '("Load and open" . hol-open-string)) 2028 2029(define-key global-map [menu-bar hol-menu hol-misc use-file] 2030 '("Use file" . hol-use-file)) 2031 2032(define-key global-map [menu-bar hol-menu hol-misc load-file] 2033 '("Load file" . hol-load-file)) 2034 2035(define-key global-map [menu-bar hol-menu hol-misc auto-load] 2036 '(menu-item "Automatic loading" hol-toggle-auto-load 2037 :button (:toggle 2038 . (and (boundp 'hol-auto-load-p) 2039 hol-auto-load-p)))) 2040 2041(define-key global-map [menu-bar hol-menu hol-misc show-load-paths] 2042 '("Show load-paths" . hol-show-current-load-paths)) 2043 2044(define-key global-map [menu-bar hol-menu hol-misc add-load-path] 2045 '("Add load-path ..." . hol-add-load-path)) 2046 2047(define-key global-map [menu-bar hol-menu hol-misc sep1] 2048 '(menu-item "--")) 2049 2050(define-key global-map [menu-bar hol-menu hol-misc hol-type-info] 2051 '("Type info of marked term" . hol-type-info)) 2052 2053(define-key global-map [menu-bar hol-menu hol-misc sep0] 2054 '(menu-item "--")) 2055 2056(define-key global-map [menu-bar hol-menu hol-misc db-find] 2057 '("DB find" . hol-db-find)) 2058 2059(define-key global-map [menu-bar hol-menu hol-misc db-match] 2060 '("DB match" . hol-db-match)) 2061 2062 2063 2064;; templates 2065(define-key 2066 global-map 2067 [menu-bar hol-menu hol-template] 2068 (cons "Templates" (make-sparse-keymap "Templates"))) 2069 2070(define-key global-map [menu-bar hol-menu hol-template new-script] 2071 '("New theory" . hol-template-new-script-file)) 2072 2073(define-key global-map [menu-bar hol-menu hol-template new-datatype] 2074 '("New datatype" . hol-template-new-datatype)) 2075 2076(define-key global-map [menu-bar hol-menu hol-template define] 2077 '("New definition" . hol-template-define)) 2078 2079(define-key global-map [menu-bar hol-menu hol-template store-thm] 2080 '("Store theorem" . hol-template-store-thm)) 2081 2082(define-key global-map [menu-bar hol-menu hol-template sep1] 2083 '(menu-item "--")) 2084 2085(define-key global-map [menu-bar hol-menu hol-template comment-star] 2086 '("Comment *" . hol-template-comment-star)) 2087 2088(define-key global-map [menu-bar hol-menu hol-template comment-equal] 2089 '("Comment =" . hol-template-comment-equal)) 2090 2091(define-key global-map [menu-bar hol-menu hol-template comment-minus] 2092 '("Comment -" . hol-template-comment-minus)) 2093 2094 2095;; printing 2096(define-key 2097 global-map 2098 [menu-bar hol-menu hol-printing] 2099 (cons "Printing switches" (make-sparse-keymap "Printing switches"))) 2100 2101(define-key global-map [menu-bar hol-menu hol-printing simplifier-trace] 2102 '("Simplifier trace" . hol-toggle-simplifier-trace)) 2103 2104(define-key global-map [menu-bar hol-menu hol-printing times] 2105 '("Show times" . hol-toggle-show-times)) 2106 2107(define-key global-map [menu-bar hol-menu hol-printing echo] 2108 '("Echo commands" . hol-toggle-echo-commands)) 2109 2110(define-key global-map [menu-bar hol-menu hol-printing quiet] 2111 '("Quiet (hide output except errors)" . hol-toggle-quietdec)) 2112 2113(define-key 2114 global-map 2115 [menu-bar hol-menu hol-printing backends] 2116 (cons "Pretty-printing backends" (make-sparse-keymap "Pretty-printing backends"))) 2117 2118(define-key global-map [menu-bar hol-menu hol-printing backends ppreset] 2119 '("Reset hol-mode pretty-printing (error recovery)" . holpp-reset)) 2120 2121(define-key global-map [menu-bar hol-menu hol-printing backends sep1] 2122 '(menu-item "--")) 2123 2124(define-key global-map [menu-bar hol-menu hol-printing backends ppstyles] 2125 '("Toggle use styles" . hol-toggle-pp-styles)) 2126 2127(define-key global-map [menu-bar hol-menu hol-printing backends ppannotations] 2128 '("Toggle use annotations" . hol-toggle-pp-annotations)) 2129 2130(define-key global-map [menu-bar hol-menu hol-printing backends pptooltip] 2131 '("Toggle show tooltips" . hol-toggle-emacs-tooltips)) 2132 2133(define-key global-map [menu-bar hol-menu hol-printing backends sep2] 2134 '(menu-item "--")) 2135 2136(define-key global-map [menu-bar hol-menu hol-printing backends ppbackend] 2137 '("Toggle pretty-printing backend" . hol-toggle-ppbackend)) 2138 2139(define-key global-map [menu-bar hol-menu hol-printing unicode] 2140 '("Unicode" . hol-toggle-unicode)) 2141 2142(define-key global-map [menu-bar hol-menu hol-printing ppcases] 2143 '("Toggle pretty-printing of cases" . hol-toggle-pp-cases)) 2144 2145(define-key global-map [menu-bar hol-menu hol-printing sep2] 2146 '(menu-item "--")) 2147 2148 2149(define-key global-map [menu-bar hol-menu hol-printing num-subgoals] 2150 '("Set no. of shown subgoals" . hol-toggle-goalstack-num-subgoals)) 2151 2152(define-key global-map [menu-bar hol-menu hol-printing num-assums] 2153 '("Set no. of shown assumptions" . hol-toggle-goalstack-num-assums)) 2154 2155(define-key global-map [menu-bar hol-menu hol-printing print-goal-at-top] 2156 '("Print goal at top" . hol-toggle-goalstack-print-goal-at-top)) 2157 2158(define-key global-map [menu-bar hol-menu hol-printing goal-fvs] 2159 '("Show free vars in goal" . hol-toggle-goalstack-fvs)) 2160 2161(define-key global-map [menu-bar hol-menu hol-printing sep1] 2162 '(menu-item "--")) 2163 2164 2165(define-key global-map [menu-bar hol-menu hol-printing show-assums] 2166 '("Show assumptions" . hol-toggle-show-assums)) 2167 2168(define-key global-map [menu-bar hol-menu hol-printing show-tags] 2169 '("Show tags" . hol-toggle-show-tags)) 2170 2171(define-key global-map [menu-bar hol-menu hol-printing show-axioms] 2172 '("Show axioms" . hol-toggle-show-axioms)) 2173 2174(define-key global-map [menu-bar hol-menu hol-printing show-num-types] 2175 '("Show numeral types" . hol-toggle-show-numeral-types)) 2176 2177(define-key global-map [menu-bar hol-menu hol-printing show-types-verbosely] 2178 '("Show types verbosely" . hol-toggle-show-types-verbosely)) 2179 2180(define-key global-map [menu-bar hol-menu hol-printing show-types] 2181 '("Show types" . hol-toggle-show-types)) 2182 2183 2184 2185 2186 2187;; HOL goals 2188(define-key 2189 global-map 2190 [menu-bar hol-menu hol-goalstack] 2191 (cons "Goalstack" (make-sparse-keymap "Goalstack"))) 2192 2193 2194(define-key global-map [menu-bar hol-menu hol-goalstack apply-tactic-goaltree] 2195 '("Apply tactic (goaltree)" . copy-region-as-goaltree-tactic)) 2196 2197(define-key global-map [menu-bar hol-menu hol-goalstack new-goaltree] 2198 '("New goaltree" . hol-do-goaltree)) 2199 2200(define-key global-map [menu-bar hol-menu hol-goalstack sep3] 2201 '(menu-item "--")) 2202 2203(define-key global-map [menu-bar hol-menu hol-goalstack restart-goal] 2204 '("Restart goal" . hol-restart-goal)) 2205 2206(define-key global-map [menu-bar hol-menu hol-goalstack drop-all] 2207 '("Drop all goals" . hol-drop-all-goals)) 2208 2209(define-key global-map [menu-bar hol-menu hol-goalstack drop-goal] 2210 '("Drop goal" . hol-drop-goal)) 2211 2212(define-key global-map [menu-bar hol-menu hol-goalstack sep1] 2213 '(menu-item "--")) 2214 2215(define-key global-map [menu-bar hol-menu hol-goalstack print-all] 2216 '("Print all goals" . hol-print-all-goals)) 2217 2218(define-key global-map [menu-bar hol-menu hol-goalstack print-top] 2219 '("Print goal" . hol-print-goal)) 2220 2221(define-key global-map [menu-bar hol-menu hol-goalstack sep0] 2222 '(menu-item "--")) 2223 2224(define-key global-map [menu-bar hol-menu hol-goalstack top-thm] 2225 '("Name top theorem" . hol-name-top-theorem)) 2226 2227(define-key global-map [menu-bar hol-menu hol-goalstack subgoal-tac] 2228 '("Subgoal tactic" . hol-subgoal-tactic)) 2229 2230(define-key global-map [menu-bar hol-menu hol-goalstack rotate] 2231 '("Rotate" . hol-rotate)) 2232 2233(define-key global-map [menu-bar hol-menu hol-goalstack back-up-user] 2234 '("Restore" . hol-user-backup)) 2235 2236(define-key global-map [menu-bar hol-menu hol-goalstack back-up-save-user] 2237 '("Save" . hol-user-save-backup)) 2238 2239(define-key global-map [menu-bar hol-menu hol-goalstack back-up] 2240 '("Back up" . hol-backup)) 2241 2242(define-key global-map [menu-bar hol-menu hol-goalstack apply-tactic] 2243 '("Apply tactic" . copy-region-as-hol-tactic)) 2244 2245(define-key global-map [menu-bar hol-menu hol-goalstack new-termination-goal] 2246 '("New termination goal" . hol-start-termination-proof)) 2247 2248(define-key global-map [menu-bar hol-menu hol-goalstack new-goal] 2249 '("New goal" . hol-do-goal)) 2250 2251 2252 2253;;process 2254(define-key 2255 global-map 2256 [menu-bar hol-menu hol-process] 2257 (cons "Process" (make-sparse-keymap "Process"))) 2258 2259(define-key global-map [menu-bar hol-menu hol-process hol-scroll-down] 2260 '("Scroll down" . hol-scroll-down)) 2261 2262(define-key global-map [menu-bar hol-menu hol-process hol-scroll-up] 2263 '("Scroll up" . hol-scroll-up)) 2264 2265(define-key global-map [menu-bar hol-menu hol-process hol-recentre] 2266 '("Recentre" . hol-recentre)) 2267 2268(define-key global-map [menu-bar hol-menu hol-process sep2] 2269 '(menu-item "--")) 2270 2271(define-key global-map [menu-bar hol-menu hol-process hol-send-string] 2272 '("Send string to HOL" . interactive-send-string-to-hol)) 2273 2274(define-key global-map [menu-bar hol-menu hol-process hol-send-region-quietly] 2275 '("Send region to HOL - hide non-errors" . copy-region-as-hol-definition-quietly)) 2276 2277(define-key global-map [menu-bar hol-menu hol-process hol-send-region] 2278 '("Send region to HOL" . copy-region-as-hol-definition)) 2279 2280(define-key global-map [menu-bar hol-menu hol-process sep1] 2281 '(menu-item "--")) 2282 2283(define-key global-map [menu-bar hol-menu hol-process toggle-hol-bare] 2284 '(menu-item "Use bare" hol-toggle-bare 2285 :button (:toggle 2286 . (and (boundp 'hol-bare-p) 2287 hol-bare-p)))) 2288 2289(define-key global-map [menu-bar hol-menu hol-process hol-show-info] 2290 '("Show HOL information" . hol-print-info)) 2291 2292(define-key global-map [menu-bar hol-menu hol-process hol-exe] 2293 '("Set HOL executable" . hol-set-executable)) 2294 2295(define-key global-map [menu-bar hol-menu hol-process hol-kill] 2296 '("Kill HOL" . hol-kill)) 2297 2298(define-key global-map [menu-bar hol-menu hol-process hol-interrupt] 2299 '("Interrupt HOL" . hol-interrupt)) 2300 2301(define-key global-map [menu-bar hol-menu hol-process sep02] 2302 '(menu-item "--")) 2303 2304(define-key global-map [menu-bar hol-menu hol-process holmake] 2305 '("Run Holmake" . holmake)) 2306 2307(define-key global-map [menu-bar hol-menu hol-process sep01] 2308 '(menu-item "--")) 2309 2310(define-key global-map [menu-bar hol-menu hol-process hol-display] 2311 '("Display HOL buffer" . hol-display)) 2312 2313(define-key global-map [menu-bar hol-menu hol-process hol-start-vertical] 2314 '("Start HOL - vertical split" . hol-vertical)) 2315 2316(define-key global-map [menu-bar hol-menu hol-process hol-start-horizontal] 2317 '("Start HOL - horizontal split" . hol-horizontal)) 2318 2319(define-key global-map [menu-bar hol-menu hol-process hol-start] 2320 '("Start HOL" . hol)) 2321 2322;; Support for snippet expansion, if yasnippet is installed. 2323(when (require 'yasnippet nil 'noerror) 2324 (let ((HOLsnippets 2325 (concat 2326 (string-remove-suffix "/bin/hol" hol-executable) 2327 "/tools/yasnippets" ""))) 2328 (setq yas-snippet-dirs (nconc yas-snippet-dirs (cons HOLsnippets '()))) 2329 (yas-reload-all) 2330 (define-key hol-map (kbd "TAB") 'yas-expand))) 2331 2332(when (locate-library "company-yasnippet") 2333 (load-library "company") 2334 (setq company-backends (cons 'company-yasnippet company-backends))) 2335