| Constant summary | |
|---|---|
| +race-webservice-url+ | "http://attempto.ifi.uzh.ch/ws/race/racews.perl" |
| Class summary | |
|---|---|
| race-proof | |
| race-reply | |
| Condition summary | |
|---|---|
| race-message | inherits from condition |
| Method summary | |
|---|---|
| race-message-description | race-message |
| race-message-importance | race-message |
| race-message-sentence-id | race-message |
| race-message-subject | race-message |
| race-message-type | race-message |
| race-proof-used-aux-axioms | race-proof |
| race-proof-used-axioms | race-proof |
| race-reply-messages | race-reply |
| race-reply-proofs | race-reply |
| race-reply-runtime | race-reply |
| race-reply-why-not | race-reply |
| Function summary | |
|---|---|
| invoke-race-webservice | &rest args &key axioms theorems mode si st ot sdt dodt iodt sti aux (uri +race-webservice-url+) (drakma-parameters (quote nil)) |
| race | &rest args &key axioms theorems mode si st ot sdt dodt iodt sti aux (uri +race-webservice-url+) (drakma-parameters (quote nil)) (signal-warning-messages t) (signal-error-messages nil) |
| :messages | [Initarg] |
| :runtime | [Initarg] |
| :proofs | [Initarg] |
| :why-not | [Initarg] |
| why-not | [Slot] |
A list of strings, the content of the race:Word elements that were in the race:WhyNot element.
| :used-axioms | [Initarg] |
| :used-aux-axioms | [Initarg] |
| :type | [Initarg] |
| :sentence-id | [Initarg] |
| :subject | [Initarg] |
| :description | [Initarg] |
| importance | [Slot] |
One of the symbols :warning, or :error.
| sentence-id | [Slot] |
An integer (or left unbound).
Returns the description of the specified race-message
Returns the subject of the specified race-message
Returns the sentence-id of the specified race-message
The URL of the RACE webservice.
| invoke-race-webservice | &rest args &key axioms theorems mode si st ot sdt dodt iodt sti aux (uri +race-webservice-url+) (drakma-parameters (quote nil)) | [Function] |
invoke-race-webservice &key axioms theorems mode si st or sdt dodt iodt sti aux drakma-parameters uri => result*
axioms --- a string
theorems --- a string or nil
mode --- one of the symbols :check-consistency, :prove, :answer-query
si, st, ot, sdt, dodt, iodt, sti, aux --- generalized booleans
uri --- a string or PURI:URI object, defaults to +race-webservice-url+
drakma-parameters --- a plist, passed to DRAKMA:HTTP-REQUEST
results --- results of DRAKMA:HTTP-REQUEST
invoke-race-webservice invokes the RACE Webservice by sending a SOAP request to URI. More documentation on the RACE Webservice is available [1].
| race | &rest args &key axioms theorems mode si st ot sdt dodt iodt sti aux (uri +race-webservice-url+) (drakma-parameters (quote nil)) (signal-warning-messages t) (signal-error-messages nil) | [Function] |
race &rest args &key signal-warning-messags signal-error-messages => reply
args --- a plist of args for invoke-race-webservice
signal-warning-messages, signal-error-messages --- booleans, defaults are t and nil respectively
reply --- a race-reply object
Race applies invoke-race-webservice with args, parses the reply, and signals warnings and errors depending on the values of signal-warning-messages and signal-error messages.
RACE messages that have importance type "warning" will, by default be signalled, while messages with importance "error" will not.
Since CXML:PARSE may or may not be able to handle a stream returned by DRAKMA:HTTP-REQUEST, any drakma-parameters is passed to invoke-race-webservice with :want-stream nil.
invoke-race-webservice is called with :allow-other-keys t (so that signal-warning-messages and signal-error-messsages can passed through) and as a result, arguments that would cause an unexpected keyword error to be signalled will not do so.