path: root/hol-light/hol-light.el

;; hol-light.el   Basic Proof General instance for HOL Light
;;
;; Copyright (C) 2010-12 LFCS Edinburgh, David Aspinall.
;;
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;;         Mark Adams <mark@proof-technologies.com>
;;
;; $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)