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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
;; pg-pgip.el Functions for processing PGIP for Proof General
;;
;; Copyright (C) 2000-2002 LFCS Edinburgh.
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;; STATUS: Experimental
;;
;; Proof General Kit uses PGIP, an XML-message protocol
;; for interactive proof. This file contains functions
;; to process PGIP commands sent from the proof assistant.
;;
;; Halt on errors during development: later may accumulate and ignore.
(defalias 'pg-pgip-error 'error)
;;;###autoload
(defun pg-pgip-process-packet (pgip)
"Process the command packet PGIP, which is parsed XML according to pg-xml-parse-*"
;; PGIP processing is split into two steps:
;; (1) process each command, altering internal data structures
;; (2) post-process for each command type, affecting external interface (menus, etc).
(mapcar 'pg-pgip-post-process
(pg-pgip-process-cmds pgip)))
(defun pg-pgip-process-cmds (pgips)
"Process the command(s) in PGIP, returning list of command symbols processed."
(let (cmdtys)
(while pgips
(let* ((pgip (car pgips))
(elt (or (car-safe (car pgip)) ; normalise to symbol
(car pgip)))
(attr (cdr-safe (car pgip)))
(attrs (and attr (if (listp (cdr attr)) ; normalise to list
attr (list attr))))
(body (cdr pgip)))
(add-to-list 'cmdtys elt)
(cond
;; <pgip>
((eq elt 'pgip)) ;; ignore pgip attributes for now
;; <usespgml>
((eq elt 'usespgml)
(proof-debug "Received usespgml message, version %s"
(pg-pgip-get-version "usespgml" attrs)))
;; <haspref>
((eq elt 'haspref)
(pg-pgip-haspref attrs (car-safe body)))
;; <prefval>
((eq elt 'prefval)
)
;; <idtable>
((eq elt 'idtable)
)
;; <addid>
((eq elt 'addid)
)
;; <delid>
((eq elt 'delid)
)
;; <menuadd>
((eq elt 'menuadd)
)
((eq elt 'menudel)
))
;; Move on to next element
(setq pgips (cdr pgips))))
;; Return list of command types processed.
cmdtys))
(defun pg-pgip-post-process (pgip)
"Perform post-processing for a PGIP command type PGIP-ELT."
(cond
((eq pgip 'pgip))
((eq pgip 'usespgml))
((or
(eq pgip 'haspref)
(eq pgip 'prefval))
;; Update preferences view/menu
(proof-assistant-menu-update))
((or
(eq pgip 'idtable)
(eq pgip 'addid)
(eq pgip 'delid))
;; Update completion tables/view
)
((or
(eq pgip 'menuadd)
(eq pgip 'menudel))
;; Update menus
)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; <haspref default="d" kind="k" description="d" class="c">name</haspref>
;;
(defun pg-pgip-haspref (attrs name)
"Issue a defpacustom from a <haspref> element with attributes ATTRS, name NAME."
(unless (stringp name)
(pg-pgip-error "pg-pgip-haspref: missing NAME in <haspref>NAME</haspref>."))
(let*
((type (pg-pgip-get-type attrs))
(default (or (pg-pgip-get-attr "haspref" 'default attrs t)
;; If no default is supplied, make one
;; [NB: boolean default is nil anyway]
(pg-pgip-default-for type)))
(kind (intern
(or
(pg-pgip-get-attr "haspref" 'kind attrs t)
;; Default to kind user
"user")))
(descr (or (pg-pgip-get-attr "haspref" 'descr attrs t) ""))
(subst (pg-pgip-subst-for type))
(setting
(pg-prover-interpret-pgip-command
(concat "<pgip><setpref name=\"" name "\">" subst "</setpref></pgip>")))
(symname (intern name))) ;; FIXME: consider Emacs ID normalising
(ignore-errors
;; FIXME: allow rest of PGIP to be processed, would be better to
;; accumulate errors somehow.
(proof-debug "haspref calling defpacustom: name:%s default:%s type:%s setting:%s" symname default type setting)
(eval
`(defpacustom ,symname ,default
(concat descr (if descr "\n")
"Setting configured by <haspref> PGIP message")
:type (quote ,type)
:setting ,setting)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Dealing with <pgiptype>
;;
(defun pg-pgip-default-for (type)
"Synthesize a default value for type TYPE."
(cond
((eq type 'boolean) nil)
((eq type 'integer) 0)
((eq type 'string) "")
((eq (car-safe type) 'choice)
(car-safe (cdr-safe type)))
(t
(pg-pgip-error "pg-pgip-default-for: unrecognized type passed in"))))
(defun pg-pgip-subst-for (type)
"Return a substitution string for type TYPE."
(cond
((eq type 'boolean) "%b")
((eq type 'integer) "%i")
(t "%s")))
(defun pg-pgip-get-type (attrs)
"Extract and check type value from ATTRS. Normalize to custom format."
(let
((rawtype (pg-pgip-get-attr "haspref" 'type attrs)))
(cond
((string-match "choice(\\(.*\\))" rawtype)
(let* ((choiceslist (match-string 1 rawtype))
(choices (split-string choiceslist "[ \f\t\n\r\v]*,[ \f\t\n\r\v]*")))
(list 'choice choices)))
((equal rawtype "boolean")
'boolean)
((equal rawtype "int")
'integer)
((equal rawtype "nat") ;; nat treated as int
'integer)
((equal rawtype "string")
'string)
(t
(error "pg-pgip-get-type: unrecognized type %s" rawtype)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Auxiliary functions for parsing
;;
(defun pg-pgip-get-attr (elt attrnm attrs &optional optional)
(let ((vrs (cdr-safe (assoc attrnm attrs))))
(if optional
vrs
(or vrs
(error "Didn't find %s attribute in %s element" attrnm elt)))))
(defun pg-pgip-get-version (elt attrs &optional optional)
(pg-pgip-get-attr elt "version" attrs optional))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Function to interface PGIP commands sent to prover.
;;
(defun pg-prover-interpret-pgip-command (pgip)
(if proof-shell-issue-pgip-cmd
(format proof-shell-issue-pgip-cmd pgip)
"")) ;; Empty setting: might be better to send a comment
;; for debugging purposes.
(provide 'pg-pgip)
;; End of `pg-pgip.el'
|
