;;; hol-light.el --- Basic Proof General instance for HOL Light ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh ;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews ;; Portions © Copyright 2015-2017 Clément Pit-Claudel ;; Author: David Aspinall ;; Mark Adams ;;; Commentary: ;; ;; See the README file in this directory for information. ;; ;;; Code: (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps (proof-try-require 'caml-font) ; use OCaml Emacs mode syntax (eval-when-compile (require 'proof-tree)) (defcustom hol-light-home (or (getenv "HOLLIGHT_HOME") (concat (getenv "HOME") "/hol_light")) "*Directory holding the local installation of HOL Light." :type 'string :group 'hol-light) (defcustom hol-light-prog-name (or (getenv "HOLLIGHT_OCMAL") (getenv "OCAML") "ocaml") "*Name of the OCaml interpreter to launch HOL Light." :type 'string :group 'hol-light) (defcustom hol-light-use-custom-toplevel t "*If non-nil, we use a custom toplevel for Proof General. This configures extra annotations inside HOL Light to help recognise portions of output from the proof assistant. If this is incompatible with your usage of HOL Light for some reason, you can change this setting to run in a degraded (less robust) way which interfaces with the standard top level. You need to restart Emacs if you change this setting." :type 'boolean :group 'hol-light) (defconst hol-light-pre-sync-cmd (format "#use \"%shol-light/pg_prompt.ml\";; " proof-home-directory) "Command used to configure prompt annotations for Proof General.") (defcustom hol-light-init-cmd (append (list (format "#cd \"%s\"" hol-light-home) "#use \"hol.ml\"") (if hol-light-use-custom-toplevel (list (format "#use \"%shol-light/pg_tactics.ml\"" proof-home-directory)) (list "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;" "let pg_undo n = (pg_repeat n (fun ()->let _ = b() in ()); p());;" "let pg_kill() = current_goalstack:=[];;" "let pg_forget id = ();;" "let pg_restart() = print_string \"*** Session restarted.\";;"))) "*Commands used to start up a running HOL Light session." :type '(list string) :group 'hol-light) ;; ;; Regular expressions for matching output with ;; standard or custom top levels ;; (defconst hol-light-plain-start-goals-regexp (concat "^\\(val it : x?goalstack = \\)" "\\(?:.+\n\\)*" "\\(?:[0-9]*[0-9] subgoals? ([0-9]+ total)\\|No subgoals\\)") "Value for `proof-shell-start-goals-regexp' with standard top level.") (defconst hol-light-annotated-start-goals-regexp hol-light-plain-start-goals-regexp "Value for `proof-shell-start-goals-regexp' with custom top level.") (defconst hol-light-plain-interrupt-regexp "Interrupted" "Value for `proof-shell-interrupt-regexp' with standard top level.") (defconst hol-light-annotated-interrupt-regexp hol-light-plain-interrupt-regexp ;; TODO "Value for `proof-shell-interrupt-regexp' with custom top level.") (defconst hol-light-plain-prompt-regexp "\\(val it : unit = ()\n\\)?^# " "Value for `proof-shell-annotated-prompt-regexp' with standard top level.") (defconst hol-light-annotated-prompt-regexp "\\(val it : unit = ()\n\\)?.*" "Value for `proof-shell-annotated-prompt-regexp' with custom top level.") (defconst hol-light-plain-error-regexp (proof-regexp-alt "Characters [0-9]+-[0-9]+:" "^Exception: Failure" "^Parse error: " "^Cannot find file" "^Error: Unbound value" "^Error: Syntax error" ;; TODO: more here ) "Value for `proof-shell-error-regexp' with standard top level.") (defconst hol-light-annotated-error-regexp ;; ".+" ;; unfortunately not enough, this is only for failwith hol-light-plain-error-regexp "Value for `proof-shell-error-regexp' with custom top level.") (defconst hol-light-plain-proof-completed-regexp "Initial goal proved" "Value for `proof-shell-proof-completed-regexp' with standard top level.") (defconst hol-light-annotated-proof-completed-regexp hol-light-plain-proof-completed-regexp ;; TODO "Value for `proof-shell-proof-completed-regexp' with standard top level.") (defconst hol-light-plain-message-start "^Warning \\|\\*\*\\*" "Value for `proof-shell-eager-annotation-start' with standard top level.") (defconst hol-light-annotated-message-start "^Warning \\|\\*\\*\\*" ;; TODO "Value for `proof-shell-eager-annotation-start' with custom top level.") (defconst hol-light-plain-message-end "\n" ;; TODO "Value for `proof-shell-eager-annotation-start' with standard top level.") (defconst hol-light-annotated-message-end "\n" ;; TODO "Value for `proof-shell-eager-annotation-start' with custom top level.") ;;; ;;; State ;;; (defvar hol-light-keywords nil) (defvar hol-light-rules nil) (defvar hol-light-tactics nil) (defvar hol-light-tacticals nil) ;;; ;;; Main configuration ;;; (proof-easy-config 'hol-light "HOL Light" proof-assistant-home-page "https://www.cl.cam.ac.uk/~jrh13/hol-light/" proof-prog-name hol-light-prog-name proof-terminal-string ";;" proof-shell-pre-sync-init-cmd hol-light-pre-sync-cmd proof-shell-init-cmd hol-light-init-cmd ;; Regexps for matching tactic script inputs: all approximations, of course. proof-goal-command-regexp "^g[ `]" proof-save-command-regexp "top_thm()" 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 "pg_kill();;" proof-undo-n-times-cmd "pg_undo %s;;" proof-forget-id-command "pg_forget \"%s\";;" proof-shell-restart-cmd "pg_restart();;" proof-showproof-command "p();;" proof-auto-multiple-files t proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) proof-shell-annotated-prompt-regexp (if hol-light-use-custom-toplevel hol-light-annotated-prompt-regexp hol-light-plain-prompt-regexp) proof-shell-interrupt-regexp (if hol-light-use-custom-toplevel hol-light-annotated-interrupt-regexp hol-light-plain-interrupt-regexp) proof-shell-start-goals-regexp (if hol-light-use-custom-toplevel hol-light-annotated-start-goals-regexp hol-light-plain-start-goals-regexp) proof-shell-error-regexp (if hol-light-use-custom-toplevel hol-light-annotated-error-regexp hol-light-plain-error-regexp) proof-shell-proof-completed-regexp (if hol-light-use-custom-toplevel hol-light-annotated-proof-completed-regexp hol-light-plain-proof-completed-regexp) proof-shell-eager-annotation-start (if hol-light-use-custom-toplevel hol-light-annotated-message-start hol-light-plain-message-start) proof-shell-eager-annotation-end (if hol-light-use-custom-toplevel hol-light-annotated-message-end hol-light-plain-message-end) ;; FIXME: add optional help topic parameter to help command. proof-info-command "help \"hol\"" ;; 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);;" ;; ;; Syntax and syntax table entries for proof scripts ;; proof-script-comment-start "(*" proof-script-comment-end "*)" 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" "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" "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 (append (bound-and-true-p caml-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\\|$\\)")) (defconst hol-light-current-goal-regexp ;; match final (focused) subgoal. (concat (regexp-quote "[*]") "\\[Goal ID \\([0-9]+\\)\\]" "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")) (defconst hol-light-additional-subgoal-regexp "\\[New Goal IDs: \\([0-9 ]+\\)\\]" "HOL Light instance of `proof-tree-additional-subgoal-ID-regexp'.") (defconst hol-light-statenumber-regexp "\\([0-9]+\\)|\\([0-9]+\\)" "Regular expression to match prompt with state numbers. The first number is a global state counter which increases with processed steps. The second number is the number of steps within the currently open proof.") (defconst hol-light-existential-regexp "\\(\\?[0-9]+\\)" "Regexp for `proof-tree-existential-regexp'.") (defconst hol-light-existentials-state-start-regexp "^(dependent evars:" "HOL Light instance of `proof-tree-existentials-state-start-regexp'.") (defconst hol-light-existentials-state-end-regexp ")\n" "HOL Light instance of `proof-tree-existentials-state-end-regexp'.") (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-branch-finished-regexp "No subgoals" proof-tree-show-sequent-command (lambda (id) (format "print_xgoal_of_id \"%s\";;" id)) proof-tree-current-goal-regexp hol-light-current-goal-regexp proof-tree-additional-subgoal-ID-regexp hol-light-additional-subgoal-regexp proof-tree-update-goal-regexp hol-light-update-goal-regexp proof-tree-cheating-regexp "CHEAT_TAC" ;; others... proof-tree-existential-regexp hol-light-existential-regexp proof-tree-existentials-state-start-regexp hol-light-existentials-state-start-regexp proof-tree-existentials-state-end-regexp hol-light-existentials-state-end-regexp ) ;; 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? ;; TEMP to fix compile. Will use Coq-stype annotated prompt for proof tree now. (defvar proof-shell-delayed-output-start nil) (defvar proof-shell-delayed-output-end nil) (defvar proof-info nil) (defvar proof-action-list nil) (defun proof-shell-action-list-item (&rest args)) (defconst hol-light-show-sequent-command "print_xgoal_of_id %s;;") (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 "Goal")) ; no named goals (when (and t ; (> proof-nesting-depth 0) ; inside a proof (string-match hol-light-statenumber-regexp proof-shell-last-prompt)) (setq proof-state-number (string-to-number (match-string 1 proof-shell-last-prompt)))) (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 "^g" 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 (format 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) ;;; ;;; Menu commands ;;; (proof-definvisible hol-light-dump-proof "dump_proof();;") (defpgdefault menu-entries '(["Dump refactored proof" hol-light-dump-proof t])) (provide 'hol-light)