blob: 31fb1b3a0a820fc98c857e1e58dd5290755d8bde (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
|
;; hol98.el Basic Proof General instance for HOL 98
;;
;; Copyright (C) 2000 LFCS Edinburgh.
;;
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; Needs improvement!
;;
;; See the README file in this directory for information.
(require 'proof-easy-config) ; easy configure mechanism
(require 'proof-syntax) ; functions for making regexps
(proof-easy-config 'hol98 "HOL"
proof-prog-name "hol.unquote"
proof-terminal-char ?\;
proof-comment-start "(*"
proof-comment-end "*)"
proof-goal-command-regexp "^g[ `]"
proof-save-command-regexp "^val .*top_thm()"
;; FIXME: next two just to suppress warnings, not set yet.
proof-goal-with-hole-regexp "^\0\1$"
proof-save-with-hol-regexp "^\0\1$"
;; proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\""
;; proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\""
proof-non-undoables-regexp "b()"
proof-goal-command "g `%s`;"
proof-save-command "val %s = top_thm(); drop();"
proof-kill-goal-command "drop();"
proof-showproof-command "p()"
proof-undo-n-times-cmd "(pg_repeat backup %s; p());"
proof-auto-multiple-files t
proof-shell-cd-cmd "FileSys.chDir \"%s\""
proof-shell-prompt-pattern "^[->] "
proof-shell-interrupt-regexp "Interrupted"
proof-shell-start-goals-regexp
(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-shell-annotated-prompt-regexp
"^\\(> val it = () : unit\n\\)?- "
proof-shell-error-regexp "^! "
proof-shell-init-cmd
"Help.displayLines:=3000;
fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"
;; FIXME: add optional help topic parameter to help command.
;; Have patch ready for PG 3.2, but PG 3.1 is strictly bug fix.
proof-info-command "help \"hol\""
proof-shell-proof-completed-regexp
"\\(\\(.\\|\n\\)*No subgoals!\n\\)"
;; FIXME: next one needs setting.
;; proof-shell-eager-annotation-start
proof-find-theorems-command "DB.match [] (%s);"
;; We must set 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"
?\| "."
?\* ". 23"
?\( "()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 the information here!
;;
hol98-keywords '("g" "expand" "e" "val" "store_thm" "top_thm" "by"
"Define" "xDefine" "Hol_defn"
"Induct" "Cases" "Cases_on" "Induct_on"
"std_ss" "arith_ss" "list_ss"
"define_type")
hol98-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")
hol98-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")
hol98-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN"
"THENL" "EVERY" "REPEAT"
"MAP_EVERY")
proof-script-font-lock-keywords
(list
(cons (proof-ids-to-regexp hol98-keywords) 'font-lock-keyword-face)
(cons (proof-ids-to-regexp hol98-tactics) 'font-lock-keyword-face)
; (cons (proof-ids-to-regexp hol98-rules) 'font-lock-keyword-face)
(cons (proof-ids-to-regexp hol98-tacticals) 'proof-tacticals-name-face))
;;
;; Some decoration of the goals output
;;
proof-goals-font-lock-keywords
(list
(cons (proof-ids-to-regexp '("Proof manager status"
"proof" "Incomplete"
"Initial goal"))
'font-lock-keyword-face))
;; End of easy config.
)
(warn "Hol Proof General is incomplete! Please help improve it!
Read the manual, make improvements and send them to proofgen@dcs.ed.ac.uk")
(provide 'hol98)
|
