race

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)
race-reply    [Class]
: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.

race-reply-why-not   race-reply  [Generic function]

Returns the why-not of the specified race-reply

race-reply-proofs   race-reply  [Generic function]

Returns the proofs of the specified race-reply

race-reply-runtime   race-reply  [Generic function]

Returns the runtime of the specified race-reply

race-reply-messages   race-reply  [Generic function]

Returns the messages of the specified race-reply

race-proof    [Class]
:used-axioms    [Initarg]
:used-aux-axioms    [Initarg]
race-proof-used-aux-axioms   race-proof  [Generic function]

Returns the used-aux-axioms of the specified race-proof

race-proof-used-axioms   race-proof  [Generic function]

Returns the used-axioms of the specified race-proof

race-message   inherits from condition  [Condition]
: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).

race-message-description   race-message  [Generic function]

Returns the description of the specified race-message

race-message-subject   race-message  [Generic function]

Returns the subject of the specified race-message

race-message-sentence-id   race-message  [Generic function]

Returns the sentence-id of the specified race-message

race-message-type   race-message  [Generic function]

Returns the type of the specified race-message

race-message-importance   race-message  [Generic function]

Returns the importance of the specified race-message

+race-webservice-url+   "http://attempto.ifi.uzh.ch/ws/race/racews.perl"  [Constant]

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]

Syntax:

invoke-race-webservice &key axioms theorems mode si st or sdt dodt iodt sti aux drakma-parameters uri => result*

Arguments and Values:

  • 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

Description:

invoke-race-webservice invokes the RACE Webservice by sending a SOAP request to URI. More documentation on the RACE Webservice is available [1].

See Also:

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]

Syntax:

race &rest args &key signal-warning-messags signal-error-messages => reply

Arguments and Values:

  • 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

Description:

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.

Notes:

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.