diff options
| -rw-r--r-- | hol-light/hol-light.el | 137 |
1 files changed, 92 insertions, 45 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 9b662038..c2fc60b5 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -1,6 +1,6 @@ ;; hol-light.el Basic Proof General instance for HOL Light ;; -;; Copyright (C) 2010 LFCS Edinburgh, David Aspinall. +;; Copyright (C) 2010-12 LFCS Edinburgh, David Aspinall. ;; ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; @@ -20,10 +20,10 @@ (defvar hol-light-tacticals nil) (proof-easy-config 'hol-light "HOL Light" - proof-prog-name "ocaml" + proof-prog-name "/usr/local/bin/ocaml" ;; std: "ocaml" proof-terminal-string ";;" - proof-script-comment-start "(*" - proof-script-comment-end "*)" + 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" @@ -32,32 +32,29 @@ proof-non-undoables-regexp "b()" ; and others.. proof-goal-command "g `%s`;;" proof-save-command "val %s = pg_top_thm_and_drop();;" - proof-kill-goal-command "drop();;" + proof-kill-goal-command "print_string \"Goal killed.\";;" ; nothing to do, repeated goals OK proof-showproof-command "p()" - proof-undo-n-times-cmd "(pg_repeat backup %s; p());;" + proof-undo-n-times-cmd "(pg_repeat b %s; p());;" proof-auto-multiple-files t - proof-shell-cd-cmd "#cd \"%s\"" + proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) proof-shell-interrupt-regexp "Interrupted" proof-shell-start-goals-regexp - (proof-regexp-alt "Proof manager status" - "OK.." - "val it =\n") + (regexp-quote "val it : goalstack = ") +; (proof-regexp-alt "Proof manager status" +; "OK.." +; "val it =\n") proof-shell-end-goals-regexp (proof-regexp-alt "^[ \t]*: GoalstackPure.goalstack" "^[ \t]*: GoalstackPure.proofs") - proof-shell-quit-cmd "quit();" - proof-assistant-home-page - "http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html" + proof-assistant-home-page "https://www.cl.cam.ac.uk/~jrh13/hol-light/" proof-shell-annotated-prompt-regexp "# " - ;; This one is nice but less reliable, I think. - ;; "\\(> val it = () : unit\n\\)?- " proof-shell-error-regexp "Characters [0-9]+-[0-9]+:" - proof-shell-init-cmd + proof-shell-init-cmd '("#cd \"/Users/da/hol_light\"" "#use \"hol.ml\"" - "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 (b(); t);;") + "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\"" @@ -92,7 +89,7 @@ ?_ "w" ?\' "w" ?\| "." - ?\* ". 23" + ?\* ". 23n" ?\( "()1" ?\) ")(4") @@ -102,40 +99,72 @@ ;; ;; 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 the information here! + ;; 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 '("ASSUME" "REFL" "BETA_CONV" "SUBST" - "ABS" "INST_TYPE" "DISCH" "MP" - "T_DEF" "FORALL_DEF" "AND_DEF" "OR_DEF" "F_DEF" - "NOT_DEF" "EXISTS_UNIQUE_DEF" "BOOL_CASES_AX" - "IMP_ANTISYM_AX" "ETA_AX" "SELECT_AX" "ONE_ONE_DEF" - "ONTO_DEF" "INFINITY_AX" "LET_DEF" "COND_DEF" "ARB_DEF") - hol-light-tactics '("ACCEPT_TAC" "ASSUME_TAC" "GEN_TAC" - "CONJ_TAC" "DISCH_TAC" "STRIP_TAC" - "SUBST_TAC" "ASM_CASES_TAC" "DISJ_CASES_TAC" - "REWRITE_TAC" "IMP_RES_TAC" "ALL_TAC" "NO_TAC" - "EQ_TAC" "EXISTS_TAC" "INDUCT_TAC" - "POP_ASM" "SUBST1_TAC" "ASSUM_LIST" - "PROVE" "PROVE_TAC" "DECIDE" "DECIDE_TAC" "RW_TAC" - "STP_TAC" "ZAP_TAC" - "EXISTS_TAC") - hol-light-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN" - "THENL" "EVERY" "REPEAT" - "MAP_EVERY") + "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) 'font-lock-keyword-face) - ; (cons (proof-ids-to-regexp hol-light-rules) '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 + ;; Some decoration of the goals output [FIXME: not yet HOL Light] ;; proof-goals-font-lock-keywords (list @@ -153,6 +182,24 @@ (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. ) |