;; hol-light.el Basic Proof General instance for HOL Light ;; ;; Copyright (C) 2010-12 LFCS Edinburgh, David Aspinall. ;; ;; Author: David Aspinall ;; Mark Adams ;; ;; $Id$ ;; ;; See the README file in this directory for information. ;; (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps (defcustom hol-light-home "/home/da/hol_light" "*Directory holding the local installation of HOL Light." :type 'string :group 'hol-light) (defcustom hol-light-startup-cmds (list (format "#cd \"%s\"" hol-light-home) "#use \"hol.ml\"" (format "#cd \"%s\"" proof-home-directory) "#use \"pt_tactics.ml\"") "*Commands used to start up a running HOL Light session." :type '(list string) :group 'hol-light) (defvar hol-light-keywords nil) (defvar hol-light-rules nil) (defvar hol-light-tactics nil) (defvar hol-light-tacticals nil) (proof-easy-config 'hol-light "HOL Light" proof-assistant-home-page "https://www.cl.cam.ac.uk/~jrh13/hol-light/" proof-prog-name "ocaml" proof-terminal-string ";;" proof-script-comment-start "(*" proof-script-comment-end "*)" ;; These are all approximations, of course. proof-goal-command-regexp "^g[ `]" proof-save-command-regexp "pg_top_thm_and_drop" proof-goal-with-hole-regexp "let \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*prove" proof-save-with-hole-regexp "let \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*top_thm()" proof-non-undoables-regexp "b()" ; and others.. proof-goal-command "g `%s`;;" proof-save-command "val %s = top_thm();;" proof-kill-goal-command "current_goalstack:=[];;" ; for cleanliness proof-showproof-command "p()" proof-undo-n-times-cmd "(pg_repeat b %s; p());;" proof-auto-multiple-files t proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) proof-shell-interrupt-regexp "Interrupted" proof-shell-start-goals-regexp (setq proof-shell-start-goals-regexp (concat "^\\(val it : x?goalstack = \\)" "\\(?:.+\n\\)*" "\\(?:[0-9]*[0-9] subgoals? ([0-9]+ total)\\|No subgoals\\)") ) proof-shell-annotated-prompt-regexp "^# " proof-shell-error-regexp (proof-regexp-alt "Characters [0-9]+-[0-9]+:" "Exception: Failure" "Parse error: ") proof-shell-init-cmd (append hol-light-startup-cmds '("let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1))" "let pg_top_thm_and_drop () = let t = top_thm() in ((let _ = b() in ()); t)")) ;; FIXME: add optional help topic parameter to help command. proof-info-command "help \"hol\"" proof-shell-proof-completed-regexp "Initial goal proved" ;; FIXME: next one needs setting so that "urgent" messages are displayed ;; eagerly from HOL. ;; proof-shell-eager-annotation-start proof-find-theorems-command "DB.match [] (%s);;" proof-forget-id-command "();;" ;; candidate for making nil, change generic ;; We must force this to use ptys since mosml doesn't flush its output ;; (on Linux, presumably on Solaris too). proof-shell-process-connection-type t ;; ;; Syntax table entries for proof scripts ;; proof-script-syntax-table-entries '(?\` "\"" ?\$ "." ?\/ "." ?\\ "." ?+ "." ?- "." ?= "." ?% "." ?< "." ?> "." ?\& "." ?. "w" ?_ "w" ?\' "w" ?\| "." ?\* ". 23n" ?\( "()1" ?\) ")(4") ;; ;; A few of the vast variety of keywords, tactics, tacticals, ;; for decorating proof scripts. ;; ;; In the future, PG will use a mechanism for passing identifier ;; lists like this from the proof assistant, we don't really ;; want to duplicate all this information here! ;; hol-light-keywords '("g" "expand" "e" "let" "store_thm" "top_thm" "by" "Define" "xDefine" "Hol_defn" "Induct" "Cases" "Cases_on" "Induct_on" "std_ss" "arith_ss" "list_ss" "define_type") hol-light-rules '("REFL" "TRANS" "MK_COMB" "ABS" "BETA" "BETA_CONV" "ASSUME" "EQ_MP" "DEDUCT_ANTISYM_RULE" "INST_TYPE" "INST" "TRUTH" "CONJ" "CONJUNCT1" "CONJUNCT2" "PINST" "PROVE_HYP" "T_DEF" "TRUTH" "EQT_ELIM" "EQT_INTRO" "AND_DEF" "CONJ" "CONJUNCT1" "CONJUNCT2" "CONJ_PAIR" "CONJUNCTS" "IMP_DEF" "MP" "DISCH" "DISCH_ALL" "UNDISCH" "UNDISCH_ALL" "IMP_ANTISYM_RULE" "ADD_ASSUM" "EQ_IMP_RULE" "IMP_TRANS" "FORALL_DEF" "SPEC" "SPECL" "SPEC_VAR" "SPEC_ALL" "ISPEC" "ISPECL" "GEN" "GENL" "GEN_ALL th" "EXISTS_DEF" "EXISTS" "SIMPLE_EXISTS" "CHOOSE" "SIMPLE_CHOOSE" "OR_DEF" "DISJ1" "DISJ2" "DISJ_CASES" "SIMPLE_DISJ_CASES" "F_DEF" "NOT_DEF" "NOT_ELIM" "NOT_INTRO" "EQF_INTRO" "EQF_ELIM" "CONTR" "EXISTS_UNIQUE_DEF" "EXISTENCE" "EQ_REFL" "REFL_CLAUSE" "EQ_SYM" "EQ_SYM_EQ" "EQ_TRANS" "AC" "BETA_THM" "ABS_SIMP" "CONJ_ASSOC" "CONJ_SYM" "CONJ_ACI" "DISJ_ASSOC" "DISJ_SYM" "DISJ_ACI" "IMP_CONJ" "IMP_IMP" "IMP_CONJ_ALT" "LEFT_OR_DISTRIB" "RIGHT_OR_DISTRIB" "FORALL_SIMP" "EXISTS_SIMP" "EQ_IMP" "EQ_CLAUSES" "NOT_CLAUSES_WEAK" "AND_CLAUSES" "OR_CLAUSES" "IMP_CLAUSES" "IMP_EQ_CLAUSE" "EXISTS_UNIQUE_THM" "EXISTS_REFL" "EXISTS_UNIQUE_REFL" "UNWIND_THM1" "UNWIND_THM2" "FORALL_UNWIND_THM2" "FORALL_UNWIND_THM1" "SWAP_FORALL_THM" "SWAP_EXISTS_THM" "FORALL_AND_THM" "AND_FORALL_THM" "LEFT_AND_FORALL_THM" "RIGHT_AND_FORALL_THM" "EXISTS_OR_THM" "OR_EXISTS_THM" "LEFT_OR_EXISTS_THM" "RIGHT_OR_EXISTS_THM" "LEFT_EXISTS_AND_THM" "RIGHT_EXISTS_AND_THM" "TRIV_EXISTS_AND_THM" "LEFT_AND_EXISTS_THM" "RIGHT_AND_EXISTS_THM" "TRIV_AND_EXISTS_THM" "TRIV_FORALL_OR_THM" "TRIV_OR_FORALL_THM" "RIGHT_IMP_FORALL_THM" "RIGHT_FORALL_IMP_THM" "LEFT_IMP_EXISTS_THM" "LEFT_FORALL_IMP_THM" "TRIV_FORALL_IMP_THM" "TRIV_EXISTS_IMP_THM" "EXISTS_UNIQUE_ALT" "EXISTS_UNIQUE") hol-light-tactics '("ABS_TAC" "ACCEPT_TAC" "ALL_TAC" "ANTS_TAC" "AP_TERM_TAC" "AP_THM_TAC" "ASSUME_TAC" "BETA_TAC" "BINOP_TAC" "CHANGED_TAC" "CHEAT_TAC" "CHOOSE_TAC" "CONJ_TAC" "CONTR_TAC" "CONV_TAC" "DISCARD_TAC" "DISCH_TAC" "DISJ1_TAC" "DISJ2_TAC" "DISJ_CASES_TAC" "EQ_TAC" "EXISTS_TAC" "FAIL_TAC" "GEN_TAC" "LABEL_TAC" "MATCH_ACCEPT_TAC" "MATCH_MP_TAC " "META_EXISTS_TAC" "META_SPEC_TAC" "MK_COMB_TAC" "MP_TAC" "NO_TAC" "RECALL_ACCEPT_TAC" "REFL_TAC" "REPLICATE_TAC" "RULE_ASSUM_TAC " "SPEC_TAC" "STRIP_ASSUME_TAC" "STRIP_GOAL_THEN" "STRIP_TAC" "STRUCT_CASES_TAC" "SUBGOAL_TAC" "SUBST1_TAC" "SUBST_ALL_TAC" "SUBST_VAR_TAC" "UNDISCH_TAC" "X_CHOOSE_TAC" "X_GEN_TAC" "X_META_EXISTS_TAC") hol-light-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN" "THENL" "EVERY" "REPEAT" "MAP_EVERY" "IMP_RES_THEN" "FIND_ASSUM" "POP_ASSUM" "ASSUM_LIST" "EVERY_ASSUM" "FIRST_ASSUM" "CONJUCTS_THEN" "DISJ_CASES_THEN" "DISCH_THEN" "X_CHOOSE_THEN" "MAP_EVERY" "CHOOSE_THEN" "STRIP_THM_THEN" "SUBGOAL_THEN" "FREEZE_THEN") proof-script-font-lock-keywords (list (cons (proof-ids-to-regexp hol-light-keywords) 'font-lock-keyword-face) (cons (proof-ids-to-regexp hol-light-tactics) 'proof-tactics-name-face) (cons (proof-ids-to-regexp hol-light-rules) 'font-lock-keyword-face) (cons (proof-ids-to-regexp hol-light-tacticals) 'proof-tacticals-name-face)) ;; ;; Some decoration of the goals output [FIXME: not yet HOL Light] ;; proof-goals-font-lock-keywords (list (cons (proof-ids-to-regexp '("Proof manager status" "proof" "Incomplete" "Initial goal proved" "Initial goal" "There are currently no proofs" "OK")) 'font-lock-keyword-face) (cons (regexp-quote "------------------------------------") 'font-lock-comment-face) (cons ": GoalstackPure.goalstack" 'proof-boring-face) (cons ": GoalstackPure.proofs" 'proof-boring-face) (cons ": Thm.thm" 'proof-boring-face) (cons "val it =" 'proof-boring-face)) ;; ;; Some decoration of the response output ;; proof-goals-font-lock-keywords (setq proof-goals-font-lock-keywords (list ;; Help system output (cons (proof-ids-to-regexp '("^----------[-]+$" "SYNOPSIS" "DESCRIPTION" "FAILURE CONDITIONS" "EXAMPLES" "SEE ALSO")) 'font-lock-keyword-face) (cons ": GoalstackPure.goalstack" 'proof-boring-face) (cons ": GoalstackPure.proofs" 'proof-boring-face) (cons ": Thm.thm" 'proof-boring-face) (cons "val it =" 'proof-boring-face))) ;; End of easy config. ) ;;; Prooftree configuration (experimental, ongoing) ;; ;; regexps for recognising additional markup in output (defvar hol-light-update-goal-regexp (concat "\\[Goal ID \\([0-9]+\\)\\]" "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")) (defvar hol-light-current-goal-regexp ;; match final (focused) subgoal (concat (regexp-quote "[*]") "\\[Goal ID \\([0-9]+\\)\\]" "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")) (defvar hol-light-newgoals-match "\\[New Goal IDs: \\([0-9 ]+\\)\\]") (defvar hol-light-statenumber-match "\\[State Counter \\([0-9]+\\)\\]") (setq ;; These ones belong in script mode config proof-tree-configured t proof-tree-get-proof-info 'hol-light-get-proof-info proof-tree-find-begin-of-unfinished-proof 'hol-light-find-begin-of-unfinished-proof ;; These ones belong in shell mode proof-tree-proof-finished-regexp "No subgoals" proof-tree-show-sequent-command (lambda (id) (format "print_xgoal_of_id \\"%s\\";;" id)) proof-tree-update-goal-regexp hol-light-update-goal-regexp proof-tree-cheating-regexp "CHEAT_TAC" ;; others... ) ;; end setq proof tree stuff ;;; get proof info: uses last goals output ;;; FIXME problem here: this is called BEFORE last goals output ;;; is set. Can we move order without harming Coq? (defun hol-light-get-proof-info () "Return proof info for Prooftree for HOL Light. See `proof-tree-get-proof-info'." (let ((proof-state-number 0) proof-name) (when (and (> 0 proof-nesting-depth) ; inside a proof (string-match hol-light-statenumber-match proof-shell-last-goals-output)) (setq proof-state-number (string-to-int (match-string 1 proof-shell-last-goals-output)))) (list proof-state-number proof-name))) (defun hol-light-find-begin-of-unfinished-proof () ;; Quick hack, we should use some internal proof script stuff here (save-excursion (re-search-backward "^xg" nil t))) ;;; FIXME: this is duplicated from coq.el. It might be kind of generic. ;;; However, for HOL Light the default behaviour is actually to print out ;;; exactly the new subgoals arising from a previous tactic allocation, ;;; or the currently focused goal (top of stack). (defun hol-light-proof-tree-get-new-subgoals () "Check for new subgoals and issue appropriate Show commands. This is a hook function for `proof-tree-urgent-action-hook'. This function examines the current goal output and searches for new unknown subgoals. Those subgoals have been generated by the last proof command and we must send their complete sequent text eventually to prooftree. Because subgoals may change with the next proof command, we must execute the additionally needed Show commands before the next real proof command. The ID's of the open goals are checked with `proof-tree-sequent-hash' in order to find out if they are new. For any new goal an appropriate Show Goal command with a 'proof-tree-show-subgoal flag is inserted into `proof-action-list'. Then, in the normal delayed output processing, the sequent text is send to prooftree as a sequent update (see `proof-tree-update-sequent') and the ID of the sequent is registered as known in `proof-tree-sequent-hash'. The not yet delayed output is in the region \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." ;; (message "CPTGNS start %s end %s" ;; proof-shell-delayed-output-start ;; proof-shell-delayed-output-end) (with-current-buffer proof-shell-buffer (let ((start proof-shell-delayed-output-start) (end proof-shell-delayed-output-end)) (goto-char start) (while (proof-re-search-forward hol-light-update-goal-regexp end t) (let ((subgoal-id (match-string-no-properties 1))) (unless (gethash subgoal-id proof-tree-sequent-hash) (setq proof-action-list (cons (proof-shell-action-list-item (hol-light-show-sequent-command subgoal-id) (proof-tree-make-show-goal-callback (car proof-info)) '(no-goals-display no-response-display proof-tree-show-subgoal)) proof-action-list)))))))) (add-hook 'proof-tree-urgent-action-hook 'hol-light-proof-tree-get-new-subgoals) (warn "Hol Light Proof General is incomplete! Please help improve it! Read the manual, make improvements, upload at http://proofgeneral.inf.ed.ac.uk/trac") (provide 'hol-light)